tsum_two_zpow_neg_add_one — Mathlib

English

The infinite sum of 2^{-(1+m)} over m ≥ 0 equals 1.

Русский

Неотрицательная бесконечная сумма ∑_{m≥0} 2^{-(1+m)} равна 1.

LaTeX

$$$$\sum_{m=0}^{\infty} 2^{-(1+m)} = 1.$$$$

Lean4

theorem tsum_two_zpow_neg_add_one : ∑' m : ℕ, 2 ^ (-1 - m : ℤ) = (1 : ℝ≥0∞) :=
  by
  simp_rw [neg_sub_left, ENNReal.zpow_neg, ← Nat.cast_one (R := ℤ), ← Nat.cast_add, zpow_natCast, ENNReal.inv_pow,
    ENNReal.tsum_geometric_add_one, one_sub_inv_two, inv_inv]
  exact ENNReal.inv_mul_cancel (Ne.symm (NeZero.ne' 2)) (Ne.symm top_ne_ofNat)

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