Documentation

Mathlib.Algebra.Order.BigOperators.Group.Finset

Big operators on a finset in ordered groups #

This file contains the results concerning the interaction of multiset big operators with ordered groups/monoids.

theorem Finset.le_sum_nonempty_of_subadditive_on_pred {ι : Type u_1} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [OrderedAddCommMonoid N] (f : MN) (p : MProp) (h_mul : ∀ (x y : M), p xp yf (x + y) f x + f y) (hp_mul : ∀ (x y : M), p xp yp (x + y)) (g : ιM) (s : Finset ι) (hs_nonempty : s.Nonempty) (hs : is, p (g i)) :
f (∑ is, g i) is, f (g i)

Let {x | p x} be an additive subsemigroup of an additive commutative monoid M. Let f : M → N be a map subadditive on {x | p x}, i.e., p x → p y → f (x + y) ≤ f x + f y. Let g i, i ∈ s, be a nonempty finite family of elements of M such that ∀ i ∈ s, p (g i). Then f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i).

theorem Finset.le_prod_nonempty_of_submultiplicative_on_pred {ι : Type u_1} {M : Type u_4} {N : Type u_5} [CommMonoid M] [OrderedCommMonoid N] (f : MN) (p : MProp) (h_mul : ∀ (x y : M), p xp yf (x * y) f x * f y) (hp_mul : ∀ (x y : M), p xp yp (x * y)) (g : ιM) (s : Finset ι) (hs_nonempty : s.Nonempty) (hs : is, p (g i)) :
f (∏ is, g i) is, f (g i)

Let {x | p x} be a subsemigroup of a commutative monoid M. Let f : M → N be a map submultiplicative on {x | p x}, i.e., p x → p y → f (x * y) ≤ f x * f y. Let g i, i ∈ s, be a nonempty finite family of elements of M such that ∀ i ∈ s, p (g i). Then f (∏ x ∈ s, g x) ≤ ∏ x ∈ s, f (g x).

theorem Finset.le_sum_nonempty_of_subadditive {ι : Type u_1} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [OrderedAddCommMonoid N] (f : MN) (h_mul : ∀ (x y : M), f (x + y) f x + f y) {s : Finset ι} (hs : s.Nonempty) (g : ιM) :
f (∑ is, g i) is, f (g i)

If f : M → N is a subadditive function, f (x + y) ≤ f x + f y and g i, i ∈ s, is a nonempty finite family of elements of M, then f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i).

theorem Finset.le_prod_nonempty_of_submultiplicative {ι : Type u_1} {M : Type u_4} {N : Type u_5} [CommMonoid M] [OrderedCommMonoid N] (f : MN) (h_mul : ∀ (x y : M), f (x * y) f x * f y) {s : Finset ι} (hs : s.Nonempty) (g : ιM) :
f (∏ is, g i) is, f (g i)

If f : M → N is a submultiplicative function, f (x * y) ≤ f x * f y and g i, i ∈ s, is a nonempty finite family of elements of M, then f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i).

theorem Finset.le_sum_of_subadditive_on_pred {ι : Type u_1} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [OrderedAddCommMonoid N] (f : MN) (p : MProp) (h_one : f 0 = 0) (h_mul : ∀ (x y : M), p xp yf (x + y) f x + f y) (hp_mul : ∀ (x y : M), p xp yp (x + y)) (g : ιM) {s : Finset ι} (hs : is, p (g i)) :
f (∑ is, g i) is, f (g i)

Let {x | p x} be a subsemigroup of a commutative additive monoid M. Let f : M → N be a map such that f 0 = 0 and f is subadditive on {x | p x}, i.e. p x → p y → f (x + y) ≤ f x + f y. Let g i, i ∈ s, be a finite family of elements of M such that ∀ i ∈ s, p (g i). Then f (∑ x ∈ s, g x) ≤ ∑ x ∈ s, f (g x).

theorem Finset.le_prod_of_submultiplicative_on_pred {ι : Type u_1} {M : Type u_4} {N : Type u_5} [CommMonoid M] [OrderedCommMonoid N] (f : MN) (p : MProp) (h_one : f 1 = 1) (h_mul : ∀ (x y : M), p xp yf (x * y) f x * f y) (hp_mul : ∀ (x y : M), p xp yp (x * y)) (g : ιM) {s : Finset ι} (hs : is, p (g i)) :
f (∏ is, g i) is, f (g i)

