The Lie derivative of differential forms on normed spaces

The Lie derivative of a differential form ω : E → E [⋀^Fin k]→L[𝕜] F along a vector field V : E → E is

L_V ω (x) (v₀, …, vₖ₋₁) = Dω(x)(V x)(v₀, …, vₖ₋₁) + ∑ i, ω(x)(v₀, …, DV(x) vᵢ, …, vₖ₋₁).

The second term is the action of DV(x) on ω(x) as a derivation, which is Mathlib's derivative of g ↦ (ω x).compContinuousLinearMap g at the identity, ContinuousAlternatingMap.fderivCompContinuousLinearMap. The definition needs no flow and is total, with junk values where ω or V is not differentiable; the within-set version takes derivatives within an arbitrary set, so it applies to chart ranges with boundary or corners.

Two characterizations follow.

• Evaluated on vector fields, L_V ω (X₀, …, Xₖ₋₁) is the derivative of ω (X₀, …, Xₖ₋₁) along V minus the terms ω (X₀, …, [V, Xᵢ], …, Xₖ₋₁) [Lee, Cor. 12.33].
• Cartan's formula L_V = ι_V ∘ d + d ∘ ι_V [Lee, Thm. 14.35], where the interior product ι_V is Mathlib's ContinuousAlternatingMap.curryLeft. In degree zero only the first term occurs.

Main declarations

• TauCeti.lieDerivFormWithin, TauCeti.lieDerivForm: the Lie derivative of a form.
• TauCeti.lieDerivFormWithin_add, TauCeti.lieDerivFormWithin_smul: linearity in the form.
• TauCeti.lieDerivFormWithin_add_left: additivity in the vector field.
• TauCeti.lieDerivFormWithin_apply_vectorField: the bracket formula.
• TauCeti.lieDerivFormWithin_eq_curryLeft_extDerivWithin_add: Cartan's formula.

References

• John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Corollary 12.33 and Theorem 14.35.

noncomputable def TauCeti.lieDerivFormWithin {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} (V : E → E) (ω : E → E [⋀^Fin k]→L[𝕜] F) (s : Set E) (x : E) : E [⋀^Fin k]→L[𝕜] F

The Lie derivative within s at x of a differential form ω along a vector field V: the derivative of ω in the direction V x, plus the action of the derivative of V on ω x as a derivation.

noncomputable def TauCeti.lieDerivForm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} (V : E → E) (ω : E → E [⋀^Fin k]→L[𝕜] F) (x : E) : E [⋀^Fin k]→L[𝕜] F

The Lie derivative of a differential form ω along a vector field V.

theorem TauCeti.lieDerivFormWithin_def {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} (V : E → E) (ω : E → E [⋀^Fin k]→L[𝕜] F) (s : Set E) (x : E) : lieDerivFormWithin V ω s x = (fderivWithin 𝕜 ω s x) (V x) + ((ω x).fderivCompContinuousLinearMap (ContinuousLinearMap.id 𝕜 E)) (fderivWithin 𝕜 V s x)

theorem TauCeti.lieDerivForm_def {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} (V : E → E) (ω : E → E [⋀^Fin k]→L[𝕜] F) (x : E) : lieDerivForm V ω x = (fderiv 𝕜 ω x) (V x) + ((ω x).fderivCompContinuousLinearMap (ContinuousLinearMap.id 𝕜 E)) (fderiv 𝕜 V x)

@[simp]

theorem TauCeti.lieDerivFormWithin_univ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} (V : E → E) (ω : E → E [⋀^Fin k]→L[𝕜] F) : lieDerivFormWithin V ω Set.univ = lieDerivForm V ω

theorem TauCeti.lieDerivFormWithin_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} {V : E → E} {s : Set E} {x : E} (ω : E → E [⋀^Fin k]→L[𝕜] F) (v : Fin k → E) : (lieDerivFormWithin V ω s x) v = ((fderivWithin 𝕜 ω s x) (V x)) v + ∑ i : Fin k, (ω x) (Function.update v i ((fderivWithin 𝕜 V s x) (v i)))

