English
For natural n, the sum of the tail of the geometric sequence with ratio 1/2 equals 2 · (1/2)^n.
Русский
Для натурального n сумма хвоста геометрической последовательности с коэффициентом 1/2 равна 2 · (1/2)^n.
LaTeX
$$$\\\\forall n \\\\in \\\\mathbb{N}, \\\\sum i, \\\\text{indicator}(n ≤ i) (2^{-1})^i = 2 \\\\cdot 2^{-n}$$$
Lean4
/-- The sum of `2⁻¹ ^ i` for `n ≤ i` equals `2 * 2⁻¹ ^ n`. -/
theorem tsum_geometric_inv_two_ge (n : ℕ) : (∑' i, ite (n ≤ i) ((2 : ℝ)⁻¹ ^ i) 0) = 2 * 2⁻¹ ^ n :=
by
have A : Summable fun i : ℕ ↦ ite (n ≤ i) ((2⁻¹ : ℝ) ^ i) 0 := by
simpa only [← piecewise_eq_indicator, one_div] using summable_geometric_two.indicator {i | n ≤ i}
have B : ((Finset.range n).sum fun i : ℕ ↦ ite (n ≤ i) ((2⁻¹ : ℝ) ^ i) 0) = 0 :=
Finset.sum_eq_zero fun i hi ↦ ite_eq_right_iff.2 fun h ↦ (lt_irrefl _ ((Finset.mem_range.1 hi).trans_le h)).elim
simp only [← Summable.sum_add_tsum_nat_add n A, B, if_true, zero_add, zero_le', le_add_iff_nonneg_left, pow_add,
_root_.tsum_mul_right, tsum_geometric_inv_two]