Let {x | p x} be a subsemigroup of a commutative monoid M. Let f : M → N be a map such that f 1 = 1 and f is submultiplicative on {x | p x}, i.e., p x → p y → f (x * y) ≤ f x * f y. Let g i, i ∈ s, be a finite family of elements of M such that ∀ i ∈ s, p (g i). Then f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i).

theorem Finset.le_sum_of_subadditive {ι : Type u_1} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [OrderedAddCommMonoid N] (f : MN) (h_one : f 0 = 0) (h_mul : ∀ (x y : M), f (x + y) f x + f y) (s : Finset ι) (g : ιM) :
f (∑ is, g i) is, f (g i)

If f : M → N is a subadditive function, f (x + y) ≤ f x + f y, f 0 = 0, and g i, i ∈ s, is a finite family of elements of M, then f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i).

theorem Finset.le_prod_of_submultiplicative {ι : Type u_1} {M : Type u_4} {N : Type u_5} [CommMonoid M] [OrderedCommMonoid N] (f : MN) (h_one : f 1 = 1) (h_mul : ∀ (x y : M), f (x * y) f x * f y) (s : Finset ι) (g : ιM) :
f (∏ is, g i) is, f (g i)

If f : M → N is a submultiplicative function, f (x * y) ≤ f x * f y, f 1 = 1, and g i, i ∈ s, is a finite family of elements of M, then f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i).

theorem Finset.sum_le_sum {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ιN} {g : ιN} {s : Finset ι} (h : is, f i g i) :
is, f i is, g i

In an ordered additive commutative monoid, if each summand f i of one finite sum is less than or equal to the corresponding summand g i of another finite sum, then ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i.

theorem Finset.prod_le_prod' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ιN} {g : ιN} {s : Finset ι} (h : is, f i g i) :
is, f i is, g i

In an ordered commutative monoid, if each factor f i of one finite product is less than or equal to the corresponding factor g i of another finite product, then ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i.

