analyticAt_inverse_one_sub — Mathlib

English

Let A be a normed algebra over 𝕜 with HasSummableGeomSeries. Then the map x ↦ (1−x)^{−1} is analytic at x = 0.

Русский

Пусть A — нормированная алгебра над 𝕜 с суммируемой геометрической серией. Тогда отображение x ↦ (1−x)^{−1} аналитично в точке x = 0.

LaTeX

$$$\operatorname{AnalyticAt}\\(\mathcal{A}\,)(x) : (1-x)^{-1} \,\text{относительно} \,0$$$

Lean4

@[fun_prop]
theorem analyticAt_inverse_one_sub (𝕜 : Type*) [NontriviallyNormedField 𝕜] (A : Type*) [NormedRing A]
    [NormedAlgebra 𝕜 A] [HasSummableGeomSeries A] : AnalyticAt 𝕜 (fun x : A ↦ Ring.inverse (1 - x)) 0 :=
  ⟨_, ⟨_, hasFPowerSeriesOnBall_inverse_one_sub 𝕜 A⟩⟩

Похожие утверждения