English
Within a complete space, the Lie bracket commutes with pullbacks when the second derivative is symmetric; this extends to a broader setting with local diffeomorphism assumptions.
Русский
В полном пространстве скобка Ли commuting с вытягиванием при симметричном втором производном; распространяется на более широкие условия локального диффеоморфизма.
LaTeX
$$$ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x = lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x $$$
Lean4
/-- 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 _root_.exists_continuousLinearEquiv_fderivWithin_symm_eq {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 ↦ (N y : E →L[𝕜] F)) s x ∧
ContDiffWithinAt 𝕜 1 (fun y ↦ ((N y).symm : F →L[𝕜] E)) s x ∧
(∀ᶠ y in 𝓝[s] x, N y = fderivWithin 𝕜 f s y) ∧
∀ v,
fderivWithin 𝕜 (fun y ↦ ((N y).symm : F →L[𝕜] E)) s x v =
-(N x).symm ∘L ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x v)) ∘L (N x).symm :=
by
classical
rcases hf with ⟨M, hM⟩
let U := {y | ∃ (N : E ≃L[𝕜] F), N = fderivWithin 𝕜 f s y}
have hU : U ∈ 𝓝[s] x :=
by
have I : range ((↑) : (E ≃L[𝕜] F) → E →L[𝕜] F) ∈ 𝓝 (fderivWithin 𝕜 f s x) :=
by
rw [← hM]
exact M.nhds
have : ContinuousWithinAt (fderivWithin 𝕜 f s) s x :=
(h'f.fderivWithin_right (m := 1) hs le_rfl hx).continuousWithinAt
exact this I
let N : E → (E ≃L[𝕜] F) := fun x ↦ if h : x ∈ U then h.choose else M
have eN : (fun y ↦ (N y : E →L[𝕜] F)) =ᶠ[𝓝[s] x] fun y ↦ fderivWithin 𝕜 f s y :=
by
filter_upwards [hU] with y hy
simpa only [hy, ↓reduceDIte, N] using Exists.choose_spec hy
have e'N : N x = fderivWithin 𝕜 f s x := by apply mem_of_mem_nhdsWithin hx eN
have hN : ContDiffWithinAt 𝕜 1 (fun y ↦ (N y : E →L[𝕜] F)) s x :=
by
have : ContDiffWithinAt 𝕜 1 (fun y ↦ fderivWithin 𝕜 f s y) s x := h'f.fderivWithin_right (m := 1) hs le_rfl hx
apply this.congr_of_eventuallyEq eN e'N
have hN' : ContDiffWithinAt 𝕜 1 (fun y ↦ ((N y).symm : F →L[𝕜] E)) s x :=
by
have : ContDiffWithinAt 𝕜 1 (ContinuousLinearMap.inverse ∘ (fun y ↦ (N y : E →L[𝕜] F))) s x :=
(contDiffAt_map_inverse (N x)).comp_contDiffWithinAt x hN
convert this with y
simp only [Function.comp_apply, ContinuousLinearMap.inverse_equiv]
refine ⟨N, hN, hN', eN, fun v ↦ ?_⟩
have A' y :
ContinuousLinearMap.compL 𝕜 F E F (N y : E →L[𝕜] F) ((N y).symm : F →L[𝕜] E) = ContinuousLinearMap.id 𝕜 F := by ext;
simp
have :
fderivWithin 𝕜 (fun y ↦ ContinuousLinearMap.compL 𝕜 F E F (N y : E →L[𝕜] F) ((N y).symm : F →L[𝕜] E)) s x v = 0 :=
by simp [A', fderivWithin_const_apply]
have I :
(N x : E →L[𝕜] F) ∘L (fderivWithin 𝕜 (fun y ↦ ((N y).symm : F →L[𝕜] E)) s x v) =
-(fderivWithin 𝕜 (fun y ↦ (N y : E →L[𝕜] F)) s x v) ∘L ((N x).symm : F →L[𝕜] E) :=
by
rw [ContinuousLinearMap.fderivWithin_of_bilinear _ (hN.differentiableWithinAt le_rfl)
(hN'.differentiableWithinAt le_rfl) (hs x hx)] at this
simpa [eq_neg_iff_add_eq_zero] using this
have B (M : F →L[𝕜] E) : M = ((N x).symm : F →L[𝕜] E) ∘L ((N x) ∘L M) := by ext; simp
rw [B (fderivWithin 𝕜 (fun y ↦ ((N y).symm : F →L[𝕜] E)) s x v), I]
simp only [ContinuousLinearMap.comp_neg, eN.fderivWithin_eq e'N]
