English
The Lie bracket of vector fields satisfies the Leibniz rule within a set: [U, [V, W]] = [[U, V], W] + [V, [U, W]] at a point x under suitable smoothness and symmetry assumptions.
Русский
Скобка Ли векторных полей удовлетворяет тождеству Лейбница внутри множества: [U, [V, W]] = [[U, V], W] + [V, [U, W]] в точке x при подходящих гладкости и симметричности.
LaTeX
$$$ lieBracketWithin 𝕜 U (lieBracketWithin 𝕜 V W s) s x = lieBracketWithin 𝕜 (lieBracketWithin 𝕜 U V s) W s x + lieBracketWithin 𝕜 V (lieBracketWithin 𝕜 U W s) s x $$$
Lean4
/-- The Lie bracket of vector fields in vector spaces satisfies the Leibniz identity
`[U, [V, W]] = [[U, V], W] + [V, [U, W]]`. -/
theorem 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_fun_sub (hs x hx) (aux₁ hV hW) (aux₁ hW hV)]
rw [fderivWithin_fun_sub (hs x hx) (aux₁ hU hV) (aux₁ hV hU)]
rw [fderivWithin_fun_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
