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

We also define the Lie bracket of two vector fields as VectorField.lieBracket 𝕜 V W x := fderiv 𝕜 W x (V x) - fderiv 𝕜 V x (W x) (together with the same notion within a set).

In addition to comprehensive API on these two notions, the main results are the following:

• VectorField.pullback_lieBracket states that the pullback of the Lie bracket is the Lie bracket of the pullbacks, when the second derivative is symmetric.
• 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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (hn : minSmoothness 𝕜 2 ≤ n) {U V W : E → E} {s : Set E} {x : E} (hs : UniqueDiffOn 𝕜 s) (h'x : x ∈ closure (interior s)) (hx : x ∈ s) (hU : ContDiffWithinAt 𝕜 n U s x) (hV : ContDiffWithinAt 𝕜 n V s x) (hW : ContDiffWithinAt 𝕜 n 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 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (hn : minSmoothness 𝕜 2 ≤ n) {U V W : E → E} {x : E} (hU : ContDiffAt 𝕜 n U x) (hV : ContDiffAt 𝕜 n V x) (hW : ContDiffAt 𝕜 n 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]].

The pullback of vector fields in a vector space

def VectorField.pullback (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (V : F → F) (x : E) : E

The pullback of a vector field under a function, defined as (f^* V) (x) = Df(x)^{-1} (V (f x)). If Df(x) is not invertible, we use the junk value 0.

Equations

• VectorField.pullback 𝕜 f V x = (fderiv 𝕜 f x).inverse (V (f x))

def VectorField.pullbackWithin (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (V : F → F) (s : Set E) (x : E) : E

The pullback within a set of a vector field under a function, defined as (f^* V) (x) = Df(x)^{-1} (V (f x)) where Df(x) is the derivative of f within s. If Df(x) is not invertible, we use the junk value 0.

Equations

• VectorField.pullbackWithin 𝕜 f V s x = (fderivWithin 𝕜 f s x).inverse (V (f x))

theorem VectorField.pullbackWithin_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {V : F → F} {s : Set E} : VectorField.pullbackWithin 𝕜 f V s = fun (x : E) => (fderivWithin 𝕜 f s x).inverse (V (f x))

theorem VectorField.pullback_eq_of_fderiv_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {M : E ≃L[𝕜] F} {x : E} (hf : ↑M = fderiv 𝕜 f x) (V : F → F) : VectorField.pullback 𝕜 f V x = M.symm (V (f x))

theorem VectorField.pullback_eq_of_not_isInvertible {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (h : ¬(fderiv 𝕜 f x).IsInvertible) (V : F → F) : VectorField.pullback 𝕜 f V x = 0

theorem VectorField.pullbackWithin_eq_of_not_isInvertible {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E} (h : ¬(fderivWithin 𝕜 f s x).IsInvertible) (V : F → F) : VectorField.pullbackWithin 𝕜 f V s x = 0

theorem VectorField.pullbackWithin_eq_of_fderivWithin_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {M : E ≃L[𝕜] F} {x : E} (hf : ↑M = fderivWithin 𝕜 f s x) (V : F → F) : VectorField.pullbackWithin 𝕜 f V s x = M.symm (V (f x))

@[simp]

theorem VectorField.pullbackWithin_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {V : F → F} : VectorField.pullbackWithin 𝕜 f V Set.univ = VectorField.pullback 𝕜 f V

theorem VectorField.fderiv_pullback {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (V : F → F) (x : E) (h'f : (fderiv 𝕜 f x).IsInvertible) : (fderiv 𝕜 f x) (VectorField.pullback 𝕜 f V x) = V (f x)

theorem VectorField.fderivWithin_pullbackWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {V : F → F} {x : E} (h'f : (fderivWithin 𝕜 f s x).IsInvertible) : (fderivWithin 𝕜 f s x) (VectorField.pullbackWithin 𝕜 f V s x) = V (f x)

theorem exists_continuousLinearEquiv_fderivWithin_symm_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] {f : E → F} {s : Set E} {x : E} (h'f : ContDiffWithinAt 𝕜 2 f s x) (hf : (fderivWithin 𝕜 f s x).IsInvertible) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) : ∃ (N : E → E ≃L[𝕜] F), ContDiffWithinAt 𝕜 1 (fun (y : E) => ↑(N y)) s x ∧ ContDiffWithinAt 𝕜 1 (fun (y : E) => ↑(N y).symm) s x ∧ (∀ᶠ (y : E) in nhdsWithin x s, ↑(N y) = fderivWithin 𝕜 f s y) ∧ ∀ (v : E), (fderivWithin 𝕜 (fun (y : E) => ↑(N y).symm) s x) v = -(↑(N x).symm).comp (((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v).comp ↑(N x).symm)

If a C^2 map has an invertible derivative within a set at a point, then nearby derivatives can be written as continuous linear equivs, which depend in a C^1 way on the point, as well as their inverse, and moreover one can compute the derivative of the inverse.

theorem VectorField.DifferentiableWithinAt.pullbackWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] {f : E → F} {V : F → F} {s : Set E} {t : Set F} {x : E} (hV : DifferentiableWithinAt 𝕜 V t (f x)) (hf : ContDiffWithinAt 𝕜 2 f s x) (hf' : (fderivWithin 𝕜 f s x).IsInvertible) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (hst : Set.MapsTo f s t) : DifferentiableWithinAt 𝕜 (VectorField.pullbackWithin 𝕜 f V s) s x

theorem exists_continuousLinearEquiv_fderiv_symm_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] {f : E → F} {x : E} (h'f : ContDiffAt 𝕜 2 f x) (hf : (fderiv 𝕜 f x).IsInvertible) : ∃ (N : E → E ≃L[𝕜] F), ContDiffAt 𝕜 1 (fun (y : E) => ↑(N y)) x ∧ ContDiffAt 𝕜 1 (fun (y : E) => ↑(N y).symm) x ∧ (∀ᶠ (y : E) in nhds x, ↑(N y) = fderiv 𝕜 f y) ∧ ∀ (v : E), (fderiv 𝕜 (fun (y : E) => ↑(N y).symm) x) v = -(↑(N x).symm).comp (((fderiv 𝕜 (fderiv 𝕜 f) x) v).comp ↑(N x).symm)

If a C^2 map has an invertible derivative at a point, then nearby derivatives can be written as continuous linear equivs, which depend in a C^1 way on the point, as well as their inverse, and moreover one can compute the derivative of the inverse.

theorem VectorField.pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} [CompleteSpace E] {f : E → F} {V W : F → F} {x : E} {t : Set F} (hf : IsSymmSndFDerivWithinAt 𝕜 f s x) (h'f : ContDiffWithinAt 𝕜 2 f s x) (hV : DifferentiableWithinAt 𝕜 V t (f x)) (hW : DifferentiableWithinAt 𝕜 W t (f x)) (hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (hst : Set.MapsTo f s t) : VectorField.pullbackWithin 𝕜 f (VectorField.lieBracketWithin 𝕜 V W t) s x = VectorField.lieBracketWithin 𝕜 (VectorField.pullbackWithin 𝕜 f V s) (VectorField.pullbackWithin 𝕜 f W s) s x

The Lie bracket commutes with taking pullbacks. This requires the function to have symmetric second derivative. Version in a complete space. One could also give a version avoiding completeness but requiring that f is a local diffeo.

theorem VectorField.pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt_of_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} [CompleteSpace E] {f : E → F} {V W : F → F} {x : E} {t : Set F} {u : Set E} (hf : IsSymmSndFDerivWithinAt 𝕜 f s x) (h'f : ContDiffWithinAt 𝕜 2 f s x) (hV : DifferentiableWithinAt 𝕜 V t (f x)) (hW : DifferentiableWithinAt 𝕜 W t (f x)) (hu : UniqueDiffOn 𝕜 u) (hx : x ∈ u) (hst : Set.MapsTo f u t) (hus : u =ᶠ[nhds x] s) : VectorField.pullbackWithin 𝕜 f (VectorField.lieBracketWithin 𝕜 V W t) s x = VectorField.lieBracketWithin 𝕜 (VectorField.pullbackWithin 𝕜 f V s) (VectorField.pullbackWithin 𝕜 f W s) s x

The Lie bracket commutes with taking pullbacks. This requires the function to have symmetric second derivative. Version in a complete space. One could also give a version avoiding completeness but requiring that f is a local diffeo. Variant where unique differentiability and the invariance property are only required in a smaller set u.

theorem VectorField.pullback_lieBracket_of_isSymmSndFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] {f : E → F} {V W : F → F} {x : E} (hf : IsSymmSndFDerivAt 𝕜 f x) (h'f : ContDiffAt 𝕜 2 f x) (hV : DifferentiableAt 𝕜 V (f x)) (hW : DifferentiableAt 𝕜 W (f x)) : VectorField.pullback 𝕜 f (VectorField.lieBracket 𝕜 V W) x = VectorField.lieBracket 𝕜 (VectorField.pullback 𝕜 f V) (VectorField.pullback 𝕜 f W) x

The Lie bracket commutes with taking pullbacks. This requires the function to have symmetric second derivative. Version in a complete space. One could also give a version avoiding completeness but requiring that f is a local diffeo.

theorem VectorField.pullbackWithin_lieBracketWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} [CompleteSpace E] {f : E → F} {V W : F → F} {x : E} {t : Set F} (hn : minSmoothness 𝕜 2 ≤ n) (h'f : ContDiffWithinAt 𝕜 n f s x) (hV : DifferentiableWithinAt 𝕜 V t (f x)) (hW : DifferentiableWithinAt 𝕜 W t (f x)) (hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (h'x : x ∈ closure (interior s)) (hst : Set.MapsTo f s t) : VectorField.pullbackWithin 𝕜 f (VectorField.lieBracketWithin 𝕜 V W t) s x = VectorField.lieBracketWithin 𝕜 (VectorField.pullbackWithin 𝕜 f V s) (VectorField.pullbackWithin 𝕜 f W s) s x

The Lie bracket commutes with taking pullbacks. This requires the function to have symmetric second derivative. Version in a complete space. One could also give a version avoiding completeness but requiring that f is a local diffeo.

theorem VectorField.pullback_lieBracket {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] (hn : minSmoothness 𝕜 2 ≤ n) {f : E → F} {V W : F → F} {x : E} (h'f : ContDiffAt 𝕜 n f x) (hV : DifferentiableAt 𝕜 V (f x)) (hW : DifferentiableAt 𝕜 W (f x)) : VectorField.pullback 𝕜 f (VectorField.lieBracket 𝕜 V W) x = VectorField.lieBracket 𝕜 (VectorField.pullback 𝕜 f V) (VectorField.pullback 𝕜 f W) x

The Lie bracket commutes with taking pullbacks. One could also give a version avoiding completeness but requiring that f is a local diffeo.