Lie brackets of vector fields on manifolds

We define the Lie bracket of two vector fields, denoted with VectorField.mlieBracket I V W x, as the pullback in the manifold of the corresponding notion in the model space (through extChartAt I x).

The main results are the following:

• VectorField.mpullback_mlieBracket states that the pullback of the Lie bracket is the Lie bracket of the pullbacks.
• VectorField.leibniz_identity_mlieBracket is the Leibniz (or Jacobi) identity [U, [V, W]] = [[U, V], W] + [V, [U, W]].

The Lie bracket of vector fields in manifolds

noncomputable def VectorField.mlieBracketWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (V W : (x : M) → TangentSpace I x) (s : Set M) (x₀ : M) : TangentSpace I x₀

The Lie bracket of two vector fields in a manifold, within a set.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def VectorField.mlieBracket {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (V W : (x : M) → TangentSpace I x) (x₀ : M) : TangentSpace I x₀

The Lie bracket of two vector fields in a manifold.

Equations

• VectorField.mlieBracket I V W x₀ = VectorField.mlieBracketWithin I V W Set.univ x₀

theorem VectorField.mlieBracketWithin_def {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {V W : (x : M) → TangentSpace I x} : mlieBracketWithin I V W s = fun (x₀ : M) => mpullback I (modelWithCornersSelf 𝕜 E) (↑(extChartAt I x₀)) (lieBracketWithin 𝕜 (mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x₀).symm) V (Set.range ↑I)) (mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x₀).symm) W (Set.range ↑I)) (↑(extChartAt I x₀).symm ⁻¹' s ∩ Set.range ↑I)) x₀

theorem VectorField.mlieBracketWithin_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {x₀ : M} {V W : (x : M) → TangentSpace I x} : mlieBracketWithin I V W s x₀ = (mfderiv% ↑(extChartAt I x₀) x₀).inverse (lieBracketWithin 𝕜 (mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x₀).symm) V (Set.range ↑I)) (mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x₀).symm) W (Set.range ↑I)) (↑(extChartAt I x₀).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x₀) x₀))

theorem VectorField.mlieBracketWithin_eq_lieBracketWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : (x : E) → TangentSpace (modelWithCornersSelf 𝕜 E) x} {s : Set E} : mlieBracketWithin (modelWithCornersSelf 𝕜 E) V W s = lieBracketWithin 𝕜 V W s

@[simp]

theorem VectorField.mlieBracketWithin_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {V W : (x : M) → TangentSpace I x} : mlieBracketWithin I V W Set.univ = mlieBracket I V W

theorem VectorField.mlieBracketWithin_eq_zero_of_eq_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {x : M} {V W : (x : M) → TangentSpace I x} (hV : V x = 0) (hW : W x = 0) : mlieBracketWithin I V W s x = 0

theorem VectorField.mlieBracketWithin_swap_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {x : M} {V W : (x : M) → TangentSpace I x} : mlieBracketWithin I V W s x = -mlieBracketWithin I W V s x

theorem VectorField.mlieBracketWithin_swap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {V W : (x : M) → TangentSpace I x} : mlieBracketWithin I V W s = -mlieBracketWithin I W V s

theorem VectorField.mlieBracket_swap_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {x : M} {V W : (x : M) → TangentSpace I x} : mlieBracket I V W x = -mlieBracket I W V x

theorem VectorField.mlieBracket_swap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {V W : (x : M) → TangentSpace I x} : mlieBracket I V W = -mlieBracket I W V

@[simp]

