English
If g is a local inverse of f with an invertible derivative f' (as a linear isomorphism), and f(g y) = y near a, then g has derivative f'.symm at a on the corresponding domain.
Русский
Если g является локальным обратным к f и производная f' обратимая, и если в окрестности точки a выполняется f(g y) = y, то у g существует производная равная f'.symm в точки a.
LaTeX
$$$$ \\text{HasFDerivWithinAt } g \\ f'^{\\,-1} \\ t a $$$$
Lean4
/-- If `f (g y) = y` for `y` in a neighborhood of `a` within `t`,
`g` maps a neighborhood of `a` within `t` to a neighborhood of `g a` within `s`,
and `f` has an invertible derivative `f'` at `g a` within `s`,
then `g` has the derivative `f'⁻¹` at `a` within `t`.
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 {g : F → E} {f' : E ≃L[𝕜] F} {a : F} {t : Set F} (hg : Tendsto g (𝓝[t] a) (𝓝[s] (g a)))
(hf : HasFDerivWithinAt f (f' : E →L[𝕜] F) s (g a)) (ha : a ∈ t) (hfg : ∀ᶠ y in 𝓝[t] a, f (g y) = y) :
HasFDerivWithinAt g (f'.symm : F →L[𝕜] E) t a :=
by
have : (fun x : F => g x - g a - f'.symm (x - a)) =O[𝓝[t] a] fun x : F => f' (g x - g a) - (x - a) :=
((f'.symm : F →L[𝕜] E).isBigO_comp _ _).congr (fun x ↦ by simp) fun _ ↦ rfl
refine .of_isLittleO <| this.trans_isLittleO ?_
clear this
refine ((hf.isLittleO.comp_tendsto hg).symm.congr' (hfg.mono ?_) .rfl).trans_isBigO ?_
· intro p hp
simp [hp, hfg.self_of_nhdsWithin ha]
· refine
((hf.isBigO_sub_rev f'.antilipschitz).comp_tendsto hg).congr' (Eventually.of_forall fun _ => rfl) (hfg.mono ?_)
rintro p hp
simp only [(· ∘ ·), hp, hfg.self_of_nhdsWithin ha]
