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]].

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.

def VectorField.lieBracket (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (V W : E → E) (x : E) : E

The Lie bracket [V, W] (x) of two vector fields at a point, defined as DW(x) (V x) - DV(x) (W x).

Equations

• VectorField.lieBracket 𝕜 V W x = (fderiv 𝕜 W x) (V x) - (fderiv 𝕜 V x) (W x)

def VectorField.lieBracketWithin (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (V W : E → E) (s : Set E) (x : E) : E

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.

Equations

• VectorField.lieBracketWithin 𝕜 V W s x = (fderivWithin 𝕜 W s x) (V x) - (fderivWithin 𝕜 V s x) (W x)

theorem VectorField.lieBracket_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} : VectorField.lieBracket 𝕜 V W = fun (x : E) => (fderiv 𝕜 W x) (V x) - (fderiv 𝕜 V x) (W x)

theorem VectorField.lieBracketWithin_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {s : Set E} : VectorField.lieBracketWithin 𝕜 V W s = fun (x : E) => (fderivWithin 𝕜 W s x) (V x) - (fderivWithin 𝕜 V s x) (W x)

@[simp]

theorem VectorField.lieBracketWithin_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} : VectorField.lieBracketWithin 𝕜 V W Set.univ = VectorField.lieBracket 𝕜 V W

theorem VectorField.lieBracketWithin_eq_zero_of_eq_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {s : Set E} {x : E} (hV : V x = 0) (hW : W x = 0) : VectorField.lieBracketWithin 𝕜 V W s x = 0

theorem VectorField.lieBracket_eq_zero_of_eq_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {x : E} (hV : V x = 0) (hW : W x = 0) : VectorField.lieBracket 𝕜 V W x = 0

theorem VectorField.lieBracketWithin_smul_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {s : Set E} {x : E} {c : 𝕜} (hV : DifferentiableWithinAt 𝕜 V s x) (hs : UniqueDiffWithinAt 𝕜 s x) : VectorField.lieBracketWithin 𝕜 (c • V) W s x = c • VectorField.lieBracketWithin 𝕜 V W s x

theorem VectorField.lieBracket_smul_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {x : E} {c : 𝕜} (hV : DifferentiableAt 𝕜 V x) : VectorField.lieBracket 𝕜 (c • V) W x = c • VectorField.lieBracket 𝕜 V W x

theorem VectorField.lieBracketWithin_smul_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {s : Set E} {x : E} {c : 𝕜} (hW : DifferentiableWithinAt 𝕜 W s x) (hs : UniqueDiffWithinAt 𝕜 s x) : VectorField.lieBracketWithin 𝕜 V (c • W) s x = c • VectorField.lieBracketWithin 𝕜 V W s x

theorem VectorField.lieBracket_smul_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {x : E} {c : 𝕜} (hW : DifferentiableAt 𝕜 W x) : VectorField.lieBracket 𝕜 V (c • W) x = c • VectorField.lieBracket 𝕜 V W x

theorem VectorField.lieBracketWithin_add_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W V₁ : E → E} {s : Set E} {x : E} (hV : DifferentiableWithinAt 𝕜 V s x) (hV₁ : DifferentiableWithinAt 𝕜 V₁ s x) (hs : UniqueDiffWithinAt 𝕜 s x) : VectorField.lieBracketWithin 𝕜 (V + V₁) W s x = VectorField.lieBracketWithin 𝕜 V W s x + VectorField.lieBracketWithin 𝕜 V₁ W s x

theorem VectorField.lieBracket_add_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W V₁ : E → E} {x : E} (hV : DifferentiableAt 𝕜 V x) (hV₁ : DifferentiableAt 𝕜 V₁ x) : VectorField.lieBracket 𝕜 (V + V₁) W x = VectorField.lieBracket 𝕜 V W x + VectorField.lieBracket 𝕜 V₁ W x

theorem VectorField.lieBracketWithin_add_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W W₁ : E → E} {s : Set E} {x : E} (hW : DifferentiableWithinAt 𝕜 W s x) (hW₁ : DifferentiableWithinAt 𝕜 W₁ s x) (hs : UniqueDiffWithinAt 𝕜 s x) : VectorField.lieBracketWithin 𝕜 V (W + W₁) s x = VectorField.lieBracketWithin 𝕜 V W s x + VectorField.lieBracketWithin 𝕜 V W₁ s x