theorem VectorField.mlieBracketWithin_self {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {V : (x : M) → TangentSpace I x} : mlieBracketWithin I V V = 0

@[simp]

theorem VectorField.mlieBracket_self {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {V : (x : M) → TangentSpace I x} : mlieBracket I V V = 0

@[simp]

theorem VectorField.mlieBracketWithin_zero_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {W : (x : M) → TangentSpace I x} : mlieBracketWithin I 0 W s = 0

We have [0, W] = 0 for all vector fields W: this depends on the junk value 0 if W is not differentiable. Version within a set.

@[simp]

theorem VectorField.mlieBracketWithin_zero_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {W : (x : M) → TangentSpace I x} : mlieBracketWithin I W 0 s = 0

We have [W, 0] = 0 for all vector fields W: this depends on the junk value 0 if W is not differentiable. Version within a set.

@[simp]

theorem VectorField.mlieBracket_zero_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {W : (x : M) → TangentSpace I x} : mlieBracket I 0 W = 0

We have [0, W] = 0 for all vector fields W: this depends on the junk value 0 if W is not differentiable.

@[simp]

theorem VectorField.mlieBracket_zero_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {W : (x : M) → TangentSpace I x} : mlieBracket I W 0 = 0

We have [W, 0] = 0 for all vector fields W: this depends on the junk value 0 if W is not differentiable.

theorem VectorField.mlieBracketWithin_congr_set' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s t : Set M} {x : M} {V W : (x : M) → TangentSpace I x} (y : M) (h : s =ᶠ[nhdsWithin x {y}ᶜ] t) : mlieBracketWithin I V W s x = mlieBracketWithin I V W t x

Variant of mlieBracketWithin_congr_set where one requires the sets to coincide only in the complement of a point.

theorem VectorField.mlieBracketWithin_congr_set {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s t : Set M} {x : M} {V W : (x : M) → TangentSpace I x} (h : s =ᶠ[nhds x] t) : mlieBracketWithin I V W s x = mlieBracketWithin I V W t x

theorem VectorField.mlieBracketWithin_inter {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s t : Set M} {x : M} {V W : (x : M) → TangentSpace I x} (ht : t ∈ nhds x) : mlieBracketWithin I V W (s ∩ t) x = mlieBracketWithin I V W s x

theorem VectorField.mlieBracketWithin_of_mem_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {x : M} {V W : (x : M) → TangentSpace I x} (h : s ∈ nhds x) : mlieBracketWithin I V W s x = mlieBracket I V W x

theorem VectorField.mlieBracketWithin_of_isOpen {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {x : M} {V W : (x : M) → TangentSpace I x} (hs : IsOpen s) (hx : x ∈ s) : mlieBracketWithin I V W s x = mlieBracket I V W x

theorem VectorField.mlieBracketWithin_eventually_congr_set' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s t : Set M} {x : M} {V W : (x : M) → TangentSpace I x} (y : M) (h : s =ᶠ[nhdsWithin x {y}ᶜ] t) : mlieBracketWithin I V W s =ᶠ[nhds x] mlieBracketWithin I V W t

Variant of mlieBracketWithin_eventually_congr_set where one requires the sets to coincide only in the complement of a point.

theorem VectorField.mlieBracketWithin_eventually_congr_set {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s t : Set M} {x : M} {V W : (x : M) → TangentSpace I x} (h : s =ᶠ[nhds x] t) : mlieBracketWithin I V W s =ᶠ[nhds x] mlieBracketWithin I V W t

theorem Filter.EventuallyEq.mlieBracketWithin_vectorField_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {x : M} {V W V₁ W₁ : (x : M) → TangentSpace I x} (hV : V₁ =ᶠ[nhdsWithin x s] V) (hxV : V₁ x = V x) (hW : W₁ =ᶠ[nhdsWithin x s] W) (hxW : W₁ x = W x) : VectorField.mlieBracketWithin I V₁ W₁ s x = VectorField.mlieBracketWithin I V W s x

theorem Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_of_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {x : M} {V W V₁ W₁ : (x : M) → TangentSpace I x} (hV : V₁ =ᶠ[nhdsWithin x s] V) (hW : W₁ =ᶠ[nhdsWithin x s] W) (hx : x ∈ s) : VectorField.mlieBracketWithin I V₁ W₁ s x = VectorField.mlieBracketWithin I V W s x

theorem Filter.EventuallyEq.mlieBracketWithin_vectorField' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s t : Set M} {x : M} {V W V₁ W₁ : (x : M) → TangentSpace I x} (hV : V₁ =ᶠ[nhdsWithin x s] V) (hW : W₁ =ᶠ[nhdsWithin x s] W) (ht : t ⊆ s) : VectorField.mlieBracketWithin I V₁ W₁ t =ᶠ[nhdsWithin x s] VectorField.mlieBracketWithin I V W t

If vector fields coincide on a neighborhood of a point within a set, then the Lie brackets also coincide on a neighborhood of this point within this set. Version where one considers the Lie bracket within a subset.

theorem Filter.EventuallyEq.mlieBracketWithin_vectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {x : M} {V W V₁ W₁ : (x : M) → TangentSpace I x} (hV : V₁ =ᶠ[nhdsWithin x s] V) (hW : W₁ =ᶠ[nhdsWithin x s] W) : VectorField.mlieBracketWithin I V₁ W₁ s =ᶠ[nhdsWithin x s] VectorField.mlieBracketWithin I V W s

theorem Filter.EventuallyEq.mlieBracketWithin_vectorField_of_insert {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {x : M} {V W V₁ W₁ : (x : M) → TangentSpace I x} (hV : V₁ =ᶠ[nhdsWithin x (insert x s)] V) (hW : W₁ =ᶠ[nhdsWithin x (insert x s)] W) : VectorField.mlieBracketWithin I V₁ W₁ s x = VectorField.mlieBracketWithin I V W s x

theorem Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {x : M} {V W V₁ W₁ : (x : M) → TangentSpace I x} (hV : V₁ =ᶠ[nhds x] V) (hW : W₁ =ᶠ[nhds x] W) : VectorField.mlieBracketWithin I V₁ W₁ s x = VectorField.mlieBracketWithin I V W s x

theorem VectorField.mlieBracketWithin_congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {x : M} {V W V₁ W₁ : (x : M) → TangentSpace I x} (hV : Set.EqOn V₁ V s) (hVx : V₁ x = V x) (hW : Set.EqOn W₁ W s) (hWx : W₁ x = W x) : mlieBracketWithin I V₁ W₁ s x = mlieBracketWithin I V W s x

theorem VectorField.mlieBracketWithin_congr' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {x : M} {V W V₁ W₁ : (x : M) → TangentSpace I x} (hV : Set.EqOn V₁ V s) (hW : Set.EqOn W₁ W s) (hx : x ∈ s) : mlieBracketWithin I V₁ W₁ s x = mlieBracketWithin I V W s x

Version of mlieBracketWithin_congr in which one assumes that the point belongs to the given set.

theorem Filter.EventuallyEq.mlieBracket_vectorField_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {x : M} {V W V₁ W₁ : (x : M) → TangentSpace I x} (hV : V₁ =ᶠ[nhds x] V) (hW : W₁ =ᶠ[nhds x] W) : VectorField.mlieBracket I V₁ W₁ x = VectorField.mlieBracket I V W x

theorem Filter.EventuallyEq.mlieBracket_vectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {x : M} {V W V₁ W₁ : (x : M) → TangentSpace I x} (hV : V₁ =ᶠ[nhds x] V) (hW : W₁ =ᶠ[nhds x] W) : VectorField.mlieBracket I V₁ W₁ =ᶠ[nhds x] VectorField.mlieBracket I V W

theorem MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {x : M} {V : (x : M) → TangentSpace I x} [IsManifold I 2 M] [CompleteSpace E] (hV : (MDiffAt[s] fun (x : M) => ⟨x, V x⟩) x) : DifferentiableWithinAt 𝕜 (VectorField.mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x).symm) V (Set.range ↑I)) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x)

theorem VectorField.mfderiv_extChartAt_inverse_comp_mfderivWithin_extChartAT_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {x : M} [IsManifold I 2 M] (Y : TangentSpace I x) : ((mfderiv% ↑(extChartAt I x) x).inverse.comp (mfderivWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x).symm) (Set.range ↑I) (↑(extChartAt I x) x)).inverse) Y = Y

