The Lie derivative of endomorphism fields on normed spaces

The Lie derivative of an endomorphism field A : E → E →L[𝕜] E along a vector field V : E → E on a normed space E is

L_V A (x) = DA(x)(V x) + A(x) ∘ DV(x) - DV(x) ∘ A(x).

As with TauCeti.lieDerivForm, the definition needs no flow and is total, with junk values where A or V is not differentiable, and TauCeti.lieDerivEndomorphismWithin localizes all derivatives to a set s.

Four properties organize the calculus of L_V A:

• Bracket formula (lieDerivEndomorphism_apply_vectorField): on a differentiable vector field W, (L_V A)(W) = [V, A W] - A [V, W], where [V, W] = DW · V - DV · W is Mathlib's VectorField.lieBracket.
• Derivation rule on composition (lieDerivEndomorphism_comp): L_V (A ∘ B) = (L_V A) ∘ B + A ∘ (L_V B). In particular, if A² = -1 near x, then L_V A anticommutes with A(x) (lieDerivEndomorphism_comp_add_comp_eq_zero).
• Commutator identity and source-bracket sign comparison (lieDerivEndomorphism_lieBracket and lieDerivEndomorphism_fderiv_sub_fderiv): for C² fields U, V, A, Mathlib's Lie bracket satisfies L_{[U, V]} A = L_U (L_V A) - L_V (L_U A), whereas the opposite bracket [U, V]_RS = DU · V - DV · U = -[U, V] used by Robbin–Salamon satisfies L_{[U, V]_RS} A = L_V (L_U A) - L_U (L_V A).
• Nijenhuis–Lie-derivative identity (lieDerivEndomorphism_apply_sub_apply): when A(x)² = -1, the derivative DX(x) cancels from (L_{A X} A)(w) - A(L_X A)(w), leaving the pointwise Nijenhuis expression of A evaluated on (X x, w).

Main declarations

• TauCeti.lieDerivEndomorphismWithin, TauCeti.lieDerivEndomorphism: the Lie derivative of an endomorphism field within a set and on the whole space.
• TauCeti.lieDerivEndomorphism_apply_vectorField: (L_V A)(W) = [V, A W] - A [V, W].
• TauCeti.lieDerivEndomorphism_comp: L_V (A ∘ B) = (L_V A) ∘ B + A ∘ (L_V B).
• TauCeti.lieDerivEndomorphism_lieBracket and TauCeti.lieDerivEndomorphism_fderiv_sub_fderiv: the native and source-bracket commutator identities.
• TauCeti.lieDerivEndomorphism_apply_sub_apply: (L_{A X} A)(w) - A(L_X A)(w) equals the Nijenhuis expression of A when A(x)² = -1.

References

• S. Kobayashi and K. Nomizu, Foundations of Differential Geometry, Vol. I, Interscience, 1963, Chapter I, Proposition 3.2 (Lie derivative of tensor fields and bracket commutator).
• J. W. Robbin and D. A. Salamon, Corrigendum to A construction of the Deligne–Mumford orbifold, J. Eur. Math. Soc. 9 (2007), 901–905 (endomorphism Lie derivative and bracket convention).

