The flat Cartan formula, and the Lie derivative of a symplectic form along its Hamiltonian field

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). Q29(c′) of specs/generator-layer-scoping.md.

Analysis/ODE/FlowDerivative.lean defines the flat Lie derivative flatLieDeriv X Ω of a 2-form along a vector field and proves that a form with vanishing Lie derivative is preserved by the flow. This file identifies that Lie derivative with the exterior calculus and applies it to the one case the corpus needs.

• flatInteriorProduct X Ω — the 1-form ι_X Ω = Ω(X, ·); differentiableAt_flatInteriorProduct;
• fderiv_apply_vecCons_const — the product rule for z ↦ Ω z (X z, u);
• ★ flatLieDeriv_eq_extDeriv_flatInteriorProduct_add — Cartan's formula on a normed space, L_X Ω = d(ι_X Ω) + ι_X (dΩ), a Fin 2/Fin 3 computation from Mathlib's extDeriv_apply;
• DifferentialForm.localRep_apply_localHamiltonianVector — in a chart, the local Hamiltonian vector satisfies ω_loc (X_loc, u) = d(H ∘ chart⁻¹) u, so DifferentialForm.flatInteriorProduct_localHamiltonianVector: ι_X ω_loc is the chart differential of H; hence d(ι_X ω_loc) = d(d(H ∘ chart⁻¹)) = 0 (extDeriv_flatInteriorProduct_localHamiltonianVector, by extDeriv_extDeriv_apply);
• DifferentialForm.extDeriv_localRep_eq_zero — the local representative of a closed form is closed on the chart's target (localRep_mextDerivFamily);
• ★★ DifferentialForm.flatLieDeriv_localHamiltonianVector_localRep_eq_zero — the flat Lie derivative of a symplectic form's local representative along its Hamiltonian field vanishes at every point of the chart's target. Together with ContDiffAt.exists_localFlow_form_invariant this says the chart flow of a Hamiltonian field preserves the form; the manifold assembly is Q29(d′).