theorem VectorField.mpullback_mfderivWithin_apply_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {x : M} {V W : (x : M) → TangentSpace I x} [IsManifold I 2 M] {f : M → 𝕜} (hf : MDiffAt[s] f x) : have V' := mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x).symm) V (Set.range ↑I); have W' := mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x).symm) W (Set.range ↑I); mpullback I (modelWithCornersSelf 𝕜 E) (↑(extChartAt I x)) (fun (x₀ : E) => (fderivWithin 𝕜 (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) x₀) (V' x₀) • W' x₀) x = (mfderivWithin I (modelWithCornersSelf 𝕜 𝕜) f s x) (V x) • W x

Pulling back through extChartAt the scalar multiplication of a vector field by the derivative of a scalar function equals the scalar multiplication by the manifold derivative.

theorem VectorField.mlieBracketWithin_smul_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {x : M} {V W : (x : M) → TangentSpace I x} [IsManifold I 2 M] [CompleteSpace E] {f : M → 𝕜} (hf : MDiffAt[s] f x) (hW : (MDiffAt[s] fun (x : M) => ⟨x, W x⟩) x) (hs : UniqueMDiffWithinAt I s x) : mlieBracketWithin I V (f • W) s x = (mfderivWithin I (modelWithCornersSelf 𝕜 𝕜) f s x) (V x) • W x + f x • mlieBracketWithin I V W s x

Product rule for Lie brackets: given two vector fields V and W on M and a function f : M → 𝕜, we have [V, f • W] = (df V) • W + f • [V, W]. Version within a set.

theorem VectorField.mlieBracket_smul_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {x : M} {V W : (x : M) → TangentSpace I x} [IsManifold I 2 M] [CompleteSpace E] {f : M → 𝕜} (hf : MDiffAt f x) (hW : (MDiffAt fun (x : M) => ⟨x, W x⟩) x) : mlieBracket I V (f • W) x = (mfderiv% f x) (V x) • W x + f x • mlieBracket I V W x

Product rule for Lie brackets: given two vector fields V and W on M and a function f : M → 𝕜, we have [V, f • W] = (df V) • W + f • [V, W].

theorem VectorField.mlieBracketWithin_smul_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {x : M} {V W : (x : M) → TangentSpace I x} [IsManifold I 2 M] [CompleteSpace E] {f : M → 𝕜} (hf : MDiffAt[s] f x) (hV : (MDiffAt[s] fun (x : M) => ⟨x, V x⟩) x) (hs : UniqueMDiffWithinAt I s x) : mlieBracketWithin I (f • V) W s x = -(mfderivWithin I (modelWithCornersSelf 𝕜 𝕜) f s x) (W x) • V x + f x • mlieBracketWithin I V W s x

Product rule for Lie brackets: given two vector fields V and W on M and a function f : M → 𝕜, we have [f • V, W] = -(df W) • V + f • [V, W]. Version within a set.

theorem VectorField.mlieBracket_smul_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {x : M} {V W : (x : M) → TangentSpace I x} [IsManifold I 2 M] [CompleteSpace E] {f : M → 𝕜} (hf : MDiffAt f x) (hV : (MDiffAt fun (x : M) => ⟨x, V x⟩) x) : mlieBracket I (f • V) W x = -(mfderiv% f x) (W x) • V x + f x • mlieBracket I V W x

Product rule for Lie brackets: given two vector fields V and W on M and a function f : M → 𝕜, we have [f • V, W] = -(df W) • V + f • [V, W].

theorem VectorField.mlieBracketWithin_const_smul_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {x : M} {V W : (x : M) → TangentSpace I x} {c : 𝕜} [IsManifold I 2 M] [CompleteSpace E] (hV : MDiffAt[s] (T% V) x) (hs : UniqueMDiffWithinAt I s x) : mlieBracketWithin I (c • V) W s x = c • mlieBracketWithin I V W s x

theorem VectorField.mlieBracket_const_smul_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {x : M} {V W : (x : M) → TangentSpace I x} {c : 𝕜} [IsManifold I 2 M] [CompleteSpace E] (hV : MDiffAt (T% V) x) : mlieBracket I (c • V) W x = c • mlieBracket I V W x

theorem VectorField.mlieBracketWithin_const_smul_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {x : M} {V W : (x : M) → TangentSpace I x} {c : 𝕜} [IsManifold I 2 M] [CompleteSpace E] (hW : MDiffAt[s] (T% W) x) (hs : UniqueMDiffWithinAt I s x) : mlieBracketWithin I V (c • W) s x = c • mlieBracketWithin I V W s x

theorem VectorField.mlieBracket_const_smul_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {x : M} {V W : (x : M) → TangentSpace I x} {c : 𝕜} [IsManifold I 2 M] [CompleteSpace E] (hW : MDiffAt (T% W) x) : mlieBracket I V (c • W) x = c • mlieBracket I V W x

theorem VectorField.mlieBracketWithin_add_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {x : M} {V W V₁ : (x : M) → TangentSpace I x} [IsManifold I 2 M] [CompleteSpace E] (hV : MDiffAt[s] (T% V) x) (hV₁ : MDiffAt[s] (T% V₁) x) (hs : UniqueMDiffWithinAt I s x) : mlieBracketWithin I (V + V₁) W s x = mlieBracketWithin I V W s x + mlieBracketWithin I V₁ W s x

theorem VectorField.mlieBracket_add_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {x : M} {V W V₁ : (x : M) → TangentSpace I x} [IsManifold I 2 M] [CompleteSpace E] (hV : MDiffAt (T% V) x) (hV₁ : MDiffAt (T% V₁) x) : mlieBracket I (V + V₁) W x = mlieBracket I V W x + mlieBracket I V₁ W x

theorem VectorField.mlieBracketWithin_add_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {x : M} {V W W₁ : (x : M) → TangentSpace I x} [IsManifold I 2 M] [CompleteSpace E] (hW : MDiffAt[s] (T% W) x) (hW₁ : MDiffAt[s] (T% W₁) x) (hs : UniqueMDiffWithinAt I s x) : mlieBracketWithin I V (W + W₁) s x = mlieBracketWithin I V W s x + mlieBracketWithin I V W₁ s x

theorem VectorField.mlieBracket_add_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {x : M} {V W W₁ : (x : M) → TangentSpace I x} [IsManifold I 2 M] [CompleteSpace E] (hW : MDiffAt (T% W) x) (hW₁ : MDiffAt (T% W₁) x) : mlieBracket I V (W + W₁) x = mlieBracket I V W x + mlieBracket I V W₁ x

theorem VectorField.mlieBracketWithin_of_mem_nhdsWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s t : Set M} {x : M} {V W : (x : M) → TangentSpace I x} [IsManifold I 2 M] [CompleteSpace E] (st : t ∈ nhdsWithin x s) (hs : UniqueMDiffWithinAt I s x) (hV : MDiffAt[t] (T% V) x) (hW : MDiffAt[t] (T% W) x) : mlieBracketWithin I V W s x = mlieBracketWithin I V W t x