noncomputable def TauCeti.lieDerivEndomorphismWithin {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (V : E → E) (A : E → E →L[𝕜] E) (s : Set E) (x : E) : E →L[𝕜] E

The Lie derivative within s at x of an endomorphism field A along a vector field V: DA|_s(x)(V x) + A(x) ∘ DV|_s(x) - DV|_s(x) ∘ A(x).

noncomputable def TauCeti.lieDerivEndomorphism {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (V : E → E) (A : E → E →L[𝕜] E) (x : E) : E →L[𝕜] E

The Lie derivative at x of an endomorphism field A along a vector field V: DA(x)(V x) + A(x) ∘ DV(x) - DV(x) ∘ A(x).

theorem TauCeti.lieDerivEndomorphismWithin_def {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (V : E → E) (A : E → E →L[𝕜] E) (s : Set E) (x : E) : lieDerivEndomorphismWithin V A s x = (fderivWithin 𝕜 A s x) (V x) + A x ∘SL fderivWithin 𝕜 V s x - fderivWithin 𝕜 V s x ∘SL A x

theorem TauCeti.lieDerivEndomorphism_def {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (V : E → E) (A : E → E →L[𝕜] E) (x : E) : lieDerivEndomorphism V A x = (fderiv 𝕜 A x) (V x) + A x ∘SL fderiv 𝕜 V x - fderiv 𝕜 V x ∘SL A x

@[simp]

theorem TauCeti.lieDerivEndomorphismWithin_univ {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (V : E → E) (A : E → E →L[𝕜] E) : lieDerivEndomorphismWithin V A Set.univ = lieDerivEndomorphism V A

theorem TauCeti.lieDerivEndomorphismWithin_apply {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (V : E → E) (A : E → E →L[𝕜] E) (s : Set E) (x w : E) : (lieDerivEndomorphismWithin V A s x) w = ((fderivWithin 𝕜 A s x) (V x)) w + (A x) ((fderivWithin 𝕜 V s x) w) - (fderivWithin 𝕜 V s x) ((A x) w)

Pointwise evaluation of lieDerivEndomorphismWithin on a vector w.

theorem TauCeti.lieDerivEndomorphism_apply {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (V : E → E) (A : E → E →L[𝕜] E) (x w : E) : (lieDerivEndomorphism V A x) w = ((fderiv 𝕜 A x) (V x)) w + (A x) ((fderiv 𝕜 V x) w) - (fderiv 𝕜 V x) ((A x) w)

Pointwise evaluation of lieDerivEndomorphism on a vector w.

Algebraic properties and locality

@[simp]

theorem TauCeti.lieDerivEndomorphismWithin_zero {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (V : E → E) (s : Set E) (x : E) : lieDerivEndomorphismWithin V 0 s x = 0

@[simp]

theorem TauCeti.lieDerivEndomorphism_zero {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (V : E → E) : lieDerivEndomorphism V 0 = 0

@[simp]

theorem TauCeti.lieDerivEndomorphismWithin_zero_left {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (A : E → E →L[𝕜] E) (s : Set E) (x : E) : lieDerivEndomorphismWithin 0 A s x = 0

@[simp]

theorem TauCeti.lieDerivEndomorphism_zero_left {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (A : E → E →L[𝕜] E) : lieDerivEndomorphism 0 A = 0

theorem TauCeti.lieDerivEndomorphismWithin_const {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (V : E → E) (A₀ : E →L[𝕜] E) (s : Set E) (x : E) : lieDerivEndomorphismWithin V (fun (x : E) => A₀) s x = A₀ ∘SL fderivWithin 𝕜 V s x - fderivWithin 𝕜 V s x ∘SL A₀

The Lie derivative of a constant endomorphism field A₀ is the commutator [A₀, DV].

theorem TauCeti.lieDerivEndomorphism_const {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (V : E → E) (A₀ : E →L[𝕜] E) (x : E) : lieDerivEndomorphism V (fun (x : E) => A₀) x = A₀ ∘SL fderiv 𝕜 V x - fderiv 𝕜 V x ∘SL A₀

The Lie derivative of a constant endomorphism field A₀ is the commutator [A₀, DV].

@[simp]

theorem TauCeti.lieDerivEndomorphismWithin_const_id {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (V : E → E) (s : Set E) (x : E) : lieDerivEndomorphismWithin V (fun (x : E) => ContinuousLinearMap.id 𝕜 E) s x = 0

@[simp]

theorem TauCeti.lieDerivEndomorphism_const_id {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (V : E → E) (x : E) : lieDerivEndomorphism V (fun (x : E) => ContinuousLinearMap.id 𝕜 E) x = 0

theorem TauCeti.lieDerivEndomorphismWithin_add {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V : E → E} {A B : E → E →L[𝕜] E} {s : Set E} {x : E} (hs : UniqueDiffWithinAt 𝕜 s x) (hA : DifferentiableWithinAt 𝕜 A s x) (hB : DifferentiableWithinAt 𝕜 B s x) : lieDerivEndomorphismWithin V (A + B) s x = lieDerivEndomorphismWithin V A s x + lieDerivEndomorphismWithin V B s x

theorem TauCeti.lieDerivEndomorphism_add {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V : E → E} {A B : E → E →L[𝕜] E} {x : E} (hA : DifferentiableAt 𝕜 A x) (hB : DifferentiableAt 𝕜 B x) : lieDerivEndomorphism V (A + B) x = lieDerivEndomorphism V A x + lieDerivEndomorphism V B x

theorem TauCeti.lieDerivEndomorphismWithin_neg {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {x : E} (V : E → E) (A : E → E →L[𝕜] E) (hs : UniqueDiffWithinAt 𝕜 s x) : lieDerivEndomorphismWithin V (-A) s x = -lieDerivEndomorphismWithin V A s x

@[simp]

theorem TauCeti.lieDerivEndomorphism_neg {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (V : E → E) (A : E → E →L[𝕜] E) : lieDerivEndomorphism V (-A) = -lieDerivEndomorphism V A

theorem TauCeti.lieDerivEndomorphismWithin_sub {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V : E → E} {A B : E → E →L[𝕜] E} {s : Set E} {x : E} (hs : UniqueDiffWithinAt 𝕜 s x) (hA : DifferentiableWithinAt 𝕜 A s x) (hB : DifferentiableWithinAt 𝕜 B s x) : lieDerivEndomorphismWithin V (A - B) s x = lieDerivEndomorphismWithin V A s x - lieDerivEndomorphismWithin V B s x

theorem TauCeti.lieDerivEndomorphism_sub {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V : E → E} {A B : E → E →L[𝕜] E} {x : E} (hA : DifferentiableAt 𝕜 A x) (hB : DifferentiableAt 𝕜 B x) : lieDerivEndomorphism V (A - B) x = lieDerivEndomorphism V A x - lieDerivEndomorphism V B x

@[simp]

theorem TauCeti.lieDerivEndomorphismWithin_smul {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V : E → E} {s : Set E} {x : E} (c : 𝕜) (A : E → E →L[𝕜] E) (hs : UniqueDiffWithinAt 𝕜 s x) : lieDerivEndomorphismWithin V (c • A) s x = c • lieDerivEndomorphismWithin V A s x

@[simp]

theorem TauCeti.lieDerivEndomorphism_smul {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V : E → E} (c : 𝕜) (A : E → E →L[𝕜] E) : lieDerivEndomorphism V (c • A) = c • lieDerivEndomorphism V A

theorem TauCeti.lieDerivEndomorphism_add_left {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U V : E → E} {A : E → E →L[𝕜] E} {x : E} (hU : DifferentiableAt 𝕜 U x) (hV : DifferentiableAt 𝕜 V x) : lieDerivEndomorphism (U + V) A x = lieDerivEndomorphism U A x + lieDerivEndomorphism V A x

theorem TauCeti.lieDerivEndomorphism_neg_left {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (V : E → E) (A : E → E →L[𝕜] E) (x : E) : lieDerivEndomorphism (-V) A x = -lieDerivEndomorphism V A x

theorem TauCeti.lieDerivEndomorphism_sub_left {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U V : E → E} {A : E → E →L[𝕜] E} {x : E} (hU : DifferentiableAt 𝕜 U x) (hV : DifferentiableAt 𝕜 V x) : lieDerivEndomorphism (U - V) A x = lieDerivEndomorphism U A x - lieDerivEndomorphism V A x

theorem TauCeti.lieDerivEndomorphism_const_smul_left {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (c : 𝕜) (V : E → E) (A : E → E →L[𝕜] E) (x : E) : lieDerivEndomorphism (c • V) A x = c • lieDerivEndomorphism V A x

theorem Filter.EventuallyEq.lieDerivEndomorphismWithin_eq_nhds {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V V₁ : E → E} {A A₁ : E → E →L[𝕜] E} {s : Set E} {x : E} (hV : V₁ =ᶠ[nhds x] V) (hA : A₁ =ᶠ[nhds x] A) : TauCeti.lieDerivEndomorphismWithin V₁ A₁ s x = TauCeti.lieDerivEndomorphismWithin V A s x

theorem Filter.EventuallyEq.lieDerivEndomorphism_eq {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V V₁ : E → E} {A A₁ : E → E →L[𝕜] E} {x : E} (hV : V₁ =ᶠ[nhds x] V) (hA : A₁ =ᶠ[nhds x] A) : TauCeti.lieDerivEndomorphism V₁ A₁ x = TauCeti.lieDerivEndomorphism V A x

theorem Filter.EventuallyEq.lieDerivEndomorphism {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V V₁ : E → E} {A A₁ : E → E →L[𝕜] E} {x : E} (hV : V₁ =ᶠ[nhds x] V) (hA : A₁ =ᶠ[nhds x] A) : TauCeti.lieDerivEndomorphism V₁ A₁ =ᶠ[nhds x] TauCeti.lieDerivEndomorphism V A

theorem TauCeti.contDiffAt_lieDerivEndomorphism {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V : E → E} {A : E → E →L[𝕜] E} {x : E} {n m : WithTop ℕ∞} (hV : ContDiffAt 𝕜 n V x) (hA : ContDiffAt 𝕜 n A x) (hmn : m + 1 ≤ n) : ContDiffAt 𝕜 m (lieDerivEndomorphism V A) x

If V and A are C^n at x with m + 1 ≤ n, then lieDerivEndomorphism V A is C^m at x.

Bracket formula and composition derivation rule

theorem TauCeti.lieDerivEndomorphismWithin_apply_vectorField {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {A : E → E →L[𝕜] E} {s : Set E} {x : E} (hs : UniqueDiffWithinAt 𝕜 s x) (hA : DifferentiableWithinAt 𝕜 A s x) (hW : DifferentiableWithinAt 𝕜 W s x) : (lieDerivEndomorphismWithin V A s x) (W x) = VectorField.lieBracketWithin 𝕜 V (fun (y : E) => (A y) (W y)) s x - (A x) (VectorField.lieBracketWithin 𝕜 V W s x)

Bracket formula for lieDerivEndomorphismWithin: evaluated on a vector field W, (L_V A)(W) = [V, A W] - A [V, W].

theorem TauCeti.lieDerivEndomorphism_apply_vectorField {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {A : E → E →L[𝕜] E} {x : E} (hA : DifferentiableAt 𝕜 A x) (hW : DifferentiableAt 𝕜 W x) : (lieDerivEndomorphism V A x) (W x) = VectorField.lieBracket 𝕜 V (fun (y : E) => (A y) (W y)) x - (A x) (VectorField.lieBracket 𝕜 V W x)

Bracket formula for lieDerivEndomorphism: evaluated on a vector field W, (L_V A)(W) = [V, A W] - A [V, W].

theorem TauCeti.lieDerivEndomorphism_apply_eq_lieBracket {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V : E → E} {A : E → E →L[𝕜] E} {x : E} (hA : DifferentiableAt 𝕜 A x) (w : E) : (lieDerivEndomorphism V A x) w = VectorField.lieBracket 𝕜 V (fun (y : E) => (A y) w) x - (A x) (VectorField.lieBracket 𝕜 V (fun (x : E) => w) x)

Specializing lieDerivEndomorphism_apply_vectorField to a constant vector field expresses (L_V A)(x) w purely in terms of vector-field brackets.

theorem TauCeti.lieDerivEndomorphismWithin_comp {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V : E → E} {A B : E → E →L[𝕜] E} {s : Set E} {x : E} (hs : UniqueDiffWithinAt 𝕜 s x) (hA : DifferentiableWithinAt 𝕜 A s x) (hB : DifferentiableWithinAt 𝕜 B s x) : lieDerivEndomorphismWithin V (fun (y : E) => A y ∘SL B y) s x = lieDerivEndomorphismWithin V A s x ∘SL B x + A x ∘SL lieDerivEndomorphismWithin V B s x

Derivation rule on composition within a set: L_V (A ∘ B) = (L_V A) ∘ B + A ∘ (L_V B). No differentiability of V is required.

theorem TauCeti.lieDerivEndomorphism_comp {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V : E → E} {A B : E → E →L[𝕜] E} {x : E} (hA : DifferentiableAt 𝕜 A x) (hB : DifferentiableAt 𝕜 B x) : lieDerivEndomorphism V (fun (y : E) => A y ∘SL B y) x = lieDerivEndomorphism V A x ∘SL B x + A x ∘SL lieDerivEndomorphism V B x

Derivation rule on composition: L_V (A ∘ B) = (L_V A) ∘ B + A ∘ (L_V B).

theorem TauCeti.lieDerivEndomorphism_comp_add_comp_eq_zero {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V : E → E} {A : E → E →L[𝕜] E} {x : E} (hA : DifferentiableAt 𝕜 A x) (hsq : (fun (y : E) => A y ∘SL A y) =ᶠ[nhds x] fun (x : E) => -ContinuousLinearMap.id 𝕜 E) : lieDerivEndomorphism V A x ∘SL A x + A x ∘SL lieDerivEndomorphism V A x = 0

If A² = -1 on a neighborhood of x and A is differentiable at x, then L_V A (x) anticommutes with A x.

Commutator identity and source-bracket sign comparison

theorem TauCeti.lieDerivEndomorphism_lieBracket {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U V : E → E} {A : E → E →L[𝕜] E} {x : E} {n : WithTop ℕ∞} (hn : minSmoothness 𝕜 2 ≤ n) (hU : ContDiffAt 𝕜 n U x) (hV : ContDiffAt 𝕜 n V x) (hA : ContDiffAt 𝕜 n A x) : lieDerivEndomorphism (VectorField.lieBracket 𝕜 U V) A x = lieDerivEndomorphism U (lieDerivEndomorphism V A) x - lieDerivEndomorphism V (lieDerivEndomorphism U A) x

Commutator identity for Mathlib's Lie bracket [U, V] = DV · U - DU · V: for C² vector fields U, V and endomorphism field A at x, L_{[U, V]} A = L_U (L_V A) - L_V (L_U A).

theorem TauCeti.lieDerivEndomorphism_fderiv_sub_fderiv {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U V : E → E} {A : E → E →L[𝕜] E} {x : E} {n : WithTop ℕ∞} (hn : minSmoothness 𝕜 2 ≤ n) (hU : ContDiffAt 𝕜 n U x) (hV : ContDiffAt 𝕜 n V x) (hA : ContDiffAt 𝕜 n A x) : lieDerivEndomorphism (fun (y : E) => (fderiv 𝕜 U y) (V y) - (fderiv 𝕜 V y) (U y)) A x = lieDerivEndomorphism V (lieDerivEndomorphism U A) x - lieDerivEndomorphism U (lieDerivEndomorphism V A) x

Source-bracket commutator identity: for the opposite bracket [U, V]_RS(y) = DU(y)(V y) - DV(y)(U y) = -lieBracket 𝕜 U V y used by Robbin–Salamon, L_{[U, V]_RS} A = L_V (L_U A) - L_U (L_V A).

Nijenhuis–Lie-derivative identities

theorem TauCeti.lieDerivEndomorphism_apply_sub_apply {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {A : E → E →L[𝕜] E} {x : E} {X : E → E} (hA : DifferentiableAt 𝕜 A x) (hX : DifferentiableAt 𝕜 X x) (hsq : ∀ (u : E), (A x) ((A x) u) = -u) (w : E) : (lieDerivEndomorphism (fun (y : E) => (A y) (X y)) A x) w - (A x) ((lieDerivEndomorphism X A x) w) = ((fderiv 𝕜 A x) ((A x) (X x))) w - ((fderiv 𝕜 A x) ((A x) w)) (X x) + (A x) (((fderiv 𝕜 A x) w) (X x)) - (A x) (((fderiv 𝕜 A x) (X x)) w)

Nijenhuis–Lie-derivative identity: if A x squares to -1, then for every differentiable vector field X, the derivative DX(x) cancels out of (L_{A X} A)(x) w - A x ((L_X A)(x) w), leaving the pointwise Nijenhuis expression of A on (X x, w).

theorem TauCeti.lieBracket_apply_sub_lieBracket_eq {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {A : E → E →L[𝕜] E} {x : E} {U W : E → E} (hA : DifferentiableAt 𝕜 A x) (hU : DifferentiableAt 𝕜 U x) (hW : DifferentiableAt 𝕜 W x) (hsq : ∀ (u : E), (A x) ((A x) u) = -u) : VectorField.lieBracket 𝕜 (fun (y : E) => (A y) (U y)) (fun (y : E) => (A y) (W y)) x - VectorField.lieBracket 𝕜 U W x - (A x) (VectorField.lieBracket 𝕜 (fun (y : E) => (A y) (U y)) W x) - (A x) (VectorField.lieBracket 𝕜 U (fun (y : E) => (A y) (W y)) x) = ((fderiv 𝕜 A x) ((A x) (U x))) (W x) - ((fderiv 𝕜 A x) ((A x) (W x))) (U x) + (A x) (((fderiv 𝕜 A x) (W x)) (U x)) - (A x) (((fderiv 𝕜 A x) (U x)) (W x))

Pointwise vector-field bracket formula for the Nijenhuis expression on a normed space: when A x squares to -1, the derivatives of U and W cancel out of [A U, A W] - [U, W] - A [A U, W] - A [U, A W].