# Results about big operators with values in an ordered algebraic structure. #

Mostly monotonicity results for the ∏ and ∑ operations.

theorem Finset.le_sum_nonempty_of_subadditive_on_pred {ι : Type u_1} {M : Type u_4} {N : Type u_5} [] (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 : ) (hs_nonempty : s.Nonempty) (hs : is, p (g i)) :
f (Finset.sum s fun (i : ι) => g i) Finset.sum s fun (i : ι) => 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 in s, g i) ≤ ∑ i in s, f (g i).

theorem Finset.le_prod_nonempty_of_submultiplicative_on_pred {ι : Type u_1} {M : Type u_4} {N : Type u_5} [] (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 : ) (hs_nonempty : s.Nonempty) (hs : is, p (g i)) :
f (Finset.prod s fun (i : ι) => g i) Finset.prod s fun (i : ι) => 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 in s, g x) ≤ ∏ x in s, f (g x).

theorem Finset.le_sum_nonempty_of_subadditive {ι : Type u_1} {M : Type u_4} {N : Type u_5} [] (f : MN) (h_mul : ∀ (x y : M), f (x + y) f x + f y) {s : } (hs : s.Nonempty) (g : ιM) :
f (Finset.sum s fun (i : ι) => g i) Finset.sum s fun (i : ι) => 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 in s, g i) ≤ ∑ i in s, f (g i).

theorem Finset.le_prod_nonempty_of_submultiplicative {ι : Type u_1} {M : Type u_4} {N : Type u_5} [] (f : MN) (h_mul : ∀ (x y : M), f (x * y) f x * f y) {s : } (hs : s.Nonempty) (g : ιM) :
f (Finset.prod s fun (i : ι) => g i) Finset.prod s fun (i : ι) => 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 in s, g i) ≤ ∏ i in s, f (g i).

theorem Finset.le_sum_of_subadditive_on_pred {ι : Type u_1} {M : Type u_4} {N : Type u_5} [] (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 : } (hs : is, p (g i)) :
f (Finset.sum s fun (i : ι) => g i) Finset.sum s fun (i : ι) => 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 in s, g x) ≤ ∑ x in s, f (g x).

theorem Finset.le_prod_of_submultiplicative_on_pred {ι : Type u_1} {M : Type u_4} {N : Type u_5} [] (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 : } (hs : is, p (g i)) :
f (Finset.prod s fun (i : ι) => g i) Finset.prod s fun (i : ι) => 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 in s, g i) ≤ ∏ i in s, f (g i).

theorem Finset.le_sum_of_subadditive {ι : Type u_1} {M : Type u_4} {N : Type u_5} [] (f : MN) (h_one : f 0 = 0) (h_mul : ∀ (x y : M), f (x + y) f x + f y) (s : ) (g : ιM) :
f (Finset.sum s fun (i : ι) => g i) Finset.sum s fun (i : ι) => 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 in s, g i) ≤ ∑ i in s, f (g i).

theorem Finset.le_prod_of_submultiplicative {ι : Type u_1} {M : Type u_4} {N : Type u_5} [] (f : MN) (h_one : f 1 = 1) (h_mul : ∀ (x y : M), f (x * y) f x * f y) (s : ) (g : ιM) :
f (Finset.prod s fun (i : ι) => g i) Finset.prod s fun (i : ι) => 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 in s, g i) ≤ ∏ i in s, f (g i).

theorem Finset.sum_le_sum {ι : Type u_1} {N : Type u_5} {f : ιN} {g : ιN} {s : } (h : is, f i g i) :
(Finset.sum s fun (i : ι) => f i) Finset.sum s fun (i : ι) => 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 in s, f i ≤ ∑ i in s, g i.

theorem Finset.prod_le_prod' {ι : Type u_1} {N : Type u_5} {f : ιN} {g : ιN} {s : } (h : is, f i g i) :
(Finset.prod s fun (i : ι) => f i) Finset.prod s fun (i : ι) => 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 in s, f i ≤ ∏ i in s, g i.

