English
For any element ξ in a normed division ring with ∥ξ∥ < 1, the geometric series ∑_{n≥0} ξ^n converges and its sum equals (1 − ξ)^{-1}. In particular, the series ∑ ξ^n = (1 − ξ)^{-1}.
Русский
Для любого элемента ξ в нормированном делении кольца с ∥ξ∥ < 1 ряд геометрической суммы ∑_{n≥0} ξ^n сходится и равен (1 − ξ)^{-1}. В частности, ∑ ξ^n = (1 − ξ)^{-1}.
LaTeX
$$$\|\xi\| < 1 \quad\Rightarrow\quad \sum_{n=0}^{\infty} \xi^{n} = (1 - \xi)^{-1}$$$
Lean4
theorem hasSum_geometric_of_norm_lt_one (h : ‖ξ‖ < 1) : HasSum (fun n : ℕ ↦ ξ ^ n) (1 - ξ)⁻¹ :=
by
have xi_ne_one : ξ ≠ 1 := by
contrapose! h
simp [h]
have A : Tendsto (fun n ↦ (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹)) :=
((tendsto_pow_atTop_nhds_zero_of_norm_lt_one h).sub tendsto_const_nhds).mul tendsto_const_nhds
rw [hasSum_iff_tendsto_nat_of_summable_norm]
· simpa [geom_sum_eq, xi_ne_one, neg_inv, div_eq_mul_inv] using A
· simp [norm_pow, summable_geometric_of_lt_one (norm_nonneg _) h]