Evaluation of the Lie derivative on a tuple of vectors.

theorem TauCeti.lieDerivForm_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} {V : E → E} {x : E} (ω : E → E [⋀^Fin k]→L[𝕜] F) (v : Fin k → E) : (lieDerivForm V ω x) v = ((fderiv 𝕜 ω x) (V x)) v + ∑ i : Fin k, (ω x) (Function.update v i ((fderiv 𝕜 V x) (v i)))

Evaluation of the Lie derivative on a tuple of vectors.

Linearity in the form

@[simp]

theorem TauCeti.lieDerivFormWithin_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} (V : E → E) (s : Set E) (x : E) : lieDerivFormWithin V 0 s x = 0

@[simp]

theorem TauCeti.lieDerivForm_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} (V : E → E) : lieDerivForm V 0 = 0

theorem TauCeti.lieDerivFormWithin_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} {V : E → E} {s : Set E} {x : E} {ω η : E → E [⋀^Fin k]→L[𝕜] F} (hs : UniqueDiffWithinAt 𝕜 s x) (hω : DifferentiableWithinAt 𝕜 ω s x) (hη : DifferentiableWithinAt 𝕜 η s x) : lieDerivFormWithin V (ω + η) s x = lieDerivFormWithin V ω s x + lieDerivFormWithin V η s x

The Lie derivative within a set is additive on forms differentiable within the set at the point, wherever derivatives within the set are unique.

theorem TauCeti.lieDerivForm_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} {V : E → E} {x : E} {ω η : E → E [⋀^Fin k]→L[𝕜] F} (hω : DifferentiableAt 𝕜 ω x) (hη : DifferentiableAt 𝕜 η x) : lieDerivForm V (ω + η) x = lieDerivForm V ω x + lieDerivForm V η x

The Lie derivative is additive on forms differentiable at the point.

@[simp]

theorem TauCeti.lieDerivFormWithin_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} {V : E → E} {s : Set E} {x : E} (c : 𝕜) (ω : E → E [⋀^Fin k]→L[𝕜] F) (hs : UniqueDiffWithinAt 𝕜 s x) : lieDerivFormWithin V (c • ω) s x = c • lieDerivFormWithin V ω s x

The Lie derivative within a set commutes with scalars wherever derivatives within the set are unique; no differentiability of the form is needed.

@[simp]

theorem TauCeti.lieDerivForm_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} {V : E → E} (c : 𝕜) (ω : E → E [⋀^Fin k]→L[𝕜] F) : lieDerivForm V (c • ω) = c • lieDerivForm V ω

Linearity in the vector field

theorem TauCeti.lieDerivFormWithin_add_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} {V : E → E} {s : Set E} {x : E} {W : E → E} (ω : E → E [⋀^Fin k]→L[𝕜] F) (hs : UniqueDiffWithinAt 𝕜 s x) (hV : DifferentiableWithinAt 𝕜 V s x) (hW : DifferentiableWithinAt 𝕜 W s x) : lieDerivFormWithin (V + W) ω s x = lieDerivFormWithin V ω s x + lieDerivFormWithin W ω s x

The Lie derivative within a set is additive in the vector field, at a point where both fields are differentiable within the set and derivatives within it are unique. No differentiability of the form is needed.

theorem TauCeti.lieDerivForm_add_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} {V : E → E} {x : E} {W : E → E} (ω : E → E [⋀^Fin k]→L[𝕜] F) (hV : DifferentiableAt 𝕜 V x) (hW : DifferentiableAt 𝕜 W x) : lieDerivForm (V + W) ω x = lieDerivForm V ω x + lieDerivForm W ω x

The Lie derivative is additive in the vector field, at a point where both fields are differentiable.

