mathlib documentation

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} [add_comm_monoid M] [ordered_add_comm_monoid N] (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 (∑ (i : ι) in s, g i) ∑ (i : ι) in s, 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] [ordered_comm_monoid N] (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 (∏ (i : ι) in s, g i) ∏ (i : ι) in s, 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] [ordered_comm_monoid N] (f : M → N) (h_mul : ∀ (x y : M), f (x * y) (f x) * f y) {s : finset ι} (hs : s.nonempty) (g : ι → M) :
f (∏ (i : ι) in s, g i) ∏ (i : ι) in s, 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} [add_comm_monoid M] [ordered_add_comm_monoid N] (f : M → N) (h_mul : ∀ (x y : M), f (x + y) f x + f y) {s : finset ι} (hs : s.nonempty) (g : ι → M) :
f (∑ (i : ι) in s, g i) ∑ (i : ι) in s, 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} [add_comm_monoid M] [ordered_add_comm_monoid N] (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 (∑ (i : ι) in s, g i) ∑ (i : ι) in s, 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] [ordered_comm_monoid N] (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 (∏ (i : ι) in s, g i) ∏ (i : ι) in s, 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] [ordered_comm_monoid N] (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 (∏ (i : ι) in s, g i) ∏ (i : ι) in s, 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} [add_comm_monoid M] [ordered_add_comm_monoid N] (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 (∑ (i : ι) in s, g i) ∑ (i : ι) in s, 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} [ordered_add_comm_monoid N] {f g : ι → N} {s : finset ι} (h : ∀ (i : ι), i sf i g i) :
∑ (i : ι) in s, f i ∑ (i : ι) in s, 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} [ordered_comm_monoid N] {f g : ι → N} {s : finset ι} (h : ∀ (i : ι), i sf i g i) :
∏ (i : ι) in s, f i ∏ (i : ι) in s, 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} [ordered_comm_monoid N] {f : ι → N} {s : finset ι} (h : ∀ (i : ι), i s1 f i) :
1 ∏ (i : ι) in s, f i
theorem finset.sum_nonneg {ι : Type u_1} {N : Type u_5} [ordered_add_comm_monoid N] {f : ι → N} {s : finset ι} (h : ∀ (i : ι), i s0 f i) :
0 ∑ (i : ι) in s, f i
theorem finset.sum_nonpos {ι : Type u_1} {N : Type u_5} [ordered_add_comm_monoid N] {f : ι → N} {s : finset ι} (h : ∀ (i : ι), i sf i 0) :
∑ (i : ι) in s, f i 0
theorem finset.prod_le_one' {ι : Type u_1} {N : Type u_5} [ordered_comm_monoid N] {f : ι → N} {s : finset ι} (h : ∀ (i : ι), i sf i 1) :
∏ (i : ι) in s, f i 1
theorem finset.prod_le_prod_of_subset_of_one_le' {ι : Type u_1} {N : Type u_5} [ordered_comm_monoid N] {f : ι → N} {s t : finset ι} (h : s t) (hf : ∀ (i : ι), i ti s1 f i) :
∏ (i : ι) in s, f i ∏ (i : ι) in t, f i
theorem finset.sum_le_sum_of_subset_of_nonneg {ι : Type u_1} {N : Type u_5} [ordered_add_comm_monoid N] {f : ι → N} {s t : finset ι} (h : s t) (hf : ∀ (i : ι), i ti s0 f i) :
∑ (i : ι) in s, f i ∑ (i : ι) in t, f i
theorem finset.sum_mono_set_of_nonneg {ι : Type u_1} {N : Type u_5} [ordered_add_comm_monoid N] {f : ι → N} (hf : ∀ (x : ι), 0 f x) :
monotone (λ (s : finset ι), ∑ (x : ι) in s, f x)
theorem finset.prod_mono_set_of_one_le' {ι : Type u_1} {N : Type u_5} [ordered_comm_monoid N] {f : ι → N} (hf : ∀ (x : ι), 1 f x) :
monotone (λ (s : finset ι), ∏ (x : ι) in s, f x)
theorem finset.sum_le_univ_sum_of_nonneg {ι : Type u_1} {N : Type u_5} [ordered_add_comm_monoid N] {f : ι → N} [fintype ι] {s : finset ι} (w : ∀ (x : ι), 0 f x) :
∑ (x : ι) in s, f x ∑ (x : ι), f x
theorem finset.prod_le_univ_prod_of_one_le' {ι : Type u_1} {N : Type u_5} [ordered_comm_monoid N] {f : ι → N} [fintype ι] {s : finset ι} (w : ∀ (x : ι), 1 f x) :
∏ (x : ι) in s, f x ∏ (x : ι), f x
theorem finset.sum_eq_zero_iff_of_nonneg {ι : Type u_1} {N : Type u_5} [ordered_add_comm_monoid N] {f : ι → N} {s : finset ι} :
(∀ (i : ι), i s0 f i)(∑ (i : ι) in s, f i = 0 ∀ (i : ι), i sf i = 0)
theorem finset.prod_eq_one_iff_of_one_le' {ι : Type u_1} {N : Type u_5} [ordered_comm_monoid N] {f : ι → N} {s : finset ι} :
(∀ (i : ι), i s1 f i)(∏ (i : ι) in s, f i = 1 ∀ (i : ι), i sf i = 1)
theorem finset.prod_eq_one_iff_of_le_one' {ι : Type u_1} {N : Type u_5} [ordered_comm_monoid N] {f : ι → N} {s : finset ι} :
(∀ (i : ι), i sf i 1)(∏ (i : ι) in s, f i = 1 ∀ (i : ι), i sf i = 1)
theorem finset.single_le_prod' {ι : Type u_1} {N : Type u_5} [ordered_comm_monoid N] {f : ι → N} {s : finset ι} (hf : ∀ (i : ι), i s1 f i) {a : ι} (h : a s) :
f a ∏ (x : ι) in s, f x
theorem finset.single_le_sum {ι : Type u_1} {N : Type u_5} [ordered_add_comm_monoid N] {f : ι → N} {s : finset ι} (hf : ∀ (i : ι), i s0 f i) {a : ι} (h : a s) :
f a ∑ (x : ι) in s, f x
theorem finset.sum_le_of_forall_le {ι : Type u_1} {N : Type u_5} [ordered_add_comm_monoid N] (s : finset ι) (f : ι → N) (n : N) (h : ∀ (x : ι), x sf x n) :
s.sum f s.card n
theorem finset.prod_le_of_forall_le {ι : Type u_1} {N : Type u_5} [ordered_comm_monoid N] (s : finset ι) (f : ι → N) (n : N) (h : ∀ (x : ι), x sf x n) :
s.prod f n ^ s.card
theorem finset.le_sum_of_forall_le {ι : Type u_1} {N : Type u_5} [ordered_add_comm_monoid N] (s : finset ι) (f : ι → N) (n : N) (h : ∀ (x : ι), x sn f x) :
s.card n s.sum f
theorem finset.le_prod_of_forall_le {ι : Type u_1} {N : Type u_5} [ordered_comm_monoid N] (s : finset ι) (f : ι → N) (n : N) (h : ∀ (x : ι), x sn f x) :
n ^ s.card s.prod f
theorem finset.card_bUnion_le_card_mul {ι : Type u_1} {β : Type u_3} [decidable_eq β] (s : finset ι) (f : ι → finset β) (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} [ordered_add_comm_monoid N] {s : finset ι} {ι' : Type u_9} [decidable_eq ι'] {t : finset ι'} {g : ι → ι'} {f : ι → N} (h : ∀ (y : ι'), y t0 ∑ (x : ι) in finset.filter (λ (x : ι), g x = y) s, f x) :
∑ (y : ι') in t, ∑ (x : ι) in finset.filter (λ (x : ι), g x = y) s, f x ∑ (x : ι) in s, f x
theorem finset.prod_fiberwise_le_prod_of_one_le_prod_fiber' {ι : Type u_1} {N : Type u_5} [ordered_comm_monoid N] {s : finset ι} {ι' : Type u_9} [decidable_eq ι'] {t : finset ι'} {g : ι → ι'} {f : ι → N} (h : ∀ (y : ι'), y t1 ∏ (x : ι) in finset.filter (λ (x : ι), g x = y) s, f x) :
∏ (y : ι') in t, ∏ (x : ι) in finset.filter (λ (x : ι), g x = y) s, f x ∏ (x : ι) in s, f x
theorem finset.prod_le_prod_fiberwise_of_prod_fiber_le_one' {ι : Type u_1} {N : Type u_5} [ordered_comm_monoid N] {s : finset ι} {ι' : Type u_9} [decidable_eq ι'] {t : finset ι'} {g : ι → ι'} {f : ι → N} (h : ∀ (y : ι'), y t∏ (x : ι) in finset.filter (λ (x : ι), g x = y) s, f x 1) :
∏ (x : ι) in s, f x ∏ (y : ι') in t, ∏ (x : ι) in finset.filter (λ (x : ι), g x = y) s, f x
theorem finset.sum_le_sum_fiberwise_of_sum_fiber_nonpos {ι : Type u_1} {N : Type u_5} [ordered_add_comm_monoid N] {s : finset ι} {ι' : Type u_9} [decidable_eq ι'] {t : finset ι'} {g : ι → ι'} {f : ι → N} (h : ∀ (y : ι'), y t∑ (x : ι) in finset.filter (λ (x : ι), g x = y) s, f x 0) :
∑ (x : ι) in s, f x ∑ (y : ι') in t, ∑ (x : ι) in finset.filter (λ (x : ι), g x = y) s, f x
theorem finset.abs_sum_le_sum_abs {ι : Type u_1} {G : Type u_2} [linear_ordered_add_comm_group G] (f : ι → G) (s : finset ι) :
|∑ (i : ι) in s, f i| ∑ (i : ι) in s, |f i|
theorem finset.abs_prod {ι : Type u_1} {R : Type u_2} [linear_ordered_comm_ring R] {f : ι → R} {s : finset ι} :
|∏ (x : ι) in s, f x| = ∏ (x : ι) in s, |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 finset.image f s(finset.filter (λ (x : α), f x = a) s).card n) :
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 finset.image f sn (finset.filter (λ (x : α), f x = a) s).card) :
theorem finset.sum_card_inter_le {α : Type u_2} [decidable_eq α] {s : finset α} {B : finset (finset α)} {n : } (h : ∀ (a : α), a s(finset.filter (has_mem.mem a) B).card n) :
∑ (t : finset α) in B, (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 : α), (finset.filter (has_mem.mem a) B).card n) :
∑ (s : finset α) in B, 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} [decidable_eq α] {s : finset α} {B : finset (finset α)} {n : } (h : ∀ (a : α), a sn (finset.filter (has_mem.mem a) B).card) :
(s.card) * n ∑ (t : finset α) in B, (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 (finset.filter (has_mem.mem a) B).card) :
(fintype.card α) * n ∑ (s : finset α) in B, 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(finset.filter (has_mem.mem a) B).card = n) :
∑ (t : finset α) in B, (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 : α), (finset.filter (has_mem.mem a) B).card = n) :
∑ (s : finset α) in B, 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.