theorem VectorField.mlieBracketWithin_subset {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s t : Set M} {x : M} {V W : (x : M) → TangentSpace I x} [IsManifold I 2 M] [CompleteSpace E] (st : s ⊆ t) (ht : UniqueMDiffWithinAt I s x) (hV : MDiffAt[t] (T% V) x) (hW : MDiffAt[t] (T% W) x) : mlieBracketWithin I V W s x = mlieBracketWithin I V W t x

theorem VectorField.mlieBracketWithin_eq_mlieBracket {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {x : M} {V W : (x : M) → TangentSpace I x} [IsManifold I 2 M] [CompleteSpace E] (hs : UniqueMDiffWithinAt I s x) (hV : MDiffAt (T% V) x) (hW : MDiffAt (T% W) x) : mlieBracketWithin I V W s x = mlieBracket I V W x

theorem DifferentiableWithinAt.mlieBracketWithin_congr_mono {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s t : Set M} {x : M} {V W V₁ W₁ : (x : M) → TangentSpace I x} [IsManifold I 2 M] [CompleteSpace E] (hV : MDiffAt[s] (T% V) x) (hVs : Set.EqOn V₁ V t) (hVx : V₁ x = V x) (hW : MDiffAt[s] (T% W) x) (hWs : Set.EqOn W₁ W t) (hWx : W₁ x = W x) (hxt : UniqueMDiffWithinAt I t x) (h₁ : t ⊆ s) : VectorField.mlieBracketWithin I V₁ W₁ t x = VectorField.mlieBracketWithin I V W s x

theorem VectorField.mpullbackWithin_mlieBracketWithin_of_isSymmSndFDerivWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I 2 M] [IsManifold I' 2 M'] [CompleteSpace E] {f : M → M'} {V W : (x : M') → TangentSpace I' x} {x₀ : M} {s : Set M} {t : Set M'} (hV : MDiffAt[t] (T% V) (f x₀)) (hW : MDiffAt[t] (T% W) (f x₀)) (hu : UniqueMDiffOn I s) (hf : ContMDiffWithinAt I I' 2 f s x₀) (hx₀ : x₀ ∈ s) (hst : f ⁻¹' t ∈ nhdsWithin x₀ s) (hsymm : IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm) (↑(extChartAt I x₀).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x₀) x₀)) : mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀ = mlieBracketWithin I (mpullbackWithin I I' f V s) (mpullbackWithin I I' f W s) s x₀

