English
For |x|<1, the sum of x^i equals (1 - x)^{-1}.
Русский
Для |x|<1 сумма x^i равна (1 - x)^{-1}.
LaTeX
$$$\\\\sum_{i=0}^{\\\\infty} x^i = (1 - x)^{-1} \\\\text{ if } ||x|| < 1$$$
Lean4
/-- Bound for the sum of a geometric series in a normed ring. This formula does not assume that the
normed ring satisfies the axiom `‖1‖ = 1`. -/
theorem tsum_geometric_le_of_norm_lt_one (x : R) (h : ‖x‖ < 1) : ‖∑' n : ℕ, x ^ n‖ ≤ ‖(1 : R)‖ - 1 + (1 - ‖x‖)⁻¹ :=
by
by_cases hx : Summable (fun n ↦ x ^ n)
· rw [hx.tsum_eq_zero_add]
simp only [_root_.pow_zero]
refine le_trans (norm_add_le _ _) ?_
have : ‖∑' b : ℕ, (fun n ↦ x ^ (n + 1)) b‖ ≤ (1 - ‖x‖)⁻¹ - 1 :=
by
refine tsum_of_norm_bounded ?_ fun b ↦ norm_pow_le' _ (Nat.succ_pos b)
convert (hasSum_nat_add_iff' 1).mpr (hasSum_geometric_of_lt_one (norm_nonneg x) h)
simp
linarith
· simp only [tsum_eq_zero_of_not_summable hx, norm_zero]
nontriviality R
have : 1 ≤ ‖(1 : R)‖ := one_le_norm_one R
have : 0 ≤ (1 - ‖x‖)⁻¹ := inv_nonneg.2 (by linarith)
linarith
