algebra.big_operators.order

source

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 (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).

source

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 (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).

source

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 (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).

source

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 (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).

source

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 (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).

source

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 (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).

source

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 (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).

source

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 (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).

source

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) :

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.

source

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) :

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.

source

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 ≤ s.prod (λ (i : ι), f i)

source

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 ≤ s.sum (λ (i : ι), f i)

source

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 ≤ s.sum (λ (i : ι), f i)

source

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 ≤ s.prod (λ (i : ι), f i)

source

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) :

s.sum (λ (i : ι), f i) ≤ 0

source

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) :

s.prod (λ (i : ι), f i) ≤ 1

source

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) :

s.prod (λ (i : ι), f i) ≤ t.prod (λ (i : ι), f i)

source

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) :

s.sum (λ (i : ι), f i) ≤ t.sum (λ (i : ι), f i)

source

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 ι), s.sum (λ (x : ι), f x))

source

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 ι), s.prod (λ (x : ι), f x))

source

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) :

s.sum (λ (x : ι), f x) ≤ finset.univ.sum (λ (x : ι), f x)

source

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) :

s.prod (λ (x : ι), f x) ≤ finset.univ.prod (λ (x : ι), f x)

source

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 ∈ s → 0 ≤ f i) → (s.sum (λ (i : ι), f i) = 0 ↔ ∀ (i : ι), i ∈ s → f i = 0)

source

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 ∈ s → 1 ≤ f i) → (s.prod (λ (i : ι), f i) = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)

source

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 ∈ s → f i ≤ 1) → (s.prod (λ (i : ι), f i) = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)

source

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 ≤ s.prod (λ (x : ι), f x)

source

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 ≤ s.sum (λ (x : ι), f x)

source

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) :

s.sum f ≤ s.card • n

source

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) :

s.prod f ≤ n ^ s.card

source

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) :

n ^ s.card ≤ s.prod f

source

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) :

s.card • n ≤ s.sum f

source

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

source

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 ≤ (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)

source

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 ≤ (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)

source

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 → (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))

source

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 → (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))

source

theorem finset.abs_sum_le_sum_abs {ι : Type u_1} {G : Type u_2} [linear_ordered_add_comm_group G] (f : ι → G) (s : finset ι) :

|s.sum (λ (i : ι), f i)| ≤ s.sum (λ (i : ι), |f i|)

source

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) :

|s.sum (λ (i : ι), f i)| = s.sum (λ (i : ι), f i)

source

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) :

|s.sum (λ (i : ι), f i)| = s.sum (λ (i : ι), f i)

source

theorem finset.abs_prod {ι : Type u_1} {R : Type u_2} [linear_ordered_comm_ring R] {f : ι → R} {s : finset ι} :

|s.prod (λ (x : ι), f x)| = s.prod (λ (x : ι), |f x|)

source

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

source

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

source

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

source

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

source

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) :

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.

source

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) :

B.sum (λ (s : finset α), 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.

source

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) :

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.

source

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 ≤ 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.

source

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) :

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.

source

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) :

B.sum (λ (s : finset α), 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.

source

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) :

s.card ≤ (s.bUnion f).card

source

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) :

s.card ≤ (s.bUnion f).card + (finset.filter (λ (i : ι), f i = ∅) s).card

source

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) :

s.card ≤ (s.bUnion f).card + 1

source

@[simp]

theorem finset.prod_eq_one_iff' {ι : Type u_1} {M : Type u_4} [canonically_ordered_monoid M] {f : ι → M} {s : finset ι} :

s.prod (λ (x : ι), f x) = 1 ↔ ∀ (x : ι), x ∈ s → f x = 1

source

@[simp]

theorem finset.sum_eq_zero_iff {ι : Type u_1} {M : Type u_4} [canonically_ordered_add_monoid M] {f : ι → M} {s : finset ι} :

s.sum (λ (x : ι), f x) = 0 ↔ ∀ (x : ι), x ∈ s → f x = 0

source

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) :