theorem VectorField.mpullbackWithin_mlieBracketWithin' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I (minSmoothness 𝕜 2) M] [IsManifold I' (minSmoothness 𝕜 2) M'] [CompleteSpace E] {n : WithTop ℕ∞} {f : M → M'} {V W : (x : M') → TangentSpace I' x} {x₀ : M} {s u : Set M} {t : Set M'} (hV : MDiffAt[t] (T% V) (f x₀)) (hW : MDiffAt[t] (T% W) (f x₀)) (hs : UniqueMDiffOn I s) (hu : UniqueMDiffOn I u) (hf : ContMDiffWithinAt I I' n f u x₀) (hx₀ : x₀ ∈ s) (hn : minSmoothness 𝕜 2 ≤ n) (hst : f ⁻¹' t ∈ nhdsWithin x₀ s) (h'x₀ : x₀ ∈ closure (interior u)) (hsu : s ⊆ u) : mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀ = mlieBracketWithin I (mpullbackWithin I I' f V s) (mpullbackWithin I I' f W s) s x₀

The pullback commutes with the Lie bracket of vector fields on manifolds. Version where one assumes that the map is smooth on a larger set u (so that the condition x₀ ∈ closure (interior u), needed to guarantee the symmetry of the second derivative, becomes easier to check.)

theorem VectorField.mpullbackWithin_mlieBracketWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I (minSmoothness 𝕜 2) M] [IsManifold I' (minSmoothness 𝕜 2) M'] [CompleteSpace E] {n : WithTop ℕ∞} {f : M → M'} {V W : (x : M') → TangentSpace I' x} {x₀ : M} {s : Set M} {t : Set M'} (hV : MDiffAt[t] (T% V) (f x₀)) (hW : MDiffAt[t] (T% W) (f x₀)) (hu : UniqueMDiffOn I s) (hf : ContMDiffWithinAt I I' n f s x₀) (hx₀ : x₀ ∈ s) (hn : minSmoothness 𝕜 2 ≤ n) (hst : f ⁻¹' t ∈ nhdsWithin x₀ s) (h'x₀ : x₀ ∈ closure (interior s)) : mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀ = mlieBracketWithin I (mpullbackWithin I I' f V s) (mpullbackWithin I I' f W s) s x₀

The pullback commutes with the Lie bracket of vector fields on manifolds.

theorem VectorField.mpullback_mlieBracketWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I (minSmoothness 𝕜 2) M] [IsManifold I' (minSmoothness 𝕜 2) M'] [CompleteSpace E] {n : WithTop ℕ∞} {f : M → M'} {V W : (x : M') → TangentSpace I' x} {x₀ : M} {s : Set M} {t : Set M'} (hV : MDiffAt[t] (T% V) (f x₀)) (hW : MDiffAt[t] (T% W) (f x₀)) (hu : UniqueMDiffOn I s) (hf : ContMDiffAt I I' n f x₀) (hx₀ : x₀ ∈ s) (hn : minSmoothness 𝕜 2 ≤ n) (hst : f ⁻¹' t ∈ nhdsWithin x₀ s) : mpullback I I' f (mlieBracketWithin I' V W t) x₀ = mlieBracketWithin I (mpullback I I' f V) (mpullback I I' f W) s x₀

