sum_geometric_two_le — Mathlib

English

For all n, the partial sum of the geometric series with ratio 1/2 is at most 2.

Русский

Для любых n частичная сумма геометрической серии с коэффициентом 1/2 не превосходит 2.

LaTeX

$$$\\\\forall n \\\\in \\\\mathbb{N}, \\\\bigl(\\\\sum i \\\\in \\\\mathrm{range}(n), (\\\\tfrac{1}{2})^i\\\\bigr) \\\\le 2$$$

Lean4

theorem sum_geometric_two_le (n : ℕ) : (∑ i ∈ range n, (1 / (2 : ℝ)) ^ i) ≤ 2 :=
  by
  have : ∀ i, 0 ≤ (1 / (2 : ℝ)) ^ i := by
    intro i
    apply pow_nonneg
    norm_num
  convert summable_geometric_two.sum_le_tsum (range n) (fun i _ ↦ this i)
  exact tsum_geometric_two.symm

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