English
A refined version asserting the existence of a neighborhood with a family of continuous linear equivalences varying smoothly, under ContDiffAt 2 f x and fderivInvertible assumptions.
Русский
Уточненная версия: существует окрестность с семейством непрерывных линейных эквивалентностей, зависящих плавно, при предпосылках ContDiffAt 2 f x и инвертируемости производной.
LaTeX
$$$ \\exists N: E \\to (E \\simeq_L F),\\; \\text{smoothness and invertible derivative conditions hold.}$$$
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_of_isSymmSndFDerivWithinAt {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 : MapsTo f s t) :
pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x =
lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x :=
by
by_cases h : (fderivWithin 𝕜 f s x).IsInvertible; swap
· simp [pullbackWithin_eq_of_not_isInvertible h, lieBracketWithin_eq]
rcases exists_continuousLinearEquiv_fderivWithin_symm_eq h'f h hu hx with ⟨M, -, M_symm_smooth, hM, M_diff⟩
have hMx : M x = fderivWithin 𝕜 f s x := (mem_of_mem_nhdsWithin hx hM :)
have AV :
fderivWithin 𝕜 (pullbackWithin 𝕜 f V s) s x = fderivWithin 𝕜 (fun y ↦ ((M y).symm : F →L[𝕜] E) (V (f y))) s x :=
by
apply Filter.EventuallyEq.fderivWithin_eq_of_mem _ hx
filter_upwards [hM] with y hy using pullbackWithin_eq_of_fderivWithin_eq hy _
have AW :
fderivWithin 𝕜 (pullbackWithin 𝕜 f W s) s x = fderivWithin 𝕜 (fun y ↦ ((M y).symm : F →L[𝕜] E) (W (f y))) s x :=
by
apply Filter.EventuallyEq.fderivWithin_eq_of_mem _ hx
filter_upwards [hM] with y hy using pullbackWithin_eq_of_fderivWithin_eq hy _
have Af : DifferentiableWithinAt 𝕜 f s x := h'f.differentiableWithinAt one_le_two
simp only [lieBracketWithin_eq, pullbackWithin_eq_of_fderivWithin_eq hMx, map_sub, AV, AW]
rw [fderivWithin_clm_apply, fderivWithin_clm_apply]
· simp [fderivWithin_comp' x hW Af hst (hu x hx), ← hMx, fderivWithin_comp' x hV Af hst (hu x hx), M_diff, hf.eq]
· exact hu x hx
· exact M_symm_smooth.differentiableWithinAt le_rfl
· exact hV.comp x Af hst
· exact hu x hx
· exact M_symm_smooth.differentiableWithinAt le_rfl
· exact hW.comp x Af hst