The pullback commutes with the Lie bracket of vector fields on manifolds.

theorem VectorField.mpullback_mlieBracket {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I (minSmoothness 𝕜 2) M] [IsManifold I' (minSmoothness 𝕜 2) M'] [CompleteSpace E] {n : WithTop ℕ∞} {f : M → M'} {V W : (x : M') → TangentSpace I' x} {x₀ : M} (hV : MDiffAt (T% V) (f x₀)) (hW : MDiffAt (T% W) (f x₀)) (hf : ContMDiffAt I I' n f x₀) (hn : minSmoothness 𝕜 2 ≤ n) : mpullback I I' f (mlieBracket I' V W) x₀ = mlieBracket I (mpullback I I' f V) (mpullback I I' f W) x₀

theorem ContMDiffWithinAt.mlieBracketWithin_vectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (minSmoothness 𝕜 2) M] [CompleteSpace E] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] {m : WithTop ℕ∞} {U V : (x : M) → TangentSpace I x} {s : Set M} {x : M} (hU : ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 E)) n (fun (x : M) => ⟨x, U x⟩) s x) (hV : ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 E)) n (fun (x : M) => ⟨x, V x⟩) s x) (hs : UniqueMDiffOn I s) (hx : x ∈ s) (hmn : minSmoothness 𝕜 (m + 1) ≤ n) : ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 E)) m (fun (x₀ : M) => ⟨x₀, VectorField.mlieBracketWithin I U V s x₀⟩) s x

