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 (∑ i ∈ s, g i) ≤ ∑ i ∈ 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 ∈ s, g i) ≤ ∑ i ∈ 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 (∏ i ∈ s, g i) ≤ ∏ i ∈ 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 ∈ s, g x) ≤ ∏ x ∈ 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 (∑ i ∈ s, g i) ≤ ∑ i ∈ 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 ∈ s, g i) ≤ ∑ i ∈ 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 (∏ i ∈ s, g i) ≤ ∏ i ∈ 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 ∈ s, g i) ≤ ∏ i ∈ 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 (∑ i ∈ s, g i) ≤ ∑ i ∈ 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 ∈ s, g x) ≤ ∑ x ∈ 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 (∏ i ∈ s, g i) ≤ ∏ i ∈ 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 ∈ s, g i) ≤ ∏ i ∈ 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 (∑ i ∈ s, g i) ≤ ∑ i ∈ 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 ∈ s, g i) ≤ ∑ i ∈ 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 (∏ i ∈ s, g i) ≤ ∏ i ∈ 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 ∈ s, g i) ≤ ∏ i ∈ 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) : ∑ i ∈ s, f i ≤ ∑ i ∈ 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 ∈ s, f i ≤ ∑ i ∈ 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) : ∏ i ∈ s, f i ≤ ∏ i ∈ 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 ∈ s, f i ≤ ∏ i ∈ s, g i.

theorem Finset.sum_nonneg {ι : Type u_1} {N : Type u_5} [OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι} (h : ∀ i ∈ s, 0 ≤ f i) : 0 ≤ ∑ i ∈ s, 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 ≤ ∏ i ∈ s, 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 ≤ ∑ i ∈ s, 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 ≤ ∏ i ∈ s, 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) : ∑ i ∈ s, 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) : ∏ i ∈ s, 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) : ∑ i ∈ s, f i ≤ ∑ i ∈ t, 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) : ∏ i ∈ s, f i ≤ ∏ i ∈ t, 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 ι) => ∑ x ∈ s, 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 ι) => ∏ x ∈ s, 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) : ∑ x ∈ s, f x ≤ ∑ 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) : ∏ x ∈ s, f x ≤ ∏ 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) → (∑ i ∈ s, 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) → (∏ i ∈ s, 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) → (∑ i ∈ s, 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) → (∏ i ∈ s, 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 ≤ ∑ x ∈ s, 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 ≤ ∏ x ∈ s, 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 ≤ ∑ k ∈ s, 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 ≤ ∏ k ∈ s, 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) : s.sum 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) : s.prod 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 ≤ s.sum 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 ≤ s.prod 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) : (s.biUnion 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 ≤ ∑ x ∈ Finset.filter (fun (x : ι) => g x = y) s, f x) : ∑ y ∈ t, ∑ x ∈ Finset.filter (fun (x : ι) => g x = y) s, f x ≤ ∑ x ∈ s, 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 ≤ ∏ x ∈ Finset.filter (fun (x : ι) => g x = y) s, f x) : ∏ y ∈ t, ∏ x ∈ Finset.filter (fun (x : ι) => g x = y) s, f x ≤ ∏ x ∈ s, 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, ∑ x ∈ Finset.filter (fun (x : ι) => g x = y) s, f x ≤ 0) : ∑ x ∈ s, f x ≤ ∑ y ∈ t, ∑ x ∈ Finset.filter (fun (x : ι) => g x = y) s, 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, ∏ x ∈ Finset.filter (fun (x : ι) => g x = y) s, f x ≤ 1) : ∏ x ∈ s, f x ≤ ∏ y ∈ t, ∏ x ∈ Finset.filter (fun (x : ι) => g x = y) s, f x

theorem Finset.abs_sum_le_sum_abs {ι : Type u_1} {G : Type u_9} [LinearOrderedAddCommGroup G] (f : ι → G) (s : Finset ι) : |∑ i ∈ s, f i| ≤ ∑ i ∈ s, |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) : |∑ i ∈ s, f i| = ∑ i ∈ s, 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) : |∑ i ∈ s, f i| = ∑ i ∈ s, f i

@[simp]

theorem Finset.addLECancellable_sum {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {s : Finset ι} {f : ι → α} : AddLECancellable (∑ i ∈ s, f i) ↔ ∀ ⦃i : ι⦄, i ∈ s → AddLECancellable (f i)

@[simp]

theorem Finset.mulLECancellable_prod {ι : Type u_1} {α : Type u_2} [CommMonoid α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {s : Finset ι} {f : ι → α} : MulLECancellable (∏ i ∈ s, f i) ↔ ∀ ⦃i : ι⦄, i ∈ s → MulLECancellable (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) : ∑ t ∈ 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} [DecidableEq α] {B : Finset (Finset α)} {n : ℕ} [Fintype α] (h : ∀ (a : α), (Finset.filter (fun (x : Finset α) => a ∈ x) B).card ≤ n) : ∑ s ∈ 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} [DecidableEq α] {s : Finset α} {B : Finset (Finset α)} {n : ℕ} (h : ∀ a ∈ s, n ≤ (Finset.filter (fun (x : Finset α) => a ∈ x) B).card) : s.card * n ≤ ∑ t ∈ 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} [DecidableEq α] {B : Finset (Finset α)} {n : ℕ} [Fintype α] (h : ∀ (a : α), n ≤ (Finset.filter (fun (x : Finset α) => a ∈ x) B).card) : Fintype.card α * n ≤ ∑ s ∈ 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} [DecidableEq α] {s : Finset α} {B : Finset (Finset α)} {n : ℕ} (h : ∀ a ∈ s, (Finset.filter (fun (x : Finset α) => a ∈ x) B).card = n) : ∑ t ∈ 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} [DecidableEq α] {B : Finset (Finset α)} {n : ℕ} [Fintype α] (h : ∀ (a : α), (Finset.filter (fun (x : Finset α) => a ∈ x) B).card = n) : ∑ s ∈ 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_biUnion {ι : Type u_1} {α : Type u_2} [DecidableEq α] {s : Finset ι} {f : ι → Finset α} (hs : (↑s).PairwiseDisjoint f) (hf : ∀ i ∈ s, (f i).Nonempty) : s.card ≤ (s.biUnion f).card

