Documentation

Mathlib.Algebra.Order.Group.Int.Sum

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 : xs, x c) :
xs, x xIoc (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 : xs, x c) :
xs, x nrange 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 : xs, c x) :
xIco c (c + s.card), x xs, 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 : xs, c x) :
nrange s.card, (c + n) xs, x

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