If two vector fields are C^n with n ≥ m + 1, then their Lie bracket is C^m.

theorem ContMDiffAt.mlieBracket_vectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (minSmoothness 𝕜 2) M] [CompleteSpace E] {m n : ℕ∞} [IsManifold I (↑n + 1) M] {U V : (x : M) → TangentSpace I x} {x : M} (hU : ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 E)) (↑n) (fun (x : M) => ⟨x, U x⟩) x) (hV : ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 E)) (↑n) (fun (x : M) => ⟨x, V x⟩) x) (hmn : minSmoothness 𝕜 (↑m + 1) ≤ ↑n) : ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 E)) (↑m) (fun (x₀ : M) => ⟨x₀, VectorField.mlieBracket I U V x₀⟩) x

If two vector fields are C^n with n ≥ m + 1, then their Lie bracket is C^m.

theorem ContMDiffOn.mlieBracketWithin_vectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} [IsManifold I (minSmoothness 𝕜 2) M] [CompleteSpace E] {m n : ℕ∞} [IsManifold I (↑n + 1) M] {U V : (x : M) → TangentSpace I x} (hU : ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 E)) (↑n) (fun (x : M) => ⟨x, U x⟩) s) (hV : ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 E)) (↑n) (fun (x : M) => ⟨x, V x⟩) s) (hs : UniqueMDiffOn I s) (hmn : minSmoothness 𝕜 (↑m + 1) ≤ ↑n) : ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 E)) (↑m) (fun (x₀ : M) => ⟨x₀, VectorField.mlieBracketWithin I U V s x₀⟩) s

