English
For b ≥ 2, the sum over the interval Ico(1, n) satisfies a similar bound: ≤ a/(b-1) plus a/(b-1) terms; yields overall bound by a/(b-1) scaled by n-1.
Русский
Для b ≥ 2 сумма по интервалу Ico(1, n) удовлетворяет аналогичному ограничению: ≤ a/(b-1) и т.д.
LaTeX
$$$hb: 2 \\le b \\Rightarrow \\sum_{i=1}^{n-1} \\frac{a}{b^i} \\le \\frac{a}{b-1}$$$
Lean4
theorem geom_sum_Ico_le {b : ℕ} (hb : 2 ≤ b) (a n : ℕ) : ∑ i ∈ Ico 1 n, a / b ^ i ≤ a / (b - 1) :=
by
rcases n with - | n
· rw [Ico_eq_empty_of_le (by cutsat), sum_empty]
exact Nat.zero_le _
rw [← add_le_add_iff_left a]
calc
(a + ∑ i ∈ Ico 1 n.succ, a / b ^ i) = a / b ^ 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i := by rw [pow_zero, Nat.div_one]
_ = ∑ i ∈ range n.succ, a / b ^ i := by
rw [range_eq_Ico, ← Finset.insert_Ico_add_one_left_eq_Ico (Nat.succ_pos _), sum_insert] <;> simp
_ ≤ a * b / (b - 1) := (Nat.geom_sum_le hb a _)
_ = (a * 1 + a * (b - 1)) / (b - 1) := by rw [← mul_add, add_tsub_cancel_of_le (by cutsat)]
_ = a + a / (b - 1) := by rw [mul_one, Nat.add_mul_div_right _ _ (tsub_pos_of_lt hb), add_comm]
