The radial primitive of a constant two-form

Every continuous bilinear form on a normed space over a nontrivially normed field determines a linear one-form by λₓ(v) = B(x, v) / 2. Its exterior derivative is one half of the alternatization of B; when B is skew-symmetric and (2 : 𝕜) ≠ 0, this says that the corresponding constant two-form is exact. This is the explicit primitive for the constant model form in the local Darboux construction.

The coordinate calculation follows the convention for exterior derivatives in Mathlib.Analysis.Calculus.DifferentialForm.Basic and parallels the evaluation calculation for the cotangent Liouville form in TauCeti/Geometry/Symplectic/Cotangent/Liouville.lean.

noncomputable def ContinuousLinearMap.liouvilleFormCLM {𝕜 : Type u_1} {V : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (B : V →L[𝕜] V →L[𝕜] F) : V →L[𝕜] V [⋀^Fin 1]→L[𝕜] F

The radial one-form associated to a continuous bilinear form B, given by λₓ(v) = B(x, v) / 2.

@[simp]

theorem ContinuousLinearMap.liouvilleFormCLM_apply {𝕜 : Type u_1} {V : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (B : V →L[𝕜] V →L[𝕜] F) (x : V) (v : Fin 1 → V) : (B.liouvilleFormCLM x) v = 2⁻¹ • (B x) (v 0)

The radial one-form evaluates by λₓ(v) = B(x, v) / 2.

theorem ContinuousLinearMap.extDeriv_liouvilleFormCLM {𝕜 : Type u_1} {V : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (B : V →L[𝕜] V →L[𝕜] F) (x : V) : extDeriv (⇑B.liouvilleFormCLM) x = 2⁻¹ • (TauCeti.ContinuousAlternatingMap.alternatizeBilinCLM 𝕜 V F) B

The exterior derivative of the radial one-form of B is one half of the alternatization of B: dλₓ(v, w) = (B(v, w) - B(w, v)) / 2.

theorem ContinuousLinearMap.extDeriv_liouvilleFormCLM_apply {𝕜 : Type u_1} {V : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (B : V →L[𝕜] V →L[𝕜] F) (x : V) (v : Fin 2 → V) : (extDeriv (⇑B.liouvilleFormCLM) x) v = 2⁻¹ • ((B (v 0)) (v 1) - (B (v 1)) (v 0))

The exterior derivative of the radial one-form of B evaluates by dλₓ(v, w) = (B(v, w) - B(w, v)) / 2.

theorem ContinuousLinearMap.extDeriv_liouvilleFormCLM_apply_of_skew {𝕜 : Type u_1} {V : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (B : V →L[𝕜] V →L[𝕜] F) (h2 : 2 ≠ 0) (hB : ∀ (v w : V), (B v) w = -(B w) v) (x : V) (v : Fin 2 → V) : (extDeriv (⇑B.liouvilleFormCLM) x) v = (B (v 0)) (v 1)

If B is skew-symmetric and (2 : 𝕜) ≠ 0, the radial one-form λₓ(v) = B(x, v) / 2 is a primitive of the constant two-form B.