theorem TauCeti.lieDerivFormWithin_apply_vectorField {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} {V : E → E} {s : Set E} {x : E} {ω : E → E [⋀^Fin k]→L[𝕜] F} (X : Fin k → E → E) (hω : DifferentiableWithinAt 𝕜 ω s x) (hX : ∀ (i : Fin k), DifferentiableWithinAt 𝕜 (X i) s x) (hs : UniqueDiffWithinAt 𝕜 s x) : ((lieDerivFormWithin V ω s x) fun (x_1 : Fin k) => X x_1 x) = (fderivWithin 𝕜 (fun (y : E) => (ω y) fun (x : Fin k) => X x y) s x) (V x) - ∑ i : Fin k, (ω x) (Function.update (fun (x_1 : Fin k) => X x_1 x) i (VectorField.lieBracketWithin 𝕜 V (X i) s x))

The bracket formula for the Lie derivative of a form within a set: evaluated on vector fields X₀, …, Xₖ₋₁, it is the derivative of ω (X₀, …, Xₖ₋₁) along V minus the evaluations of ω with one field Xᵢ replaced by the bracket [V, Xᵢ].

theorem TauCeti.lieDerivForm_apply_vectorField {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} {V : E → E} {x : E} {ω : E → E [⋀^Fin k]→L[𝕜] F} (X : Fin k → E → E) (hω : DifferentiableAt 𝕜 ω x) (hX : ∀ (i : Fin k), DifferentiableAt 𝕜 (X i) x) : ((lieDerivForm V ω x) fun (x_1 : Fin k) => X x_1 x) = (fderiv 𝕜 (fun (y : E) => (ω y) fun (x : Fin k) => X x y) x) (V x) - ∑ i : Fin k, (ω x) (Function.update (fun (x_1 : Fin k) => X x_1 x) i (VectorField.lieBracket 𝕜 V (X i) x))

The bracket formula for the Lie derivative of a form: evaluated on vector fields X₀, …, Xₖ₋₁, it is the derivative of ω (X₀, …, Xₖ₋₁) along V minus the evaluations of ω with one field Xᵢ replaced by the bracket [V, Xᵢ].

theorem TauCeti.lieDerivFormWithin_eq_curryLeft_extDerivWithin_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} {V : E → E} {s : Set E} {x : E} {ω : E → E [⋀^Fin (k + 1)]→L[𝕜] F} (hω : DifferentiableWithinAt 𝕜 ω s x) (hV : DifferentiableWithinAt 𝕜 V s x) (hs : UniqueDiffWithinAt 𝕜 s x) : lieDerivFormWithin V ω s x = (extDerivWithin ω s x).curryLeft (V x) + extDerivWithin (fun (y : E) => (ω y).curryLeft (V y)) s x

Cartan's formula within a set, L_V ω = ι_V dω + d (ι_V ω), where the interior product ι_V inserts V into the first slot.

theorem TauCeti.lieDerivForm_eq_curryLeft_extDeriv_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} {V : E → E} {x : E} {ω : E → E [⋀^Fin (k + 1)]→L[𝕜] F} (hω : DifferentiableAt 𝕜 ω x) (hV : DifferentiableAt 𝕜 V x) : lieDerivForm V ω x = (extDeriv ω x).curryLeft (V x) + extDeriv (fun (y : E) => (ω y).curryLeft (V y)) x

Cartan's formula L_V ω = ι_V dω + d (ι_V ω), where the interior product ι_V inserts V into the first slot.

theorem TauCeti.lieDerivFormWithin_eq_curryLeft_extDerivWithin {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (V : E → E) (ω : E → E [⋀^Fin 0]→L[𝕜] F) (s : Set E) (x : E) : lieDerivFormWithin V ω s x = (extDerivWithin ω s x).curryLeft (V x)

Cartan's formula in degree zero, L_V f = ι_V df, holds for every function and vector field.

theorem TauCeti.lieDerivForm_eq_curryLeft_extDeriv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (V : E → E) (ω : E → E [⋀^Fin 0]→L[𝕜] F) (x : E) : lieDerivForm V ω x = (extDeriv ω x).curryLeft (V x)

Cartan's formula in degree zero, L_V f = ι_V df, holds for every function and vector field.