s.sum (λ (x : ι), f x) ≤ t.sum (λ (x : ι), f x)

source

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) :

s.prod (λ (x : ι), f x) ≤ t.prod (λ (x : ι), f x)

source

theorem finset.sum_mono_set {ι : Type u_1} {M : Type u_4} [canonically_ordered_add_monoid M] (f : ι → M) :

monotone (λ (s : finset ι), s.sum (λ (x : ι), f x))

source

theorem finset.prod_mono_set' {ι : Type u_1} {M : Type u_4} [canonically_ordered_monoid M] (f : ι → M) :

monotone (λ (s : finset ι), s.prod (λ (x : ι), f x))

source

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) :

s.prod (λ (x : ι), f x) ≤ t.prod (λ (x : ι), f x)

source

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) :

s.sum (λ (x : ι), f x) ≤ t.sum (λ (x : ι), f x)

source

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) :

s.prod (λ (i : ι), f i) < s.prod (λ (i : ι), g i)

source

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) :

s.sum (λ (i : ι), f i) < s.sum (λ (i : ι), g i)

source

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) :

s.prod (λ (i : ι), f i) < s.prod (λ (i : ι), g i)

source

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) :

s.sum (λ (i : ι), f i) < s.sum (λ (i : ι), g i)

source

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 ∈ t → j ∉ s → 1 ≤ f j) :

s.prod (λ (j : ι), f j) < t.prod (λ (j : ι), f j)

source

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 ∈ t → j ∉ s → 0 ≤ f j) :

s.sum (λ (j : ι), f j) < t.sum (λ (j : ι), f j)

source

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 ∈ s → k ≠ i → 0 ≤ f k) :

f i < s.sum (λ (k : ι), f k)

source

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 ∈ s → k ≠ i → 1 ≤ f k) :

f i < s.prod (λ (k : ι), f k)

source

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 < s.sum (λ (i : ι), f i)

source

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 < s.prod (λ (i : ι), f i)

source

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) :

s.sum (λ (i : ι), f i) < 0

source

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) :

s.prod (λ (i : ι), f i) < 1

source

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 : ∃ (i : ι) (H : i ∈ s), 0 < f i) :

0 < s.sum (λ (i : ι), f i)

source

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 : ∃ (i : ι) (H : i ∈ s), 1 < f i) :

1 < s.prod (λ (i : ι), f i)

source

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 : ∃ (i : ι) (H : i ∈ s), f i < 0) :

s.sum (λ (i : ι), f i) < 0

source

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 : ∃ (i : ι) (H : i ∈ s), f i < 1) :

s.prod (λ (i : ι), f i) < 1

source

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) :

s.sum (λ (i : ι), f i) = s.sum (λ (i : ι), g i) ↔ ∀ (i : ι), i ∈ s → f i = g i

source

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) :

s.prod (λ (i : ι), f i) = s.prod (λ (i : ι), g i) ↔ ∀ (i : ι), i ∈ s → f i = g i

source

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 : s.sum (λ (i : ι), f i) < s.sum (λ (i : ι), g i)) :

∃ (i : ι) (H : i ∈ s), f i < g i

source

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 : s.prod (λ (i : ι), f i) < s.prod (λ (i : ι), g i)) :

∃ (i : ι) (H : i ∈ s), f i < g i

source

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 : s.prod (λ (i : ι), f i) ≤ s.prod (λ (i : ι), g i)) :

∃ (i : ι) (H : i ∈ s), f i ≤ g i

source

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 : s.sum (λ (i : ι), f i) ≤ s.sum (λ (i : ι), g i)) :

∃ (i : ι) (H : i ∈ s), f i ≤ g i

source

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₁ : s.sum (λ (i : ι), f i) = 0) (h₂ : ∃ (i : ι) (H : i ∈ s), f i ≠ 0) :

∃ (i : ι) (H : i ∈ s), 0 < f i

source

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₁ : s.prod (λ (i : ι), f i) = 1) (h₂ : ∃ (i : ι) (H : i ∈ s), f i ≠ 1) :

