Big operators on a finset in ordered groups

This file contains the results concerning the interaction of multiset big operators with ordered groups/monoids.

theorem Finset.le_sum_nonempty_of_subadditive_on_pred {ι : Type u_1} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [OrderedAddCommMonoid 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 ∈ s, p (g i)) : f (Finset.sum s fun (i : ι) => g i) ≤ Finset.sum s fun (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} [CommMonoid M] [OrderedCommMonoid 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 ∈ s, p (g i)) : f (Finset.prod s fun (i : ι) => g i) ≤ Finset.prod s fun (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_sum_nonempty_of_subadditive {ι : Type u_1} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [OrderedAddCommMonoid N] (f : M → N) (h_mul : ∀ (x y : M), f (x + y) ≤ f x + f y) {s : Finset ι} (hs : s.Nonempty) (g : ι → M) : f (Finset.sum s fun (i : ι) => g i) ≤ Finset.sum s fun (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_prod_nonempty_of_submultiplicative {ι : Type u_1} {M : Type u_4} {N : Type u_5} [CommMonoid M] [OrderedCommMonoid N] (f : M → N) (h_mul : ∀ (x y : M), f (x * y) ≤ f x * f y) {s : Finset ι} (hs : s.Nonempty) (g : ι → M) : f (Finset.prod s fun (i : ι) => g i) ≤ Finset.prod s fun (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_of_subadditive_on_pred {ι : Type u_1} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [OrderedAddCommMonoid 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 ∈ s, p (g i)) : f (Finset.sum s fun (i : ι) => g i) ≤ Finset.sum s fun (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} [CommMonoid M] [OrderedCommMonoid 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 ∈ s, p (g i)) : f (Finset.prod s fun (i : ι) => g i) ≤ Finset.prod s fun (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_sum_of_subadditive {ι : Type u_1} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [OrderedAddCommMonoid 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 (Finset.sum s fun (i : ι) => g i) ≤ Finset.sum s fun (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.le_prod_of_submultiplicative {ι : Type u_1} {M : Type u_4} {N : Type u_5} [CommMonoid M] [OrderedCommMonoid 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 (Finset.prod s fun (i : ι) => g i) ≤ Finset.prod s fun (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.sum_le_sum {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ι → N} {g : ι → N} {s : Finset ι} (h : ∀ i ∈ s, f i ≤ g i) : (Finset.sum s fun (i : ι) => f i) ≤ Finset.sum s fun (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} [OrderedCommMonoid N] {f : ι → N} {g : ι → N} {s : Finset ι} (h : ∀ i ∈ s, f i ≤ g i) : (Finset.prod s fun (i : ι) => f i) ≤ Finset.prod s fun (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 GCongr.sum_le_sum {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ι → N} {g : ι → N} {s : Finset ι} (h : ∀ i ∈ s, f i ≤ g i) : Finset.sum s f ≤ Finset.sum s g

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 s.sum f ≤ s.sum g.

This is a variant (beta-reduced) version of the standard lemma Finset.sum_le_sum, convenient for the gcongr tactic.

theorem GCongr.prod_le_prod' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ι → N} {g : ι → N} {s : Finset ι} (h : ∀ i ∈ s, f i ≤ g i) : Finset.prod s f ≤ Finset.prod s g

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 s.prod f ≤ s.prod g.

This is a variant (beta-reduced) version of the standard lemma Finset.prod_le_prod', convenient for the gcongr tactic.

theorem Finset.sum_nonneg {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι} (h : ∀ i ∈ s, 0 ≤ f i) : 0 ≤ Finset.sum s fun (i : ι) => f i

theorem Finset.one_le_prod' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ι → N} {s : Finset ι} (h : ∀ i ∈ s, 1 ≤ f i) : 1 ≤ Finset.prod s fun (i : ι) => f i

theorem Finset.sum_nonneg' {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι} (h : ∀ (i : ι), 0 ≤ f i) : 0 ≤ Finset.sum s fun (i : ι) => f i

theorem Finset.one_le_prod'' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ι → N} {s : Finset ι} (h : ∀ (i : ι), 1 ≤ f i) : 1 ≤ Finset.prod s fun (i : ι) => f i

theorem Finset.sum_nonpos {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι} (h : ∀ i ∈ s, f i ≤ 0) : (Finset.sum s fun (i : ι) => f i) ≤ 0

theorem Finset.prod_le_one' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ι → N} {s : Finset ι} (h : ∀ i ∈ s, f i ≤ 1) : (Finset.prod s fun (i : ι) => f i) ≤ 1

theorem Finset.sum_le_sum_of_subset_of_nonneg {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι} {t : Finset ι} (h : s ⊆ t) (hf : ∀ i ∈ t, i ∉ s → 0 ≤ f i) : (Finset.sum s fun (i : ι) => f i) ≤ Finset.sum t fun (i : ι) => f i

theorem Finset.prod_le_prod_of_subset_of_one_le' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ι → N} {s : Finset ι} {t : Finset ι} (h : s ⊆ t) (hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i) : (Finset.prod s fun (i : ι) => f i) ≤ Finset.prod t fun (i : ι) => f i

theorem Finset.sum_mono_set_of_nonneg {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ι → N} (hf : ∀ (x : ι), 0 ≤ f x) : Monotone fun (s : Finset ι) => Finset.sum s fun (x : ι) => f x

theorem Finset.prod_mono_set_of_one_le' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ι → N} (hf : ∀ (x : ι), 1 ≤ f x) : Monotone fun (s : Finset ι) => Finset.prod s fun (x : ι) => f x

theorem Finset.sum_le_univ_sum_of_nonneg {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ι → N} [Fintype ι] {s : Finset ι} (w : ∀ (x : ι), 0 ≤ f x) : (Finset.sum s fun (x : ι) => f x) ≤ Finset.sum Finset.univ fun (x : ι) => f x

theorem Finset.prod_le_univ_prod_of_one_le' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ι → N} [Fintype ι] {s : Finset ι} (w : ∀ (x : ι), 1 ≤ f x) : (Finset.prod s fun (x : ι) => f x) ≤ Finset.prod Finset.univ fun (x : ι) => f x

theorem Finset.sum_eq_zero_iff_of_nonneg {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι} : (∀ i ∈ s, 0 ≤ f i) → ((Finset.sum s fun (i : ι) => f i) = 0 ↔ ∀ i ∈ s, f i = 0)

theorem Finset.prod_eq_one_iff_of_one_le' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ι → N} {s : Finset ι} : (∀ i ∈ s, 1 ≤ f i) → ((Finset.prod s fun (i : ι) => f i) = 1 ↔ ∀ i ∈ s, f i = 1)

theorem Finset.sum_eq_zero_iff_of_nonpos {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι} : (∀ i ∈ s, f i ≤ 0) → ((Finset.sum s fun (i : ι) => f i) = 0 ↔ ∀ i ∈ s, f i = 0)

theorem Finset.prod_eq_one_iff_of_le_one' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ι → N} {s : Finset ι} : (∀ i ∈ s, f i ≤ 1) → ((Finset.prod s fun (i : ι) => f i) = 1 ↔ ∀ i ∈ s, f i = 1)

theorem Finset.single_le_sum {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι} (hf : ∀ i ∈ s, 0 ≤ f i) {a : ι} (h : a ∈ s) : f a ≤ Finset.sum s fun (x : ι) => f x

theorem Finset.single_le_prod' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ι → N} {s : Finset ι} (hf : ∀ i ∈ s, 1 ≤ f i) {a : ι} (h : a ∈ s) : f a ≤ Finset.prod s fun (x : ι) => f x

theorem Finset.add_le_sum {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι} {i : ι} {j : ι} (hf : ∀ i ∈ s, 0 ≤ f i) (hi : i ∈ s) (hj : j ∈ s) (hne : i ≠ j) : f i + f j ≤ Finset.sum s fun (k : ι) => f k

theorem Finset.mul_le_prod {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {f : ι → N} {s : Finset ι} {i : ι} {j : ι} (hf : ∀ i ∈ s, 1 ≤ f i) (hi : i ∈ s) (hj : j ∈ s) (hne : i ≠ j) : f i * f j ≤ Finset.prod s fun (k : ι) => f k

theorem Finset.sum_le_card_nsmul {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] (s : Finset ι) (f : ι → N) (n : N) (h : ∀ x ∈ s, f x ≤ n) : Finset.sum s f ≤ s.card • n

theorem Finset.prod_le_pow_card {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] (s : Finset ι) (f : ι → N) (n : N) (h : ∀ x ∈ s, f x ≤ n) : Finset.prod s f ≤ n ^ s.card

theorem Finset.card_nsmul_le_sum {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] (s : Finset ι) (f : ι → N) (n : N) (h : ∀ x ∈ s, n ≤ f x) : s.card • n ≤ Finset.sum s f

theorem Finset.pow_card_le_prod {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] (s : Finset ι) (f : ι → N) (n : N) (h : ∀ x ∈ s, n ≤ f x) : n ^ s.card ≤ Finset.prod s f

theorem Finset.card_biUnion_le_card_mul {ι : Type u_1} {β : Type u_3} [DecidableEq β] (s : Finset ι) (f : ι → Finset β) (n : ℕ) (h : ∀ a ∈ s, (f a).card ≤ n) : (Finset.biUnion s f).card ≤ s.card * n

theorem Finset.sum_fiberwise_le_sum_of_sum_fiber_nonneg {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {s : Finset ι} {ι' : Type u_9} [DecidableEq ι'] {t : Finset ι'} {g : ι → ι'} {f : ι → N} (h : ∀ y ∉ t, 0 ≤ Finset.sum (Finset.filter (fun (x : ι) => g x = y) s) fun (x : ι) => f x) : (Finset.sum t fun (y : ι') => Finset.sum (Finset.filter (fun (x : ι) => g x = y) s) fun (x : ι) => f x) ≤ Finset.sum s fun (x : ι) => f x

theorem Finset.prod_fiberwise_le_prod_of_one_le_prod_fiber' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {s : Finset ι} {ι' : Type u_9} [DecidableEq ι'] {t : Finset ι'} {g : ι → ι'} {f : ι → N} (h : ∀ y ∉ t, 1 ≤ Finset.prod (Finset.filter (fun (x : ι) => g x = y) s) fun (x : ι) => f x) : (Finset.prod t fun (y : ι') => Finset.prod (Finset.filter (fun (x : ι) => g x = y) s) fun (x : ι) => f x) ≤ Finset.prod s fun (x : ι) => f x

theorem Finset.sum_le_sum_fiberwise_of_sum_fiber_nonpos {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {s : Finset ι} {ι' : Type u_9} [DecidableEq ι'] {t : Finset ι'} {g : ι → ι'} {f : ι → N} (h : ∀ y ∉ t, (Finset.sum (Finset.filter (fun (x : ι) => g x = y) s) fun (x : ι) => f x) ≤ 0) : (Finset.sum s fun (x : ι) => f x) ≤ Finset.sum t fun (y : ι') => Finset.sum (Finset.filter (fun (x : ι) => g x = y) s) fun (x : ι) => f x

theorem Finset.prod_le_prod_fiberwise_of_prod_fiber_le_one' {ι : Type u_1} {N : Type u_5} [OrderedCommMonoid N] {s : Finset ι} {ι' : Type u_9} [DecidableEq ι'] {t : Finset ι'} {g : ι → ι'} {f : ι → N} (h : ∀ y ∉ t, (Finset.prod (Finset.filter (fun (x : ι) => g x = y) s) fun (x : ι) => f x) ≤ 1) : (Finset.prod s fun (x : ι) => f x) ≤ Finset.prod t fun (y : ι') => Finset.prod (Finset.filter (fun (x : ι) => g x = y) s) fun (x : ι) => f x

theorem Finset.abs_sum_le_sum_abs {ι : Type u_1} {G : Type u_9} [LinearOrderedAddCommGroup G] (f : ι → G) (s : Finset ι) : |Finset.sum s fun (i : ι) => f i| ≤ Finset.sum s fun (i : ι) => |f i|

theorem Finset.abs_sum_of_nonneg {ι : Type u_1} {G : Type u_9} [LinearOrderedAddCommGroup G] {f : ι → G} {s : Finset ι} (hf : ∀ i ∈ s, 0 ≤ f i) : |Finset.sum s fun (i : ι) => f i| = Finset.sum s fun (i : ι) => f i

theorem Finset.abs_sum_of_nonneg' {ι : Type u_1} {G : Type u_9} [LinearOrderedAddCommGroup G] {f : ι → G} {s : Finset ι} (hf : ∀ (i : ι), 0 ≤ f i) : |Finset.sum s fun (i : ι) => f i| = Finset.sum s fun (i : ι) => f i

theorem Finset.card_le_mul_card_image_of_maps_to {α : Type u_2} {β : Type u_3} [DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β} (Hf : ∀ a ∈ s, f a ∈ t) (n : ℕ) (hn : ∀ a ∈ t, (Finset.filter (fun (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} [DecidableEq β] {f : α → β} (s : Finset α) (n : ℕ) (hn : ∀ a ∈ Finset.image f s, (Finset.filter (fun (x : α) => f x = a) s).card ≤ n) : s.card ≤ n * (Finset.image f s).card

theorem Finset.mul_card_image_le_card_of_maps_to {α : Type u_2} {β : Type u_3} [DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β} (Hf : ∀ a ∈ s, f a ∈ t) (n : ℕ) (hn : ∀ a ∈ t, n ≤ (Finset.filter (fun (x : α) => f x = a) s).card) : n * t.card ≤ s.card

theorem Finset.mul_card_image_le_card {α : Type u_2} {β : Type u_3} [DecidableEq β] {f : α → β} (s : Finset α) (n : ℕ) (hn : ∀ a ∈ Finset.image f s, n ≤ (Finset.filter (fun (x : α) => f x = a) s).card) : n * (Finset.image f s).card ≤ s.card

theorem Finset.sum_card_inter_le {α : Type u_2} [DecidableEq α] {s : Finset α} {B : Finset (Finset α)} {n : ℕ} (h : ∀ a ∈ s, (Finset.filter (fun (x : Finset α) => a ∈ x) B).card ≤ n) : (Finset.sum B fun (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} [DecidableEq α] {B : Finset (Finset α)} {n : ℕ} [Fintype α] (h : ∀ (a : α), (Finset.filter (fun (x : Finset α) => a ∈ x) B).card ≤ n) : (Finset.sum B fun (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.

theorem Finset.le_sum_card_inter {α : Type u_2} [DecidableEq α] {s : Finset α} {B : Finset (Finset α)} {n : ℕ} (h : ∀ a ∈ s, n ≤ (Finset.filter (fun (x : Finset α) => a ∈ x) B).card) : s.card * n ≤ Finset.sum B fun (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} [DecidableEq α] {B : Finset (Finset α)} {n : ℕ} [Fintype α] (h : ∀ (a : α), n ≤ (Finset.filter (fun (x : Finset α) => a ∈ x) B).card) : Fintype.card α * n ≤ Finset.sum B fun (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} [DecidableEq α] {s : Finset α} {B : Finset (Finset α)} {n : ℕ} (h : ∀ a ∈ s, (Finset.filter (fun (x : Finset α) => a ∈ x) B).card = n) : (Finset.sum B fun (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} [DecidableEq α] {B : Finset (Finset α)} {n : ℕ} [Fintype α] (h : ∀ (a : α), (Finset.filter (fun (x : Finset α) => a ∈ x) B).card = n) : (Finset.sum B fun (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.

theorem Finset.card_le_card_biUnion {ι : Type u_1} {α : Type u_2} [DecidableEq α] {s : Finset ι} {f : ι → Finset α} (hs : Set.PairwiseDisjoint (↑s) f) (hf : ∀ i ∈ s, (f i).Nonempty) : s.card ≤ (Finset.biUnion s f).card

theorem Finset.card_le_card_biUnion_add_card_fiber {ι : Type u_1} {α : Type u_2} [DecidableEq α] {s : Finset ι} {f : ι → Finset α} (hs : Set.PairwiseDisjoint (↑s) f) : s.card ≤ (Finset.biUnion s f).card + (Finset.filter (fun (i : ι) => f i = ∅) s).card

theorem Finset.card_le_card_biUnion_add_one {ι : Type u_1} {α : Type u_2} [DecidableEq α] {s : Finset ι} {f : ι → Finset α} (hf : Function.Injective f) (hs : Set.PairwiseDisjoint (↑s) f) : s.card ≤ (Finset.biUnion s f).card + 1

theorem CanonicallyOrderedAddCommMonoid.single_le_sum {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedAddCommMonoid M] {f : ι → M} {s : Finset ι} {i : ι} (hi : i ∈ s) : f i ≤ Finset.sum s fun (j : ι) => f j

In a canonically-ordered additive monoid, a sum bounds each of its terms.

See also Finset.single_le_sum.

theorem CanonicallyOrderedCommMonoid.single_le_prod {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedCommMonoid M] {f : ι → M} {s : Finset ι} {i : ι} (hi : i ∈ s) : f i ≤ Finset.prod s fun (j : ι) => f j

In a canonically-ordered monoid, a product bounds each of its terms.

See also Finset.single_le_prod'.

@[simp]

theorem Finset.sum_eq_zero_iff {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedAddCommMonoid M] {f : ι → M} {s : Finset ι} : (Finset.sum s fun (x : ι) => f x) = 0 ↔ ∀ x ∈ s, f x = 0

@[simp]

theorem Finset.prod_eq_one_iff' {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedCommMonoid M] {f : ι → M} {s : Finset ι} : (Finset.prod s fun (x : ι) => f x) = 1 ↔ ∀ x ∈ s, f x = 1

theorem Finset.sum_le_sum_of_subset {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedAddCommMonoid M] {f : ι → M} {s : Finset ι} {t : Finset ι} (h : s ⊆ t) : (Finset.sum s fun (x : ι) => f x) ≤ Finset.sum t fun (x : ι) => f x

theorem Finset.prod_le_prod_of_subset' {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedCommMonoid M] {f : ι → M} {s : Finset ι} {t : Finset ι} (h : s ⊆ t) : (Finset.prod s fun (x : ι) => f x) ≤ Finset.prod t fun (x : ι) => f x

theorem Finset.sum_mono_set {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedAddCommMonoid M] (f : ι → M) : Monotone fun (s : Finset ι) => Finset.sum s fun (x : ι) => f x

theorem Finset.prod_mono_set' {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedCommMonoid M] (f : ι → M) : Monotone fun (s : Finset ι) => Finset.prod s fun (x : ι) => f x

theorem Finset.sum_le_sum_of_ne_zero {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedAddCommMonoid M] {f : ι → M} {s : Finset ι} {t : Finset ι} (h : ∀ x ∈ s, f x ≠ 0 → x ∈ t) : (Finset.sum s fun (x : ι) => f x) ≤ Finset.sum t fun (x : ι) => f x

theorem Finset.prod_le_prod_of_ne_one' {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedCommMonoid M] {f : ι → M} {s : Finset ι} {t : Finset ι} (h : ∀ x ∈ s, f x ≠ 1 → x ∈ t) : (Finset.prod s fun (x : ι) => f x) ≤ Finset.prod t fun (x : ι) => f x

theorem Finset.sum_lt_sum {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ι → M} {g : ι → M} {s : Finset ι} (hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) : (Finset.sum s fun (i : ι) => f i) < Finset.sum s fun (i : ι) => g i

theorem Finset.prod_lt_prod' {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ι → M} {g : ι → M} {s : Finset ι} (hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) : (Finset.prod s fun (i : ι) => f i) < Finset.prod s fun (i : ι) => g i

theorem Finset.sum_lt_sum_of_nonempty {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ι → M} {g : ι → M} {s : Finset ι} (hs : s.Nonempty) (hlt : ∀ i ∈ s, f i < g i) : (Finset.sum s fun (i : ι) => f i) < Finset.sum s fun (i : ι) => g i

theorem Finset.prod_lt_prod_of_nonempty' {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ι → M} {g : ι → M} {s : Finset ι} (hs : s.Nonempty) (hlt : ∀ i ∈ s, f i < g i) : (Finset.prod s fun (i : ι) => f i) < Finset.prod s fun (i : ι) => g i

theorem GCongr.sum_lt_sum_of_nonempty {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ι → M} {g : ι → M} {s : Finset ι} (hs : s.Nonempty) (Hlt : ∀ i ∈ s, f i < g i) : Finset.sum s f < Finset.sum s g

In an ordered additive commutative monoid, if each summand f i of one nontrivial finite sum is strictly less than the corresponding summand g i of another nontrivial finite sum, then s.sum f < s.sum g.

This is a variant (beta-reduced) version of the standard lemma Finset.sum_lt_sum_of_nonempty, convenient for the gcongr tactic.

theorem GCongr.prod_lt_prod_of_nonempty' {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ι → M} {g : ι → M} {s : Finset ι} (hs : s.Nonempty) (Hlt : ∀ i ∈ s, f i < g i) : Finset.prod s f < Finset.prod s g

In an ordered commutative monoid, if each factor f i of one nontrivial finite product is strictly less than the corresponding factor g i of another nontrivial finite product, then s.prod f < s.prod g.

This is a variant (beta-reduced) version of the standard lemma Finset.prod_lt_prod_of_nonempty', convenient for the gcongr tactic.

theorem Finset.sum_lt_sum_of_subset {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ι → M} {s : Finset ι} {t : Finset ι} (h : s ⊆ t) {i : ι} (ht : i ∈ t) (hs : i ∉ s) (hlt : 0 < f i) (hle : ∀ j ∈ t, j ∉ s → 0 ≤ f j) : (Finset.sum s fun (j : ι) => f j) < Finset.sum t fun (j : ι) => f j

theorem Finset.prod_lt_prod_of_subset' {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ι → M} {s : Finset ι} {t : Finset ι} (h : s ⊆ t) {i : ι} (ht : i ∈ t) (hs : i ∉ s) (hlt : 1 < f i) (hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j) : (Finset.prod s fun (j : ι) => f j) < Finset.prod t fun (j : ι) => f j

theorem Finset.single_lt_sum {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ι → M} {s : Finset ι} {i : ι} {j : ι} (hij : j ≠ i) (hi : i ∈ s) (hj : j ∈ s) (hlt : 0 < f j) (hle : ∀ k ∈ s, k ≠ i → 0 ≤ f k) : f i < Finset.sum s fun (k : ι) => f k

theorem Finset.single_lt_prod' {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ι → M} {s : Finset ι} {i : ι} {j : ι} (hij : j ≠ i) (hi : i ∈ s) (hj : j ∈ s) (hlt : 1 < f j) (hle : ∀ k ∈ s, k ≠ i → 1 ≤ f k) : f i < Finset.prod s fun (k : ι) => f k

theorem Finset.sum_pos {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ι → M} {s : Finset ι} (h : ∀ i ∈ s, 0 < f i) (hs : s.Nonempty) : 0 < Finset.sum s fun (i : ι) => f i

theorem Finset.one_lt_prod {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ι → M} {s : Finset ι} (h : ∀ i ∈ s, 1 < f i) (hs : s.Nonempty) : 1 < Finset.prod s fun (i : ι) => f i

theorem Finset.sum_neg {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ι → M} {s : Finset ι} (h : ∀ i ∈ s, f i < 0) (hs : s.Nonempty) : (Finset.sum s fun (i : ι) => f i) < 0

theorem Finset.prod_lt_one {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ι → M} {s : Finset ι} (h : ∀ i ∈ s, f i < 1) (hs : s.Nonempty) : (Finset.prod s fun (i : ι) => f i) < 1

theorem Finset.sum_pos' {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ι → M} {s : Finset ι} (h : ∀ i ∈ s, 0 ≤ f i) (hs : ∃ i ∈ s, 0 < f i) : 0 < Finset.sum s fun (i : ι) => f i

theorem Finset.one_lt_prod' {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ι → M} {s : Finset ι} (h : ∀ i ∈ s, 1 ≤ f i) (hs : ∃ i ∈ s, 1 < f i) : 1 < Finset.prod s fun (i : ι) => f i

theorem Finset.sum_neg' {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ι → M} {s : Finset ι} (h : ∀ i ∈ s, f i ≤ 0) (hs : ∃ i ∈ s, f i < 0) : (Finset.sum s fun (i : ι) => f i) < 0

theorem Finset.prod_lt_one' {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ι → M} {s : Finset ι} (h : ∀ i ∈ s, f i ≤ 1) (hs : ∃ i ∈ s, f i < 1) : (Finset.prod s fun (i : ι) => f i) < 1

theorem Finset.sum_eq_sum_iff_of_le {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {s : Finset ι} {f : ι → M} {g : ι → M} (h : ∀ i ∈ s, f i ≤ g i) : ((Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => g i) ↔ ∀ i ∈ s, f i = g i

theorem Finset.prod_eq_prod_iff_of_le {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {s : Finset ι} {f : ι → M} {g : ι → M} (h : ∀ i ∈ s, f i ≤ g i) : ((Finset.prod s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => g i) ↔ ∀ i ∈ s, f i = g i

theorem Finset.sum_sdiff_le_sum_sdiff {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ι → M} {s : Finset ι} {t : Finset ι} [DecidableEq ι] : ((Finset.sum (s \ t) fun (i : ι) => f i) ≤ Finset.sum (t \ s) fun (i : ι) => f i) ↔ (Finset.sum s fun (i : ι) => f i) ≤ Finset.sum t fun (i : ι) => f i

theorem Finset.prod_sdiff_le_prod_sdiff {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ι → M} {s : Finset ι} {t : Finset ι} [DecidableEq ι] : ((Finset.prod (s \ t) fun (i : ι) => f i) ≤ Finset.prod (t \ s) fun (i : ι) => f i) ↔ (Finset.prod s fun (i : ι) => f i) ≤ Finset.prod t fun (i : ι) => f i

theorem Finset.sum_sdiff_lt_sum_sdiff {ι : Type u_1} {M : Type u_4} [OrderedCancelAddCommMonoid M] {f : ι → M} {s : Finset ι} {t : Finset ι} [DecidableEq ι] : ((Finset.sum (s \ t) fun (i : ι) => f i) < Finset.sum (t \ s) fun (i : ι) => f i) ↔ (Finset.sum s fun (i : ι) => f i) < Finset.sum t fun (i : ι) => f i

theorem Finset.prod_sdiff_lt_prod_sdiff {ι : Type u_1} {M : Type u_4} [OrderedCancelCommMonoid M] {f : ι → M} {s : Finset ι} {t : Finset ι} [DecidableEq ι] : ((Finset.prod (s \ t) fun (i : ι) => f i) < Finset.prod (t \ s) fun (i : ι) => f i) ↔ (Finset.prod s fun (i : ι) => f i) < Finset.prod t fun (i : ι) => f i

theorem Finset.exists_lt_of_sum_lt {ι : Type u_1} {M : Type u_4} [LinearOrderedCancelAddCommMonoid M] {f : ι → M} {g : ι → M} {s : Finset ι} (Hlt : (Finset.sum s fun (i : ι) => f i) < Finset.sum s fun (i : ι) => g i) : ∃ i ∈ s, f i < g i

theorem Finset.exists_lt_of_prod_lt' {ι : Type u_1} {M : Type u_4} [LinearOrderedCancelCommMonoid M] {f : ι → M} {g : ι → M} {s : Finset ι} (Hlt : (Finset.prod s fun (i : ι) => f i) < Finset.prod s fun (i : ι) => g i) : ∃ i ∈ s, f i < g i

theorem Finset.exists_le_of_sum_le {ι : Type u_1} {M : Type u_4} [LinearOrderedCancelAddCommMonoid M] {f : ι → M} {g : ι → M} {s : Finset ι} (hs : s.Nonempty) (Hle : (Finset.sum s fun (i : ι) => f i) ≤ Finset.sum s fun (i : ι) => g i) : ∃ i ∈ s, f i ≤ g i

theorem Finset.exists_le_of_prod_le' {ι : Type u_1} {M : Type u_4} [LinearOrderedCancelCommMonoid M] {f : ι → M} {g : ι → M} {s : Finset ι} (hs : s.Nonempty) (Hle : (Finset.prod s fun (i : ι) => f i) ≤ Finset.prod s fun (i : ι) => g i) : ∃ i ∈ s, f i ≤ g i

theorem Finset.exists_pos_of_sum_zero_of_exists_nonzero {ι : Type u_1} {M : Type u_4} [LinearOrderedCancelAddCommMonoid M] {s : Finset ι} (f : ι → M) (h₁ : (Finset.sum s fun (i : ι) => f i) = 0) (h₂ : ∃ i ∈ s, f i ≠ 0) : ∃ i ∈ s, 0 < f i

theorem Finset.exists_one_lt_of_prod_one_of_exists_ne_one' {ι : Type u_1} {M : Type u_4} [LinearOrderedCancelCommMonoid M] {s : Finset ι} (f : ι → M) (h₁ : (Finset.prod s fun (i : ι) => f i) = 1) (h₂ : ∃ i ∈ s, f i ≠ 1) : ∃ i ∈ s, 1 < f i

theorem Fintype.sum_mono {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedAddCommMonoid M] : Monotone fun (f : ι → M) => Finset.sum Finset.univ fun (i : ι) => f i

theorem Fintype.prod_mono' {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCommMonoid M] : Monotone fun (f : ι → M) => Finset.prod Finset.univ fun (i : ι) => f i

theorem Fintype.sum_nonneg {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedAddCommMonoid M] {f : ι → M} (hf : 0 ≤ f) : 0 ≤ Finset.sum Finset.univ fun (i : ι) => f i

theorem Fintype.one_le_prod {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCommMonoid M] {f : ι → M} (hf : 1 ≤ f) : 1 ≤ Finset.prod Finset.univ fun (i : ι) => f i

theorem Fintype.sum_nonpos {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedAddCommMonoid M] {f : ι → M} (hf : f ≤ 0) : (Finset.sum Finset.univ fun (i : ι) => f i) ≤ 0

theorem Fintype.prod_le_one {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCommMonoid M] {f : ι → M} (hf : f ≤ 1) : (Finset.prod Finset.univ fun (i : ι) => f i) ≤ 1

theorem Fintype.sum_eq_zero_iff_of_nonneg {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedAddCommMonoid M] {f : ι → M} (hf : 0 ≤ f) : (Finset.sum Finset.univ fun (i : ι) => f i) = 0 ↔ f = 0

theorem Fintype.prod_eq_one_iff_of_one_le {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCommMonoid M] {f : ι → M} (hf : 1 ≤ f) : (Finset.prod Finset.univ fun (i : ι) => f i) = 1 ↔ f = 1

theorem Fintype.sum_eq_zero_iff_of_nonpos {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedAddCommMonoid M] {f : ι → M} (hf : f ≤ 0) : (Finset.sum Finset.univ fun (i : ι) => f i) = 0 ↔ f = 0

theorem Fintype.prod_eq_one_iff_of_le_one {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCommMonoid M] {f : ι → M} (hf : f ≤ 1) : (Finset.prod Finset.univ fun (i : ι) => f i) = 1 ↔ f = 1

abbrev Fintype.sum_strictMono.match_1 {ι : Type u_1} {M : Type u_2} [OrderedCancelAddCommMonoid M] : ∀ (x x_1 : ι → M) (motive : (x ≤ x_1 ∧ ∃ (i : ι), x i < x_1 i) → Prop) (x_2 : x ≤ x_1 ∧ ∃ (i : ι), x i < x_1 i), (∀ (hle : x ≤ x_1) (i : ι) (hlt : x i < x_1 i), motive ⋯) → motive x_2

Equations

• ⋯ = ⋯

theorem Fintype.sum_strictMono {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelAddCommMonoid M] : StrictMono fun (f : ι → M) => Finset.sum Finset.univ fun (x : ι) => f x

theorem Fintype.prod_strictMono' {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelCommMonoid M] : StrictMono fun (f : ι → M) => Finset.prod Finset.univ fun (x : ι) => f x

theorem Fintype.sum_pos {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelAddCommMonoid M] {f : ι → M} (hf : 0 < f) : 0 < Finset.sum Finset.univ fun (i : ι) => f i

theorem Fintype.one_lt_prod {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelCommMonoid M] {f : ι → M} (hf : 1 < f) : 1 < Finset.prod Finset.univ fun (i : ι) => f i

theorem Fintype.sum_neg {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelAddCommMonoid M] {f : ι → M} (hf : f < 0) : (Finset.sum Finset.univ fun (i : ι) => f i) < 0

theorem Fintype.prod_lt_one {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelCommMonoid M] {f : ι → M} (hf : f < 1) : (Finset.prod Finset.univ fun (i : ι) => f i) < 1

theorem Fintype.sum_pos_iff_of_nonneg {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelAddCommMonoid M] {f : ι → M} (hf : 0 ≤ f) : (0 < Finset.sum Finset.univ fun (i : ι) => f i) ↔ 0 < f

theorem Fintype.one_lt_prod_iff_of_one_le {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelCommMonoid M] {f : ι → M} (hf : 1 ≤ f) : (1 < Finset.prod Finset.univ fun (i : ι) => f i) ↔ 1 < f

theorem Fintype.sum_neg_iff_of_nonpos {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelAddCommMonoid M] {f : ι → M} (hf : f ≤ 0) : (Finset.sum Finset.univ fun (i : ι) => f i) < 0 ↔ f < 0

theorem Fintype.prod_lt_one_iff_of_le_one {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelCommMonoid M] {f : ι → M} (hf : f ≤ 1) : (Finset.prod Finset.univ fun (i : ι) => f i) < 1 ↔ f < 1

theorem Multiset.finset_sum_eq_sup_iff_disjoint {α : Type u_2} [DecidableEq α] {β : Type u_9} {i : Finset β} {f : β → Multiset α} : Finset.sum i f = Finset.sup i f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Multiset.Disjoint (f x) (f y)

theorem Multiset.sup_powerset_len {α : Type u_9} [DecidableEq α] (x : Multiset α) : (Finset.sup (Finset.range (Multiset.card x + 1)) fun (k : ℕ) => Multiset.powersetCard k x) = Multiset.powerset x

def Mathlib.Meta.Positivity.evalFinsetSum : Mathlib.Meta.Positivity.PositivityExt

The positivity extension which proves that ∑ i in s, f i is nonnegative if f is, and positive if each f i is and s is nonempty.

TODO: The following example does not work

example (s : Finset ℕ) (f : ℕ → ℤ) (hf : ∀ n, 0 ≤ f n) : 0 ≤ s.sum f := by positivity

because compareHyp can't look for assumptions behind binders.