English
If A is a normed ring with HasSummableGeomSeries, then the inverse map x ↦ (1−x)^{-1} admits a power-series expansion about 0, namely the geometric series.
Русский
Если A — нормированный кольцо с суммируемой геометрической серией, то отображение x ↦ (1−x)^{−1} имеет ряд степенной вокруг 0, равный геометрическому ряду.
LaTeX
$$HasFPowerSeriesOnBall\( (\lambda x, Ring.inverse (1 - x)) \( \text{formalMultilinearSeries_geometric }(\mathbb{k},A) \) 0 1$$
Lean4
theorem hasFPowerSeriesOnBall_inverse_one_sub (𝕜 : Type*) [NontriviallyNormedField 𝕜] (A : Type*) [NormedRing A]
[NormedAlgebra 𝕜 A] [HasSummableGeomSeries A] :
HasFPowerSeriesOnBall (fun x : A ↦ Ring.inverse (1 - x)) (formalMultilinearSeries_geometric 𝕜 A) 0 1 :=
by
constructor
· exact one_le_formalMultilinearSeries_geometric_radius 𝕜 A
· exact one_pos
· intro y hy
simp only [EMetric.mem_ball, edist_dist, dist_zero_right, ofReal_lt_one] at hy
simp only [zero_add, NormedRing.inverse_one_sub _ hy, Units.oneSub, Units.inv_mk, formalMultilinearSeries_geometric,
ContinuousMultilinearMap.mkPiAlgebraFin_apply, List.ofFn_const, List.prod_replicate]
exact (summable_geometric_of_norm_lt_one hy).hasSum
