English
For any 𝕜 and 𝕝 with a normed algebra structure, the map x ↦ (1−x)^{-1} is analytic at 0.
Русский
Для любых 𝕜 и 𝕝 с нормированной алгеброй отображение x ↦ (1−x)^{-1} аналитично в 0.
LaTeX
$$$\operatorname{AnalyticAt} 𝕜\, (x \mapsto (1 - x)^{-1})\ 0$$$
Lean4
/-- If `A` is a normed algebra over `𝕜` with summable geometric series, then inversion on `A` is
analytic at any unit. -/
@[fun_prop]
theorem analyticAt_inverse {𝕜 : Type*} [NontriviallyNormedField 𝕜] {A : Type*} [NormedRing A] [NormedAlgebra 𝕜 A]
[HasSummableGeomSeries A] (z : Aˣ) : AnalyticAt 𝕜 Ring.inverse (z : A) :=
by
rcases subsingleton_or_nontrivial A with hA | hA
· convert analyticAt_const (v := (0 : A))
· let f1 : A → A := fun a ↦ a * z.inv
let f2 : A → A := fun b ↦ Ring.inverse (1 - b)
let f3 : A → A := fun c ↦ 1 - z.inv * c
have feq : ∀ᶠ y in 𝓝 (z : A), (f1 ∘ f2 ∘ f3) y = Ring.inverse y :=
by
have : Metric.ball (z : A) (‖(↑z⁻¹ : A)‖⁻¹) ∈ 𝓝 (z : A) :=
by
apply Metric.ball_mem_nhds
simp
filter_upwards [this] with y hy
simp only [Metric.mem_ball, dist_eq_norm] at hy
have : y = Units.ofNearby z y hy := rfl
rw [this, Eq.comm]
simp only [Ring.inverse_unit, Function.comp_apply]
simp [Units.ofNearby, f1, f2, f3, Units.add, _root_.mul_sub]
rw [← Ring.inverse_unit]
congr
simp
apply AnalyticAt.congr _ feq
apply (analyticAt_id.mul analyticAt_const).comp
apply AnalyticAt.comp
· simp only [Units.inv_eq_val_inv, Units.inv_mul, sub_self, f2, f3]
exact analyticAt_inverse_one_sub 𝕜 A
· exact analyticAt_const.sub (analyticAt_const.mul analyticAt_id)
