tsum_geometric_inv_two

Mathlib.Analysis.SpecificLimits.Basic

URI: https://scilib.ai/kg/mathlib#tsum_geometric_inv_two

English

Sum over i of ite(n ≤ i) (2⁻¹)^i equals 2 · 2⁻¹^n.

Русский

Сумма по i от нуля до ∞ индикатора n ≤ i умноженного на 2⁻¹^i равна 2 · 2⁻¹^n.

LaTeX

$$$\\\\sum' i, \\\\mathbf{1}_{\\\\{i \\\\mid n \\\\le i\\\\}} (2^{-1})^i = 2 \\\\cdot 2^{-n}$$$

Lean4

theorem tsum_geometric_inv_two : (∑' n : ℕ, (2 : ℝ)⁻¹ ^ n) = 2 :=
  (inv_eq_one_div (2 : ℝ)).symm ▸ tsum_geometric_two

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

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

Разделы

Аффилиация

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