# mathlibdocumentation

algebra.big_operators.order

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 : M N) (p : M Prop) (h_mul : (x y : M), p x p y f (x + y) f x + f y) (hp_mul : (x y : M), p x p y p (x + y)) (g : ι M) (s : finset ι) (hs_nonempty : s.nonempty) (hs : (i : ι), i s p (g i)) :
f (s.sum (λ (i : ι), g i)) s.sum (λ (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} [comm_monoid M] (f : M N) (p : M Prop) (h_mul : (x y : M), p x p y f (x * y) f x * f y) (hp_mul : (x y : M), p x p y p (x * y)) (g : ι M) (s : finset ι) (hs_nonempty : s.nonempty) (hs : (i : ι), i s p (g i)) :
f (s.prod (λ (i : ι), g i)) s.prod (λ (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_prod_nonempty_of_submultiplicative {ι : Type u_1} {M : Type u_4} {N : Type u_5} [comm_monoid M] (f : M N) (h_mul : (x y : M), f (x * y) f x * f y) {s : finset ι} (hs : s.nonempty) (g : ι M) :
f (s.prod (λ (i : ι), g i)) s.prod (λ (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_nonempty_of_subadditive {ι : Type u_1} {M : Type u_4} {N : Type u_5} (f : M N) (h_mul : (x y : M), f (x + y) f x + f y) {s : finset ι} (hs : s.nonempty) (g : ι M) :
f (s.sum (λ (i : ι), g i)) s.sum (λ (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_sum_of_subadditive_on_pred {ι : Type u_1} {M : Type u_4} {N : Type u_5} (f : M N) (p : M Prop) (h_one : f 0 = 0) (h_mul : (x y : M), p x p y f (x + y) f x + f y) (hp_mul : (x y : M), p x p y p (x + y)) (g : ι M) {s : finset ι} (hs : (i : ι), i s p (g i)) :
f (s.sum (λ (i : ι), g i)) s.sum (λ (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} [comm_monoid M] (f : M N) (p : M Prop) (h_one : f 1 = 1) (h_mul : (x y : M), p x p y f (x * y) f x * f y) (hp_mul : (x y : M), p x p y p (x * y)) (g : ι M) {s : finset ι} (hs : (i : ι), i s p (g i)) :
f (s.prod (λ (i : ι), g i)) s.prod (λ (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_prod_of_submultiplicative {ι : Type u_1} {M : Type u_4} {N : Type u_5} [comm_monoid M] (f : M N) (h_one : f 1 = 1) (h_mul : (x y : M), f (x * y) f x * f y) (s : finset ι) (g : ι M) :
f (s.prod (λ (i : ι), g i)) s.prod (λ (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.le_sum_of_subadditive {ι : Type u_1} {M : Type u_4} {N : Type u_5} (f : M N) (h_one : f 0 = 0) (h_mul : (x y : M), f (x + y) f x + f y) (s : finset ι) (g : ι M) :
f (s.sum (λ (i : ι), g i)) s.sum (λ (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.sum_le_sum {ι : Type u_1} {N : Type u_5} {f g : ι N} {s : finset ι} (h : (i : ι), i s f i g i) :
s.sum (λ (i : ι), f i) s.sum (λ (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 g : ι N} {s : finset ι} (h : (i : ι), i s f i g i) :
s.prod (λ (i : ι), f i) s.prod (λ (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 finset.one_le_prod' {ι : Type u_1} {N : Type u_5} {f : ι N} {s : finset ι} (h : (i : ι), i s 1 f i) :
1 s.prod (λ (i : ι), f i)
theorem finset.sum_nonneg {ι : Type u_1} {N : Type u_5} {f : ι N} {s : finset ι} (h : (i : ι), i s 0 f i) :
0 s.sum (λ (i : ι), f i)
theorem finset.sum_nonneg' {ι : Type u_1} {N : Type u_5} {f : ι N} {s : finset ι} (h : (i : ι), 0 f i) :
0 s.sum (λ (i : ι), f i)
theorem finset.one_le_prod'' {ι : Type u_1} {N : Type u_5} {f : ι N} {s : finset ι} (h : (i : ι), 1 f i) :
1 s.prod (λ (i : ι), f i)
theorem finset.sum_nonpos {ι : Type u_1} {N : Type u_5} {f : ι N} {s : finset ι} (h : (i : ι), i s f i 0) :
s.sum (λ (i : ι), f i) 0
theorem finset.prod_le_one' {ι : Type u_1} {N : Type u_5} {f : ι N} {s : finset ι} (h : (i : ι), i s f i 1) :
s.prod (λ (i : ι), f i) 1
theorem finset.prod_le_prod_of_subset_of_one_le' {ι : Type u_1} {N : Type u_5} {f : ι N} {s t : finset ι} (h : s t) (hf : (i : ι), i t i s 1 f i) :
s.prod (λ (i : ι), f i) t.prod (λ (i : ι), f i)
theorem finset.sum_le_sum_of_subset_of_nonneg {ι : Type u_1} {N : Type u_5} {f : ι N} {s t : finset ι} (h : s t) (hf : (i : ι), i t i s 0 f i) :
s.sum (λ (i : ι), f i) t.sum (λ (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 (λ (s : finset ι), s.sum (λ (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 (λ (s : finset ι), s.prod (λ (x : ι), f x))
theorem finset.sum_le_univ_sum_of_nonneg {ι : Type u_1} {N : Type u_5} {f : ι N} [fintype ι] {s : finset ι} (w : (x : ι), 0 f x) :
s.sum (λ (x : ι), f x) finset.univ.sum (λ (x : ι), f x)
theorem finset.prod_le_univ_prod_of_one_le' {ι : Type u_1} {N : Type u_5} {f : ι N} [fintype ι] {s : finset ι} (w : (x : ι), 1 f x) :
s.prod (λ (x : ι), f x) finset.univ.prod (λ (x : ι), f x)
theorem finset.sum_eq_zero_iff_of_nonneg {ι : Type u_1} {N : Type u_5} {f : ι N} {s : finset ι} :
( (i : ι), i s 0 f i) (s.sum (λ (i : ι), f i) = 0 (i : ι), i s f i = 0)
theorem finset.prod_eq_one_iff_of_one_le' {ι : Type u_1} {N : Type u_5} {f : ι N} {s : finset ι} :
( (i : ι), i s 1 f i) (s.prod (λ (i : ι), f i) = 1 (i : ι), i s f i = 1)
theorem finset.prod_eq_one_iff_of_le_one' {ι : Type u_1} {N : Type u_5} {f : ι N} {s : finset ι} :
( (i : ι), i s f i 1) (s.prod (λ (i : ι), f i) = 1 (i : ι), i s f i = 1)
theorem finset.single_le_prod' {ι : Type u_1} {N : Type u_5} {f : ι N} {s : finset ι} (hf : (i : ι), i s 1 f i) {a : ι} (h : a s) :
f a s.prod (λ (x : ι), f x)
theorem finset.single_le_sum {ι : Type u_1} {N : Type u_5} {f : ι N} {s : finset ι} (hf : (i : ι), i s 0 f i) {a : ι} (h : a s) :
f a s.sum (λ (x : ι), f x)
theorem finset.sum_le_card_nsmul {ι : Type u_1} {N : Type u_5} (s : finset ι) (f : ι N) (n : N) (h : (x : ι), x s f x n) :
s.sum f s.card n
theorem finset.prod_le_pow_card {ι : Type u_1} {N : Type u_5} (s : finset ι) (f : ι N) (n : N) (h : (x : ι), x s f x n) :
s.prod f n ^ s.card
theorem finset.pow_card_le_prod {ι : Type u_1} {N : Type u_5} (s : finset ι) (f : ι N) (n : N) (h : (x : ι), x s n f x) :
n ^ s.card s.prod f
theorem finset.card_nsmul_le_sum {ι : Type u_1} {N : Type u_5} (s : finset ι) (f : ι N) (n : N) (h : (x : ι), x s n f x) :
s.card n s.sum f
theorem finset.card_bUnion_le_card_mul {ι : Type u_1} {β : Type u_3} [decidable_eq β] (s : finset ι) (f : ι ) (n : ) (h : (a : ι), a s (f a).card n) :
(s.bUnion f).card s.card * n
theorem finset.sum_fiberwise_le_sum_of_sum_fiber_nonneg {ι : Type u_1} {N : Type u_5} {s : finset ι} {ι' : Type u_9} [decidable_eq ι'] {t : finset ι'} {g : ι ι'} {f : ι N} (h : (y : ι'), y t 0 (finset.filter (λ (x : ι), g x = y) s).sum (λ (x : ι), f x)) :
t.sum (λ (y : ι'), (finset.filter (λ (x : ι), g x = y) s).sum (λ (x : ι), f x)) s.sum (λ (x : ι), f x)
theorem finset.prod_fiberwise_le_prod_of_one_le_prod_fiber' {ι : Type u_1} {N : Type u_5} {s : finset ι} {ι' : Type u_9} [decidable_eq ι'] {t : finset ι'} {g : ι ι'} {f : ι N} (h : (y : ι'), y t 1 (finset.filter (λ (x : ι), g x = y) s).prod (λ (x : ι), f x)) :
t.prod (λ (y : ι'), (finset.filter (λ (x : ι), g x = y) s).prod (λ (x : ι), f x)) s.prod (λ (x : ι), f x)
theorem finset.prod_le_prod_fiberwise_of_prod_fiber_le_one' {ι : Type u_1} {N : Type u_5} {s : finset ι} {ι' : Type u_9} [decidable_eq ι'] {t : finset ι'} {g : ι ι'} {f : ι N} (h : (y : ι'), y t (finset.filter (λ (x : ι), g x = y) s).prod (λ (x : ι), f x) 1) :
s.prod (λ (x : ι), f x) t.prod (λ (y : ι'), (finset.filter (λ (x : ι), g x = y) s).prod (λ (x : ι), f x))
theorem finset.sum_le_sum_fiberwise_of_sum_fiber_nonpos {ι : Type u_1} {N : Type u_5} {s : finset ι} {ι' : Type u_9} [decidable_eq ι'] {t : finset ι'} {g : ι ι'} {f : ι N} (h : (y : ι'), y t (finset.filter (λ (x : ι), g x = y) s).sum (λ (x : ι), f x) 0) :
s.sum (λ (x : ι), f x) t.sum (λ (y : ι'), (finset.filter (λ (x : ι), g x = y) s).sum (λ (x : ι), f x))
theorem finset.abs_sum_le_sum_abs {ι : Type u_1} {G : Type u_2} (f : ι G) (s : finset ι) :
|s.sum (λ (i : ι), f i)| s.sum (λ (i : ι), |f i|)
theorem finset.abs_sum_of_nonneg {ι : Type u_1} {G : Type u_2} {f : ι G} {s : finset ι} (hf : (i : ι), i s 0 f i) :
|s.sum (λ (i : ι), f i)| = s.sum (λ (i : ι), f i)
theorem finset.abs_sum_of_nonneg' {ι : Type u_1} {G : Type u_2} {f : ι G} {s : finset ι} (hf : (i : ι), 0 f i) :
|s.sum (λ (i : ι), f i)| = s.sum (λ (i : ι), f i)
theorem finset.abs_prod {ι : Type u_1} {R : Type u_2} {f : ι R} {s : finset ι} :
|s.prod (λ (x : ι), f x)| = s.prod (λ (x : ι), |f x|)
theorem finset.card_le_mul_card_image_of_maps_to {α : Type u_2} {β : Type u_3} [decidable_eq β] {f : α β} {s : finset α} {t : finset β} (Hf : (a : α), a s f a t) (n : ) (hn : (a : β), a t (finset.filter (λ (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} [decidable_eq β] {f : α β} (s : finset α) (n : ) (hn : (a : β), a s (finset.filter (λ (x : α), f x = a) s).card n) :
s.card n * s).card
theorem finset.mul_card_image_le_card_of_maps_to {α : Type u_2} {β : Type u_3} [decidable_eq β] {f : α β} {s : finset α} {t : finset β} (Hf : (a : α), a s f a t) (n : ) (hn : (a : β), a t n (finset.filter (λ (x : α), f x = a) s).card) :
n * t.card s.card
theorem finset.mul_card_image_le_card {α : Type u_2} {β : Type u_3} [decidable_eq β] {f : α β} (s : finset α) (n : ) (hn : (a : β), a s n (finset.filter (λ (x : α), f x = a) s).card) :
n * s).card s.card
theorem finset.sum_card_inter_le {α : Type u_2} [decidable_eq α] {s : finset α} {B : finset (finset α)} {n : } (h : (a : α), a s B).card n) :
B.sum (λ (t : finset α), (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} [decidable_eq α] {B : finset (finset α)} {n : } [fintype α] (h : (a : α), B).card n) :
B.sum (λ (s : finset α), 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} [decidable_eq α] {s : finset α} {B : finset (finset α)} {n : } (h : (a : α), a s n B).card) :
s.card * n B.sum (λ (t : finset α), (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} [decidable_eq α] {B : finset (finset α)} {n : } [fintype α] (h : (a : α), n B).card) :
B.sum (λ (s : finset α), 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} [decidable_eq α] {s : finset α} {B : finset (finset α)} {n : } (h : (a : α), a s B).card = n) :
B.sum (λ (t : finset α), (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} [decidable_eq α] {B : finset (finset α)} {n : } [fintype α] (h : (a : α), B).card = n) :
B.sum (λ (s : finset α), 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_bUnion {ι : Type u_1} {α : Type u_2} [decidable_eq α] {s : finset ι} {f : ι } (hs : s.pairwise_disjoint f) (hf : (i : ι), i s (f i).nonempty) :
theorem finset.card_le_card_bUnion_add_card_fiber {ι : Type u_1} {α : Type u_2} [decidable_eq α] {s : finset ι} {f : ι } (hs : s.pairwise_disjoint f) :
s.card (s.bUnion f).card + (finset.filter (λ (i : ι), f i = ) s).card
theorem finset.card_le_card_bUnion_add_one {ι : Type u_1} {α : Type u_2} [decidable_eq α] {s : finset ι} {f : ι } (hf : function.injective f) (hs : s.pairwise_disjoint f) :
s.card (s.bUnion f).card + 1
@[simp]
theorem finset.prod_eq_one_iff' {ι : Type u_1} {M : Type u_4} {f : ι M} {s : finset ι} :
s.prod (λ (x : ι), f x) = 1 (x : ι), x s f x = 1
@[simp]
theorem finset.sum_eq_zero_iff {ι : Type u_1} {M : Type u_4} {f : ι M} {s : finset ι} :
s.sum (λ (x : ι), f x) = 0 (x : ι), x s f x = 0
theorem finset.sum_le_sum_of_subset {ι : Type u_1} {M : Type u_4} {f : ι M} {s t : finset ι} (h : s t) :
s.sum (λ (x : ι), f x) t.sum (λ (x : ι), f x)
theorem finset.prod_le_prod_of_subset' {ι : Type u_1} {M : Type u_4} {f : ι M} {s t : finset ι} (h : s t) :
s.prod (λ (x : ι), f x) t.prod (λ (x : ι), f x)
theorem finset.sum_mono_set {ι : Type u_1} {M : Type u_4} (f : ι M) :
monotone (λ (s : finset ι), s.sum (λ (x : ι), f x))
theorem finset.prod_mono_set' {ι : Type u_1} {M : Type u_4} (f : ι M) :
monotone (λ (s : finset ι), s.prod (λ (x : ι), f x))
theorem finset.prod_le_prod_of_ne_one' {ι : Type u_1} {M : Type u_4} {f : ι M} {s t : finset ι} (h : (x : ι), x s f x 1 x t) :
s.prod (λ (x : ι), f x) t.prod (λ (x : ι), f x)
theorem finset.sum_le_sum_of_ne_zero {ι : Type u_1} {M : Type u_4} {f : ι M} {s t : finset ι} (h : (x : ι), x s f x 0 x t) :
s.sum (λ (x : ι), f x) t.sum (λ (x : ι), f x)
theorem finset.prod_lt_prod' {ι : Type u_1} {M : Type u_4} {f g : ι M} {s : finset ι} (Hle : (i : ι), i s f i g i) (Hlt : (i : ι) (H : i s), f i < g i) :
s.prod (λ (i : ι), f i) < s.prod (λ (i : ι), g i)
theorem finset.sum_lt_sum {ι : Type u_1} {M : Type u_4} {f g : ι M} {s : finset ι} (Hle : (i : ι), i s f i g i) (Hlt : (i : ι) (H : i s), f i < g i) :
s.sum (λ (i : ι), f i) < s.sum (λ (i : ι), g i)
theorem finset.prod_lt_prod_of_nonempty' {ι : Type u_1} {M : Type u_4} {f g : ι M} {s : finset ι} (hs : s.nonempty) (Hlt : (i : ι), i s f i < g i) :
s.prod (λ (i : ι), f i) < s.prod (λ (i : ι), g i)
theorem finset.sum_lt_sum_of_nonempty {ι : Type u_1} {M : Type u_4} {f g : ι M} {s : finset ι} (hs : s.nonempty) (Hlt : (i : ι), i s f i < g i) :
s.sum (λ (i : ι), f i) < s.sum (λ (i : ι), g i)
theorem finset.prod_lt_prod_of_subset' {ι : Type u_1} {M : Type u_4} {f : ι M} {s t : finset ι} (h : s t) {i : ι} (ht : i t) (hs : i s) (hlt : 1 < f i) (hle : (j : ι), j t j s 1 f j) :
s.prod (λ (j : ι), f j) < t.prod (λ (j : ι), f j)
theorem finset.sum_lt_sum_of_subset {ι : Type u_1} {M : Type u_4} {f : ι M} {s t : finset ι} (h : s t) {i : ι} (ht : i t) (hs : i s) (hlt : 0 < f i) (hle : (j : ι), j t j s 0 f j) :
s.sum (λ (j : ι), f j) < t.sum (λ (j : ι), f j)
theorem finset.single_lt_sum {ι : Type u_1} {M : Type u_4} {f : ι M} {s : finset ι} {i j : ι} (hij : j i) (hi : i s) (hj : j s) (hlt : 0 < f j) (hle : (k : ι), k s k i 0 f k) :
f i < s.sum (λ (k : ι), f k)
theorem finset.single_lt_prod' {ι : Type u_1} {M : Type u_4} {f : ι M} {s : finset ι} {i j : ι} (hij : j i) (hi : i s) (hj : j s) (hlt : 1 < f j) (hle : (k : ι), k s k i 1 f k) :
f i < s.prod (λ (k : ι), f k)
theorem finset.sum_pos {ι : Type u_1} {M : Type u_4} {f : ι M} {s : finset ι} (h : (i : ι), i s 0 < f i) (hs : s.nonempty) :
0 < s.sum (λ (i : ι), f i)
theorem finset.one_lt_prod {ι : Type u_1} {M : Type u_4} {f : ι M} {s : finset ι} (h : (i : ι), i s 1 < f i) (hs : s.nonempty) :
1 < s.prod (λ (i : ι), f i)
theorem finset.sum_neg {ι : Type u_1} {M : Type u_4} {f : ι M} {s : finset ι} (h : (i : ι), i s f i < 0) (hs : s.nonempty) :
s.sum (λ (i : ι), f i) < 0
theorem finset.prod_lt_one {ι : Type u_1} {M : Type u_4} {f : ι M} {s : finset ι} (h : (i : ι), i s f i < 1) (hs : s.nonempty) :
s.prod (λ (i : ι), f i) < 1
theorem finset.sum_pos' {ι : Type u_1} {M : Type u_4} {f : ι M} {s : finset ι} (h : (i : ι), i s 0 f i) (hs : (i : ι) (H : i s), 0 < f i) :
0 < s.sum (λ (i : ι), f i)
theorem finset.one_lt_prod' {ι : Type u_1} {M : Type u_4} {f : ι M} {s : finset ι} (h : (i : ι), i s 1 f i) (hs : (i : ι) (H : i s), 1 < f i) :
1 < s.prod (λ (i : ι), f i)
theorem finset.sum_neg' {ι : Type u_1} {M : Type u_4} {f : ι M} {s : finset ι} (h : (i : ι), i s f i 0) (hs : (i : ι) (H : i s), f i < 0) :
s.sum (λ (i : ι), f i) < 0
theorem finset.prod_lt_one' {ι : Type u_1} {M : Type u_4} {f : ι M} {s : finset ι} (h : (i : ι), i s f i 1) (hs : (i : ι) (H : i s), f i < 1) :
s.prod (λ (i : ι), f i) < 1
theorem finset.sum_eq_sum_iff_of_le {ι : Type u_1} {M : Type u_4} {s : finset ι} {f g : ι M} (h : (i : ι), i s f i g i) :
s.sum (λ (i : ι), f i) = s.sum (λ (i : ι), g i) (i : ι), i s f i = g i
theorem finset.prod_eq_prod_iff_of_le {ι : Type u_1} {M : Type u_4} {s : finset ι} {f g : ι M} (h : (i : ι), i s f i g i) :
s.prod (λ (i : ι), f i) = s.prod (λ (i : ι), g i) (i : ι), i s f i = g i
theorem finset.exists_lt_of_sum_lt {ι : Type u_1} {M : Type u_4} {f g : ι M} {s : finset ι} (Hlt : s.sum (λ (i : ι), f i) < s.sum (λ (i : ι), g i)) :
(i : ι) (H : i s), f i < g i
theorem finset.exists_lt_of_prod_lt' {ι : Type u_1} {M : Type u_4} {f g : ι M} {s : finset ι} (Hlt : s.prod (λ (i : ι), f i) < s.prod (λ (i : ι), g i)) :
(i : ι) (H : i s), f i < g i
theorem finset.exists_le_of_prod_le' {ι : Type u_1} {M : Type u_4} {f g : ι M} {s : finset ι} (hs : s.nonempty) (Hle : s.prod (λ (i : ι), f i) s.prod (λ (i : ι), g i)) :
(i : ι) (H : i s), f i g i
theorem finset.exists_le_of_sum_le {ι : Type u_1} {M : Type u_4} {f g : ι M} {s : finset ι} (hs : s.nonempty) (Hle : s.sum (λ (i : ι), f i) s.sum (λ (i : ι), g i)) :
(i : ι) (H : i s), f i g i
theorem finset.exists_pos_of_sum_zero_of_exists_nonzero {ι : Type u_1} {M : Type u_4} {s : finset ι} (f : ι M) (h₁ : s.sum (λ (i : ι), f i) = 0) (h₂ : (i : ι) (H : i s), f i 0) :
(i : ι) (H : 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 : finset ι} (f : ι M) (h₁ : s.prod (λ (i : ι), f i) = 1) (h₂ : (i : ι) (H : i s), f i 1) :
(i : ι) (H : i s), 1 < f i
theorem finset.prod_nonneg {ι : Type u_1} {R : Type u_8} {f : ι R} {s : finset ι} (h0 : (i : ι), i s 0 f i) :
0 s.prod (λ (i : ι), f i)
theorem finset.prod_le_prod {ι : Type u_1} {R : Type u_8} {f g : ι R} {s : finset ι} (h0 : (i : ι), i s 0 f i) (h1 : (i : ι), i s f i g i) :
s.prod (λ (i : ι), f i) s.prod (λ (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 finset.prod_le_one {ι : Type u_1} {R : Type u_8} {f : ι R} {s : finset ι} (h0 : (i : ι), i s 0 f i) (h1 : (i : ι), i s f i 1) :
s.prod (λ (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 : finset ι} {i : ι} {f g h : ι R} (hi : i s) (h2i : g i + h i f i) (hgf : (j : ι), j s j i g j f j) (hhf : (j : ι), j s j i h j f j) (hg : (i : ι), i s 0 g i) (hh : (i : ι), i s 0 h i) :
s.prod (λ (i : ι), g i) + s.prod (λ (i : ι), h i) s.prod (λ (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 ordered_comm_semiring.

theorem finset.prod_pos {ι : Type u_1} {R : Type u_8} [nontrivial R] {f : ι R} {s : finset ι} (h0 : (i : ι), i s 0 < f i) :
0 < s.prod (λ (i : ι), f i)
@[simp]
theorem canonically_ordered_comm_semiring.multiset_prod_pos {R : Type u_8} [nontrivial R] {m : multiset R} :
0 < m.prod (x : R), x m 0 < x
@[simp]
theorem canonically_ordered_comm_semiring.prod_pos {ι : Type u_1} {R : Type u_8} {f : ι R} {s : finset ι} [nontrivial R] :
0 < s.prod (λ (i : ι), f i) (i : ι), i s 0 < f i

Note that the name is to match canonically_ordered_comm_semiring.mul_pos.

theorem finset.prod_add_prod_le' {ι : Type u_1} {R : Type u_8} {f g h : ι R} {s : finset ι} {i : ι} (hi : i s) (h2i : g i + h i f i) (hgf : (j : ι), j s j i g j f j) (hhf : (j : ι), j s j i h j f j) :
s.prod (λ (i : ι), g i) + s.prod (λ (i : ι), h i) s.prod (λ (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 canonically_ordered_comm_semiring.

theorem fintype.prod_mono' {ι : Type u_1} {M : Type u_4} [fintype ι]  :
monotone (λ (f : ι M), finset.univ.prod (λ (i : ι), f i))
theorem fintype.sum_mono {ι : Type u_1} {M : Type u_4} [fintype ι]  :
monotone (λ (f : ι M), finset.univ.sum (λ (i : ι), f i))
theorem fintype.sum_strict_mono {ι : Type u_1} {M : Type u_4} [fintype ι]  :
strict_mono (λ (f : ι M), finset.univ.sum (λ (x : ι), f x))
theorem fintype.prod_strict_mono' {ι : Type u_1} {M : Type u_4} [fintype ι]  :
strict_mono (λ (f : ι M), finset.univ.prod (λ (x : ι), f x))
theorem with_top.prod_lt_top {ι : Type u_1} {R : Type u_8} [nontrivial R] [decidable_eq R] [has_lt R] {s : finset ι} {f : ι } (h : (i : ι), i s f i ) :
s.prod (λ (i : ι), f i) <

A product of finite numbers is still finite

theorem with_top.sum_eq_top_iff {ι : Type u_1} {M : Type u_4} {s : finset ι} {f : ι } :
s.sum (λ (i : ι), f i) = (i : ι) (H : i s), f i =

A sum of numbers is infinite iff one of them is infinite

theorem with_top.sum_lt_top_iff {ι : Type u_1} {M : Type u_4} [has_lt M] {s : finset ι} {f : ι } :
s.sum (λ (i : ι), f i) < (i : ι), i s f i <

A sum of finite numbers is still finite

theorem with_top.sum_lt_top {ι : Type u_1} {M : Type u_4} [has_lt M] {s : finset ι} {f : ι } (h : (i : ι), i s f i ) :
s.sum (λ (i : ι), f i) <

A sum of finite numbers is still finite

theorem absolute_value.sum_le {ι : Type u_1} {R : Type u_8} {S : Type u_9} [semiring R] (abv : S) (s : finset ι) (f : ι R) :
abv (s.sum (λ (i : ι), f i)) s.sum (λ (i : ι), abv (f i))
theorem is_absolute_value.abv_sum {ι : Type u_1} {R : Type u_8} {S : Type u_9} [semiring R] (abv : R S) [is_absolute_value abv] (f : ι R) (s : finset ι) :
abv (s.sum (λ (i : ι), f i)) s.sum (λ (i : ι), abv (f i))
theorem absolute_value.map_prod {ι : Type u_1} {R : Type u_8} {S : Type u_9} [nontrivial R] (abv : S) (f : ι R) (s : finset ι) :
abv (s.prod (λ (i : ι), f i)) = s.prod (λ (i : ι), abv (f i))
theorem is_absolute_value.map_prod {ι : Type u_1} {R : Type u_8} {S : Type u_9} [nontrivial R] (abv : R S) [is_absolute_value abv] (f : ι R) (s : finset ι) :
abv (s.prod (λ (i : ι), f i)) = s.prod (λ (i : ι), abv (f i))