theorem Finset.card_le_card_biUnion_add_card_fiber {ι : Type u_1} {α : Type u_2} [DecidableEq α] {s : Finset ι} {f : ι → Finset α} (hs : (↑s).PairwiseDisjoint f) : s.card ≤ (s.biUnion 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 : (↑s).PairwiseDisjoint f) : s.card ≤ (s.biUnion 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 ≤ ∑ j ∈ s, 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 ≤ ∏ j ∈ s, 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 ι} : ∑ x ∈ s, 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 ι} : ∏ x ∈ s, 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) : ∑ x ∈ s, f x ≤ ∑ x ∈ t, 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) : ∏ x ∈ s, f x ≤ ∏ x ∈ t, f x

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

theorem Finset.prod_mono_set' {ι : Type u_1} {M : Type u_4} [CanonicallyOrderedCommMonoid M] (f : ι → M) : Monotone fun (s : Finset ι) => ∏ x ∈ s, 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) : ∑ x ∈ s, f x ≤ ∑ x ∈ t, 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) : ∏ x ∈ s, f x ≤ ∏ x ∈ t, 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) : ∑ i ∈ s, f i < ∑ i ∈ s, 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) : ∏ i ∈ s, f i < ∏ i ∈ s, 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) : ∑ i ∈ s, f i < ∑ i ∈ s, g i

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.

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) : ∏ i ∈ s, f i < ∏ i ∈ s, g i

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.

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) : ∑ j ∈ s, f j < ∑ j ∈ t, 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) : ∏ j ∈ s, f j < ∏ j ∈ t, 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 < ∑ k ∈ s, 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 < ∏ k ∈ s, 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 < ∑ i ∈ s, 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 < ∏ i ∈ s, 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) : ∑ i ∈ s, 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) : ∏ i ∈ s, 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 < ∑ i ∈ s, 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 < ∏ i ∈ s, 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) : ∑ i ∈ s, 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) : ∏ i ∈ s, 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) : ∑ i ∈ s, f i = ∑ i ∈ s, 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) : ∏ i ∈ s, f i = ∏ i ∈ s, 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 ι] : ∑ i ∈ s \ t, f i ≤ ∑ i ∈ t \ s, f i ↔ ∑ i ∈ s, f i ≤ ∑ i ∈ t, 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 ι] : ∏ i ∈ s \ t, f i ≤ ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i ≤ ∏ i ∈ t, 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 ι] : ∑ i ∈ s \ t, f i < ∑ i ∈ t \ s, f i ↔ ∑ i ∈ s, f i < ∑ i ∈ t, 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 ι] : ∏ i ∈ s \ t, f i < ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i < ∏ i ∈ t, 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 : ∑ i ∈ s, f i < ∑ i ∈ s, 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 : ∏ i ∈ s, f i < ∏ i ∈ s, 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 : ∑ i ∈ s, f i ≤ ∑ i ∈ s, 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 : ∏ i ∈ s, f i ≤ ∏ i ∈ s, 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₁ : ∑ i ∈ s, 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₁ : ∏ i ∈ s, 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) => ∑ i : ι, f i

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

theorem Fintype.sum_nonneg {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedAddCommMonoid M] {f : ι → M} (hf : 0 ≤ f) : 0 ≤ ∑ i : ι, f i

theorem Fintype.one_le_prod {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCommMonoid M] {f : ι → M} (hf : 1 ≤ f) : 1 ≤ ∏ i : ι, f i

theorem Fintype.sum_nonpos {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedAddCommMonoid M] {f : ι → M} (hf : f ≤ 0) : ∑ i : ι, f i ≤ 0

theorem Fintype.prod_le_one {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCommMonoid M] {f : ι → M} (hf : f ≤ 1) : ∏ 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) : ∑ 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) : ∏ 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) : ∑ 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) : ∏ i : ι, f i = 1 ↔ f = 1

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

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

theorem Fintype.sum_pos {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelAddCommMonoid M] {f : ι → M} (hf : 0 < f) : 0 < ∑ i : ι, f i

theorem Fintype.one_lt_prod {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelCommMonoid M] {f : ι → M} (hf : 1 < f) : 1 < ∏ i : ι, f i

theorem Fintype.sum_neg {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelAddCommMonoid M] {f : ι → M} (hf : f < 0) : ∑ i : ι, f i < 0

theorem Fintype.prod_lt_one {ι : Type u_1} {M : Type u_4} [Fintype ι] [OrderedCancelCommMonoid M] {f : ι → M} (hf : f < 1) : ∏ 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 < ∑ 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 < ∏ 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) : ∑ 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) : ∏ 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 α} : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → (f x).Disjoint (f y)

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

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

The positivity extension which proves that ∑ i ∈ 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.