English
If 0 ≤ r < 1, then the geometric series sums to (1 − r)^{-1}. More generally, HasSum (n ↦ r^n) = (1 − r)^{-1}.
Русский
Если 0 ≤ r < 1, то геометрическая серия сходится к (1 − r)^{-1}. Более точно, HasSum (n ↦ r^n) = (1 − r)^{-1}.
LaTeX
$$$\\\\forall r \\\\in \\\\mathbb{R}, \\\\ 0 \\\\le r \\\\wedge r < 1 \\\\Rightarrow HasSum (\\\\lambda n, r^n) (1 - r)^{-1}.$$$
Lean4
theorem hasSum_geometric_of_lt_one {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) : HasSum (fun n : ℕ ↦ r ^ n) (1 - r)⁻¹ :=
have : r ≠ 1 := ne_of_lt h₂
have : Tendsto (fun n ↦ (r ^ n - 1) * (r - 1)⁻¹) atTop (𝓝 ((0 - 1) * (r - 1)⁻¹)) :=
((tendsto_pow_atTop_nhds_zero_of_lt_one h₁ h₂).sub tendsto_const_nhds).mul tendsto_const_nhds
(hasSum_iff_tendsto_nat_of_nonneg (pow_nonneg h₁) _).mpr <| by simp_all [neg_inv, geom_sum_eq, div_eq_mul_inv]