@[simp]
theorem finset.prod_eq_one_iff' {ι : Type u_1} {M : Type u_4} [canonically_ordered_monoid M] {f : ι → M} {s : finset ι} :
∏ (x : ι) in s, f x = 1 ∀ (x : ι), x sf x = 1
@[simp]
theorem finset.sum_eq_zero_iff {ι : Type u_1} {M : Type u_4} [canonically_ordered_add_monoid M] {f : ι → M} {s : finset ι} :
∑ (x : ι) in s, f x = 0 ∀ (x : ι), x sf x = 0
theorem finset.sum_le_sum_of_subset {ι : Type u_1} {M : Type u_4} [canonically_ordered_add_monoid M] {f : ι → M} {s t : finset ι} (h : s t) :
∑ (x : ι) in s, f x ∑ (x : ι) in t, f x
theorem finset.prod_le_prod_of_subset' {ι : Type u_1} {M : Type u_4} [canonically_ordered_monoid M] {f : ι → M} {s t : finset ι} (h : s t) :
∏ (x : ι) in s, f x ∏ (x : ι) in t, f x
theorem finset.sum_mono_set {ι : Type u_1} {M : Type u_4} [canonically_ordered_add_monoid M] (f : ι → M) :
monotone (λ (s : finset ι), ∑ (x : ι) in s, f x)
theorem finset.prod_mono_set' {ι : Type u_1} {M : Type u_4} [canonically_ordered_monoid M] (f : ι → M) :
monotone (λ (s : finset ι), ∏ (x : ι) in s, f x)
theorem finset.prod_le_prod_of_ne_one' {ι : Type u_1} {M : Type u_4} [canonically_ordered_monoid M] {f : ι → M} {s t : finset ι} (h : ∀ (x : ι), x sf x 1x t) :
∏ (x : ι) in s, f x ∏ (x : ι) in t, f x
theorem finset.sum_le_sum_of_ne_zero {ι : Type u_1} {M : Type u_4} [canonically_ordered_add_monoid M] {f : ι → M} {s t : finset ι} (h : ∀ (x : ι), x sf x 0x t) :
∑ (x : ι) in s, f x ∑ (x : ι) in t, f x
theorem finset.prod_lt_prod' {ι : Type u_1} {M : Type u_4} [ordered_cancel_comm_monoid M] {f g : ι → M} {s : finset ι} (Hle : ∀ (i : ι), i sf i g i) (Hlt : ∃ (i : ι) (H : i s), f i < g i) :
∏ (i : ι) in s, f i < ∏ (i : ι) in s, g i
theorem finset.sum_lt_sum {ι : Type u_1} {M : Type u_4} [ordered_cancel_add_comm_monoid M] {f g : ι → M} {s : finset ι} (Hle : ∀ (i : ι), i sf i g i) (Hlt : ∃ (i : ι) (H : i s), f i < g i) :
∑ (i : ι) in s, f i < ∑ (i : ι) in s, g i
theorem finset.prod_lt_prod_of_nonempty' {ι : Type u_1} {M : Type u_4} [ordered_cancel_comm_monoid M] {f g : ι → M} {s : finset ι} (hs : s.nonempty) (Hlt : ∀ (i : ι), i sf i < g i) :
∏ (i : ι) in s, f i < ∏ (i : ι) in s, g i
theorem finset.sum_lt_sum_of_nonempty {ι : Type u_1} {M : Type u_4} [ordered_cancel_add_comm_monoid M] {f g : ι → M} {s : finset ι} (hs : s.nonempty) (Hlt : ∀ (i : ι), i sf i < g i) :
∑ (i : ι) in s, f i < ∑ (i : ι) in s, g i
theorem finset.prod_lt_prod_of_subset' {ι : Type u_1} {M : Type u_4} [ordered_cancel_comm_monoid M] {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) :
∏ (j : ι) in s, f j < ∏ (j : ι) in t, f j
theorem finset.sum_lt_sum_of_subset {ι : Type u_1} {M : Type u_4} [ordered_cancel_add_comm_monoid M] {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) :
∑ (j : ι) in s, f j < ∑ (j : ι) in t, f j
theorem finset.single_lt_sum {ι : Type u_1} {M : Type u_4} [ordered_cancel_add_comm_monoid M] {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 < ∑ (k : ι) in s, f k
theorem finset.single_lt_prod' {ι : Type u_1} {M : Type u_4} [ordered_cancel_comm_monoid M] {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 < ∏ (k : ι) in s, f k
theorem finset.sum_pos {ι : Type u_1} {M : Type u_4} [ordered_cancel_add_comm_monoid M] {f : ι → M} {s : finset ι} (h : ∀ (i : ι), i s0 < f i) (hs : s.nonempty) :
0 < ∑ (i : ι) in s, f i
theorem finset.one_lt_prod {ι : Type u_1} {M : Type u_4} [ordered_cancel_comm_monoid M] {f : ι → M} {s : finset ι} (h : ∀ (i : ι), i s1 < f i) (hs : s.nonempty) :
1 < ∏ (i : ι) in s, f i
theorem finset.sum_neg {ι : Type u_1} {M : Type u_4} [ordered_cancel_add_comm_monoid M] {f : ι → M} {s : finset ι} (h : ∀ (i : ι), i sf i < 0) (hs : s.nonempty) :
∑ (i : ι) in s, f i < 0
theorem finset.prod_lt_one {ι : Type u_1} {M : Type u_4} [ordered_cancel_comm_monoid M] {f : ι → M} {s : finset ι} (h : ∀ (i : ι), i sf i < 1) (hs : s.nonempty) :
∏ (i : ι) in s, f i < 1
theorem finset.exists_lt_of_sum_lt {ι : Type u_1} {M : Type u_4} [linear_ordered_cancel_add_comm_monoid M] {f g : ι → M} {s : finset ι} (Hlt : ∑ (i : ι) in s, f i < ∑ (i : ι) in s, g i) :
∃ (i : ι) (H : i s), f i < g i
theorem finset.exists_lt_of_prod_lt' {ι : Type u_1} {M : Type u_4} [linear_ordered_cancel_comm_monoid M] {f g : ι → M} {s : finset ι} (Hlt : ∏ (i : ι) in s, f i < ∏ (i : ι) in s, g i) :
∃ (i : ι) (H : i s), f i < g i
theorem finset.exists_le_of_prod_le' {ι : Type u_1} {M : Type u_4} [linear_ordered_cancel_comm_monoid M] {f g : ι → M} {s : finset ι} (hs : s.nonempty) (Hle : ∏ (i : ι) in s, f i ∏ (i : ι) in s, g i) :
∃ (i : ι) (H : i s), f i g i
theorem finset.exists_le_of_sum_le {ι : Type u_1} {M : Type u_4} [linear_ordered_cancel_add_comm_monoid M] {f g : ι → M} {s : finset ι} (hs : s.nonempty) (Hle : ∑ (i : ι) in s, f i ∑ (i : ι) in s, 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} [linear_ordered_cancel_add_comm_monoid M] {s : finset ι} (f : ι → M) (h₁ : ∑ (i : ι) in s, 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} [linear_ordered_cancel_comm_monoid M] {s : finset ι} (f : ι → M) (h₁ : ∏ (i : ι) in s, 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} [ordered_comm_semiring R] {f : ι → R} {s : finset ι} (h0 : ∀ (i : ι), i s0 f i) :
0 ∏ (i : ι) in s, f i
theorem finset.prod_pos {ι : Type u_1} {R : Type u_8} [ordered_comm_semiring R] {f : ι → R} {s : finset ι} [nontrivial R] (h0 : ∀ (i : ι), i s0 < f i) :
0 < ∏ (i : ι) in s, f i
theorem finset.prod_le_prod {ι : Type u_1} {R : Type u_8} [ordered_comm_semiring R] {f g : ι → R} {s : finset ι} (h0 : ∀ (i : ι), i s0 f i) (h1 : ∀ (i : ι), i sf i g i) :
∏ (i : ι) in s, f i ∏ (i : ι) in s, 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} [ordered_comm_semiring R] {f : ι → R} {s : finset ι} (h0 : ∀ (i : ι), i s0 f i) (h1 : ∀ (i : ι), i sf i 1) :
∏ (i : ι) in s, 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} [ordered_comm_semiring R] {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) :
∏ (i : ι) in s, g i + ∏ (i : ι) in s, h i ∏ (i : ι) in s, 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} [canonically_ordered_comm_semiring R] {f g : ι → R} {s : finset ι} (h : ∀ (i : ι), i sf i g i) :
∏ (i : ι) in s, f i ∏ (i : ι) in s, g i
theorem finset.prod_add_prod_le' {ι : Type u_1} {R : Type u_8} [canonically_ordered_comm_semiring R] {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) :
∏ (i : ι) in s, g i + ∏ (i : ι) in s, h i ∏ (i : ι) in s, 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 ι] [ordered_comm_monoid M] :
monotone (λ (f : ι → M), ∏ (i : ι), f i)
theorem fintype.sum_mono {ι : Type u_1} {M : Type u_4} [fintype ι] [ordered_add_comm_monoid M] :
monotone (λ (f : ι → M), ∑ (i : ι), f i)
theorem fintype.sum_strict_mono {ι : Type u_1} {M : Type u_4} [fintype ι] [ordered_cancel_add_comm_monoid M] :
strict_mono (λ (f : ι → M), ∑ (x : ι), f x)
theorem fintype.prod_strict_mono' {ι : Type u_1} {M : Type u_4} [fintype ι] [ordered_cancel_comm_monoid M] :
strict_mono (λ (f : ι → M), ∏ (x : ι), f x)
theorem with_top.prod_lt_top {ι : Type u_1} {R : Type u_8} [canonically_ordered_comm_semiring R] [nontrivial R] [decidable_eq R] {s : finset ι} {f : ι → with_top R} (h : ∀ (i : ι), i sf i ) :
∏ (i : ι) in s, f i <

