English
If an open partial homeomorphism is C^n at a point and its derivative is invertible, then the inverse is C^n at the corresponding point.
Русский
Для открытого частичного гомоморфизма, если он гладок до порядка n в точке и производная обратима, то обратная функция гладкая до порядка n в соответствующей точке.
LaTeX
$$$\\text{OpenPartialHomeomorph contDiffAt_symm: }\\forall f, \\; (ha)\\; (hf)\\; (hf' ) \\Rightarrow \\mathrm{ContDiffAt}_{\\mathbb{k}}\\ n f^{ -1 }$$$
Lean4
/-- If `f` is a local homeomorphism and the point `a` is in its target,
and if `f` is `n` times continuously differentiable at `f.symm a`,
and if the derivative at `f.symm a` is a continuous linear equivalence,
then `f.symm` is `n` times continuously differentiable at the point `a`.
This is one of the easy parts of the inverse function theorem: it assumes that we already have
an inverse function. -/
theorem contDiffAt_symm [CompleteSpace E] (f : OpenPartialHomeomorph E F) {f₀' : E ≃L[𝕜] F} {a : F} (ha : a ∈ f.target)
(hf₀' : HasFDerivAt f (f₀' : E →L[𝕜] F) (f.symm a)) (hf : ContDiffAt 𝕜 n f (f.symm a)) : ContDiffAt 𝕜 n f.symm a :=
by
match n with
| ω =>
apply AnalyticAt.contDiffAt
exact f.analyticAt_symm ha hf.analyticAt hf₀'.fderiv
| (n : ℕ∞) =>
-- We prove this by induction on `n`
induction n using ENat.nat_induction with
| zero =>
apply contDiffAt_zero.2
exact ⟨f.target, IsOpen.mem_nhds f.open_target ha, f.continuousOn_invFun⟩
| succ n IH =>
obtain ⟨f', ⟨u, hu, hff'⟩, hf'⟩ := contDiffAt_succ_iff_hasFDerivAt.mp hf
apply
contDiffAt_succ_iff_hasFDerivAt.2
-- For showing `n.succ` times continuous differentiability (the main inductive step), it
-- suffices to produce the derivative and show that it is `n` times continuously
-- differentiable
have eq_f₀' : f' (f.symm a) = f₀' := (hff' (f.symm a) (mem_of_mem_nhds hu)).unique hf₀'
refine ⟨inverse ∘ f' ∘ f.symm, ?_, ?_⟩
· -- We first check that the derivative of `f` is that formula
have h_nhds : {y : E | ∃ e : E ≃L[𝕜] F, ↑e = f' y} ∈ 𝓝 (f.symm a) :=
by
have hf₀' := f₀'.nhds
rw [← eq_f₀'] at hf₀'
exact hf'.continuousAt.preimage_mem_nhds hf₀'
obtain ⟨t, htu, ht, htf⟩ := mem_nhds_iff.mp (Filter.inter_mem hu h_nhds)
use f.target ∩ f.symm ⁻¹' t
refine ⟨IsOpen.mem_nhds ?_ ?_, ?_⟩
· exact f.isOpen_inter_preimage_symm ht
· exact mem_inter ha (mem_preimage.mpr htf)
intro x hx
obtain ⟨hxu, e, he⟩ := htu hx.2
have h_deriv : HasFDerivAt f (e : E →L[𝕜] F) (f.symm x) :=
by
rw [he]
exact hff' (f.symm x) hxu
convert f.hasFDerivAt_symm hx.1 h_deriv
simp [← he]
· -- Then we check that the formula, being a composition of `ContDiff` pieces, is
-- itself `ContDiff`
have h_deriv₁ : ContDiffAt 𝕜 n inverse (f' (f.symm a)) :=
by
rw [eq_f₀']
exact contDiffAt_map_inverse _
have h_deriv₂ : ContDiffAt 𝕜 n f.symm a := by
refine IH (hf.of_le ?_)
norm_cast
exact Nat.le_succ n
exact (h_deriv₁.comp _ hf').comp _ h_deriv₂
| top Itop => exact contDiffAt_infty.mpr fun n ↦ Itop n (contDiffAt_infty.mp hf n)