theorem GCongr.sum_le_sum {ι : Type u_1} {N : Type u_5} {f : ιN} {g : ιN} {s : } (h : is, f i 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 s.sum f ≤ s.sum g.

This is a variant (beta-reduced) version of the standard lemma Finset.sum_le_sum, convenient for the gcongr tactic.

theorem GCongr.prod_le_prod' {ι : Type u_1} {N : Type u_5} {f : ιN} {g : ιN} {s : } (h : is, f i 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 s.prod f ≤ s.prod g.

This is a variant (beta-reduced) version of the standard lemma Finset.prod_le_prod', convenient for the gcongr tactic.

theorem Finset.sum_nonneg {ι : Type u_1} {N : Type u_5} {f : ιN} {s : } (h : is, 0 f i) :
0 Finset.sum s fun (i : ι) => f i
theorem Finset.one_le_prod' {ι : Type u_1} {N : Type u_5} {f : ιN} {s : } (h : is, 1 f i) :
1 Finset.prod s fun (i : ι) => f i
theorem Finset.sum_nonneg' {ι : Type u_1} {N : Type u_5} {f : ιN} {s : } (h : ∀ (i : ι), 0 f i) :
0 Finset.sum s fun (i : ι) => f i
theorem Finset.one_le_prod'' {ι : Type u_1} {N : Type u_5} {f : ιN} {s : } (h : ∀ (i : ι), 1 f i) :
1 Finset.prod s fun (i : ι) => f i
theorem Finset.sum_nonpos {ι : Type u_1} {N : Type u_5} {f : ιN} {s : } (h : is, f i 0) :
(Finset.sum s fun (i : ι) => f i) 0
theorem Finset.prod_le_one' {ι : Type u_1} {N : Type u_5} {f : ιN} {s : } (h : is, f i 1) :
(Finset.prod s fun (i : ι) => f i) 1
theorem Finset.sum_le_sum_of_subset_of_nonneg {ι : Type u_1} {N : Type u_5} {f : ιN} {s : } {t : } (h : s t) (hf : it, is0 f i) :
(Finset.sum s fun (i : ι) => f i) Finset.sum t fun (i : ι) => f i
theorem Finset.prod_le_prod_of_subset_of_one_le' {ι : Type u_1} {N : Type u_5} {f : ιN} {s : } {t : } (h : s t) (hf : it, is1 f i) :
(Finset.prod s fun (i : ι) => f i) Finset.prod t fun (i : ι) => f i
theorem Finset.sum_mono_set_of_nonneg {ι : Type u_1} {N : Type u_5} {f : ιN} (hf : ∀ (x : ι), 0 f x) :
Monotone fun (s : ) => Finset.sum s fun (x : ι) => f x
theorem Finset.prod_mono_set_of_one_le' {ι : Type u_1} {N : Type u_5} {f : ιN} (hf : ∀ (x : ι), 1 f x) :
Monotone fun (s : ) => Finset.prod s fun (x : ι) => f x
theorem Finset.sum_le_univ_sum_of_nonneg {ι : Type u_1} {N : Type u_5} {f : ιN} [] {s : } (w : ∀ (x : ι), 0 f x) :
(Finset.sum s fun (x : ι) => f x) Finset.sum Finset.univ fun (x : ι) => f x
theorem Finset.prod_le_univ_prod_of_one_le' {ι : Type u_1} {N : Type u_5} {f : ιN} [] {s : } (w : ∀ (x : ι), 1 f x) :
(Finset.prod s fun (x : ι) => f x) Finset.prod Finset.univ fun (x : ι) => f x
theorem Finset.sum_eq_zero_iff_of_nonneg {ι : Type u_1} {N : Type u_5} {f : ιN} {s : } :
(is, 0 f i)((Finset.sum s fun (i : ι) => f i) = 0 is, f i = 0)
theorem Finset.prod_eq_one_iff_of_one_le' {ι : Type u_1} {N : Type u_5} {f : ιN} {s : } :
(is, 1 f i)((Finset.prod s fun (i : ι) => f i) = 1 is, f i = 1)
theorem Finset.sum_eq_zero_iff_of_nonpos {ι : Type u_1} {N : Type u_5} {f : ιN} {s : } :
(is, f i 0)((Finset.sum s fun (i : ι) => f i) = 0 is, f i = 0)
theorem Finset.prod_eq_one_iff_of_le_one' {ι : Type u_1} {N : Type u_5} {f : ιN} {s : } :
(is, f i 1)((Finset.prod s fun (i : ι) => f i) = 1 is, f i = 1)
theorem Finset.single_le_sum {ι : Type u_1} {N : Type u_5} {f : ιN} {s : } (hf : is, 0 f i) {a : ι} (h : a s) :
f a Finset.sum s fun (x : ι) => f x
theorem Finset.single_le_prod' {ι : Type u_1} {N : Type u_5} {f : ιN} {s : } (hf : is, 1 f i) {a : ι} (h : a s) :
f a Finset.prod s fun (x : ι) => f x
theorem Finset.add_le_sum {ι : Type u_1} {N : Type u_5} {f : ιN} {s : } {i : ι} {j : ι} (hf : is, 0 f i) (hi : i s) (hj : j s) (hne : i j) :
f i + f j Finset.sum s fun (k : ι) => f k
theorem Finset.mul_le_prod {ι : Type u_1} {N : Type u_5} {f : ιN} {s : } {i : ι} {j : ι} (hf : is, 1 f i) (hi : i s) (hj : j s) (hne : i j) :
f i * f j Finset.prod s fun (k : ι) => f k
theorem Finset.sum_le_card_nsmul {ι : Type u_1} {N : Type u_5} (s : ) (f : ιN) (n : N) (h : xs, f x n) :
s.card n
theorem Finset.prod_le_pow_card {ι : Type u_1} {N : Type u_5} (s : ) (f : ιN) (n : N) (h : xs, f x n) :
n ^ s.card
theorem Finset.card_nsmul_le_sum {ι : Type u_1} {N : Type u_5} (s : ) (f : ιN) (n : N) (h : xs, n f x) :
s.card n
theorem Finset.pow_card_le_prod {ι : Type u_1} {N : Type u_5} (s : ) (f : ιN) (n : N) (h : xs, n f x) :
n ^ s.card
theorem Finset.card_biUnion_le_card_mul {ι : Type u_1} {β : Type u_3} [] (s : ) (f : ι) (n : ) (h : as, (f a).card n) :
().card s.card * n
theorem Finset.sum_fiberwise_le_sum_of_sum_fiber_nonneg {ι : Type u_1} {N : Type u_5} {s : } {ι' : Type u_9} [] {t : Finset ι'} {g : ιι'} {f : ιN} (h : yt, 0 Finset.sum (Finset.filter (fun (x : ι) => g x = y) s) fun (x : ι) => f x) :
(Finset.sum t fun (y : ι') => Finset.sum (Finset.filter (fun (x : ι) => g x = y) s) fun (x : ι) => f x) Finset.sum s fun (x : ι) => f x
theorem Finset.prod_fiberwise_le_prod_of_one_le_prod_fiber' {ι : Type u_1} {N : Type u_5} {s : } {ι' : Type u_9} [] {t : Finset ι'} {g : ιι'} {f : ιN} (h : yt, 1 Finset.prod (Finset.filter (fun (x : ι) => g x = y) s) fun (x : ι) => f x) :
(Finset.prod t fun (y : ι') => Finset.prod (Finset.filter (fun (x : ι) => g x = y) s) fun (x : ι) => f x) Finset.prod s fun (x : ι) => f x
theorem Finset.sum_le_sum_fiberwise_of_sum_fiber_nonpos {ι : Type u_1} {N : Type u_5} {s : } {ι' : Type u_9} [] {t : Finset ι'} {g : ιι'} {f : ιN} (h : yt, (Finset.sum (Finset.filter (fun (x : ι) => g x = y) s) fun (x : ι) => f x) 0) :
(Finset.sum s fun (x : ι) => f x) Finset.sum t fun (y : ι') => Finset.sum (Finset.filter (fun (x : ι) => g x = y) s) fun (x : ι) => f x
theorem Finset.prod_le_prod_fiberwise_of_prod_fiber_le_one' {ι : Type u_1} {N : Type u_5} {s : } {ι' : Type u_9} [] {t : Finset ι'} {g : ιι'} {f : ιN} (h : yt, (Finset.prod (Finset.filter (fun (x : ι) => g x = y) s) fun (x : ι) => f x) 1) :
(Finset.prod s fun (x : ι) => f x) Finset.prod t fun (y : ι') => Finset.prod (Finset.filter (fun (x : ι) => g x = y) s) fun (x : ι) => f x
theorem Finset.abs_sum_le_sum_abs {ι : Type u_1} {G : Type u_9} (f : ιG) (s : ) :
|Finset.sum s fun (i : ι) => f i| Finset.sum s fun (i : ι) => |f i|
theorem Finset.abs_sum_of_nonneg {ι : Type u_1} {G : Type u_9} {f : ιG} {s : } (hf : is, 0 f i) :
|Finset.sum s fun (i : ι) => f i| = Finset.sum s fun (i : ι) => f i
theorem Finset.abs_sum_of_nonneg' {ι : Type u_1} {G : Type u_9} {f : ιG} {s : } (hf : ∀ (i : ι), 0 f i) :
|Finset.sum s fun (i : ι) => f i| = Finset.sum s fun (i : ι) => f i
theorem Finset.abs_prod {ι : Type u_1} {R : Type u_9} {f : ιR} {s : } :
|Finset.prod s fun (x : ι) => f x| = Finset.prod s fun (x : ι) => |f x|
theorem Finset.card_le_mul_card_image_of_maps_to {α : Type u_2} {β : Type u_3} [] {f : αβ} {s : } {t : } (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} [] {f : αβ} (s : ) (n : ) (hn : a, (Finset.filter (fun (x : α) => f x = a) s).card n) :
s.card n * ().card
theorem Finset.mul_card_image_le_card_of_maps_to {α : Type u_2} {β : Type u_3} [] {f : αβ} {s : } {t : } (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} [] {f : αβ} (s : ) (n : ) (hn : a, n (Finset.filter (fun (x : α) => f x = a) s).card) :
n * ().card s.card
theorem Finset.sum_card_inter_le {α : Type u_2} [] {s : } {B : Finset ()} {n : } (h : as, (Finset.filter (fun (x : ) => a x) B).card n) :
(Finset.sum B fun (t : ) => (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} [] {B : Finset ()} {n : } [] (h : ∀ (a : α), (Finset.filter (fun (x : ) => a x) B).card n) :
(Finset.sum B fun (s : ) => s.card)

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} [] {s : } {B : Finset ()} {n : } (h : as, n (Finset.filter (fun (x : ) => a x) B).card) :
s.card * n Finset.sum B fun (t : ) => (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} [] {B : Finset ()} {n : } [] (h : ∀ (a : α), n (Finset.filter (fun (x : ) => a x) B).card) :
Finset.sum B fun (s : ) => 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} [] {s : } {B : Finset ()} {n : } (h : as, (Finset.filter (fun (x : ) => a x) B).card = n) :
(Finset.sum B fun (t : ) => (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} [] {B : Finset ()} {n : } [] (h : ∀ (a : α), (Finset.filter (fun (x : ) => a x) B).card = n) :
(Finset.sum B fun (s : ) => s.card) =

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} [] {s : } {f : ι} (hs : Set.PairwiseDisjoint (s) f) (hf : is, (f i).Nonempty) :
s.card ().card
theorem Finset.card_le_card_biUnion_add_card_fiber {ι : Type u_1} {α : Type u_2} [] {s : } {f : ι} (hs : Set.PairwiseDisjoint (s) f) :
s.card ().card + (Finset.filter (fun (i : ι) => f i = ) s).card
theorem Finset.card_le_card_biUnion_add_one {ι : Type u_1} {α : Type u_2} [] {s : } {f : ι} (hf : ) (hs : Set.PairwiseDisjoint (s) f) :
s.card ().card + 1
@[simp]
theorem Finset.sum_eq_zero_iff {ι : Type u_1} {M : Type u_4} {f : ιM} {s : } :
(Finset.sum s fun (x : ι) => f x) = 0 xs, f x = 0
@[simp]
theorem Finset.prod_eq_one_iff' {ι : Type u_1} {M : Type u_4} {f : ιM} {s : } :
(Finset.prod s fun (x : ι) => f x) = 1 xs, f x = 1
theorem Finset.sum_le_sum_of_subset {ι : Type u_1} {M : Type u_4} {f : ιM} {s : } {t : } (h : s t) :
(Finset.sum s fun (x : ι) => f x) Finset.sum t fun (x : ι) => f x
theorem Finset.prod_le_prod_of_subset' {ι : Type u_1} {M : Type u_4} {f : ιM} {s : } {t : } (h : s t) :
(Finset.prod s fun (x : ι) => f x) Finset.prod t fun (x : ι) => f x
theorem Finset.sum_mono_set {ι : Type u_1} {M : Type u_4} (f : ιM) :
Monotone fun (s : ) => Finset.sum s fun (x : ι) => f x
theorem Finset.prod_mono_set' {ι : Type u_1} {M : Type u_4} (f : ιM) :
Monotone fun (s : ) => Finset.prod s fun (x : ι) => f x
theorem Finset.sum_le_sum_of_ne_zero {ι : Type u_1} {M : Type u_4} {f : ιM} {s : } {t : } (h : xs, f x 0x t) :
(Finset.sum s fun (x : ι) => f x) Finset.sum t fun (x : ι) => f x
theorem Finset.prod_le_prod_of_ne_one' {ι : Type u_1} {M : Type u_4} {f : ιM} {s : } {t : } (h : xs, f x 1x t) :
(Finset.prod s fun (x : ι) => f x) Finset.prod t fun (x : ι) => f x
theorem Finset.sum_lt_sum {ι : Type u_1} {M : Type u_4} {f : ιM} {g : ιM} {s : } (hle : is, f i g i) (hlt : ∃ i ∈ s, f i < g i) :
(Finset.sum s fun (i : ι) => f i) < Finset.sum s fun (i : ι) => g i
theorem Finset.prod_lt_prod' {ι : Type u_1} {M : Type u_4} {f : ιM} {g : ιM} {s : } (hle : is, f i g i) (hlt : ∃ i ∈ s, f i < g i) :
(Finset.prod s fun (i : ι) => f i) < Finset.prod s fun (i : ι) => g i
theorem Finset.sum_lt_sum_of_nonempty {ι : Type u_1} {M : Type u_4} {f : ιM} {g : ιM} {s : } (hs : s.Nonempty) (hlt : is, f i < g i) :
(Finset.sum s fun (i : ι) => f i) < Finset.sum s fun (i : ι) => g i
theorem Finset.prod_lt_prod_of_nonempty' {ι : Type u_1} {M : Type u_4} {f : ιM} {g : ιM} {s : } (hs : s.Nonempty) (hlt : is, f i < g i) :
(Finset.prod s fun (i : ι) => f i) < Finset.prod s fun (i : ι) => g i
theorem GCongr.sum_lt_sum_of_nonempty {ι : Type u_1} {M : Type u_4} {f : ιM} {g : ιM} {s : } (hs : s.Nonempty) (Hlt : is, f i < 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.

This is a variant (beta-reduced) version of the standard lemma Finset.sum_lt_sum_of_nonempty, convenient for the gcongr tactic.

theorem GCongr.prod_lt_prod_of_nonempty' {ι : Type u_1} {M : Type u_4} {f : ιM} {g : ιM} {s : } (hs : s.Nonempty) (Hlt : is, f i < 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.

This is a variant (beta-reduced) version of the standard lemma Finset.prod_lt_prod_of_nonempty', convenient for the gcongr tactic.

theorem Finset.sum_lt_sum_of_subset {ι : Type u_1} {M : Type u_4} {f : ιM} {s : } {t : } (h : s t) {i : ι} (ht : i t) (hs : is) (hlt : 0 < f i) (hle : jt, js0 f j) :
(Finset.sum s fun (j : ι) => f j) < Finset.sum t fun (j : ι) => f j
theorem Finset.prod_lt_prod_of_subset' {ι : Type u_1} {M : Type u_4} {f : ιM} {s : } {t : } (h : s t) {i : ι} (ht : i t) (hs : is) (hlt : 1 < f i) (hle : jt, js1 f j) :
(Finset.prod s fun (j : ι) => f j) < Finset.prod t fun (j : ι) => f j
theorem Finset.single_lt_sum {ι : Type u_1} {M : Type u_4} {f : ιM} {s : } {i : ι} {j : ι} (hij : j i) (hi : i s) (hj : j s) (hlt : 0 < f j) (hle : ks, k i0 f k) :
f i < Finset.sum s fun (k : ι) => f k
theorem Finset.single_lt_prod' {ι : Type u_1} {M : Type u_4} {f : ιM} {s : } {i : ι} {j : ι} (hij : j i) (hi : i s) (hj : j s) (hlt : 1 < f j) (hle : ks, k i1 f k) :
f i < Finset.prod s fun (k : ι) => f k
theorem Finset.sum_pos {ι : Type u_1} {M : Type u_4} {f : ιM} {s : } (h : is, 0 < f i) (hs : s.Nonempty) :
0 < Finset.sum s fun (i : ι) => f i
theorem Finset.one_lt_prod {ι : Type u_1} {M : Type u_4} {f : ιM} {s : } (h : is, 1 < f i) (hs : s.Nonempty) :
1 < Finset.prod s fun (i : ι) => f i
theorem Finset.sum_neg {ι : Type u_1} {M : Type u_4} {f : ιM} {s : } (h : is, f i < 0) (hs : s.Nonempty) :
(Finset.sum s fun (i : ι) => f i) < 0
theorem Finset.prod_lt_one {ι : Type u_1} {M : Type u_4} {f : ιM} {s : } (h : is, f i < 1) (hs : s.Nonempty) :
(Finset.prod s fun (i : ι) => f i) < 1
theorem Finset.sum_pos' {ι : Type u_1} {M : Type u_4} {f : ιM} {s : } (h : is, 0 f i) (hs : ∃ i ∈ s, 0 < f i) :
0 < Finset.sum s fun (i : ι) => f i
theorem Finset.one_lt_prod' {ι : Type u_1} {M : Type u_4} {f : ιM} {s : } (h : is, 1 f i) (hs : ∃ i ∈ s, 1 < f i) :
1 < Finset.prod s fun (i : ι) => f i
theorem Finset.sum_neg' {ι : Type u_1} {M : Type u_4} {f : ιM} {s : } (h : is, f i 0) (hs : ∃ i ∈ s, f i < 0) :
(Finset.sum s fun (i : ι) => f i) < 0
theorem Finset.prod_lt_one' {ι : Type u_1} {M : Type u_4} {f : ιM} {s : } (h : is, f i 1) (hs : ∃ i ∈ s, f i < 1) :
(Finset.prod s fun (i : ι) => f i) < 1
theorem Finset.sum_eq_sum_iff_of_le {ι : Type u_1} {M : Type u_4} {s : } {f : ιM} {g : ιM} (h : is, f i g i) :
((Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => g i) is, f i = g i
theorem Finset.prod_eq_prod_iff_of_le {ι : Type u_1} {M : Type u_4} {s : } {f : ιM} {g : ιM} (h : is, f i g i) :
((Finset.prod s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => g i) is, f i = g i
theorem Finset.sum_sdiff_le_sum_sdiff {ι : Type u_1} {M : Type u_4} {f : ιM} {s : } {t : } [] :
((Finset.sum (s \ t) fun (i : ι) => f i) Finset.sum (t \ s) fun (i : ι) => f i) (Finset.sum s fun (i : ι) => f i) Finset.sum t fun (i : ι) => f i
theorem Finset.prod_sdiff_le_prod_sdiff {ι : Type u_1} {M : Type u_4} {f : ιM} {s : } {t : } [] :
((Finset.prod (s \ t) fun (i : ι) => f i) Finset.prod (t \ s) fun (i : ι) => f i) (Finset.prod s fun (i : ι) => f i) Finset.prod t fun (i : ι) => f i
theorem Finset.sum_sdiff_lt_sum_sdiff {ι : Type u_1} {M : Type u_4} {f : ιM} {s : } {t : } [] :
((Finset.sum (s \ t) fun (i : ι) => f i) < Finset.sum (t \ s) fun (i : ι) => f i) (Finset.sum s fun (i : ι) => f i) < Finset.sum t fun (i : ι) => f i
theorem Finset.prod_sdiff_lt_prod_sdiff {ι : Type u_1} {M : Type u_4} {f : ιM} {s : } {t : } [] :
((Finset.prod (s \ t) fun (i : ι) => f i) < Finset.prod (t \ s) fun (i : ι) => f i) (Finset.prod s fun (i : ι) => f i) < Finset.prod t fun (i : ι) => f i
theorem Finset.exists_lt_of_sum_lt {ι : Type u_1} {M : Type u_4} {f : ιM} {g : ιM} {s : } (Hlt : (Finset.sum s fun (i : ι) => f i) < Finset.sum s fun (i : ι) => g i) :
∃ i ∈ s, f i < g i
theorem Finset.exists_lt_of_prod_lt' {ι : Type u_1} {M : Type u_4} {f : ιM} {g : ιM} {s : } (Hlt : (Finset.prod s fun (i : ι) => f i) < Finset.prod s fun (i : ι) => g i) :
∃ i ∈ s, f i < g i
theorem Finset.exists_le_of_sum_le {ι : Type u_1} {M : Type u_4} {f : ιM} {g : ιM} {s : } (hs : s.Nonempty) (Hle : (Finset.sum s fun (i : ι) => f i) Finset.sum s fun (i : ι) => g i) :
∃ i ∈ s, f i g i
theorem Finset.exists_le_of_prod_le' {ι : Type u_1} {M : Type u_4} {f : ιM} {g : ιM} {s : } (hs : s.Nonempty) (Hle : (Finset.prod s fun (i : ι) => f i) Finset.prod s fun (i : ι) => g i) :
∃ i ∈ s, f i g i
theorem Finset.exists_pos_of_sum_zero_of_exists_nonzero {ι : Type u_1} {M : Type u_4} {s : } (f : ιM) (h₁ : (Finset.sum s fun (i : ι) => f i) = 0) (h₂ : ∃ i ∈ s, f i 0) :
∃ i ∈ s, 0 < f i
theorem Finset.exists_one_lt_of_prod_one_of_exists_ne_one' {ι : Type u_1} {M : Type u_4} {s : } (f : ιM) (h₁ : (Finset.prod s fun (i : ι) => f i) = 1) (h₂ : ∃ i ∈ s, f i 1) :
∃ i ∈ s, 1 < f i
theorem Finset.prod_nonneg {ι : Type u_1} {R : Type u_8} {f : ιR} {s : } (h0 : is, 0 f i) :
0 Finset.prod s fun (i : ι) => f i
theorem Finset.prod_le_prod {ι : Type u_1} {R : Type u_8} {f : ιR} {g : ιR} {s : } (h0 : is, 0 f i) (h1 : is, f i g i) :
(Finset.prod s fun (i : ι) => f i) Finset.prod s fun (i : ι) => g i

If all f i, i ∈ s, are nonnegative and each f i is less than or equal to g i, then the product of f i is less than or equal to the product of g i. See also Finset.prod_le_prod' for the case of an ordered commutative multiplicative monoid.

theorem GCongr.prod_le_prod {ι : Type u_1} {R : Type u_8} {f : ιR} {g : ιR} {s : } (h0 : is, 0 f i) (h1 : is, f i g i) :

If all f i, i ∈ s, are nonnegative and each f i is less than or equal to g i, then the product of f i is less than or equal to the product of g i.

This is a variant (beta-reduced) version of the standard lemma Finset.prod_le_prod, convenient for the gcongr tactic.

theorem Finset.prod_le_one {ι : Type u_1} {R : Type u_8} {f : ιR} {s : } (h0 : is, 0 f i) (h1 : is, f i 1) :
(Finset.prod s fun (i : ι) => f i) 1

If each f i, i ∈ s belongs to [0, 1], then their product is less than or equal to one. See also Finset.prod_le_one' for the case of an ordered commutative multiplicative monoid.

theorem Finset.prod_add_prod_le {ι : Type u_1} {R : Type u_8} {s : } {i : ι} {f : ιR} {g : ιR} {h : ιR} (hi : i s) (h2i : g i + h i f i) (hgf : js, j ig j f j) (hhf : js, j ih j f j) (hg : is, 0 g i) (hh : is, 0 h i) :
((Finset.prod s fun (i : ι) => g i) + Finset.prod s fun (i : ι) => h i) Finset.prod s fun (i : ι) => f i

If g, h ≤ f and g i + h i ≤ f i, then the product of f over s is at least the sum of the products of g and h. This is the version for OrderedCommSemiring.

theorem Finset.prod_pos {ι : Type u_1} {R : Type u_8} {f : ιR} {s : } (h0 : is, 0 < f i) :
0 < Finset.prod s fun (i : ι) => f i
theorem Finset.prod_lt_prod {ι : Type u_1} {R : Type u_8} {f : ιR} {g : ιR} {s : } (hf : is, 0 < f i) (hfg : is, f i g i) (hlt : ∃ i ∈ s, f i < g i) :
(Finset.prod s fun (i : ι) => f i) < Finset.prod s fun (i : ι) => g i
theorem Finset.prod_lt_prod_of_nonempty {ι : Type u_1} {R : Type u_8} {f : ιR} {g : ιR} {s : } (hf : is, 0 < f i) (hfg : is, f i < g i) (h_ne : s.Nonempty) :
(Finset.prod s fun (i : ι) => f i) < Finset.prod s fun (i : ι) => g i
theorem Finset.sum_mul_sq_le_sq_mul_sq {ι : Type u_1} {α : Type u_2} [] (s : ) (f : ια) (g : ια) :
(Finset.sum s fun (i : ι) => f i * g i) ^ 2 (Finset.sum s fun (i : ι) => f i ^ 2) * Finset.sum s fun (i : ι) => g i ^ 2

Cauchy-Schwarz inequality for finsets.

@[simp]
theorem CanonicallyOrderedCommSemiring.prod_pos {ι : Type u_1} {R : Type u_8} {f : ιR} {s : } [] :
(0 < Finset.prod s fun (i : ι) => f i) is, 0 < f i

Note that the name is to match CanonicallyOrderedCommSemiring.mul_pos.

theorem Finset.prod_add_prod_le' {ι : Type u_1} {R : Type u_8} {f : ιR} {g : ιR} {h : ιR} {s : } {i : ι} (hi : i s) (h2i : g i + h i f i) (hgf : js, j ig j f j) (hhf : js, j ih j f j) :
((Finset.prod s fun (i : ι) => g i) + Finset.prod s fun (i : ι) => h i) Finset.prod s fun (i : ι) => f i

If g, h ≤ f and g i + h i ≤ f i, then the product of f over s is at least the sum of the products of g and h. This is the version for CanonicallyOrderedCommSemiring.

theorem Fintype.sum_mono {ι : Type u_1} {M : Type u_4} [] :
Monotone fun (f : ιM) => Finset.sum Finset.univ fun (i : ι) => f i
theorem Fintype.prod_mono' {ι : Type u_1} {M : Type u_4} [] :
Monotone fun (f : ιM) => Finset.prod Finset.univ fun (i : ι) => f i
theorem Fintype.sum_nonneg {ι : Type u_1} {M : Type u_4} [] {f : ιM} (hf : 0 f) :
0 Finset.sum Finset.univ fun (i : ι) => f i
theorem Fintype.one_le_prod {ι : Type u_1} {M : Type u_4} [] {f : ιM} (hf : 1 f) :
1 Finset.prod Finset.univ fun (i : ι) => f i
theorem Fintype.sum_nonpos {ι : Type u_1} {M : Type u_4} [] {f : ιM} (hf : f 0) :
(Finset.sum Finset.univ fun (i : ι) => f i) 0
theorem Fintype.prod_le_one {ι : Type u_1} {M : Type u_4} [] {f : ιM} (hf : f 1) :
(Finset.prod Finset.univ fun (i : ι) => f i) 1
theorem Fintype.sum_eq_zero_iff_of_nonneg {ι : Type u_1} {M : Type u_4} [] {f : ιM} (hf : 0 f) :
(Finset.sum Finset.univ fun (i : ι) => f i) = 0 f = 0
theorem Fintype.prod_eq_one_iff_of_one_le {ι : Type u_1} {M : Type u_4} [] {f : ιM} (hf : 1 f) :
(Finset.prod Finset.univ fun (i : ι) => f i) = 1 f = 1
theorem Fintype.sum_eq_zero_iff_of_nonpos {ι : Type u_1} {M : Type u_4} [] {f : ιM} (hf : f 0) :
(Finset.sum Finset.univ fun (i : ι) => f i) = 0 f = 0
theorem Fintype.prod_eq_one_iff_of_le_one {ι : Type u_1} {M : Type u_4} [] {f : ιM} (hf : f 1) :
(Finset.prod Finset.univ fun (i : ι) => f i) = 1 f = 1
abbrev Fintype.sum_strictMono.match_1 {ι : Type u_1} {M : Type u_2} :
∀ (x x_1 : ιM) (motive : (x x_1 ∃ (i : ι), x i < x_1 i)Prop) (x_2 : x x_1 ∃ (i : ι), x i < x_1 i), (∀ (hle : x x_1) (i : ι) (hlt : x i < x_1 i), motive (_ : x x_1 ∃ (i : ι), x i < x_1 i))motive x_2
Equations
• (_ : motive x) = (_ : motive x)
Instances For
theorem Fintype.sum_strictMono {ι : Type u_1} {M : Type u_4} [] :
StrictMono fun (f : ιM) => Finset.sum Finset.univ fun (x : ι) => f x
theorem Fintype.prod_strictMono' {ι : Type u_1} {M : Type u_4} [] :
StrictMono fun (f : ιM) => Finset.prod Finset.univ fun (x : ι) => f x
theorem Fintype.sum_pos {ι : Type u_1} {M : Type u_4} [] {f : ιM} (hf : 0 < f) :
0 < Finset.sum Finset.univ fun (i : ι) => f i
theorem Fintype.one_lt_prod {ι : Type u_1} {M : Type u_4} [] {f : ιM} (hf : 1 < f) :
1 < Finset.prod Finset.univ fun (i : ι) => f i
theorem Fintype.sum_neg {ι : Type u_1} {M : Type u_4} [] {f : ιM} (hf : f < 0) :
(Finset.sum Finset.univ fun (i : ι) => f i) < 0
theorem Fintype.prod_lt_one {ι : Type u_1} {M : Type u_4} [] {f : ιM} (hf : f < 1) :
(Finset.prod Finset.univ fun (i : ι) => f i) < 1
theorem Fintype.sum_pos_iff_of_nonneg {ι : Type u_1} {M : Type u_4} [] {f : ιM} (hf : 0 f) :
(0 < Finset.sum Finset.univ fun (i : ι) => f i) 0 < f
theorem Fintype.one_lt_prod_iff_of_one_le {ι : Type u_1} {M : Type u_4} [] {f : ιM} (hf : 1 f) :
(1 < Finset.prod Finset.univ fun (i : ι) => f i) 1 < f
theorem Fintype.sum_neg_iff_of_nonpos {ι : Type u_1} {M : Type u_4} [] {f : ιM} (hf : f 0) :
(Finset.sum Finset.univ fun (i : ι) => f i) < 0 f < 0
theorem Fintype.prod_lt_one_iff_of_le_one {ι : Type u_1} {M : Type u_4} [] {f : ιM} (hf : f 1) :
(Finset.prod Finset.univ fun (i : ι) => f i) < 1 f < 1
theorem AbsoluteValue.sum_le {ι : Type u_1} {R : Type u_8} {S : Type u_9} [] [] (abv : ) (s : ) (f : ιR) :
abv (Finset.sum s fun (i : ι) => f i) Finset.sum s fun (i : ι) => abv (f i)
theorem IsAbsoluteValue.abv_sum {ι : Type u_1} {R : Type u_8} {S : Type u_9} [] [] (abv : RS) [] (f : ιR) (s : ) :
abv (Finset.sum s fun (i : ι) => f i) Finset.sum s fun (i : ι) => abv (f i)
@[deprecated IsAbsoluteValue.abv_sum]
theorem abv_sum_le_sum_abv {ι : Type u_1} {R : Type u_8} {S : Type u_9} [] [] (abv : RS) [] (f : ιR) (s : ) :
abv (Finset.sum s fun (i : ι) => f i) Finset.sum s fun (i : ι) => abv (f i)

Alias of IsAbsoluteValue.abv_sum.

theorem AbsoluteValue.map_prod {ι : Type u_1} {R : Type u_8} {S : Type u_9} [] [] (abv : ) (f : ιR) (s : ) :
abv (Finset.prod s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => abv (f i)
theorem IsAbsoluteValue.map_prod {ι : Type u_1} {R : Type u_8} {S : Type u_9} [] [] (abv : RS) [] (f : ιR) (s : ) :
abv (Finset.prod s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => abv (f i)

The positivity extension which proves that ∑ i in 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