English
Let s be a Finset of integers and c ∈ ℤ with c ≤ x for all x ∈ s. Then ∑_{x∈Ico c (c+|s|)} x ≤ ∑_{x∈s} x.
Русский
Пусть s — конечное множество целых чисел и c ≤ x для всех x ∈ s. Тогда ∑_{x∈Ico(c, c+|s|)} x ≤ ∑_{x∈s} x.
LaTeX
$$$\sum_{x \in Ico\, c\,(c+|s|)} x \le \sum_{x \in s} x$$$
Lean4
/-- Sharp lower bound for the sum of a finset of integers that is bounded below, `Ico` version. -/
theorem sum_Ico_le_sum {s : Finset ℤ} {c : ℤ} (hs : ∀ x ∈ s, c ≤ x) : ∑ x ∈ Ico c (c + #s), x ≤ ∑ x ∈ s, x :=
by
set r := Ico c (c + #s)
calc
_ ≤ ∑ x ∈ r ∩ s, x + #(r \ s) • (c + #s) :=
by
rw [← sum_inter_add_sum_diff r s _]
refine add_le_add_left (sum_le_card_nsmul _ _ _ fun x mx ↦ ?_) _
rw [mem_sdiff, mem_Ico] at mx; exact mx.1.2.le
_ = ∑ x ∈ s ∩ r, x + #(s \ r) • (c + #s) :=
by
rw [inter_comm, card_sdiff_comm]
rw [Int.card_Ico, add_sub_cancel_left, Int.toNat_natCast]
_ ≤ _ := by
rw [← sum_inter_add_sum_diff s r _]
refine add_le_add_left (card_nsmul_le_sum _ _ _ fun x mx ↦ ?_) _
rw [mem_sdiff, mem_Ico, not_and] at mx
have := mx.2 (hs _ mx.1); omega
