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 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 (∑ (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 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 (∏ (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 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 (∑ (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 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 (∏ (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 ∈ s → f 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 ∈ s → f 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 ∈ s → 1 ≤ 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 ∈ s → 0 ≤ f i) :
0 ≤ ∑ (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 : ι), 0 ≤ f i) :
0 ≤ ∑ (i : ι) in s, f i
theorem
finset.one_le_prod''
{ι : Type u_1}
{N : Type u_5}
[ordered_comm_monoid N]
{f : ι → N}
{s : finset ι}
(h : ∀ (i : ι), 1 ≤ f i) :
1 ≤ ∏ (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 ∈ s → f 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 ∈ s → f 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 ∈ t → i ∉ s → 1 ≤ 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 ∈ t → i ∉ s → 0 ≤ 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) :
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) :
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 ι} :
theorem
finset.prod_eq_one_iff_of_one_le'
{ι : Type u_1}
{N : Type u_5}
[ordered_comm_monoid N]
{f : ι → N}
{s : finset ι} :
theorem
finset.prod_eq_one_iff_of_le_one'
{ι : Type u_1}
{N : Type u_5}
[ordered_comm_monoid N]
{f : ι → N}
{s : finset ι} :
theorem
finset.single_le_prod'
{ι : Type u_1}
{N : Type u_5}
[ordered_comm_monoid N]
{f : ι → N}
{s : finset ι}
(hf : ∀ (i : ι), i ∈ s → 1 ≤ 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 ∈ s → 0 ≤ f i)
{a : ι}
(h : a ∈ s) :
f a ≤ ∑ (x : ι) in s, f x
theorem
finset.sum_le_card_nsmul
{ι : Type u_1}
{N : Type u_5}
[ordered_add_comm_monoid N]
(s : finset ι)
(f : ι → N)
(n : N)
(h : ∀ (x : ι), x ∈ s → f x ≤ n) :
theorem
finset.prod_le_pow_card
{ι : Type u_1}
{N : Type u_5}
[ordered_comm_monoid N]
(s : finset ι)
(f : ι → N)
(n : N)
(h : ∀ (x : ι), x ∈ s → f x ≤ n) :
theorem
finset.pow_card_le_prod
{ι : Type u_1}
{N : Type u_5}
[ordered_comm_monoid N]
(s : finset ι)
(f : ι → N)
(n : N)
(h : ∀ (x : ι), x ∈ s → n ≤ f x) :
theorem
finset.card_nsmul_le_sum
{ι : Type u_1}
{N : Type u_5}
[ordered_add_comm_monoid N]
(s : finset ι)
(f : ι → N)
(n : N)
(h : ∀ (x : ι), x ∈ s → n ≤ f x) :
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 ∉ t → 0 ≤ ∑ (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 ∉ t → 1 ≤ ∏ (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 ι) :
theorem
finset.abs_sum_of_nonneg
{ι : Type u_1}
{G : Type u_2}
[linear_ordered_add_comm_group G]
{f : ι → G}
{s : finset ι}
(hf : ∀ (i : ι), i ∈ s → 0 ≤ f i) :
theorem
finset.abs_sum_of_nonneg'
{ι : Type u_1}
{G : Type u_2}
[linear_ordered_add_comm_group G]
{f : ι → G}
{s : finset ι}
(hf : ∀ (i : ι), 0 ≤ f i) :
theorem
finset.abs_prod
{ι : Type u_1}
{R : Type u_2}
[linear_ordered_comm_ring R]
{f : ι → R}
{s : finset ι} :
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) :
s.card ≤ n * (finset.image f 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 s → n ≤ (finset.filter (λ (x : α), f x = a) s).card) :
n * (finset.image f 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 → (finset.filter (has_mem.mem a) B).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 ∈ s → n ≤ (finset.filter (has_mem.mem a) B).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) :
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.
theorem
finset.card_le_card_bUnion
{ι : Type u_1}
{α : Type u_2}
[decidable_eq α]
{s : finset ι}
{f : ι → finset α}
(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 : ι → finset α}
(hs : ↑s.pairwise_disjoint f) :
theorem
finset.card_le_card_bUnion_add_one
{ι : Type u_1}
{α : Type u_2}
[decidable_eq α]
{s : finset ι}
{f : ι → finset α}
(hf : function.injective f)
(hs : ↑s.pairwise_disjoint f) :
@[simp]
theorem
finset.prod_eq_one_iff'
{ι : Type u_1}
{M : Type u_4}
[canonically_ordered_monoid M]
{f : ι → M}
{s : finset ι} :
@[simp]
theorem
finset.sum_eq_zero_iff
{ι : Type u_1}
{M : Type u_4}
[canonically_ordered_add_monoid M]
{f : ι → M}
{s : finset ι} :
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) :
theorem
finset.prod_mono_set'
{ι : Type u_1}
{M : Type u_4}
[canonically_ordered_monoid M]
(f : ι → M) :
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 ∈ s → f x ≠ 1 → x ∈ 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 ∈ s → f x ≠ 0 → x ∈ 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 ∈ s → f 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 ∈ s → f 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 ∈ s → f 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 ∈ s → f i < g i) :
∑ (i : ι) in s, f i < ∑ (i : ι) in s, g i
theorem
finset.sum_pos
{ι : Type u_1}
{M : Type u_4}
[ordered_cancel_add_comm_monoid M]
{f : ι → M}
{s : finset ι}
(h : ∀ (i : ι), i ∈ s → 0 < 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 ∈ s → 1 < 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 ∈ s → f 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 ∈ s → f i < 1)
(hs : s.nonempty) :
∏ (i : ι) in s, f i < 1
theorem
finset.sum_eq_sum_iff_of_le
{ι : Type u_1}
{M : Type u_4}
[ordered_cancel_add_comm_monoid M]
{s : finset ι}
{f g : ι → M}
(h : ∀ (i : ι), i ∈ s → f i ≤ g i) :
theorem
finset.prod_eq_prod_iff_of_le
{ι : Type u_1}
{M : Type u_4}
[ordered_cancel_comm_monoid M]
{s : finset ι}
{f g : ι → M}
(h : ∀ (i : ι), i ∈ s → f i ≤ g i) :
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) :
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) :
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) :
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) :
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) :
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) :
theorem
finset.prod_nonneg
{ι : Type u_1}
{R : Type u_8}
[ordered_comm_semiring R]
{f : ι → R}
{s : finset ι}
(h0 : ∀ (i : ι), i ∈ s → 0 ≤ 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 ∈ s → 0 < 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 ∈ s → 0 ≤ f i)
(h1 : ∀ (i : ι), i ∈ s → f 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 ∈ s → 0 ≤ f i)
(h1 : ∀ (i : ι), i ∈ s → f 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 ∈ 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) :
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 ∈ s → f 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 ∈ s → j ≠ i → g j ≤ f j)
(hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j) :
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 ∈ 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 ∈ s → 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]
[ordered_semiring S]
(abv : absolute_value R S)
(s : finset ι)
(f : ι → R) :
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 ι) :
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)