# mathlibdocumentation

algebra.big_operators.order

# 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 : M → N) (p : M → Prop) (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 : ∀ (i : ι), i sp (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 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 : ∀ (i : ι), i sp (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 xp yf (x + y) f x + f y) (hp_mul : ∀ (x y : M), p xp yp (x + y)) (g : ι → M) {s : finset ι} (hs : ∀ (i : ι), i sp (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 xp yf (x * y) f x * f y) (hp_mul : ∀ (x y : M), p xp yp (x * y)) (g : ι → M) {s : finset ι} (hs : ∀ (i : ι), i sp (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 sf 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 sf 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 s1 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 s0 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 sf 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 sf 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 ti s1 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 ti s0 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 s0 f i)(s.sum (λ (i : ι), f i) = 0 ∀ (i : ι), i sf i = 0)
theorem finset.prod_eq_one_iff_of_one_le' {ι : Type u_1} {N : Type u_5} {f : ι → N} {s : finset ι} :
(∀ (i : ι), i s1 f i)(s.prod (λ (i : ι), f i) = 1 ∀ (i : ι), i sf i = 1)
theorem finset.prod_eq_one_iff_of_le_one' {ι : Type u_1} {N : Type u_5} {f : ι → N} {s : finset ι} :
(∀ (i : ι), i sf i 1)(s.prod (λ (i : ι), f i) = 1 ∀ (i : ι), i sf i = 1)
theorem finset.single_le_prod' {ι : Type u_1} {N : Type u_5} {f : ι → N} {s : finset ι} (hf : ∀ (i : ι), i s1 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 s0 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 sf 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 sf 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 sn 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 sn 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 t0 (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 t1 (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 s0 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 sf 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 sf a t) (n : ) (hn : ∀ (a : β), a tn (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 sn (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 sn 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 sf 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 sf 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 sf x 1x 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 sf x 0x 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 sf 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 sf 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 sf 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 sf 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 tj s1 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 tj s0 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 sk i0 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 sk i1 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 s0 < 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 s1 < 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 sf 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 sf i < 1) (hs : s.nonempty) :
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 sf i g i) :
s.sum (λ (i : ι), f i) = s.sum (λ (i : ι), g i) ∀ (i : ι), i sf 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 sf i g i) :
s.prod (λ (i : ι), f i) = s.prod (λ (i : ι), g i) ∀ (i : ι), i sf 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 s0 f i) :
0 s.prod (λ (i : ι), f i)
theorem finset.prod_pos {ι : Type u_1} {R : Type u_8} {f : ι → R} {s : finset ι} [nontrivial R] (h0 : ∀ (i : ι), i s0 < 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 s0 f i) (h1 : ∀ (i : ι), i sf 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 s0 f i) (h1 : ∀ (i : ι), i sf 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 sj ig j f j) (hhf : ∀ (j : ι), j sj ih j f j) (hg : ∀ (i : ι), i s0 g i) (hh : ∀ (i : ι), i s0 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_le_prod' {ι : Type u_1} {R : Type u_8} {f g : ι → R} {s : finset ι} (h : ∀ (i : ι), i sf i g i) :
s.prod (λ (i : ι), f i) s.prod (λ (i : ι), g i)
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 sj ig j f j) (hhf : ∀ (j : ι), j sj ih 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] {s : finset ι} {f : ι → } (h : ∀ (i : ι), i sf i ) :
s.prod (λ (i : ι), f i) <

A product of finite numbers is still finite

theorem with_top.sum_lt_top {ι : Type u_1} {M : Type u_4} {s : finset ι} {f : ι → } (h : ∀ (i : ι), i sf i ) :
s.sum (λ (i : ι), f i) <

A sum 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} {s : finset ι} {f : ι → } :
s.sum (λ (i : ι), f i) < ∀ (i : ι), i sf 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))