English
The series ∑ r^n in ENNReal equals (1 − r)^{-1}; the result holds by considering cases r < 1 and r ≥ 1.
Русский
Серия ∑ r^n в ENNReal равна (1 − r)^{-1}; разбираются случаи r < 1 и r ≥ 1.
LaTeX
$$$\\\\forall r \\\\in \\\\mathbb{R}_{\\\\ge 0}∞, \\\\text{tends to } (1 - r)^{-1}.$$$
Lean4
/-- The series `pow r` converges to `(1-r)⁻¹`. For `r < 1` the RHS is a finite number,
and for `1 ≤ r` the RHS equals `∞`. -/
@[simp]
theorem tsum_geometric (r : ℝ≥0∞) : ∑' n : ℕ, r ^ n = (1 - r)⁻¹ :=
by
rcases lt_or_ge r 1 with hr | hr
· rcases ENNReal.lt_iff_exists_coe.1 hr with ⟨r, rfl, hr'⟩
norm_cast at *
convert ENNReal.tsum_coe_eq (NNReal.hasSum_geometric hr)
rw [ENNReal.coe_inv <| ne_of_gt <| tsub_pos_iff_lt.2 hr, coe_sub, coe_one]
· rw [tsub_eq_zero_iff_le.mpr hr, ENNReal.inv_zero, ENNReal.tsum_eq_iSup_nat, iSup_eq_top]
refine fun a ha ↦ (ENNReal.exists_nat_gt (lt_top_iff_ne_top.1 ha)).imp fun n hn ↦ lt_of_lt_of_le hn ?_
calc
(n : ℝ≥0∞) = ∑ i ∈ range n, 1 := by rw [sum_const, nsmul_one, card_range]
_ ≤ ∑ i ∈ range n, r ^ i := by gcongr; apply one_le_pow₀ hr
