The paired wedge as a continuous trilinear map

The paired wedge depends continuously and linearly on each of its three inputs: the bilinear pairing and the two alternating maps. pairedWedgeCLM bundles this dependence, with the binomial operator-norm bound. This permits applying the usual calculus of continuous linear maps to families of forms, including pairings that vary with the base point. For real-valued forms, wedgeApplyCLM v bundles the evaluation (ψ, φ) ↦ (φ ∧ ψ) v of the wedge on a fixed family of vectors as a continuous bilinear map, the form used to integrate wedges against test forms.

The construction uses ContinuousAlternatingMap.pairedWedge and its norm bound, together with Mathlib's LinearMap.mkContinuous₂. The normalization follows John M. Lee, Introduction to Smooth Manifolds, second edition, Chapter 14.

noncomputable def ContinuousAlternatingMap.pairedWedgeCLM {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 : ℕ} : (F₁ →L[ℝ] F₂ →L[ℝ] F₃) →L[ℝ] E [⋀^Fin k]→L[ℝ] F₁ →L[ℝ] E [⋀^Fin l]→L[ℝ] F₂ →L[ℝ] E [⋀^Fin (k + l)]→L[ℝ] F₃

The paired wedge, bundled as a continuous linear map in the pairing with values in continuous bilinear maps of alternating maps.

@[simp]

theorem ContinuousAlternatingMap.pairedWedgeCLM_apply {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 : ℕ} (μ : F₁ →L[ℝ] F₂ →L[ℝ] F₃) (φ : E [⋀^Fin k]→L[ℝ] F₁) (ψ : E [⋀^Fin l]→L[ℝ] F₂) : ((pairedWedgeCLM μ) φ) ψ = pairedWedge μ ⋯ φ ψ

Evaluation of the bundled paired wedge recovers ContinuousAlternatingMap.pairedWedge.

theorem ContinuousAlternatingMap.norm_pairedWedgeCLM_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 : ℕ} : ‖pairedWedgeCLM‖ ≤ ↑((k + l).choose k)

The operator norm of the bundled paired wedge is bounded by the binomial coefficient.

noncomputable def ContinuousAlternatingMap.wedgeApplyCLM {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {k l : ℕ} (v : Fin (k + l) → E) : E [⋀^Fin l]→L[ℝ] ℝ →L[ℝ] E [⋀^Fin k]→L[ℝ] ℝ →L[ℝ] ℝ

The real wedge evaluated on a family v of k + l vectors, as the continuous bilinear map (ψ, φ) ↦ (φ ∧ ψ) v of an l-form ψ and a k-form φ.

@[simp]

theorem ContinuousAlternatingMap.wedgeApplyCLM_apply {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {k l : ℕ} (v : Fin (k + l) → E) (ψ : E [⋀^Fin l]→L[ℝ] ℝ) (φ : E [⋀^Fin k]→L[ℝ] ℝ) : ((wedgeApplyCLM v) ψ) φ = (φ.wedge ψ) v

Evaluation of wedgeApplyCLM v is the wedge evaluated on v.