geom_sum_le — Mathlib

English

For b ≥ 2, and natural a, n, the finite geometric sum is bounded by a b / (b-1).

Русский

При b ≥ 2 и натуралах a, n геометрическая сумма ограничена сверху выражением $a b/(b-1)$.

LaTeX

$$$hb: 2 \\le b \\Rightarrow \\forall a,n:\\ \\sum_{i=0}^{n-1} \\frac{a}{b^i} \\le \\frac{a b}{b-1}$$$

Lean4

theorem geom_sum_le {b : ℕ} (hb : 2 ≤ b) (a n : ℕ) : ∑ i ∈ range n, a / b ^ i ≤ a * b / (b - 1) :=
  by
  refine (Nat.le_div_iff_mul_le <| tsub_pos_of_lt hb).2 ?_
  rcases n with - | n
  · rw [sum_range_zero, zero_mul]
    exact Nat.zero_le _
  rw [mul_comm]
  exact (Nat.pred_mul_geom_sum_le a b n).trans tsub_le_self

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