English
Let m ≥ 2 be a natural number and let s be a finite set of natural numbers such that every element k of s satisfies k < n. Then the sum of m^k over k in s is strictly less than m^n.
Русский
Пусть m ≥ 2 — натуральное число и пусть s — конечное множество натуральных чисел, для каждого k ∈ s выполняется k < n. Тогда сумма m^k по k ∈ s строго меньше m^n.
LaTeX
$$$2 \le m$ и (\forall k \in s, k < n) \Rightarrow \sum_{k \in s} m^k < m^n$$
Lean4
/-- If all the elements of a finset of naturals are less than `n`, then the sum of their powers of
`m ≥ 2` is less than `m ^ n`. -/
theorem geomSum_lt (hm : 2 ≤ m) (hs : ∀ k ∈ s, k < n) : ∑ k ∈ s, m ^ k < m ^ n :=
calc
∑ k ∈ s, m ^ k ≤ ∑ k ∈ range n, m ^ k := sum_le_sum_of_subset fun _ hk ↦ mem_range.2 <| hs _ hk
_ = (m ^ n - 1) / (m - 1) := (Nat.geomSum_eq hm _)
_ ≤ m ^ n - 1 := (Nat.div_le_self _ _)
_ < m ^ n := tsub_lt_self (Nat.pow_pos <| by cutsat) (by cutsat)