theorem VectorField.lieBracket_add_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W W₁ : E → E} {x : E} (hW : DifferentiableAt 𝕜 W x) (hW₁ : DifferentiableAt 𝕜 W₁ x) : VectorField.lieBracket 𝕜 V (W + W₁) x = VectorField.lieBracket 𝕜 V W x + VectorField.lieBracket 𝕜 V W₁ x

theorem VectorField.lieBracketWithin_swap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {s : Set E} : VectorField.lieBracketWithin 𝕜 V W s = -VectorField.lieBracketWithin 𝕜 W V s

theorem VectorField.lieBracket_swap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {x : E} : VectorField.lieBracket 𝕜 V W x = -VectorField.lieBracket 𝕜 W V x

@[simp]

theorem VectorField.lieBracketWithin_self {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V : E → E} {s : Set E} : VectorField.lieBracketWithin 𝕜 V V s = 0

@[simp]

theorem VectorField.lieBracket_self {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V : E → E} : VectorField.lieBracket 𝕜 V V = 0

theorem ContDiffWithinAt.lieBracketWithin_vectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {s : Set E} {x : E} {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 (VectorField.lieBracketWithin 𝕜 V W s) s x

theorem ContDiffAt.lieBracket_vectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {x : E} {m n : ℕ∞} (hV : ContDiffAt 𝕜 n V x) (hW : ContDiffAt 𝕜 n W x) (hmn : m + 1 ≤ n) : ContDiffAt 𝕜 m (VectorField.lieBracket 𝕜 V W) x

theorem ContDiffOn.lieBracketWithin_vectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {s : Set E} {m n : ℕ∞} (hV : ContDiffOn 𝕜 n V s) (hW : ContDiffOn 𝕜 n W s) (hs : UniqueDiffOn 𝕜 s) (hmn : m + 1 ≤ n) : ContDiffOn 𝕜 m (VectorField.lieBracketWithin 𝕜 V W s) s

theorem ContDiff.lieBracket_vectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {m n : ℕ∞} (hV : ContDiff 𝕜 n V) (hW : ContDiff 𝕜 n W) (hmn : m + 1 ≤ n) : ContDiff 𝕜 m (VectorField.lieBracket 𝕜 V W)

theorem VectorField.lieBracketWithin_of_mem_nhdsWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {s t : Set E} {x : E} (st : t ∈ nhdsWithin x s) (hs : UniqueDiffWithinAt 𝕜 s x) (hV : DifferentiableWithinAt 𝕜 V t x) (hW : DifferentiableWithinAt 𝕜 W t x) : VectorField.lieBracketWithin 𝕜 V W s x = VectorField.lieBracketWithin 𝕜 V W t x

theorem VectorField.lieBracketWithin_subset {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {s t : Set E} {x : E} (st : s ⊆ t) (ht : UniqueDiffWithinAt 𝕜 s x) (hV : DifferentiableWithinAt 𝕜 V t x) (hW : DifferentiableWithinAt 𝕜 W t x) : VectorField.lieBracketWithin 𝕜 V W s x = VectorField.lieBracketWithin 𝕜 V W t x

theorem VectorField.lieBracketWithin_inter {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {s t : Set E} {x : E} (ht : t ∈ nhds x) : VectorField.lieBracketWithin 𝕜 V W (s ∩ t) x = VectorField.lieBracketWithin 𝕜 V W s x

theorem VectorField.lieBracketWithin_of_mem_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {s : Set E} {x : E} (h : s ∈ nhds x) : VectorField.lieBracketWithin 𝕜 V W s x = VectorField.lieBracket 𝕜 V W x

theorem VectorField.lieBracketWithin_of_isOpen {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {s : Set E} {x : E} (hs : IsOpen s) (hx : x ∈ s) : VectorField.lieBracketWithin 𝕜 V W s x = VectorField.lieBracket 𝕜 V W x

theorem VectorField.lieBracketWithin_eq_lieBracket {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {s : Set E} {x : E} (hs : UniqueDiffWithinAt 𝕜 s x) (hV : DifferentiableAt 𝕜 V x) (hW : DifferentiableAt 𝕜 W x) : VectorField.lieBracketWithin 𝕜 V W s x = VectorField.lieBracket 𝕜 V W x

theorem VectorField.lieBracketWithin_congr_set' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {s t : Set E} {x : E} (y : E) (h : s =ᶠ[nhdsWithin x {y}ᶜ] t) : VectorField.lieBracketWithin 𝕜 V W s x = VectorField.lieBracketWithin 𝕜 V W t x

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

theorem VectorField.lieBracketWithin_congr_set {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {s t : Set E} {x : E} (h : s =ᶠ[nhds x] t) : VectorField.lieBracketWithin 𝕜 V W s x = VectorField.lieBracketWithin 𝕜 V W t x

theorem VectorField.lieBracketWithin_eventually_congr_set' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {s t : Set E} {x : E} (y : E) (h : s =ᶠ[nhdsWithin x {y}ᶜ] t) : VectorField.lieBracketWithin 𝕜 V W s =ᶠ[nhds x] VectorField.lieBracketWithin 𝕜 V W t

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

theorem VectorField.lieBracketWithin_eventually_congr_set {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {s t : Set E} {x : E} (h : s =ᶠ[nhds x] t) : VectorField.lieBracketWithin 𝕜 V W s =ᶠ[nhds x] VectorField.lieBracketWithin 𝕜 V W t

theorem DifferentiableWithinAt.lieBracketWithin_congr_mono {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W V₁ W₁ : E → E} {s t : Set E} {x : E} (hV : DifferentiableWithinAt 𝕜 V s x) (hVs : Set.EqOn V₁ V t) (hVx : V₁ x = V x) (hW : DifferentiableWithinAt 𝕜 W s x) (hWs : Set.EqOn W₁ W t) (hWx : W₁ x = W x) (hxt : UniqueDiffWithinAt 𝕜 t x) (h₁ : t ⊆ s) : VectorField.lieBracketWithin 𝕜 V₁ W₁ t x = VectorField.lieBracketWithin 𝕜 V W s x

theorem Filter.EventuallyEq.lieBracketWithin_vectorField_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W V₁ W₁ : E → E} {s : Set E} {x : E} (hV : V₁ =ᶠ[nhdsWithin x s] V) (hxV : V₁ x = V x) (hW : W₁ =ᶠ[nhdsWithin x s] W) (hxW : W₁ x = W x) : VectorField.lieBracketWithin 𝕜 V₁ W₁ s x = VectorField.lieBracketWithin 𝕜 V W s x

theorem Filter.EventuallyEq.lieBracketWithin_vectorField_eq_of_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W V₁ W₁ : E → E} {s : Set E} {x : E} (hV : V₁ =ᶠ[nhdsWithin x s] V) (hW : W₁ =ᶠ[nhdsWithin x s] W) (hx : x ∈ s) : VectorField.lieBracketWithin 𝕜 V₁ W₁ s x = VectorField.lieBracketWithin 𝕜 V W s x

theorem Filter.EventuallyEq.lieBracketWithin_vectorField' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W V₁ W₁ : E → E} {s t : Set E} {x : E} (hV : V₁ =ᶠ[nhdsWithin x s] V) (hW : W₁ =ᶠ[nhdsWithin x s] W) (ht : t ⊆ s) : VectorField.lieBracketWithin 𝕜 V₁ W₁ t =ᶠ[nhdsWithin x s] VectorField.lieBracketWithin 𝕜 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.lieBracketWithin_vectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W V₁ W₁ : E → E} {s : Set E} {x : E} (hV : V₁ =ᶠ[nhdsWithin x s] V) (hW : W₁ =ᶠ[nhdsWithin x s] W) : VectorField.lieBracketWithin 𝕜 V₁ W₁ s =ᶠ[nhdsWithin x s] VectorField.lieBracketWithin 𝕜 V W s

theorem Filter.EventuallyEq.lieBracketWithin_vectorField_eq_of_insert {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W V₁ W₁ : E → E} {s : Set E} {x : E} (hV : V₁ =ᶠ[nhdsWithin x (insert x s)] V) (hW : W₁ =ᶠ[nhdsWithin x (insert x s)] W) : VectorField.lieBracketWithin 𝕜 V₁ W₁ s x = VectorField.lieBracketWithin 𝕜 V W s x

theorem Filter.EventuallyEq.lieBracketWithin_vectorField_eq_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W V₁ W₁ : E → E} {s : Set E} {x : E} (hV : V₁ =ᶠ[nhds x] V) (hW : W₁ =ᶠ[nhds x] W) : VectorField.lieBracketWithin 𝕜 V₁ W₁ s x = VectorField.lieBracketWithin 𝕜 V W s x

theorem VectorField.lieBracketWithin_congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W V₁ W₁ : E → E} {s : Set E} {x : E} (hV : Set.EqOn V₁ V s) (hVx : V₁ x = V x) (hW : Set.EqOn W₁ W s) (hWx : W₁ x = W x) : VectorField.lieBracketWithin 𝕜 V₁ W₁ s x = VectorField.lieBracketWithin 𝕜 V W s x

theorem VectorField.lieBracketWithin_congr' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W V₁ W₁ : E → E} {s : Set E} {x : E} (hV : Set.EqOn V₁ V s) (hW : Set.EqOn W₁ W s) (hx : x ∈ s) : VectorField.lieBracketWithin 𝕜 V₁ W₁ s x = VectorField.lieBracketWithin 𝕜 V W s x

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

theorem Filter.EventuallyEq.lieBracket_vectorField_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W V₁ W₁ : E → E} {x : E} (hV : V₁ =ᶠ[nhds x] V) (hW : W₁ =ᶠ[nhds x] W) : VectorField.lieBracket 𝕜 V₁ W₁ x = VectorField.lieBracket 𝕜 V W x

theorem Filter.EventuallyEq.lieBracket_vectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W V₁ W₁ : E → E} {x : E} (hV : V₁ =ᶠ[nhds x] V) (hW : W₁ =ᶠ[nhds x] W) : VectorField.lieBracket 𝕜 V₁ W₁ =ᶠ[nhds x] VectorField.lieBracket 𝕜 V W

theorem VectorField.leibniz_identity_lieBracketWithin_of_isSymmSndFDerivWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {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) : VectorField.lieBracketWithin 𝕜 U (VectorField.lieBracketWithin 𝕜 V W s) s x = VectorField.lieBracketWithin 𝕜 (VectorField.lieBracketWithin 𝕜 U V s) W s x + VectorField.lieBracketWithin 𝕜 V (VectorField.lieBracketWithin 𝕜 U W s) s x

The Lie bracket of vector fields in vector spaces satisfies the Leibniz identity [U, [V, W]] = [[U, V], W] + [V, [U, W]].

theorem VectorField.leibniz_identity_lieBracketWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [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) : VectorField.lieBracketWithin 𝕜 U (VectorField.lieBracketWithin 𝕜 V W s) s x = VectorField.lieBracketWithin 𝕜 (VectorField.lieBracketWithin 𝕜 U V s) W s x + VectorField.lieBracketWithin 𝕜 V (VectorField.lieBracketWithin 𝕜 U W s) s x

The Lie bracket of vector fields in vector spaces satisfies the Leibniz identity [U, [V, W]] = [[U, V], W] + [V, [U, W]].

theorem VectorField.leibniz_identity_lieBracket {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [IsRCLikeNormedField 𝕜] {U V W : E → E} {x : E} (hU : ContDiffAt 𝕜 2 U x) (hV : ContDiffAt 𝕜 2 V x) (hW : ContDiffAt 𝕜 2 W x) : VectorField.lieBracket 𝕜 U (VectorField.lieBracket 𝕜 V W) x = VectorField.lieBracket 𝕜 (VectorField.lieBracket 𝕜 U V) W x + VectorField.lieBracket 𝕜 V (VectorField.lieBracket 𝕜 U W) x

The Lie bracket of vector fields in vector spaces satisfies the Leibniz identity [U, [V, W]] = [[U, V], W] + [V, [U, W]].