English
The Lie bracket commutes with pullbacks within a set: pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x equals lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x, under symmetry and differentiability assumptions.
Русский
Скобка Ли коммутирует с вытягиванием внутри множества: pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x = lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x при симметрии и условиях дифференцируемости.
LaTeX
$$$ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x = lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x $$$
Lean4
/-- 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 pullbackWithin_lieBracketWithin {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 : MapsTo f s t) :
pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x =
lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x :=
pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt (h'f.isSymmSndFDerivWithinAt hn hu h'x hx)
(h'f.of_le (le_minSmoothness.trans hn)) hV hW hu hx hst
