feat: the Lie bracket of vector fields in vector spaces (#18852)

Author: sgouezel

Mathlib.lean

@@ -1172,6 +1172,7 @@ import Mathlib.Analysis.Calculus.SmoothSeries
 import Mathlib.Analysis.Calculus.TangentCone
 import Mathlib.Analysis.Calculus.Taylor
 import Mathlib.Analysis.Calculus.UniformLimitsDeriv
+import Mathlib.Analysis.Calculus.VectorField
 import Mathlib.Analysis.Complex.AbelLimit
 import Mathlib.Analysis.Complex.AbsMax
 import Mathlib.Analysis.Complex.Angle

Mathlib/Analysis/Calculus/VectorField.lean

@@ -0,0 +1,343 @@
+/-
+Copyright (c) 2024 Sébastien Gouëzel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sébastien Gouëzel
+-/
+import Mathlib.Analysis.Calculus.FDeriv.Symmetric
+
+/-!
+# Vector fields in vector spaces
+
+We study functions of the form `V : E → E` on a vector space, thinking of these as vector fields.
+We define several notions in this context, with the aim to generalize them to vector fields on
+manifolds.
+
+Notably, we define the pullback of a vector field under a map, as
+`VectorField.pullback 𝕜 f V x := (fderiv 𝕜 f x).inverse (V (f x))` (together with the same notion
+within a set).
+
+In addition to comprehensive API on this notion, the main result is the following:
+* `VectorField.leibniz_identity_lieBracket` is the Leibniz
+  identity `[U, [V, W]] = [[U, V], W] + [V, [U, W]]`.
+
+-/
+
+open Set
+open scoped Topology
+
+noncomputable section
+
+variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+  {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+  {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
+  {V W V₁ W₁ : E → E} {s t : Set E} {x : E}
+
+/-!
+### The Lie bracket of vector fields in a vector space
+
+We define the Lie bracket of two vector fields, and call it `lieBracket 𝕜 V W x`. We also define
+a version localized to sets, `lieBracketWithin 𝕜 V W s x`. We copy the relevant API
+of `fderivWithin` and `fderiv` for these notions to get a comprehensive API.
+-/
+
+namespace VectorField
+
+variable (𝕜) in
+/-- The Lie bracket `[V, W] (x)` of two vector fields at a point, defined as
+`DW(x) (V x) - DV(x) (W x)`. -/
+def lieBracket (V W : E → E) (x : E) : E :=
+  fderiv 𝕜 W x (V x) - fderiv 𝕜 V x (W x)
+
+variable (𝕜) in
+/-- The Lie bracket `[V, W] (x)` of two vector fields within a set at a point, defined as
+`DW(x) (V x) - DV(x) (W x)` where the derivatives are taken inside `s`. -/
+def lieBracketWithin (V W : E → E) (s : Set E) (x : E) : E :=
+  fderivWithin 𝕜 W s x (V x) - fderivWithin 𝕜 V s x (W x)
+
+lemma lieBracket_eq :
+    lieBracket 𝕜 V W = fun x ↦ fderiv 𝕜 W x (V x) - fderiv 𝕜 V x (W x) := rfl
+
+lemma lieBracketWithin_eq :
+    lieBracketWithin 𝕜 V W s =
+      fun x ↦ fderivWithin 𝕜 W s x (V x) - fderivWithin 𝕜 V s x (W x) := rfl
+
+@[simp]
+theorem lieBracketWithin_univ : lieBracketWithin 𝕜 V W univ = lieBracket 𝕜 V W := by
+  ext1 x
+  simp [lieBracketWithin, lieBracket]
+
+lemma lieBracketWithin_eq_zero_of_eq_zero (hV : V x = 0) (hW : W x = 0) :
+    lieBracketWithin 𝕜 V W s x = 0 := by
+  simp [lieBracketWithin, hV, hW]
+
+lemma lieBracket_eq_zero_of_eq_zero (hV : V x = 0) (hW : W x = 0) :
+    lieBracket 𝕜 V W x = 0 := by
+  simp [lieBracket, hV, hW]
+
+lemma lieBracketWithin_smul_left {c : 𝕜} (hV : DifferentiableWithinAt 𝕜 V s x)
+    (hs : UniqueDiffWithinAt 𝕜 s x) :
+    lieBracketWithin 𝕜 (c • V) W s x =
+      c • lieBracketWithin 𝕜 V W s x := by
+  simp only [lieBracketWithin, Pi.add_apply, map_add, Pi.smul_apply, map_smul, smul_sub]
+  rw [fderivWithin_const_smul' hs hV]
+  rfl
+
+lemma lieBracket_smul_left {c : 𝕜} (hV : DifferentiableAt 𝕜 V x) :
+    lieBracket 𝕜 (c • V) W x = c • lieBracket 𝕜 V W x := by
+  simp only [← differentiableWithinAt_univ, ← lieBracketWithin_univ] at hV ⊢
+  exact lieBracketWithin_smul_left hV uniqueDiffWithinAt_univ
+
+lemma lieBracketWithin_smul_right {c : 𝕜} (hW : DifferentiableWithinAt 𝕜 W s x)
+    (hs : UniqueDiffWithinAt 𝕜 s x) :
+    lieBracketWithin 𝕜 V (c • W) s x =
+      c • lieBracketWithin 𝕜 V W s x := by
+  simp only [lieBracketWithin, Pi.add_apply, map_add, Pi.smul_apply, map_smul, smul_sub]
+  rw [fderivWithin_const_smul' hs hW]
+  rfl
+
+lemma lieBracket_smul_right {c : 𝕜} (hW : DifferentiableAt 𝕜 W x) :
+    lieBracket 𝕜 V (c • W) x = c • lieBracket 𝕜 V W x := by
+  simp only [← differentiableWithinAt_univ, ← lieBracketWithin_univ] at hW ⊢
+  exact lieBracketWithin_smul_right hW uniqueDiffWithinAt_univ
+
+lemma lieBracketWithin_add_left (hV : DifferentiableWithinAt 𝕜 V s x)
+    (hV₁ : DifferentiableWithinAt 𝕜 V₁ s x) (hs : UniqueDiffWithinAt 𝕜 s x) :
+    lieBracketWithin 𝕜 (V + V₁) W s x =
+      lieBracketWithin 𝕜 V W s x + lieBracketWithin 𝕜 V₁ W s x := by
+  simp only [lieBracketWithin, Pi.add_apply, map_add]
+  rw [fderivWithin_add' hs hV hV₁, ContinuousLinearMap.add_apply]
+  abel
+
+lemma lieBracket_add_left (hV : DifferentiableAt 𝕜 V x) (hV₁ : DifferentiableAt 𝕜 V₁ x) :
+    lieBracket 𝕜 (V + V₁) W  x =
+      lieBracket 𝕜 V W x + lieBracket 𝕜 V₁ W x := by
+  simp only [lieBracket, Pi.add_apply, map_add]
+  rw [fderiv_add' hV hV₁, ContinuousLinearMap.add_apply]
+  abel
+
+lemma lieBracketWithin_add_right (hW : DifferentiableWithinAt 𝕜 W s x)
+    (hW₁ : DifferentiableWithinAt 𝕜 W₁ s x) (hs :  UniqueDiffWithinAt 𝕜 s x) :
+    lieBracketWithin 𝕜 V (W + W₁) s x =
+      lieBracketWithin 𝕜 V W s x + lieBracketWithin 𝕜 V W₁ s x := by
+  simp only [lieBracketWithin, Pi.add_apply, map_add]
+  rw [fderivWithin_add' hs hW hW₁, ContinuousLinearMap.add_apply]
+  abel
+
+lemma lieBracket_add_right (hW : DifferentiableAt 𝕜 W x) (hW₁ : DifferentiableAt 𝕜 W₁ x) :
+    lieBracket 𝕜 V (W + W₁) x =
+      lieBracket 𝕜 V W x + lieBracket 𝕜 V W₁ x := by
+  simp only [lieBracket, Pi.add_apply, map_add]
+  rw [fderiv_add' hW hW₁, ContinuousLinearMap.add_apply]
+  abel
+
+lemma lieBracketWithin_swap : lieBracketWithin 𝕜 V W s = - lieBracketWithin 𝕜 W V s := by
+  ext x; simp [lieBracketWithin]
+
+lemma lieBracket_swap : lieBracket 𝕜 V W x = - lieBracket 𝕜 W V x := by
+  simp [lieBracket]
+
+@[simp] lemma lieBracketWithin_self : lieBracketWithin 𝕜 V V s = 0 := by
+  ext x; simp [lieBracketWithin]
+
+@[simp] lemma lieBracket_self : lieBracket 𝕜 V V = 0 := by
+  ext x; simp [lieBracket]
+
+lemma _root_.ContDiffWithinAt.lieBracketWithin_vectorField
+    {m n : ℕ∞} (hV : ContDiffWithinAt 𝕜 n V s x)
+    (hW : ContDiffWithinAt 𝕜 n W s x) (hs : UniqueDiffOn 𝕜 s) (hmn : m + 1 ≤ n) (hx : x ∈ s) :
+    ContDiffWithinAt 𝕜 m (lieBracketWithin 𝕜 V W s) s x := by
+  apply ContDiffWithinAt.sub
+  · exact ContDiffWithinAt.clm_apply (hW.fderivWithin_right hs hmn hx)
+      (hV.of_le (le_trans le_self_add hmn))
+  · exact ContDiffWithinAt.clm_apply (hV.fderivWithin_right hs hmn hx)
+      (hW.of_le (le_trans le_self_add hmn))
+
+lemma _root_.ContDiffAt.lieBracket_vectorField {m n : ℕ∞} (hV : ContDiffAt 𝕜 n V x)
+    (hW : ContDiffAt 𝕜 n W x) (hmn : m + 1 ≤ n) :
+    ContDiffAt 𝕜 m (lieBracket 𝕜 V W) x := by
+  rw [← contDiffWithinAt_univ] at hV hW ⊢
+  simp_rw [← lieBracketWithin_univ]
+  exact hV.lieBracketWithin_vectorField hW uniqueDiffOn_univ hmn (mem_univ _)
+
+lemma _root_.ContDiffOn.lieBracketWithin_vectorField {m n : ℕ∞} (hV : ContDiffOn 𝕜 n V s)
+    (hW : ContDiffOn 𝕜 n W s) (hs : UniqueDiffOn 𝕜 s) (hmn : m + 1 ≤ n) :
+    ContDiffOn 𝕜 m (lieBracketWithin 𝕜 V W s) s :=
+  fun x hx ↦ (hV x hx).lieBracketWithin_vectorField (hW x hx) hs hmn hx
+
+lemma _root_.ContDiff.lieBracket_vectorField {m n : ℕ∞} (hV : ContDiff 𝕜 n V)
+    (hW : ContDiff 𝕜 n W) (hmn : m + 1 ≤ n) :
+    ContDiff 𝕜 m (lieBracket 𝕜 V W) :=
+  contDiff_iff_contDiffAt.2 (fun _ ↦ hV.contDiffAt.lieBracket_vectorField hW.contDiffAt hmn)
+
+theorem lieBracketWithin_of_mem_nhdsWithin (st : t ∈ 𝓝[s] x) (hs : UniqueDiffWithinAt 𝕜 s x)
+    (hV : DifferentiableWithinAt 𝕜 V t x) (hW : DifferentiableWithinAt 𝕜 W t x) :
+    lieBracketWithin 𝕜 V W s x = lieBracketWithin 𝕜 V W t x := by
+  simp [lieBracketWithin, fderivWithin_of_mem_nhdsWithin st hs hV,
+    fderivWithin_of_mem_nhdsWithin st hs hW]
+
+theorem lieBracketWithin_subset (st : s ⊆ t) (ht : UniqueDiffWithinAt 𝕜 s x)
+    (hV : DifferentiableWithinAt 𝕜 V t x) (hW : DifferentiableWithinAt 𝕜 W t x) :
+    lieBracketWithin 𝕜 V W s x = lieBracketWithin 𝕜 V W t x :=
+  lieBracketWithin_of_mem_nhdsWithin (nhdsWithin_mono _ st self_mem_nhdsWithin) ht hV hW
+
+theorem lieBracketWithin_inter (ht : t ∈ 𝓝 x) :
+    lieBracketWithin 𝕜 V W (s ∩ t) x = lieBracketWithin 𝕜 V W s x := by
+  simp [lieBracketWithin, fderivWithin_inter, ht]
+
+theorem lieBracketWithin_of_mem_nhds (h : s ∈ 𝓝 x) :
+    lieBracketWithin 𝕜 V W s x = lieBracket 𝕜 V W x := by
+  rw [← lieBracketWithin_univ, ← univ_inter s, lieBracketWithin_inter h]
+
+theorem lieBracketWithin_of_isOpen (hs : IsOpen s) (hx : x ∈ s) :
+    lieBracketWithin 𝕜 V W s x = lieBracket 𝕜 V W x :=
+  lieBracketWithin_of_mem_nhds (hs.mem_nhds hx)
+
+theorem lieBracketWithin_eq_lieBracket (hs : UniqueDiffWithinAt 𝕜 s x)
+    (hV : DifferentiableAt 𝕜 V x) (hW : DifferentiableAt 𝕜 W x) :
+    lieBracketWithin 𝕜 V W s x = lieBracket 𝕜 V W x := by
+  simp [lieBracketWithin, lieBracket, fderivWithin_eq_fderiv, hs, hV, hW]
+
+/-- Variant of `lieBracketWithin_congr_set` where one requires the sets to coincide only in
+the complement of a point. -/
+theorem lieBracketWithin_congr_set' (y : E) (h : s =ᶠ[𝓝[{y}ᶜ] x] t) :
+    lieBracketWithin 𝕜 V W s x = lieBracketWithin 𝕜 V W t x := by
+  simp [lieBracketWithin, fderivWithin_congr_set' _ h]
+
+theorem lieBracketWithin_congr_set (h : s =ᶠ[𝓝 x] t) :
+    lieBracketWithin 𝕜 V W s x = lieBracketWithin 𝕜 V W t x :=
+  lieBracketWithin_congr_set' x <| h.filter_mono inf_le_left
+
+/-- Variant of `lieBracketWithin_eventually_congr_set` where one requires the sets to coincide only
+in  the complement of a point. -/
+theorem lieBracketWithin_eventually_congr_set' (y : E) (h : s =ᶠ[𝓝[{y}ᶜ] x] t) :
+    lieBracketWithin 𝕜 V W s =ᶠ[𝓝 x] lieBracketWithin 𝕜 V W t :=
+  (eventually_nhds_nhdsWithin.2 h).mono fun _ => lieBracketWithin_congr_set' y
+
+theorem lieBracketWithin_eventually_congr_set (h : s =ᶠ[𝓝 x] t) :
+    lieBracketWithin 𝕜 V W s =ᶠ[𝓝 x] lieBracketWithin 𝕜 V W t :=
+  lieBracketWithin_eventually_congr_set' x <| h.filter_mono inf_le_left
+
+theorem _root_.DifferentiableWithinAt.lieBracketWithin_congr_mono
+    (hV : DifferentiableWithinAt 𝕜 V s x) (hVs : EqOn V₁ V t) (hVx : V₁ x = V x)
+    (hW : DifferentiableWithinAt 𝕜 W s x) (hWs : EqOn W₁ W t) (hWx : W₁ x = W x)
+    (hxt : UniqueDiffWithinAt 𝕜 t x) (h₁ : t ⊆ s) :
+    lieBracketWithin 𝕜 V₁ W₁ t x = lieBracketWithin 𝕜 V W s x := by
+  simp [lieBracketWithin, hV.fderivWithin_congr_mono, hW.fderivWithin_congr_mono, hVs, hVx,
+    hWs, hWx, hxt, h₁]
+
+theorem _root_.Filter.EventuallyEq.lieBracketWithin_vectorField_eq
+    (hV : V₁ =ᶠ[𝓝[s] x] V) (hxV : V₁ x = V x) (hW : W₁ =ᶠ[𝓝[s] x] W) (hxW : W₁ x = W x) :
+    lieBracketWithin 𝕜 V₁ W₁ s x = lieBracketWithin 𝕜 V W s x := by
+  simp only [lieBracketWithin, hV.fderivWithin_eq hxV, hW.fderivWithin_eq hxW, hxV, hxW]
+
+theorem _root_.Filter.EventuallyEq.lieBracketWithin_vectorField_eq_of_mem
+    (hV : V₁ =ᶠ[𝓝[s] x] V) (hW : W₁ =ᶠ[𝓝[s] x] W) (hx : x ∈ s) :
+    lieBracketWithin 𝕜 V₁ W₁ s x = lieBracketWithin 𝕜 V W s x :=
+  hV.lieBracketWithin_vectorField_eq (mem_of_mem_nhdsWithin hx hV :)
+    hW (mem_of_mem_nhdsWithin hx hW :)
+
+/-- 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 _root_.Filter.EventuallyEq.lieBracketWithin_vectorField'
+    (hV : V₁ =ᶠ[𝓝[s] x] V) (hW : W₁ =ᶠ[𝓝[s] x] W) (ht : t ⊆ s) :
+    lieBracketWithin 𝕜 V₁ W₁ t =ᶠ[𝓝[s] x] lieBracketWithin 𝕜 V W t := by
+  filter_upwards [hV.fderivWithin' ht (𝕜 := 𝕜), hW.fderivWithin' ht (𝕜 := 𝕜), hV, hW]
+    with x hV' hW' hV hW
+  simp [lieBracketWithin, hV', hW', hV, hW]
+
+protected theorem _root_.Filter.EventuallyEq.lieBracketWithin_vectorField
+    (hV : V₁ =ᶠ[𝓝[s] x] V) (hW : W₁ =ᶠ[𝓝[s] x] W) :
+    lieBracketWithin 𝕜 V₁ W₁ s =ᶠ[𝓝[s] x] lieBracketWithin 𝕜 V W s :=
+  hV.lieBracketWithin_vectorField' hW Subset.rfl
+
+protected theorem _root_.Filter.EventuallyEq.lieBracketWithin_vectorField_eq_of_insert
+    (hV : V₁ =ᶠ[𝓝[insert x s] x] V) (hW : W₁ =ᶠ[𝓝[insert x s] x] W) :
+    lieBracketWithin 𝕜 V₁ W₁ s x = lieBracketWithin 𝕜 V W s x := by
+  apply mem_of_mem_nhdsWithin (mem_insert x s) (hV.lieBracketWithin_vectorField' hW
+    (subset_insert x s))
+
+theorem _root_.Filter.EventuallyEq.lieBracketWithin_vectorField_eq_nhds
+    (hV : V₁ =ᶠ[𝓝 x] V) (hW : W₁ =ᶠ[𝓝 x] W) :
+    lieBracketWithin 𝕜 V₁ W₁ s x = lieBracketWithin 𝕜 V W s x :=
+  (hV.filter_mono nhdsWithin_le_nhds).lieBracketWithin_vectorField_eq hV.self_of_nhds
+    (hW.filter_mono nhdsWithin_le_nhds) hW.self_of_nhds
+
+theorem lieBracketWithin_congr
+    (hV : EqOn V₁ V s) (hVx : V₁ x = V x) (hW : EqOn W₁ W s) (hWx : W₁ x = W x) :
+    lieBracketWithin 𝕜 V₁ W₁ s x = lieBracketWithin 𝕜 V W s x :=
+  (hV.eventuallyEq.filter_mono inf_le_right).lieBracketWithin_vectorField_eq hVx
+    (hW.eventuallyEq.filter_mono inf_le_right) hWx
+
+/-- Version of `lieBracketWithin_congr` in which one assumes that the point belongs to the
+given set. -/
+theorem lieBracketWithin_congr' (hV : EqOn V₁ V s) (hW : EqOn W₁ W s) (hx : x ∈ s) :
+    lieBracketWithin 𝕜 V₁ W₁ s x = lieBracketWithin 𝕜 V W s x :=
+  lieBracketWithin_congr hV (hV hx) hW (hW hx)
+
+theorem _root_.Filter.EventuallyEq.lieBracket_vectorField_eq
+    (hV : V₁ =ᶠ[𝓝 x] V) (hW : W₁ =ᶠ[𝓝 x] W) :
+    lieBracket 𝕜 V₁ W₁ x = lieBracket 𝕜 V W x := by
+  rw [← lieBracketWithin_univ, ← lieBracketWithin_univ, hV.lieBracketWithin_vectorField_eq_nhds hW]
+
+protected theorem _root_.Filter.EventuallyEq.lieBracket_vectorField
+    (hV : V₁ =ᶠ[𝓝 x] V) (hW : W₁ =ᶠ[𝓝 x] W) : lieBracket 𝕜 V₁ W₁ =ᶠ[𝓝 x] lieBracket 𝕜 V W := by
+  filter_upwards [hV.eventuallyEq_nhds, hW.eventuallyEq_nhds] with y hVy hWy
+  exact hVy.lieBracket_vectorField_eq hWy
+
+/-- The Lie bracket of vector fields in vector spaces satisfies the Leibniz identity
+`[U, [V, W]] = [[U, V], W] + [V, [U, W]]`. -/
+lemma leibniz_identity_lieBracketWithin_of_isSymmSndFDerivWithinAt
+    {U V W : E → E} {s : Set E} {x : E} (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s)
+    (hU : ContDiffWithinAt 𝕜 2 U s x) (hV : ContDiffWithinAt 𝕜 2 V s x)
+    (hW : ContDiffWithinAt 𝕜 2 W s x)
+    (h'U : IsSymmSndFDerivWithinAt 𝕜 U s x) (h'V : IsSymmSndFDerivWithinAt 𝕜 V s x)
+    (h'W : IsSymmSndFDerivWithinAt 𝕜 W s x) :
+    lieBracketWithin 𝕜 U (lieBracketWithin 𝕜 V W s) s x =
+      lieBracketWithin 𝕜 (lieBracketWithin 𝕜 U V s) W s x
+      + lieBracketWithin 𝕜 V (lieBracketWithin 𝕜 U W s) s x := by
+  simp only [lieBracketWithin_eq, map_sub]
+  have aux₁ {U V : E → E} (hU : ContDiffWithinAt 𝕜 2 U s x) (hV : ContDiffWithinAt 𝕜 2 V s x) :
+      DifferentiableWithinAt 𝕜 (fun x ↦ (fderivWithin 𝕜 V s x) (U x)) s x :=
+    have := hV.fderivWithin_right_apply (hU.of_le one_le_two) hs le_rfl hx
+    this.differentiableWithinAt le_rfl
+  have aux₂ {U V : E → E} (hU : ContDiffWithinAt 𝕜 2 U s x) (hV : ContDiffWithinAt 𝕜 2 V s x) :
+      fderivWithin 𝕜 (fun y ↦ (fderivWithin 𝕜 U s y) (V y)) s x =
+        (fderivWithin 𝕜 U s x).comp (fderivWithin 𝕜 V s x) +
+        (fderivWithin 𝕜 (fderivWithin 𝕜 U s) s x).flip (V x) := by
+    refine fderivWithin_clm_apply (hs x hx) ?_ (hV.differentiableWithinAt one_le_two)
+    exact (hU.fderivWithin_right hs le_rfl hx).differentiableWithinAt le_rfl
+  rw [fderivWithin_sub (hs x hx) (aux₁ hV hW) (aux₁ hW hV)]
+  rw [fderivWithin_sub (hs x hx) (aux₁ hU hV) (aux₁ hV hU)]
+  rw [fderivWithin_sub (hs x hx) (aux₁ hU hW) (aux₁ hW hU)]
+  rw [aux₂ hW hV, aux₂ hV hW, aux₂ hV hU, aux₂ hU hV, aux₂ hW hU, aux₂ hU hW]
+  simp only [ContinuousLinearMap.coe_sub', Pi.sub_apply, ContinuousLinearMap.add_apply,
+    ContinuousLinearMap.coe_comp', Function.comp_apply, ContinuousLinearMap.flip_apply, h'V.eq,
+    h'U.eq, h'W.eq]
+  abel
+
+/-- The Lie bracket of vector fields in vector spaces satisfies the Leibniz identity
+`[U, [V, W]] = [[U, V], W] + [V, [U, W]]`. -/
+lemma leibniz_identity_lieBracketWithin [IsRCLikeNormedField 𝕜] {U V W : E → E} {s : Set E} {x : E}
+    (hs : UniqueDiffOn 𝕜 s) (h'x : x ∈ closure (interior s)) (hx : x ∈ s)
+    (hU : ContDiffWithinAt 𝕜 2 U s x) (hV : ContDiffWithinAt 𝕜 2 V s x)
+    (hW : ContDiffWithinAt 𝕜 2 W s x) :
+    lieBracketWithin 𝕜 U (lieBracketWithin 𝕜 V W s) s x =
+      lieBracketWithin 𝕜 (lieBracketWithin 𝕜 U V s) W s x
+      + lieBracketWithin 𝕜 V (lieBracketWithin 𝕜 U W s) s x := by
+  apply leibniz_identity_lieBracketWithin_of_isSymmSndFDerivWithinAt hs hx hU hV hW
+  · exact hU.isSymmSndFDerivWithinAt le_rfl hs h'x hx
+  · exact hV.isSymmSndFDerivWithinAt le_rfl hs h'x hx
+  · exact hW.isSymmSndFDerivWithinAt le_rfl hs h'x hx
+
+/-- The Lie bracket of vector fields in vector spaces satisfies the Leibniz identity
+`[U, [V, W]] = [[U, V], W] + [V, [U, W]]`. -/
+lemma leibniz_identity_lieBracket [IsRCLikeNormedField 𝕜] {U V W : E → E} {x : E}
+    (hU : ContDiffAt 𝕜 2 U x) (hV : ContDiffAt 𝕜 2 V x) (hW : ContDiffAt 𝕜 2 W x) :
+    lieBracket 𝕜 U (lieBracket 𝕜 V W) x =
+      lieBracket 𝕜 (lieBracket 𝕜 U V) W x + lieBracket 𝕜 V (lieBracket 𝕜 U W) x := by
+  simp only [← lieBracketWithin_univ, ← contDiffWithinAt_univ] at hU hV hW ⊢
+  exact leibniz_identity_lieBracketWithin uniqueDiffOn_univ (by simp) (mem_univ _) hU hV hW
+
+end VectorField