A product of finite numbers is still finite

theorem with_top.sum_lt_top {ι : Type u_1} {M : Type u_4} [ordered_add_comm_monoid M] {s : finset ι} {f : ι → with_top M} (h : ∀ (i : ι), i sf i ) :
∑ (i : ι) in s, f i <

A sum of finite numbers is still finite

theorem with_top.sum_eq_top_iff {ι : Type u_1} {M : Type u_4} [ordered_add_comm_monoid M] {s : finset ι} {f : ι → with_top M} :
∑ (i : ι) in s, 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} [ordered_add_comm_monoid M] {s : finset ι} {f : ι → with_top M} :
∑ (i : ι) in s, 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] [ordered_semiring S] (abv : absolute_value R S) (s : finset ι) (f : ι → R) :
abv (∑ (i : ι) in s, f i) ∑ (i : ι) in s, abv (f i)
theorem is_absolute_value.abv_sum {ι : Type u_1} {R : Type u_8} {S : Type u_9} [semiring R] [ordered_semiring S] (abv : R → S) [is_absolute_value abv] (f : ι → R) (s : finset ι) :
abv (∑ (i : ι) in s, f i) ∑ (i : ι) in s, abv (f i)
theorem absolute_value.map_prod {ι : Type u_1} {R : Type u_8} {S : Type u_9} [comm_semiring R] [nontrivial R] [linear_ordered_comm_ring S] (abv : absolute_value R S) (f : ι → R) (s : finset ι) :
abv (∏ (i : ι) in s, f i) = ∏ (i : ι) in s, abv (f i)
theorem is_absolute_value.map_prod {ι : Type u_1} {R : Type u_8} {S : Type u_9} [comm_semiring R] [nontrivial R] [linear_ordered_comm_ring S] (abv : R → S) [is_absolute_value abv] (f : ι → R) (s : finset ι) :
abv (∏ (i : ι) in s, f i) = ∏ (i : ι) in s, abv (f i)