English
If IsSymmSndFDerivWithinAt holds and the differentiability and growth conditions are met, then pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x equals lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x whenever u, x, and other assumptions satisfy eventual equality.
Русский
Если выполняются изотр симметричной двойной производной внутри и даны условия дифференцируемости и роста, то pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x равно lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x при выполнении условий эквивалентности вдоль nhds 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 pullback_lieBracket_of_isSymmSndFDerivAt {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)) :
pullback 𝕜 f (lieBracket 𝕜 V W) x = lieBracket 𝕜 (pullback 𝕜 f V) (pullback 𝕜 f W) x :=
by
simp only [← lieBracketWithin_univ, ← pullbackWithin_univ, ← isSymmSndFDerivWithinAt_univ,
← differentiableWithinAt_univ] at hf h'f hV hW ⊢
exact
pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt hf h'f hV hW uniqueDiffOn_univ (mem_univ _)
(mapsTo_univ _ _)
