Sharp bounds for sums of bounded finsets of integers

The sum of a finset of integers with cardinality s where all elements are at most c can be given a sharper upper bound than #s * c, because the elements are distinct.

This file provides these sharp bounds, both in the upper-bounded and analogous lower-bounded cases.

theorem Finset.sum_le_sum_Ioc {s : Finset ℤ} {c : ℤ} (hs : ∀ x ∈ s, x ≤ c) : ∑ x ∈ s, x ≤ ∑ x ∈ Ioc (c - ↑s.card) c, x

Sharp upper bound for the sum of a finset of integers that is bounded above, Ioc version.

theorem Finset.sum_le_sum_range {s : Finset ℤ} {c : ℤ} (hs : ∀ x ∈ s, x ≤ c) : ∑ x ∈ s, x ≤ ∑ n ∈ range s.card, (c - ↑n)

Sharp upper bound for the sum of a finset of integers that is bounded above, range version.

theorem Finset.sum_Ico_le_sum {s : Finset ℤ} {c : ℤ} (hs : ∀ x ∈ s, c ≤ x) : ∑ x ∈ Ico c (c + ↑s.card), x ≤ ∑ x ∈ s, x

Sharp lower bound for the sum of a finset of integers that is bounded below, Ico version.

theorem Finset.sum_range_le_sum {s : Finset ℤ} {c : ℤ} (hs : ∀ x ∈ s, c ≤ x) : ∑ n ∈ range s.card, (c + ↑n) ≤ ∑ x ∈ s, x

Sharp lower bound for the sum of a finset of integers that is bounded below, range version.