sum_lt — Mathlib

English

From the previous identity, the sum ∑_{i=0}^{n-1} d(2d+1)^i is strictly less than (2d+1)^n.

Русский

Из предыдущей формулы следует, что сумма ∑_{i=0}^{n-1} d(2d+1)^i строго меньше (2d+1)^n.

LaTeX

$$$ \\sum_{i=0}^{n-1} d(2d+1)^i < (2d+1)^n $$$

Lean4

theorem sum_lt : (∑ i : Fin n, d * (2 * d + 1) ^ (i : ℕ)) < (2 * d + 1) ^ n :=
  sum_eq.trans_lt <| (Nat.div_le_self _ 2).trans_lt <| pred_lt (pow_pos (succ_pos _) _).ne'

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