Norm estimates and interior products of paired wedges

The paired wedge is ContinuousAlternatingMap.pairedWedge. This file proves its binomial operator-norm bound on real seminormed spaces and its interior-product antiderivation rule on normed spaces, using Mathlib's ContinuousAlternatingMap.curryLeft.

The normalization is the signed-permutation sum divided by the two input factorials, so the interior-product rule has unit constants.

References

• John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Graduate Texts in Mathematics 218, Springer, 2013, Lemma 14.13.

theorem ContinuousAlternatingMap.norm_pairedWedge_le {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [SeminormedAddCommGroup F₁] [NormedSpace ℝ F₁] [SeminormedAddCommGroup F₂] [NormedSpace ℝ F₂] [SeminormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} (mu : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (phi : E [⋀^Fin k]→L[ℝ] F₁) (psi : E [⋀^Fin l]→L[ℝ] F₂) : ‖pairedWedge mu ⋯ phi psi‖ ≤ ↑((k + l).choose k) * ‖mu‖ * ‖phi‖ * ‖psi‖

The norm of the paired wedge is bounded by the number of (k, l)-shuffles times the norms of the pairing and the two forms.

theorem ContinuousAlternatingMap.curryLeft_pairedWedge {E : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F₃ : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] [NormedAddCommGroup F₂] [NormedSpace ℝ F₂] [NormedAddCommGroup F₃] [NormedSpace ℝ F₃] {k l : ℕ} (mu : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (phi : E [⋀^Fin (k + 1)]→L[ℝ] F₁) (psi : E [⋀^Fin (l + 1)]→L[ℝ] F₂) (v : E) (w : Fin (k + 1 + l) → E) : ((pairedWedge mu ⋯ phi psi).curryLeft v) w = (pairedWedge mu ⋯ (phi.curryLeft v) psi) (w ∘ Fin.cast ⋯) + (-1) ^ (k + 1) • (pairedWedge mu ⋯ phi (psi.curryLeft v)) w

The interior product is an antiderivation of degree -1 for the paired wedge: ι_v (φ ∧ ψ) = ι_v φ ∧ ψ + (-1) ^ (k + 1) φ ∧ ι_v ψ for a (k + 1)-form φ, where the interior product ι_v is ContinuousAlternatingMap.curryLeft. The degree k + (l + 1) of the first term is identified with k + 1 + l by Fin.cast. The coefficient spaces are normed because Mathlib's curryLeft requires a normed target, both for the input forms and for their paired wedge.