hasSum_geometric — Mathlib

English

For any a ∈ ℝ, the geometric sum with appropriate indexing equals a.

Русский

Для любого a ∈ ℝ геометрическая сумма с соответствующей индексацией равна a.

LaTeX

$$$\\\\forall a \\\\in \\\\mathbb{R}, \\\\text{HasSum } (n \\\\mapsto a/2 / 2^n) a$$$

Lean4

/-- **Sum of a Geometric Series** -/
theorem hasSum_geometric {r : ℝ≥0} (hr : r < 1) : HasSum (fun n : ℕ ↦ r ^ n) (1 - r)⁻¹ :=
  by
  apply NNReal.hasSum_coe.1
  push_cast
  rw [NNReal.coe_sub (le_of_lt hr)]
  exact hasSum_geometric_of_lt_one r.coe_nonneg hr

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