English
For Finset s ⊆ ℤ and c ∈ ℤ, sum over range(#s) of (c − n) bounds sum over s: ∑_{x∈s} x ≤ ∑_{n ∈ range(#s)} (c − n).
Русский
Для конечного множества s ⊆ ℤ и c ∈ ℤ справедливо ∑_{x∈s} x ≤ ∑_{n∈range(|s|)} (c − n).
LaTeX
$$$\sum_{x \in s} x \le \sum_{n \in range\,#s} (c - n)$$$
Lean4
/-- Sharp upper bound for the sum of a finset of integers that is bounded above, `range` version. -/
theorem sum_le_sum_range {s : Finset ℤ} {c : ℤ} (hs : ∀ x ∈ s, x ≤ c) : ∑ x ∈ s, x ≤ ∑ n ∈ range #s, (c - n) :=
by
convert sum_le_sum_Ioc hs
refine sum_nbij (c - ·) ?_ ?_ ?_ (fun _ _ ↦ rfl)
· intro x mx; rw [mem_Ioc]; dsimp only; rw [mem_range] at mx; cutsat
· intro x mx y my (h : c - x = c - y); cutsat
· intro x mx; simp_rw [coe_range, Set.mem_image, Set.mem_Iio]
rw [mem_coe, mem_Ioc] at mx
use (c - x).toNat; cutsat