If two vector fields are C^n with n ≥ m + 1, then their Lie bracket is C^m.

theorem ContDiff.mlieBracket_vectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (minSmoothness 𝕜 2) M] [CompleteSpace E] {m n : ℕ∞} [IsManifold I (↑n + 1) M] {U V : (x : M) → TangentSpace I x} (hU : ContMDiff I (I.prod (modelWithCornersSelf 𝕜 E)) ↑n fun (x : M) => ⟨x, U x⟩) (hV : ContMDiff I (I.prod (modelWithCornersSelf 𝕜 E)) ↑n fun (x : M) => ⟨x, V x⟩) (hmn : minSmoothness 𝕜 (↑m + 1) ≤ ↑n) : ContMDiff I (I.prod (modelWithCornersSelf 𝕜 E)) ↑m fun (x₀ : M) => ⟨x₀, VectorField.mlieBracket I U V x₀⟩

If two vector fields are C^n with n ≥ m + 1, then their Lie bracket is C^m.

theorem VectorField.leibniz_identity_mlieBracketWithin_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (minSmoothness 𝕜 3) M] [CompleteSpace E] {U V W : (x : M) → TangentSpace I x} {s : Set M} {x : M} (hs : UniqueMDiffOn I s) (h's : x ∈ closure (interior s)) (hx : x ∈ s) (hU : ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 E)) (minSmoothness 𝕜 2) (fun (x : M) => ⟨x, U x⟩) s x) (hV : ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 E)) (minSmoothness 𝕜 2) (fun (x : M) => ⟨x, V x⟩) s x) (hW : ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 E)) (minSmoothness 𝕜 2) (fun (x : M) => ⟨x, W x⟩) s x) : mlieBracketWithin I U (mlieBracketWithin I V W s) s x = mlieBracketWithin I (mlieBracketWithin I U V s) W s x + mlieBracketWithin I V (mlieBracketWithin I U W s) s x

The Lie bracket of vector fields in manifolds satisfies the Leibniz identity [U, [V, W]] = [[U, V], W] + [V, [U, W]] (also called Jacobi identity).

theorem VectorField.leibniz_identity_mlieBracket_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (minSmoothness 𝕜 3) M] [CompleteSpace E] {U V W : (x : M) → TangentSpace I x} {x : M} (hU : ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 E)) (minSmoothness 𝕜 2) (fun (x : M) => ⟨x, U x⟩) x) (hV : ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 E)) (minSmoothness 𝕜 2) (fun (x : M) => ⟨x, V x⟩) x) (hW : ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 E)) (minSmoothness 𝕜 2) (fun (x : M) => ⟨x, W x⟩) x) : mlieBracket I U (mlieBracket I V W) x = mlieBracket I (mlieBracket I U V) W x + mlieBracket I V (mlieBracket I U W) x

The Lie bracket of vector fields in manifolds satisfies the Leibniz identity [U, [V, W]] = [[U, V], W] + [V, [U, W]] (also called Jacobi identity).

theorem VectorField.leibniz_identity_mlieBracket {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (minSmoothness 𝕜 3) M] [CompleteSpace E] {U V W : (x : M) → TangentSpace I x} (hU : ContMDiff I (I.prod (modelWithCornersSelf 𝕜 E)) (minSmoothness 𝕜 2) fun (x : M) => ⟨x, U x⟩) (hV : ContMDiff I (I.prod (modelWithCornersSelf 𝕜 E)) (minSmoothness 𝕜 2) fun (x : M) => ⟨x, V x⟩) (hW : ContMDiff I (I.prod (modelWithCornersSelf 𝕜 E)) (minSmoothness 𝕜 2) fun (x : M) => ⟨x, W x⟩) : mlieBracket I U (mlieBracket I V W) = mlieBracket I (mlieBracket I U V) W + mlieBracket I V (mlieBracket I U W)

The Lie bracket of vector fields in manifolds satisfies the Leibniz identity [U, [V, W]] = [[U, V], W] + [V, [U, W]] (also called Jacobi identity).