English
Under suitable differentiability assumptions, the inverse of a differentiable map has derivative equal to the inverse of the derivative map.
Русский
При подходящих предположениях о дифференцируемости обратная производная имеет производную, равную обратной производной производной.
LaTeX
$$$$ \\text{HasFDerivWithinAt } g \\ f'^{\\,-1} \\ t a $$$$
Lean4
/-- If `f (g y) = y` for `y` in some neighborhood of `a`, `g` is continuous at `a`, and `f` has an
invertible derivative `f'` at `g a` in the strict sense, then `g` has the derivative `f'⁻¹` at `a`
in the strict sense.
This is one of the easy parts of the inverse function theorem: it assumes that we already have an
inverse function. -/
theorem of_local_left_inverse {f : E → F} {f' : E ≃L[𝕜] F} {g : F → E} {a : F} (hg : ContinuousAt g a)
(hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) (g a)) (hfg : ∀ᶠ y in 𝓝 a, f (g y) = y) :
HasStrictFDerivAt g (f'.symm : F →L[𝕜] E) a :=
by
replace hg := hg.prodMap' hg
replace hfg := hfg.prodMk_nhds hfg
have :
(fun p : F × F => g p.1 - g p.2 - f'.symm (p.1 - p.2)) =O[𝓝 (a, a)] fun p : F × F =>
f' (g p.1 - g p.2) - (p.1 - p.2) :=
by
refine ((f'.symm : F →L[𝕜] E).isBigO_comp _ _).congr (fun x => ?_) fun _ => rfl
simp
refine .of_isLittleO <| this.trans_isLittleO ?_
clear this
refine ((hf.isLittleO.comp_tendsto hg).symm.congr' (hfg.mono ?_) (Eventually.of_forall fun _ => rfl)).trans_isBigO ?_
· rintro p ⟨hp1, hp2⟩
simp [hp1, hp2]
· refine (hf.isBigO_sub_rev.comp_tendsto hg).congr' (Eventually.of_forall fun _ => rfl) (hfg.mono ?_)
rintro p ⟨hp1, hp2⟩
simp only [(· ∘ ·), hp1, hp2, Prod.map]