noncomputable def flatInteriorProduct {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (X : E → E) (Ω : E → E [⋀^Fin 2]→L[ℝ] ℝ) (z : E) : E [⋀^Fin 1]→L[ℝ] ℝ

The flat interior product ι_X Ω of a 2-form with a vector field: the 1-form v ↦ Ω z (X z, v).

Equations

• flatInteriorProduct X Ω z = (Ω z).curryLeft (X z)

theorem flatInteriorProduct_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (X : E → E) (Ω : E → E [⋀^Fin 2]→L[ℝ] ℝ) (z : E) (m : Fin 1 → E) : (flatInteriorProduct X Ω z) m = (Ω z) (Matrix.vecCons (X z) m)

theorem differentiableAt_flatInteriorProduct {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : E → E} {Ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {z : E} (hX : ContDiffAt ℝ 1 X z) (hΩ : ContDiffAt ℝ 1 Ω z) : DifferentiableAt ℝ (flatInteriorProduct X Ω) z

theorem Fin.removeNth_zero_two {β : Type u_2} (m : Fin 2 → β) : removeNth 0 m = ![m 1]

Fin.removeNth on two-element tuples.

theorem Fin.removeNth_one_two {β : Type u_2} (m : Fin 2 → β) : removeNth 1 m = ![m 0]

theorem Fin.removeNth_zero_three {β : Type u_2} (a : β) (m : Fin 2 → β) : removeNth 0 (Matrix.vecCons a m) = m

Fin.removeNth on three-element tuples.

theorem Fin.removeNth_one_three {β : Type u_2} (a : β) (m : Fin 2 → β) : removeNth 1 (Matrix.vecCons a m) = ![a, m 1]

theorem Fin.removeNth_two_three {β : Type u_2} (a : β) (m : Fin 2 → β) : removeNth 2 (Matrix.vecCons a m) = ![a, m 0]

theorem fderiv_apply_vecCons_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : E → E} {Ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {z : E} (hX : DifferentiableAt ℝ X z) (hΩ : DifferentiableAt ℝ Ω z) (u v : E) : (fderiv ℝ (fun (z : E) => (Ω z) ![X z, u]) z) v = ((fderiv ℝ Ω z) v) ![X z, u] + (Ω z) ![(fderiv ℝ X z) v, u]

The derivative of z ↦ Ω z ![X z, u] in the direction v.

theorem ContinuousAlternatingMap.apply_swap_two {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ξ : E [⋀^Fin 2]→L[ℝ] ℝ) (a b : E) : ξ ![b, a] = -ξ ![a, b]

Antisymmetry of a 2-form on the model.

theorem flatLieDeriv_eq_extDeriv_flatInteriorProduct_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : E → E} {Ω : E → E [⋀^Fin 2]→L[ℝ] ℝ} {z : E} (hX' : ContDiffAt ℝ 1 X z) (hΩ' : ContDiffAt ℝ 1 Ω z) (m : Fin 2 → E) : flatLieDeriv X Ω z m = (extDeriv (flatInteriorProduct X Ω) z) m + (extDeriv Ω z) (Matrix.vecCons (X z) m)

★ The flat Cartan formula for a 2-form: L_X Ω = d(ι_X Ω) + ι_X (dΩ).

theorem DifferentialForm.localRep_apply_localHamiltonianVector {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] (α : DifferentialForm (modelWithCornersSelf ℝ E) M (↑⊤) (Fin 2) ℝ) (H : M → ℝ) (hnd : ∀ (x : M) (v : TangentSpace (modelWithCornersSelf ℝ E) x), v ≠ 0 → ∃ (w : TangentSpace (modelWithCornersSelf ℝ E) x), (α x) ![v, w] ≠ 0) (x₀ : M) {w : E} (hw : w ∈ (chartAt E x₀).target) (u : E) : (localRep (fun (x : M) => α x) x₀ w) ![α.localHamiltonianVector H x₀ w, u] = (fderiv ℝ (H ∘ ↑(chartAt E x₀).symm) w) u

The defining identity of the local Hamiltonian vector, in the chart: ω_loc (X_loc w, u) = d(H ∘ chart⁻¹)_w u.

theorem DifferentialForm.flatInteriorProduct_localHamiltonianVector {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] (α : DifferentialForm (modelWithCornersSelf ℝ E) M (↑⊤) (Fin 2) ℝ) (H : M → ℝ) (hnd : ∀ (x : M) (v : TangentSpace (modelWithCornersSelf ℝ E) x), v ≠ 0 → ∃ (w : TangentSpace (modelWithCornersSelf ℝ E) x), (α x) ![v, w] ≠ 0) (x₀ : M) {w : E} (hw : w ∈ (chartAt E x₀).target) : flatInteriorProduct (α.localHamiltonianVector H x₀) (localRep (fun (x : M) => α x) x₀) w = (ContinuousAlternatingMap.ofSubsingleton ℝ E ℝ 0) (fderiv ℝ (H ∘ ↑(chartAt E x₀).symm) w)

The interior product of the local representative with the local Hamiltonian vector is the chart differential of H, as a 1-form.

theorem DifferentialForm.extDeriv_flatInteriorProduct_localHamiltonianVector {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] (α : DifferentialForm (modelWithCornersSelf ℝ E) M (↑⊤) (Fin 2) ℝ) (H : M → ℝ) (hnd : ∀ (x : M) (v : TangentSpace (modelWithCornersSelf ℝ E) x), v ≠ 0 → ∃ (w : TangentSpace (modelWithCornersSelf ℝ E) x), (α x) ![v, w] ≠ 0) (hH : ContMDiff (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ ℝ) (↑⊤) H) (x₀ : M) {w : E} (hw : w ∈ (chartAt E x₀).target) : extDeriv (flatInteriorProduct (α.localHamiltonianVector H x₀) (localRep (fun (x : M) => α x) x₀)) w = 0

d(ι_X ω_loc) = d(d(H ∘ chart⁻¹)) = 0 in the chart.

theorem DifferentialForm.extDeriv_localRep_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] (α : DifferentialForm (modelWithCornersSelf ℝ E) M (↑⊤) (Fin 2) ℝ) (hα : α.IsSymplectic) (x₀ : M) {w : E} (hw : w ∈ (chartAt E x₀).target) : extDeriv (localRep (fun (x : M) => α x) x₀) w = 0

The local representative of a closed form is closed in the chart: d ω_loc = 0 on the chart's target.

theorem DifferentialForm.flatLieDeriv_localHamiltonianVector_localRep_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {M : Type u_2} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (↑⊤) M] (α : DifferentialForm (modelWithCornersSelf ℝ E) M (↑⊤) (Fin 2) ℝ) (H : M → ℝ) (hα : α.IsSymplectic) (hH : ContMDiff (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ ℝ) (↑⊤) H) (x₀ : M) {w : E} (hw : w ∈ (chartAt E x₀).target) (m : Fin 2 → E) : flatLieDeriv (α.localHamiltonianVector H x₀) (localRep (fun (x : M) => α x) x₀) w m = 0

★★ The flat Lie derivative of the local representative of a symplectic form along the local Hamiltonian vector vanishes, at every point of the chart's target: Cartan's formula with d(ι_X ω_loc) = d(dH) = 0 (extDeriv_flatInteriorProduct_localHamiltonianVector) and the closedness of the local representative (extDeriv_localRep_eq_zero).