hasSum_geometric_of_abs_lt_one — Mathlib

English

For real r with |r| < 1, the geometric series ∑_{n≥0} r^n converges and equals (1 − r)^{-1}.

Русский

Для действительного r с |r| < 1 ряд геометрической суммы сходится и равен (1 − r)^{-1}.

LaTeX

$$$|r| < 1 \Rightarrow \sum_{n=0}^{\infty} r^{n} = (1 - r)^{-1}$$$

Lean4

theorem hasSum_geometric_of_abs_lt_one {r : ℝ} (h : |r| < 1) : HasSum (fun n : ℕ ↦ r ^ n) (1 - r)⁻¹ :=
  hasSum_geometric_of_norm_lt_one h

Похожие утверждения