English
Let s be a Finset of integers and c an integer, if every x ∈ s satisfies x ≤ c, then the sum over s is bounded above by the sum over Ioc (c − |s|, c) of x, i.e., ∑_{x∈s} x ≤ ∑_{x∈Ioc(c−|s|, c)} x.
Русский
Пусть s — конечное множество целых чисел, и каждый элемент x ∈ s удовлетворяет x ≤ c. Тогда сумма по s не превышает сумму по Ioc(c − |s|, c).
LaTeX
$$$\forall s \subseteq \mathbb{Z}, \ c \in \mathbb{Z},\ (\forall x \in s, x \le c) \Rightarrow \sum_{x \in s} x \le \sum_{x \in Ioc(c - |s|, c)} x$$$
Lean4
/-- Sharp upper bound for the sum of a finset of integers that is bounded above, `Ioc` version. -/
theorem sum_le_sum_Ioc {s : Finset ℤ} {c : ℤ} (hs : ∀ x ∈ s, x ≤ c) : ∑ x ∈ s, x ≤ ∑ x ∈ Ioc (c - #s) c, x :=
by
set r := Ioc (c - #s) c
calc
_ ≤ ∑ x ∈ s ∩ r, x + #(s \ r) • (c - #s) :=
by
rw [← sum_inter_add_sum_diff s r _]
gcongr
refine sum_le_card_nsmul _ _ _ fun x mx ↦ ?_
rw [mem_sdiff, mem_Ioc, not_and'] at mx
have := mx.2 (hs _ mx.1); omega
_ = ∑ x ∈ r ∩ s, x + #(r \ s) • (c - #s) :=
by
rw [inter_comm, card_sdiff_comm]
rw [Int.card_Ioc, sub_sub_cancel, Int.toNat_natCast]
_ ≤ _ := by
rw [← sum_inter_add_sum_diff r s _]
gcongr
refine card_nsmul_le_sum _ _ _ fun x mx ↦ ?_
rw [mem_sdiff, mem_Ioc] at mx; exact mx.1.1.le
