English
If f is ContDiff 𝕜 n on a domain and f has no zeros, then x ↦ f(x)^{-1} is ContDiff 𝕜 n on that domain.
Русский
Если f — ContDiff 𝕜 n на множестве и f не обращается в ноль, то x↦f(x)^{-1} — ContDiff 𝕜 n на этом множестве.
LaTeX
$$$\\mathrm{ContDiff}_{\\mathbb{k}}\\ n\\ f \\Rightarrow (\\forall x, f(x)\\neq 0) \\Rightarrow \\mathrm{ContDiff}_{\\mathbb{k}}\\ n\\ (x\\mapsto f(x)^{-1})$$$
Lean4
/-- At a continuous linear equivalence `e : E ≃L[𝕜] F` between Banach spaces, the operation of
inversion is `C^n`, for all `n`. -/
@[fun_prop]
theorem contDiffAt_map_inverse [CompleteSpace E] (e : E ≃L[𝕜] F) : ContDiffAt 𝕜 n inverse (e : E →L[𝕜] F) :=
by
nontriviality E
let O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp (e.symm : F →L[𝕜] E)
let O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (e.symm : F →L[𝕜] E).comp f
have : ContinuousLinearMap.inverse = O₁ ∘ Ring.inverse ∘ O₂ := funext (inverse_eq_ringInverse e)
rw [this]
-- `O₁` and `O₂` are `ContDiff`,
-- so we reduce to proving that `Ring.inverse` is `ContDiff`
have h₁ : ContDiff 𝕜 n O₁ := contDiff_id.clm_comp contDiff_const
have h₂ : ContDiff 𝕜 n O₂ := contDiff_const.clm_comp contDiff_id
refine h₁.contDiffAt.comp _ (ContDiffAt.comp _ ?_ h₂.contDiffAt)
convert contDiffAt_ringInverse 𝕜 (1 : (E →L[𝕜] E)ˣ)
simp [O₂, one_def]