theorem Finset.sum_nonneg {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ιN} {s : Finset ι} (h : is, 0 f i) :
0 is, f i
theorem Finset.one_le_prod' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ιN} {s : Finset ι} (h : is, 1 f i) :
1 is, f i
theorem Finset.sum_nonneg' {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ιN} {s : Finset ι} (h : ∀ (i : ι), 0 f i) :
0 is, f i
theorem Finset.one_le_prod'' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ιN} {s : Finset ι} (h : ∀ (i : ι), 1 f i) :
1 is, f i
theorem Finset.sum_nonpos {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ιN} {s : Finset ι} (h : is, f i 0) :
is, f i 0
theorem Finset.prod_le_one' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ιN} {s : Finset ι} (h : is, f i 1) :
is, f i 1
theorem Finset.sum_le_sum_of_subset_of_nonneg {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ιN} {s : Finset ι} {t : Finset ι} (h : s t) (hf : it, is0 f i) :
is, f i it, f i
theorem Finset.prod_le_prod_of_subset_of_one_le' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ιN} {s : Finset ι} {t : Finset ι} (h : s t) (hf : it, is1 f i) :
is, f i it, f i
theorem Finset.sum_mono_set_of_nonneg {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ιN} (hf : ∀ (x : ι), 0 f x) :
Monotone fun (s : Finset ι) => xs, f x
theorem Finset.prod_mono_set_of_one_le' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ιN} (hf : ∀ (x : ι), 1 f x) :
Monotone fun (s : Finset ι) => xs, f x
theorem Finset.sum_le_univ_sum_of_nonneg {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ιN} [Fintype ι] {s : Finset ι} (w : ∀ (x : ι), 0 f x) :
xs, f x x : ι, f x
theorem Finset.prod_le_univ_prod_of_one_le' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ιN} [Fintype ι] {s : Finset ι} (w : ∀ (x : ι), 1 f x) :
xs, f x x : ι, f x
theorem Finset.sum_eq_zero_iff_of_nonneg {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ιN} {s : Finset ι} :
(∀ is, 0 f i)(is, f i = 0 is, f i = 0)
theorem Finset.prod_eq_one_iff_of_one_le' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ιN} {s : Finset ι} :
(∀ is, 1 f i)(is, f i = 1 is, f i = 1)
theorem Finset.sum_eq_zero_iff_of_nonpos {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ιN} {s : Finset ι} :
(∀ is, f i 0)(is, f i = 0 is, f i = 0)
theorem Finset.prod_eq_one_iff_of_le_one' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ιN} {s : Finset ι} :
(∀ is, f i 1)(is, f i = 1 is, f i = 1)
theorem Finset.single_le_sum {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ιN} {s : Finset ι} (hf : is, 0 f i) {a : ι} (h : a s) :
f a xs, f x
theorem Finset.single_le_prod' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ιN} {s : Finset ι} (hf : is, 1 f i) {a : ι} (h : a s) :
f a xs, f x
theorem Finset.add_le_sum {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ιN} {s : Finset ι} {i : ι} {j : ι} (hf : is, 0 f i) (hi : i s) (hj : j s) (hne : i j) :
f i + f j ks, f k
theorem Finset.mul_le_prod {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ιN} {s : Finset ι} {i : ι} {j : ι} (hf : is, 1 f i) (hi : i s) (hj : j s) (hne : i j) :
f i * f j ks, f k
theorem Finset.sum_le_card_nsmul {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] (s : Finset ι) (f : ιN) (n : N) (h : xs, f x n) :
s.sum f s.card n
theorem Finset.prod_le_pow_card {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] (s : Finset ι) (f : ιN) (n : N) (h : xs, f x n) :
s.prod f n ^ s.card
theorem Finset.card_nsmul_le_sum {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] (s : Finset ι) (f : ιN) (n : N) (h : xs, n f x) :
s.card n s.sum f
theorem Finset.pow_card_le_prod {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] (s : Finset ι) (f : ιN) (n : N) (h : xs, n f x) :
n ^ s.card s.prod f
theorem Finset.card_biUnion_le_card_mul {ι : Type u_1} {β : Type u_3} [DecidableEq β] (s : Finset ι) (f : ιFinset β) (n : ) (h : as, (f a).card n) :
(s.biUnion f).card s.card * n
theorem Finset.sum_fiberwise_le_sum_of_sum_fiber_nonneg {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {s : Finset ι} {ι' : Type u_9} [DecidableEq ι'] {t : Finset ι'} {g : ιι'} {f : ιN} (h : yt, 0 xFinset.filter (fun (x : ι) => g x = y) s, f x) :
yt, xFinset.filter (fun (x : ι) => g x = y) s, f x xs, f x
theorem Finset.prod_fiberwise_le_prod_of_one_le_prod_fiber' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {s : Finset ι} {ι' : Type u_9} [DecidableEq ι'] {t : Finset ι'} {g : ιι'} {f : ιN} (h : yt, 1 xFinset.filter (fun (x : ι) => g x = y) s, f x) :
yt, xFinset.filter (fun (x : ι) => g x = y) s, f x xs, f x
theorem Finset.sum_le_sum_fiberwise_of_sum_fiber_nonpos {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {s : Finset ι} {ι' : Type u_9} [DecidableEq ι'] {t : Finset ι'} {g : ιι'} {f : ιN} (h : yt, xFinset.filter (fun (x : ι) => g x = y) s, f x 0) :
xs, f x yt, xFinset.filter (fun (x : ι) => g x = y) s, f x
theorem Finset.prod_le_prod_fiberwise_of_prod_fiber_le_one' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {s : Finset ι} {ι' : Type u_9} [DecidableEq ι'] {t : Finset ι'} {g : ιι'} {f : ιN} (h : yt, xFinset.filter (fun (x : ι) => g x = y) s, f x 1) :
xs, f x yt, xFinset.filter (fun (x : ι) => g x = y) s, f x
theorem Finset.abs_sum_le_sum_abs {ι : Type u_1} {G : Type u_9} [LinearOrderedAddCommGroup G] (f : ιG) (s : Finset ι) :
|is, f i| is, |f i|
theorem Finset.abs_sum_of_nonneg {ι : Type u_1} {G : Type u_9} [LinearOrderedAddCommGroup G] {f : ιG} {s : Finset ι} (hf : is, 0 f i) :
|is, f i| = is, f i
theorem Finset.abs_sum_of_nonneg' {ι : Type u_1} {G : Type u_9} [LinearOrderedAddCommGroup G] {f : ιG} {s : Finset ι} (hf : ∀ (i : ι), 0 f i) :
|is, f i| = is, f i
@[simp]
theorem Finset.addLECancellable_sum {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {s : Finset ι} {f : ια} :
AddLECancellable (∑ is, f i) ∀ ⦃i : ι⦄, i sAddLECancellable (f i)
@[simp]
theorem Finset.mulLECancellable_prod {ι : Type u_1} {α : Type u_2} [CommMonoid α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {s : Finset ι} {f : ια} :
MulLECancellable (∏ is, f i) ∀ ⦃i : ι⦄, i sMulLECancellable (f i)
theorem Finset.card_le_mul_card_image_of_maps_to {α : Type u_2} {β : Type u_3} [DecidableEq β] {f : αβ} {s : Finset α} {t : Finset β} (Hf : as, f a t) (n : ) (hn : at, (Finset.filter (fun (x : α) => f x = a) s).card n) :
s.card n * t.card
theorem Finset.card_le_mul_card_image {α : Type u_2} {β : Type u_3} [DecidableEq β] {f : αβ} (s : Finset α) (n : ) (hn : aFinset.image f s, (Finset.filter (fun (x : α) => f x = a) s).card n) :
s.card n * (Finset.image f s).card
theorem Finset.mul_card_image_le_card_of_maps_to {α : Type u_2} {β : Type u_3} [DecidableEq β] {f : αβ} {s : Finset α} {t : Finset β} (Hf : as, f a t) (n : ) (hn : at, n (Finset.filter (fun (x : α) => f x = a) s).card) :
n * t.card s.card
theorem Finset.mul_card_image_le_card {α : Type u_2} {β : Type u_3} [DecidableEq β] {f : αβ} (s : Finset α) (n : ) (hn : aFinset.image f s, n (Finset.filter (fun (x : α) => f x = a) s).card) :
n * (Finset.image f s).card s.card
theorem Finset.sum_card_inter_le {α : Type u_2} [DecidableEq α] {s : Finset α} {B : Finset (Finset α)} {n : } (h : as, (Finset.filter (fun (x : Finset α) => a x) B).card n) :
tB, (s t).card s.card * n

If every element belongs to at most n Finsets, then the sum of their sizes is at most n times how many they are.

theorem Finset.sum_card_le {α : Type u_2} [DecidableEq α] {B : Finset (Finset α)} {n : } [Fintype α] (h : ∀ (a : α), (Finset.filter (fun (x : Finset α) => a x) B).card n) :
sB, s.card Fintype.card α * n

If every element belongs to at most n Finsets, then the sum of their sizes is at most n times how many they are.

theorem Finset.le_sum_card_inter {α : Type u_2} [DecidableEq α] {s : Finset α} {B : Finset (Finset α)} {n : } (h : as, n (Finset.filter (fun (x : Finset α) => a x) B).card) :
s.card * n tB, (s t).card

If every element belongs to at least n Finsets, then the sum of their sizes is at least n times how many they are.

theorem Finset.le_sum_card {α : Type u_2} [DecidableEq α] {B : Finset (Finset α)} {n : } [Fintype α] (h : ∀ (a : α), n (Finset.filter (fun (x : Finset α) => a x) B).card) :
Fintype.card α * n sB, s.card

If every element belongs to at least n Finsets, then the sum of their sizes is at least n times how many they are.

theorem Finset.sum_card_inter {α : Type u_2} [DecidableEq α] {s : Finset α} {B : Finset (Finset α)} {n : } (h : as, (Finset.filter (fun (x : Finset α) => a x) B).card = n) :
tB, (s t).card = s.card * n

If every element belongs to exactly n Finsets, then the sum of their sizes is n times how many they are.

theorem Finset.sum_card {α : Type u_2} [DecidableEq α] {B : Finset (Finset α)} {n : } [Fintype α] (h : ∀ (a : α), (Finset.filter (fun (x : Finset α) => a x) B).card = n) :
sB, s.card = Fintype.card α * n

If every element belongs to exactly n Finsets, then the sum of their sizes is n times how many they are.

theorem Finset.card_le_card_biUnion {ι : Type u_1} {α : Type u_2} [DecidableEq α] {s : Finset ι} {f : ιFinset α} (hs : (↑s).PairwiseDisjoint f) (hf : is, (f i).Nonempty) :
s.card (s.biUnion f).card
theorem Finset.card_le_card_biUnion_add_card_fiber {ι : Type u_1} {α : Type u_2} [DecidableEq α] {s : Finset ι} {f : ιFinset α} (hs : (↑s).PairwiseDisjoint f) :
s.card (s.biUnion f).card + (Finset.filter (fun (i : ι) => f i = ) s).card
theorem Finset.card_le_card_biUnion_add_one {ι : Type u_1} {α : Type u_2} [DecidableEq α] {s : Finset ι} {f : ιFinset α} (hf : Function.Injective f) (hs : (↑s).PairwiseDisjoint f) :
s.card (s.biUnion f).card + 1
theorem CanonicallyOrderedAddCommMonoid.single_le_sum {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedAddCommMonoid M] {f : ιM} {s : Finset ι} {i : ι} (hi : i s) :
f i js, f j

In a canonically-ordered additive monoid, a sum bounds each of its terms.

See also Finset.single_le_sum.

theorem CanonicallyOrderedCommMonoid.single_le_prod {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedCommMonoid M] {f : ιM} {s : Finset ι} {i : ι} (hi : i s) :
f i js, f j

In a canonically-ordered monoid, a product bounds each of its terms.

See also Finset.single_le_prod'.

@[simp]
theorem Finset.sum_eq_zero_iff {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedAddCommMonoid M] {f : ιM} {s : Finset ι} :
xs, f x = 0 xs, f x = 0
@[simp]
theorem Finset.prod_eq_one_iff' {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedCommMonoid M] {f : ιM} {s : Finset ι} :
xs, f x = 1 xs, f x = 1
theorem Finset.sum_le_sum_of_subset {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedAddCommMonoid M] {f : ιM} {s : Finset ι} {t : Finset ι} (h : s t) :
xs, f x xt, f x
theorem Finset.prod_le_prod_of_subset' {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedCommMonoid M] {f : ιM} {s : Finset ι} {t : Finset ι} (h : s t) :
xs, f x xt, f x
theorem Finset.sum_mono_set {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedAddCommMonoid M] (f : ιM) :
Monotone fun (s : Finset ι) => xs, f x
theorem Finset.prod_mono_set' {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedCommMonoid M] (f : ιM) :
Monotone fun (s : Finset ι) => xs, f x
theorem Finset.sum_le_sum_of_ne_zero {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedAddCommMonoid M] {f : ιM} {s : Finset ι} {t : Finset ι} (h : xs, f x 0x t) :
xs, f x xt, f x
theorem Finset.prod_le_prod_of_ne_one' {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedCommMonoid M] {f : ιM} {s : Finset ι} {t : Finset ι} (h : xs, f x 1x t) :
xs, f x xt, f x
theorem Finset.sum_lt_sum {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ιM} {g : ιM} {s : Finset ι} (hle : is, f i g i) (hlt : is, f i < g i) :
is, f i < is, g i
theorem Finset.prod_lt_prod' {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ιM} {g : ιM} {s : Finset ι} (hle : is, f i g i) (hlt : is, f i < g i) :
is, f i < is, g i
theorem Finset.sum_lt_sum_of_nonempty {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ιM} {g : ιM} {s : Finset ι} (hs : s.Nonempty) (hlt : is, f i < g i) :
is, f i < is, g i

In an ordered additive commutative monoid, if each summand f i of one nontrivial finite sum is strictly less than the corresponding summand g i of another nontrivial finite sum, then s.sum f < s.sum g.

theorem Finset.prod_lt_prod_of_nonempty' {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ιM} {g : ιM} {s : Finset ι} (hs : s.Nonempty) (hlt : is, f i < g i) :
is, f i < is, g i

In an ordered commutative monoid, if each factor f i of one nontrivial finite product is strictly less than the corresponding factor g i of another nontrivial finite product, then s.prod f < s.prod g.

theorem Finset.sum_lt_sum_of_subset {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ιM} {s : Finset ι} {t : Finset ι} (h : s t) {i : ι} (ht : i t) (hs : is) (hlt : 0 < f i) (hle : jt, js0 f j) :
js, f j < jt, f j
theorem Finset.prod_lt_prod_of_subset' {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ιM} {s : Finset ι} {t : Finset ι} (h : s t) {i : ι} (ht : i t) (hs : is) (hlt : 1 < f i) (hle : jt, js1 f j) :
js, f j < jt, f j
theorem Finset.single_lt_sum {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ιM} {s : Finset ι} {i : ι} {j : ι} (hij : j i) (hi : i s) (hj : j s) (hlt : 0 < f j) (hle : ks, k i0 f k) :
f i < ks, f k
theorem Finset.single_lt_prod' {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ιM} {s : Finset ι} {i : ι} {j : ι} (hij : j i) (hi : i s) (hj : j s) (hlt : 1 < f j) (hle : ks, k i1 f k) :
f i < ks, f k
theorem Finset.sum_pos {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ιM} {s : Finset ι} (h : is, 0 < f i) (hs : s.Nonempty) :
0 < is, f i
theorem Finset.one_lt_prod {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ιM} {s : Finset ι} (h : is, 1 < f i) (hs : s.Nonempty) :
1 < is, f i
theorem Finset.sum_neg {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ιM} {s : Finset ι} (h : is, f i < 0) (hs : s.Nonempty) :
is, f i < 0
theorem Finset.prod_lt_one {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ιM} {s : Finset ι} (h : is, f i < 1) (hs : s.Nonempty) :
is, f i < 1
theorem Finset.sum_pos' {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ιM} {s : Finset ι} (h : is, 0 f i) (hs : is, 0 < f i) :
0 < is, f i
theorem Finset.one_lt_prod' {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ιM} {s : Finset ι} (h : is, 1 f i) (hs : is, 1 < f i) :
1 < is, f i
theorem Finset.sum_neg' {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ιM} {s : Finset ι} (h : is, f i 0) (hs : is, f i < 0) :
is, f i < 0
theorem Finset.prod_lt_one' {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ιM} {s : Finset ι} (h : is, f i 1) (hs : is, f i < 1) :
is, f i < 1
theorem Finset.sum_eq_sum_iff_of_le {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {s : Finset ι} {f : ιM} {g : ιM} (h : is, f i g i) :
is, f i = is, g i is, f i = g i
theorem Finset.prod_eq_prod_iff_of_le {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {s : Finset ι} {f : ιM} {g : ιM} (h : is, f i g i) :
is, f i = is, g i is, f i = g i
theorem Finset.sum_sdiff_le_sum_sdiff {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ιM} {s : Finset ι} {t : Finset ι} [DecidableEq ι] :
is \ t, f i it \ s, f i is, f i it, f i
theorem Finset.prod_sdiff_le_prod_sdiff {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ιM} {s : Finset ι} {t : Finset ι} [DecidableEq ι] :
is \ t, f i it \ s, f i is, f i it, f i
theorem Finset.sum_sdiff_lt_sum_sdiff {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ιM} {s : Finset ι} {t : Finset ι} [DecidableEq ι] :
is \ t, f i < it \ s, f i is, f i < it, f i
theorem Finset.prod_sdiff_lt_prod_sdiff {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ιM} {s : Finset ι} {t : Finset ι} [DecidableEq ι] :
is \ t, f i < it \ s, f i is, f i < it, f i
theorem Finset.exists_lt_of_sum_lt {ι : Type u_1} {M : Type u_4} [LinearOrderedCancelAddCommMonoid M] {f : ιM} {g : ιM} {s : Finset ι} (Hlt : is, f i < is, g i) :
is, f i < g i
theorem Finset.exists_lt_of_prod_lt' {ι : Type u_1} {M : Type u_4} [LinearOrderedCancelCommMonoid M] {f : ιM} {g : ιM} {s : Finset ι} (Hlt : is, f i < is, g i) :
is, f i < g i
theorem Finset.exists_le_of_sum_le {ι : Type u_1} {M : Type u_4} [LinearOrderedCancelAddCommMonoid M] {f : ιM} {g : ιM} {s : Finset ι} (hs : s.Nonempty) (Hle : is, f i is, g i) :
is, f i g i
theorem Finset.exists_le_of_prod_le' {ι : Type u_1} {M : Type u_4} [LinearOrderedCancelCommMonoid M] {f : ιM} {g : ιM} {s : Finset ι} (hs : s.Nonempty) (Hle : is, f i is, g i) :
is, f i g i
theorem Finset.exists_pos_of_sum_zero_of_exists_nonzero {ι : Type u_1} {M : Type u_4} [LinearOrderedCancelAddCommMonoid M] {s : Finset ι} (f : ιM) (h₁ : is, f i = 0) (h₂ : is, f i 0) :
is, 0 < f i
theorem Finset.exists_one_lt_of_prod_one_of_exists_ne_one' {ι : Type u_1} {M : Type u_4} [LinearOrderedCancelCommMonoid M] {s : Finset ι} (f : ιM) (h₁ : is, f i = 1) (h₂ : is, f i 1) :
is, 1 < f i
theorem Fintype.sum_mono {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedAddCommMonoid M] :
Monotone fun (f : ιM) => i : ι, f i
theorem Fintype.prod_mono' {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCommMonoid M] :
Monotone fun (f : ιM) => i : ι, f i
theorem Fintype.sum_nonneg {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedAddCommMonoid M] {f : ιM} (hf : 0 f) :
0 i : ι, f i
theorem Fintype.one_le_prod {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCommMonoid M] {f : ιM} (hf : 1 f) :
1 i : ι, f i
theorem Fintype.sum_nonpos {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedAddCommMonoid M] {f : ιM} (hf : f 0) :
i : ι, f i 0
theorem Fintype.prod_le_one {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCommMonoid M] {f : ιM} (hf : f 1) :
i : ι, f i 1
theorem Fintype.sum_eq_zero_iff_of_nonneg {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedAddCommMonoid M] {f : ιM} (hf : 0 f) :
i : ι, f i = 0 f = 0
theorem Fintype.prod_eq_one_iff_of_one_le {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCommMonoid M] {f : ιM} (hf : 1 f) :
i : ι, f i = 1 f = 1
theorem Fintype.sum_eq_zero_iff_of_nonpos {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedAddCommMonoid M] {f : ιM} (hf : f 0) :
i : ι, f i = 0 f = 0
theorem Fintype.prod_eq_one_iff_of_le_one {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCommMonoid M] {f : ιM} (hf : f 1) :
i : ι, f i = 1 f = 1
theorem Fintype.sum_strictMono {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelAddCommMonoid M] :
StrictMono fun (f : ιM) => x : ι, f x
theorem Fintype.prod_strictMono' {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelCommMonoid M] :
StrictMono fun (f : ιM) => x : ι, f x
theorem Fintype.sum_pos {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelAddCommMonoid M] {f : ιM} (hf : 0 < f) :
0 < i : ι, f i
theorem Fintype.one_lt_prod {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelCommMonoid M] {f : ιM} (hf : 1 < f) :
1 < i : ι, f i
theorem Fintype.sum_neg {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelAddCommMonoid M] {f : ιM} (hf : f < 0) :
i : ι, f i < 0
theorem Fintype.prod_lt_one {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelCommMonoid M] {f : ιM} (hf : f < 1) :
i : ι, f i < 1
theorem Fintype.sum_pos_iff_of_nonneg {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelAddCommMonoid M] {f : ιM} (hf : 0 f) :
0 < i : ι, f i 0 < f
theorem Fintype.one_lt_prod_iff_of_one_le {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelCommMonoid M] {f : ιM} (hf : 1 f) :
1 < i : ι, f i 1 < f
theorem Fintype.sum_neg_iff_of_nonpos {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelAddCommMonoid M] {f : ιM} (hf : f 0) :
i : ι, f i < 0 f < 0
theorem Fintype.prod_lt_one_iff_of_le_one {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelCommMonoid M] {f : ιM} (hf : f 1) :
i : ι, f i < 1 f < 1
theorem Multiset.finset_sum_eq_sup_iff_disjoint {α : Type u_2} [DecidableEq α] {β : Type u_9} {i : Finset β} {f : βMultiset α} :
i.sum f = i.sup f xi, yi, x y(f x).Disjoint (f y)
theorem Multiset.sup_powerset_len {α : Type u_9} [DecidableEq α] (x : Multiset α) :
((Finset.range (Multiset.card x + 1)).sup fun (k : ) => Multiset.powersetCard k x) = x.powerset

The positivity extension which proves that ∑ i ∈ s, f i is nonnegative if f is, and positive if each f i is and s is nonempty.

TODO: The following example does not work

example (s : Finset ℕ) (f : ℕ → ℤ) (hf : ∀ n, 0 ≤ f n) : 0 ≤ s.sum f := by positivity

because compareHyp can't look for assumptions behind binders.

Instances For