∃ (i : ι) (H : i ∈ s), 1 < f i

source

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 ≤ s.prod (λ (i : ι), f i)

source

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) :

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.

source

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) :

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.

source

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) :

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.

source

theorem finset.prod_pos {ι : Type u_1} {R : Type u_8} [strict_ordered_comm_semiring R] [nontrivial R] {f : ι → R} {s : finset ι} (h0 : ∀ (i : ι), i ∈ s → 0 < f i) :

0 < s.prod (λ (i : ι), f i)

source

@[simp]

theorem canonically_ordered_comm_semiring.multiset_prod_pos {R : Type u_8} [canonically_ordered_comm_semiring R] [nontrivial R] {m : multiset R} :

0 < m.prod ↔ ∀ (x : R), x ∈ m → 0 < x

source

@[simp]

theorem canonically_ordered_comm_semiring.prod_pos {ι : Type u_1} {R : Type u_8} [canonically_ordered_comm_semiring R] {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.

source

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) :

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.

source

theorem fintype.prod_mono' {ι : Type u_1} {M : Type u_4} [fintype ι] [ordered_comm_monoid M] :

monotone (λ (f : ι → M), finset.univ.prod (λ (i : ι), f i))

source

theorem fintype.sum_mono {ι : Type u_1} {M : Type u_4} [fintype ι] [ordered_add_comm_monoid M] :

monotone (λ (f : ι → M), finset.univ.sum (λ (i : ι), f i))

source

theorem fintype.sum_strict_mono {ι : Type u_1} {M : Type u_4} [fintype ι] [ordered_cancel_add_comm_monoid M] :

strict_mono (λ (f : ι → M), finset.univ.sum (λ (x : ι), f x))

source

theorem fintype.prod_strict_mono' {ι : Type u_1} {M : Type u_4} [fintype ι] [ordered_cancel_comm_monoid M] :

strict_mono (λ (f : ι → M), finset.univ.prod (λ (x : ι), f x))

source

theorem with_top.prod_lt_top {ι : Type u_1} {R : Type u_8} [comm_monoid_with_zero R] [no_zero_divisors R] [nontrivial R] [decidable_eq R] [has_lt R] {s : finset ι} {f : ι → with_top R} (h : ∀ (i : ι), i ∈ s → f i ≠ ⊤) :

s.prod (λ (i : ι), f i) < ⊤

A product of finite numbers is still finite

source

theorem with_top.sum_eq_top_iff {ι : Type u_1} {M : Type u_4} [add_comm_monoid M] {s : finset ι} {f : ι → with_top M} :

s.sum (λ (i : ι), f i) = ⊤ ↔ ∃ (i : ι) (H : i ∈ s), f i = ⊤

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

source

theorem with_top.sum_lt_top_iff {ι : Type u_1} {M : Type u_4} [add_comm_monoid M] [has_lt M] {s : finset ι} {f : ι → with_top M} :

s.sum (λ (i : ι), f i) < ⊤ ↔ ∀ (i : ι), i ∈ s → f i < ⊤

A sum of finite numbers is still finite

source

theorem with_top.sum_lt_top {ι : Type u_1} {M : Type u_4} [add_comm_monoid M] [has_lt M] {s : finset ι} {f : ι → with_top M} (h : ∀ (i : ι), i ∈ s → f i ≠ ⊤) :

s.sum (λ (i : ι), f i) < ⊤

A sum of finite numbers is still finite

source

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 (s.sum (λ (i : ι), f i)) ≤ s.sum (λ (i : ι), ⇑abv (f i))

source

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 (s.sum (λ (i : ι), f i)) ≤ s.sum (λ (i : ι), abv (f i))

source

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 (s.prod (λ (i : ι), f i)) = s.prod (λ (i : ι), ⇑abv (f i))

source

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 (s.prod (λ (i : ι), f i)) = s.prod (λ (i : ι), abv (f i))

mathlib3 documentation

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