summable_geometric

Mathlib.Analysis.SpecificLimits.Basic

URI: https://scilib.ai/kg/mathlib#NNReal.summable_geometric

English

If r ∈ NNReal and r < 1, then ∑ r^n = (1 − r)^{-1}. In particular, the series is summable with HasSum.

Русский

Если r ∈ NNReal и r < 1, то ∑ r^n = (1 − r)^{-1}; ряд суммируем.

LaTeX

$$$\\\\forall r \\\\in \\\\mathbb{NNReal}, \\\\ r < 1 \\\\Rightarrow \\\\ sum r^n = (1 - r)^{-1}.$$$

Lean4

theorem summable_geometric {r : ℝ≥0} (hr : r < 1) : Summable fun n : ℕ ↦ r ^ n :=
  ⟨_, NNReal.hasSum_geometric hr⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru