Finset.sum_eq_zero_iff_of_nonneg
theorem Finset.sum_eq_zero_iff_of_nonneg :
∀ {ι : Type u_1} {N : Type u_5} [inst : OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι},
(∀ i ∈ s, 0 ≤ f i) → ((s.sum fun i => f i) = 0 ↔ ∀ i ∈ s, f i = 0)
The theorem `Finset.sum_eq_zero_iff_of_nonneg` states that for any type `ι`, any `OrderedAddCommMonoid` `N`, any function `f` from `ι` to `N`, and any finite set `s` of elements from type `ι`, if every element `i` in the set `s` is such that `f(i)` is non-negative (i.e., `0 ≤ f i`), then the sum of `f(i)` for all `i` in the set `s` (represented as `Finset.sum s f`) being zero is equivalent to each `f(i)` for all `i` in `s` being zero. In other words, if all the function values are non-negative, the sum is zero if and only if every function value is zero.
More concisely: For any OrderedAddCommMonoid N, function f from ι to N, and finite set s of ι, if ∀ i ∈ s, 0 ≤ f i then Finset.sum s f = 0 if and only if ∀ i ∈ s, f i = 0.
|
GCongr.sum_lt_sum_of_nonempty
theorem GCongr.sum_lt_sum_of_nonempty :
∀ {ι : Type u_1} {M : Type u_4} [inst : OrderedCancelAddCommMonoid M] {f g : ι → M} {s : Finset ι},
s.Nonempty → (∀ i ∈ s, f i < g i) → s.sum f < s.sum g
This theorem states that, in the context of an ordered additive commutative monoid, if we have two non-empty finite sums, where each summand `f i` of the first sum is strictly less than the corresponding summand `g i` of the second sum, then the total of the first sum is less than the total of the second sum. The theorem is a simplified version of the standard lemma `Finset.sum_lt_sum_of_nonempty`, designed to be useful for the `gcongr` tactic.
More concisely: In an ordered additive commutative monoid, if every summand of the first finite sum is strictly smaller than the corresponding summand of the second finite sum, then the total of the first sum is less than the total of the second sum.
|
Finset.sum_mono_set
theorem Finset.sum_mono_set :
∀ {ι : Type u_1} {M : Type u_4} [inst : CanonicallyOrderedAddCommMonoid M] (f : ι → M),
Monotone fun s => s.sum fun x => f x
The theorem `Finset.sum_mono_set` states that for any type `ι`, any type `M` that is a canonically ordered commutative monoid with an additive identity, and any function `f` from `ι` to `M`, the function that takes a finite set `s` of elements from `ι` and maps it to the sum of `f(x)` for all `x` in `s` is monotone. In other words, if `s` and `t` are two finite sets of elements from `ι` such that `s` is a subset of `t`, then the sum of `f(x)` over all `x` in `s` is less than or equal to the sum of `f(x)` over all `x` in `t`. This is due to the fact that adding more terms in the sum (when moving from `s` to `t`) cannot decrease the total sum, given that `M` is a canonically ordered commutative monoid (i.e., an algebraic structure where addition is commutative, associative, and has an identity, and where the order relation is compatible with the addition).
More concisely: Given a type `ι`, a canonically ordered commutative monoid `M` with an additive identity, and a function `f` from `ι` to `M`, the sum function `s => ∑ x in s, f x` is monotone on finite sets `s` of `ι`.
|
Finset.sum_card_inter
theorem Finset.sum_card_inter :
∀ {α : Type u_2} [inst : DecidableEq α] {s : Finset α} {B : Finset (Finset α)} {n : ℕ},
(∀ a ∈ s, (Finset.filter (fun x => a ∈ x) B).card = n) → (B.sum fun t => (s ∩ t).card) = s.card * n
The theorem `Finset.sum_card_inter` states that for any type `α` with a decidable equality, a given Finset `s` of type `α`, a Finset `B` of Finsets of type `α`, and a natural number `n`, if every element of `s` belongs to exactly `n` Finsets in `B`, then the sum of the sizes of the intersections of `s` and each Finset in `B` is equal to the size of `s` multiplied by `n`. In simpler terms, if each element in `s` is found in `n` number of sets in `B`, then the total number of elements over all intersections of `s` and the sets in `B` is `n` times the number of elements in `s`.
More concisely: For a decidably equal type `α`, given a Finset `s` of `α`, a Finset `B` of Finsets of `α`, and a natural number `n`, if every element of `s` is in exactly `n` Finsets in `B`, then the sum of the sizes of the intersections of `s` and each Finset in `B` equals the product of `n` and the size of `s`.
|
Finset.le_sum_of_subadditive_on_pred
theorem Finset.le_sum_of_subadditive_on_pred :
∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N]
(f : M → N) (p : M → Prop),
f 0 = 0 →
(∀ (x y : M), p x → p y → f (x + y) ≤ f x + f y) →
(∀ (x y : M), p x → p y → p (x + y)) →
∀ (g : ι → M) {s : Finset ι}, (∀ i ∈ s, p (g i)) → f (s.sum fun i => g i) ≤ s.sum fun i => f (g i)
This theorem states that if we have a subsemigroup `{x | p x}` of a commutative additive monoid `M`, and a map `f: M -> N` such that `f 0 = 0` and `f` is subadditive on this subsemigroup, i.e., for all `x` and `y` satisfying predicate `p`, `f (x + y) ≤ f x + f y`. Further, we have a finite family of elements `g i` where `i` belongs to a set `s`, and each of these elements satisfies the predicate `p`. Under these conditions, the value of `f` applied to the sum of the `g i`'s is less than or equal to the sum of the values of `f` applied to each `g i` individually.
More concisely: If `{x | p x}` is a subsemigroup of a commutative additive monoid `M`, `f: M -> N` is a map with `f 0 = 0` and subadditive on `{x | p x}`, and `g i` (i in some set `s`) are elements of `{x | p x}`, then `Σ i in s, f (g i) ≤ f (Σ i in s, g i)`.
|
Finset.single_le_sum
theorem Finset.single_le_sum :
∀ {ι : Type u_1} {N : Type u_5} [inst : OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι},
(∀ i ∈ s, 0 ≤ f i) → ∀ {a : ι}, a ∈ s → f a ≤ s.sum fun x => f x
The theorem `Finset.single_le_sum` states that for any type `ι`, type `N` which is an ordered additive commutative monoid, a function `f` from `ι` to `N`, and a finite set `s` of type `ι`, if each element `i` of the set `s` when applied to the function `f` results in a non-negative value, then for any element `a` of the set `s`, the value of the function `f` at `a` is less than or equal to the sum of the function `f` applied to each element of the set `s`. In other words, the value of a single application of the function `f` is always less than or equal to the sum of the values of the function `f` over all elements of the set `s`, given that the function `f` returns non-negative values for all elements of `s`.
More concisely: For any ordered additive commutative monoid N, function f from a finite set s to N with non-negative values, and all a in s, we have f a ≤ ∑ i in s f i.
|
Finset.le_sum_nonempty_of_subadditive_on_pred
theorem Finset.le_sum_nonempty_of_subadditive_on_pred :
∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N]
(f : M → N) (p : M → Prop),
(∀ (x y : M), p x → p y → f (x + y) ≤ f x + f y) →
(∀ (x y : M), p x → p y → p (x + y)) →
∀ (g : ι → M) (s : Finset ι),
s.Nonempty → (∀ i ∈ s, p (g i)) → f (s.sum fun i => g i) ≤ s.sum fun i => f (g i)
This theorem states that if we have an additive subsemigroup of an additive commutative monoid `M` denoted as `{x | p x}` and a map `f : M → N` that is subadditive on `{x | p x}` (i.e., `f (x + y) ≤ f x + f y` for any `x, y` satisfying `p`), then for any nonempty finite family of elements `g i` in `M` (for each `i` in a finite set `s`) that satisfy `p`, the function `f` applied to the sum of the family elements is less than or equal to the sum of the function `f` applied to each element of the family. In other words, if `f` is subadditive on `{x | p x}`, it preserves the order under the operation of sum in a finite nonempty family of elements that satisfy `p`.
More concisely: If `f : {x in M | p x} -> N` is subadditive on the additive subsemigroup `{x in M | p x}`, then for any finite nonempty family `(g i : M)_i in s` satisfying `p`, we have `f (sum i in s g i) <= sum i in s (f g i)`.
|
Finset.sum_lt_sum
theorem Finset.sum_lt_sum :
∀ {ι : Type u_1} {M : Type u_4} [inst : OrderedCancelAddCommMonoid M] {f g : ι → M} {s : Finset ι},
(∀ i ∈ s, f i ≤ g i) → (∃ i ∈ s, f i < g i) → (s.sum fun i => f i) < s.sum fun i => g i
The theorem `Finset.sum_lt_sum` states that for any finite set `s` of a certain type `ι` and for any two functions `f` and `g` from `ι` to a type `M` (which is an ordered cancel additive commutative monoid), if for each element `i` in `s`, `f(i)` is less than or equal to `g(i)` and there exists an element `i` in `s` for which `f(i)` is strictly less than `g(i)`, then the sum of `f(i)` over all `i` in `s` is strictly less than the sum of `g(i)` over all `i` in `s`. In other words, if every value of `f` is less than or equal to the corresponding value of `g` and at least one value of `f` is strictly less, then the total sum of `f`'s values is strictly less than the total sum of `g`'s values.
More concisely: If `f` and `g` are functions from a finite set `s` to an ordered cancel additive commutative monoid, where `f(i) ≤ g(i)` for all `i` in `s` and there exists an `i` in `s` with `f(i) < g(i)`, then `∑(i in s) f(i) < ∑(i in s) g(i)`.
|
Finset.prod_lt_prod_of_nonempty'
theorem Finset.prod_lt_prod_of_nonempty' :
∀ {ι : Type u_1} {M : Type u_4} [inst : OrderedCancelCommMonoid M] {f g : ι → M} {s : Finset ι},
s.Nonempty → (∀ i ∈ s, f i < g i) → (s.prod fun i => f i) < s.prod fun i => g i
The theorem `Finset.prod_lt_prod_of_nonempty'` states that for any nonempty finite set `s` of elements of any type `ι`, and for any two functions `f` and `g` from `ι` to a type `M` that has an ordered cancelable commutative monoid structure, if every element `i` in `s` satisfies `f(i) < g(i)`, then the product of `f(i)` as `i` ranges over `s` is strictly less than the product of `g(i)` as `i` ranges over `s`. In mathematical notation, if `s` is nonempty and $\forall i \in s, f(i) < g(i)$, then $\prod_{i \in s} f(i) < \prod_{i \in s} g(i)$.
More concisely: If `s` is a nonempty finite set and `f(i) < g(i)` for all `i` in `s`, then $\prod\_{i \in s} f(i) < \prod\_{i \in s} g(i)$.
|
GCongr.prod_le_prod'
theorem GCongr.prod_le_prod' :
∀ {ι : Type u_1} {N : Type u_5} [inst : OrderedCommMonoid N] {f g : ι → N} {s : Finset ι},
(∀ i ∈ s, f i ≤ g i) → s.prod f ≤ s.prod g
This theorem states that in an ordered commutative monoid, if each factor `f i` of a finite product is less than or equal to the corresponding factor `g i` of another finite product, then the entire product of `f i`'s is less than or equal to the entire product of `g i`'s. Here, `f` and `g` are functions that map from some type `ι` to the monoid `N`, and `s` is a finite set of elements from `ι`. This theorem is a simplified version of the standard lemma `Finset.prod_le_prod'`, designed to be useful for the `gcongr` tactic.
More concisely: In an ordered commutative monoid, if for all i in a finite set s, fi ≤ gi holds, then ∏(fi) ≤ ∏(gi).
|
GCongr.sum_le_sum
theorem GCongr.sum_le_sum :
∀ {ι : Type u_1} {N : Type u_5} [inst : OrderedAddCommMonoid N] {f g : ι → N} {s : Finset ι},
(∀ i ∈ s, f i ≤ g i) → s.sum f ≤ s.sum g
This theorem states that, within an ordered additive commutative monoid (a structure with addition as a commutative operation and an order relation compatible with the addition), if for each element `i` in a finite set `s`, the value of function `f` at `i` is less than or equal to the value of function `g` at `i`, then the sum of values of `f` over `s` is less than or equal to the sum of values of `g` over `s`. In other words, if each term of one sum is not greater than the corresponding term of another sum, then the total of the first sum is not greater than the total of the second sum. This is a useful theorem when working with inequalities involving sums in an ordered additively commutative structure.
More concisely: If `f` and `g` are functions on a finite set `s` in an ordered additive commutative monoid such that `f i ≤ gi` for all `i ∈ s`, then `∑ i in s f i ≤ ∑ i in s gi`.
|
Finset.le_prod_nonempty_of_submultiplicative_on_pred
theorem Finset.le_prod_nonempty_of_submultiplicative_on_pred :
∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : CommMonoid M] [inst_1 : OrderedCommMonoid N] (f : M → N)
(p : M → Prop),
(∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y) →
(∀ (x y : M), p x → p y → p (x * y)) →
∀ (g : ι → M) (s : Finset ι),
s.Nonempty → (∀ i ∈ s, p (g i)) → f (s.prod fun i => g i) ≤ s.prod fun i => f (g i)
This theorem states that if you have a subset of a commutative monoid `M`, denoted `{x | p x}`, which forms a subsemigroup, and a map `f` from `M` to `N` that is submultiplicative on that subset (i.e., for any `x` and `y` in that subset, `f(x * y)` is less than or equal to `f(x) * f(y)`), then for any nonempty finite family of elements `g i` of `M` (for `i` in some set `s`), where each `g i` satisfies the property `p`, it follows that `f` of the product of the `g i` (over all `i` in `s`) is less than or equal to the product of `f(g i)` (over all `i` in `s`).
In other words, if `f` is submultiplicative on a subsemigroup, then applying `f` to the product of a nonempty family of elements from that subsemigroup is no greater than the product of applying `f` to each element individually.
More concisely: If `f` is a submultiplicative map from a subsemigroup `{x | p x}` of a commutative monoid `M` to a monoid `N`, then for any finite nonempty family `(g\_i)_i` of elements of `{x | p x}`, `f(∏\_i g\_i) ≤ ∏\_i f(g\_i)`.
|
Finset.sum_pos
theorem Finset.sum_pos :
∀ {ι : Type u_1} {M : Type u_4} [inst : OrderedCancelAddCommMonoid M] {f : ι → M} {s : Finset ι},
(∀ i ∈ s, 0 < f i) → s.Nonempty → 0 < s.sum fun i => f i
The theorem `Finset.sum_pos` states that for any type `ι`, any `M` which is an ordered, cancellative, commutative monoid, any function `f` from `ι` to `M`, and any finite set `s` of `ι`, if every element `i` in `s` has the property that `f(i)` is greater than zero, and if `s` is not empty, then the sum of `f(i)` for all `i` in `s` (denoted by `Finset.sum s fun i => f i`) is also greater than zero. In other words, the sum of positive values over a nonempty finite set is also positive.
More concisely: For any ordered, cancellative, commutative monoid M and function f from a nonempty finite set ι to M with f(i) > 0 for all i in ι, the sum of f(i) over i in ι is greater than zero.
|
Finset.le_sum_card_inter
theorem Finset.le_sum_card_inter :
∀ {α : Type u_2} [inst : DecidableEq α] {s : Finset α} {B : Finset (Finset α)} {n : ℕ},
(∀ a ∈ s, n ≤ (Finset.filter (fun x => a ∈ x) B).card) → s.card * n ≤ B.sum fun t => (s ∩ t).card
This theorem states that if every element of a finite set `s` belongs to at least `n` finite sets in a collection `B`, then the sum of the sizes of the finite sets in `B` (counting only the elements that also belong to `s`) is at least `n` times the number of elements in `s`. In other words, this theorem provides a lower bound for the sum of the sizes of intersections of `s` with the finite sets in `B`, in terms of the number of appearances of each element of `s` in the finite sets of `B`.
More concisely: If every element of a finite set `s` belongs to at least `n` sets in a collection `B` of finite sets, then the sum of the cardinalities of the intersections of `s` with sets in `B` is at least `n` times the cardinality of `s`.
|
GCongr.prod_lt_prod_of_nonempty'
theorem GCongr.prod_lt_prod_of_nonempty' :
∀ {ι : Type u_1} {M : Type u_4} [inst : OrderedCancelCommMonoid M] {f g : ι → M} {s : Finset ι},
s.Nonempty → (∀ i ∈ s, f i < g i) → s.prod f < s.prod g
This theorem says that in an ordered commutative monoid, if every element `f i` in a non-empty finite set `s` is strictly smaller than the corresponding element `g i`, then the product of all elements `f i` in `s` is strictly smaller than the product of all elements `g i` in `s`. This is a streamlined version of the standard lemma `Finset.prod_lt_prod_of_nonempty'`, and is useful for the `gcongr` tactic.
More concisely: In an ordered commutative monoid, if every element of a non-empty finite set is strictly smaller than the corresponding element in another set, then the product of the elements from the first set is strictly smaller than the product of the elements from the second set.
|
Finset.prod_eq_one_iff_of_one_le'
theorem Finset.prod_eq_one_iff_of_one_le' :
∀ {ι : Type u_1} {N : Type u_5} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι},
(∀ i ∈ s, 1 ≤ f i) → ((s.prod fun i => f i) = 1 ↔ ∀ i ∈ s, f i = 1)
The theorem `Finset.prod_eq_one_iff_of_one_le'` states that for any type `ι`, any ordered commutative monoid `N`, any function `f` from `ι` to `N`, and any finite set `s` of type `ι`, if all elements `i` of `s` satisfy the condition `1 ≤ f i` (i.e., the value of the function `f` at `i` is greater than or equal to 1), then the product of all the function values `f i` for `i` in `s` is equal to 1 if and only if all the function values `f i` for `i` in `s`, are equal to 1. In mathematical terms, it says that if $\forall i \in s, 1 \leq f(i)$, then $\prod_{i \in s} f(i) = 1 \iff \forall i \in s, f(i) = 1$.
More concisely: For any ordered commutative monoid N, function f from a finite set ι to N with 1 ≤ fi for all i ∈ ι, if and only if all fi are equal to 1, then the product of all fi is equal to 1.
|
Finset.prod_le_prod'
theorem Finset.prod_le_prod' :
∀ {ι : Type u_1} {N : Type u_5} [inst : OrderedCommMonoid N] {f g : ι → N} {s : Finset ι},
(∀ i ∈ s, f i ≤ g i) → (s.prod fun i => f i) ≤ s.prod fun i => g i
This theorem states that in an ordered commutative monoid, if each element of a finite product, computed using a function `f`, is less than or equal to the corresponding element in another finite product computed using a function `g`, then the total product of `f` elements is less than or equal to the total product of `g` elements. More formally, for any `i` in a finite set `s`, if `f i` is less than or equal to `g i`, then the product of all `f i` (denoted as `∏ i in s, f i`) is less than or equal to the product of all `g i` (denoted as `∏ i in s, g i`).
More concisely: In an ordered commutative monoid, if for all elements `i` in a finite set `s`, `f i` is less than or equal to `g i`, then the product of all `f i` is less than or equal to the product of all `g i`.
|
Finset.le_sum_card
theorem Finset.le_sum_card :
∀ {α : Type u_2} [inst : DecidableEq α] {B : Finset (Finset α)} {n : ℕ} [inst_1 : Fintype α],
(∀ (a : α), n ≤ (Finset.filter (fun x => a ∈ x) B).card) → Fintype.card α * n ≤ B.sum fun s => s.card
The theorem `Finset.le_sum_card` states that for any type `α` with decidable equality, given a Finset `B` of Finsents of `α`, and a natural number `n`, if every element of the type `α` belongs to at least `n` Finsets in `B`, then the total number of elements in `α` multiplied by `n` is less than or equal to the sum of the sizes of all the Finsets in `B`. In other words, if every element is in at least `n` of the Finsets, then the total count of elements is at least `n` times the number of such elements. Here, `Fintype.card` refers to the number of elements in `α`, and `s.card` refers to the size of each Finset `s` in `B`.
More concisely: If every element in a type `α` belongs to at least `n` Finsets in a Finset `B` of `α`, then the sum of the sizes of all Finsets in `B` is greater than or equal to the product of the number of elements in `α` and `n`.
|
Finset.sum_nonneg
theorem Finset.sum_nonneg :
∀ {ι : Type u_1} {N : Type u_5} [inst : OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι},
(∀ i ∈ s, 0 ≤ f i) → 0 ≤ s.sum fun i => f i
This theorem states that if we have a function `f : ι → N`, where `ι` is an arbitrary type and `N` is an ordered additive commutative monoid, and a finite set `s` of elements of type `ι`, then if every element `i` in `s` satisfies the condition that `f(i)` is greater than or equal to zero, then the sum of `f(i)` over all `i` in `s` is also greater than or equal to zero. In mathematical terms, this can be written as: if `∀ i ∈ s, 0 ≤ f(i)`, then `0 ≤ ∑ i ∈ s, f(i)`.
More concisely: If `f : ι → N` is a function from an arbitrary type `ι` to an ordered additive commutative monoid `N`, and `s ⊆ ι` is finite with `0 ≤ f(i)` for all `i ∈ s`, then `0 ≤ ∑ i ∈ s, f(i)`.
|
Finset.sum_card_le
theorem Finset.sum_card_le :
∀ {α : Type u_2} [inst : DecidableEq α] {B : Finset (Finset α)} {n : ℕ} [inst_1 : Fintype α],
(∀ (a : α), (Finset.filter (fun x => a ∈ x) B).card ≤ n) → (B.sum fun s => s.card) ≤ Fintype.card α * n
This theorem states that for any type `α` with decidable equality and for any finite set `B` of finite subsets of `α` and any natural number `n`, if every element in `α` belongs to at most `n` subsets in `B`, then the sum of the sizes of all subsets in `B` is less than or equal to `n` times the number of elements in `α`.
Here, `Finset.filter` is used to extract the subsets of `B` that contain a particular element `a`. The `.card` function then calculates the number of such subsets. The condition `(∀ (a : α), (Finset.filter (fun x => a ∈ x) B).card ≤ n)` ensures that each element of `α` is in at most `n` subsets of `B`. The theorem then concludes that under these conditions, the total sum of the sizes (number of elements) of all subsets in `B` is less than or equal to the total number of elements in `α` (given by `Fintype.card α`) multiplied by `n`.
More concisely: For any type `α` with decidable equality, any finite set `B` of finite subsets of `α`, and any natural number `n`, if each element of `α` belongs to at most `n` subsets in `B`, then the sum of the sizes of all subsets in `B` is less than or equal to `n` times the number of elements in `α`.
|
Finset.one_le_prod'
theorem Finset.one_le_prod' :
∀ {ι : Type u_1} {N : Type u_5} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι},
(∀ i ∈ s, 1 ≤ f i) → 1 ≤ s.prod fun i => f i
The theorem `Finset.one_le_prod'` states that for any type ι and any ordered commutative monoid N, given a function `f` mapping elements of type ι to elements of type N and a finite set `s` of type ι, if all the elements in `s`, when applied to the function `f`, return a value greater than or equal to 1, then the product of these values (calculated as `Finset.prod s f`) is also greater than or equal to 1.
More concisely: If `f : ι -> N` is a function and `s : Finset ι` is a finite set such that `∀ x ∈ s, f x ≥ 1`, then `Finset.prod s f ≥ 1`.
|
Finset.le_sum_of_subadditive
theorem Finset.le_sum_of_subadditive :
∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N]
(f : M → N),
f 0 = 0 →
(∀ (x y : M), f (x + y) ≤ f x + f y) →
∀ (s : Finset ι) (g : ι → M), f (s.sum fun i => g i) ≤ s.sum fun i => f (g i)
The theorem `Finset.le_sum_of_subadditive` states that for any type `ι`, and any commutative monoids `M` and `N` (possibly ordered), given a function `f` from `M` to `N` which is subadditive (i.e., `f` satisfies the inequality `f (x + y) ≤ f x + f y` for all `x` and `y` in `M`) and maps the zero element of `M` to the zero element of `N`, then for any finite set `s` of type `ι` and any function `g` from `ι` to `M`, the function `f` applied to the sum of the elements of `s` mapped via `g` is less than or equal to the sum of `f` applied to each of the elements of `s` mapped via `g`. In mathematical notation, for a subadditive function `f` and any finite set `s` with elements `i`, we have `f (∑ i in s, g i) ≤ ∑ i in s, f (g i)`.
More concisely: For any commutative monoid M and N, subadditive function f from M to N mapping the zero element to zero, and finite set s of type ι along with a function g from ι to M, we have f (∑ i in s, g i) ≤ ∑ i in s, f (g i).
|
Finset.sum_le_sum_of_subset_of_nonneg
theorem Finset.sum_le_sum_of_subset_of_nonneg :
∀ {ι : Type u_1} {N : Type u_5} [inst : OrderedAddCommMonoid N] {f : ι → N} {s t : Finset ι},
s ⊆ t → (∀ i ∈ t, i ∉ s → 0 ≤ f i) → (s.sum fun i => f i) ≤ t.sum fun i => f i
The theorem `Finset.sum_le_sum_of_subset_of_nonneg` states that for any types `ι` and `N`, given an ordered additive commutative monoid on `N`, a function `f` from `ι` to `N`, and two finite sets `s` and `t` of type `ι`: if `s` is a subset of `t` and for every element `i` in `t` that is not in `s`, the function `f` applied to `i` is non-negative, then the sum of the function `f` applied to each element in `s` is less than or equal to the sum of the function `f` applied to each element in `t`. In mathematical terms, if $s \subseteq t$ and for all $i \in t \setminus s$, $f(i) \geq 0$, then $\sum_{i\in s} f(i) \leq \sum_{i\in t} f(i)$.
More concisely: If $s$ is a subset of $t$ in an ordered additive commutative monoid and for all $i \in t \setminus s$, $f(i) \ge 0$, then $\sum\_{i \in s} f(i) \le \sum\_{i \in t} f(i)$.
|
Finset.prod_le_prod_of_subset_of_one_le'
theorem Finset.prod_le_prod_of_subset_of_one_le' :
∀ {ι : Type u_1} {N : Type u_5} [inst : OrderedCommMonoid N] {f : ι → N} {s t : Finset ι},
s ⊆ t → (∀ i ∈ t, i ∉ s → 1 ≤ f i) → (s.prod fun i => f i) ≤ t.prod fun i => f i
This theorem states that given any two finite sets `s` and `t` of elements from a type `ι`, with `s` being a subset of `t`, a function `f` from `ι` to a type `N` (where `N` forms an ordered commutative monoid), if for every element `i` in `t` but not in `s`, `f(i)` is greater than or equal to `1`, then the product of `f(i)` for all `i` in `s` is less than or equal to the product of `f(i)` for all `i` in `t`. In other words, if we have a function that maps elements of `t` not in `s` to values greater than or equal to `1`, then taking the product over all elements of the smaller set `s` will produce a value that is less than or equal to taking the product over all elements of the larger set `t`.
More concisely: Given a finite subset `s` of a set `ι`, a function `f` from `ι` to an ordered commutative monoid `N` with `s ⊆ t` such that `f(i) ≥ 1` for all `i ∈ t \ s`, we have `∏(i ∈ s) f(i) ≤ ∏(i ∈ t) f(i)`.
|
Finset.le_prod_of_submultiplicative_on_pred
theorem Finset.le_prod_of_submultiplicative_on_pred :
∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : CommMonoid M] [inst_1 : OrderedCommMonoid N] (f : M → N)
(p : M → Prop),
f 1 = 1 →
(∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y) →
(∀ (x y : M), p x → p y → p (x * y)) →
∀ (g : ι → M) {s : Finset ι}, (∀ i ∈ s, p (g i)) → f (s.prod fun i => g i) ≤ s.prod fun i => f (g i)
This theorem states that for a commutative monoid `M`, a subsemigroup defined by some predicate `p`, and a submultiplicative map `f` from `M` to another ordered commutative monoid `N` that preserves the identity, the value of `f` applied to the product of a finite family of elements from the subsemigroup (given as `g i` for `i` in a finite set `s`) is less than or equal to the product of the values of `f` applied to each element in the finite family. The elements of the family are chosen such that they satisfy the predicate `p`.
More concisely: For a commutative monoid `M`, a subsemigroup `S` defined by predicate `p`, and a submultiplicative map `f` from `M` to an ordered commutative monoid `N` preserving the identity, if `g i` (for `i` in a finite set `s`) are elements of `S` satisfying `p(gi)`, then `f (∏ i in s gi) ≤ ∏ i in s (fi)`.
|
Finset.sum_le_sum
theorem Finset.sum_le_sum :
∀ {ι : Type u_1} {N : Type u_5} [inst : OrderedAddCommMonoid N] {f g : ι → N} {s : Finset ι},
(∀ i ∈ s, f i ≤ g i) → (s.sum fun i => f i) ≤ s.sum fun i => g i
This theorem states that in an ordered additive commutative monoid, if for every element `i` in a finite set `s`, the function `f(i)` is less than or equal to the function `g(i)`, then the sum of the values of `f(i)` (where `i` ranges over all elements in `s`) is less than or equal to the sum of the values of `g(i)`. That is, if each of the individual terms of two finite sums are in a non-decreasing order, then the total sums are also in the same non-decreasing order.
More concisely: In an ordered additive commutative monoid, if for all elements `i` in a finite set `s`, `f(i) ≤ g(i)`, then `∑ i in s, f(i) ≤ ∑ i in s, g(i)`.
|
Finset.sum_pos'
theorem Finset.sum_pos' :
∀ {ι : Type u_1} {M : Type u_4} [inst : OrderedCancelAddCommMonoid M] {f : ι → M} {s : Finset ι},
(∀ i ∈ s, 0 ≤ f i) → (∃ i ∈ s, 0 < f i) → 0 < s.sum fun i => f i
The theorem `Finset.sum_pos'` states that for any type `ι` and any type `M` that is an ordered cancel add commutative monoid, and for any function `f` from `ι` to `M` and any finite set `s` of `ι`, if every element `i` in `s` satisfies `0 ≤ f i`, and there exists an element `i` in `s` such that `0 < f i`, then the sum of `f i` for all `i` in `s` is greater than zero. In other words, if all elements of a set are non-negative and at least one element is positive, then the sum of function values over the set is positive.
More concisely: If `M` is an ordered, cancel add commutative monoid and `f : ι -> M` satisfies `0 <= f i` for all `i` in a finite set `s` with `0 < f (some i in s)`, then `∑ i in s, f i > 0`.
|
Finset.sum_lt_sum_of_nonempty
theorem Finset.sum_lt_sum_of_nonempty :
∀ {ι : Type u_1} {M : Type u_4} [inst : OrderedCancelAddCommMonoid M] {f g : ι → M} {s : Finset ι},
s.Nonempty → (∀ i ∈ s, f i < g i) → (s.sum fun i => f i) < s.sum fun i => g i
The theorem `Finset.sum_lt_sum_of_nonempty` states that for any ordered cancel-additive commutative monoid `M`, any type `ι`, and any finite set `s` of type `ι`, if `s` is nonempty and for each element `i` in `s` a function `f` applied on `i` is less than a function `g` applied on the same `i`, then the sum of the results of `f` over all elements of `s` is less than the sum of the results of `g` over all elements of `s`. In other words, if we have a nonempty finite set and two functions such that one always outputs smaller values than the other for elements of this set, then the total sum of the smaller values is also less than the total sum of the larger values.
More concisely: If `M` is an ordered cancel-additive commutative monoid, `ι` is a type, `s` is a nonempty finite set of `ι`, and for all `i` in `s`, `f i < g i`, then `∑ i in s, f i < ∑ i in s, g i`.
|
Finset.le_prod_nonempty_of_submultiplicative
theorem Finset.le_prod_nonempty_of_submultiplicative :
∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : CommMonoid M] [inst_1 : OrderedCommMonoid N] (f : M → N),
(∀ (x y : M), f (x * y) ≤ f x * f y) →
∀ {s : Finset ι}, s.Nonempty → ∀ (g : ι → M), f (s.prod fun i => g i) ≤ s.prod fun i => f (g i)
This theorem states that if `f` is a function from `M` to `N` with the property that it is submultiplicative, meaning for any `x` and `y` in `M`, `f(x*y)` is less than or equal to `f(x) * f(y)`, and `g` is a function where for each `i` in the nonempty finite set `s`, `g(i)` is an element of `M`, then `f` of the product of all elements `g(i)` for `i` in `s`, is less than or equal to the product of all `f(g(i))` for `i` in `s`. This is under the condition that `M` and `N` are commutative monoids, with `N` also being ordered.
More concisely: If `f` is a submultiplicative function from the commutative monoid `M` to the ordered monoid `N`, then `f(∏ₙ g(i).for i in finset s) ≤ ∏ₙ f(g(i)).for i in finset s`, where `g(i)` is in `M` for all `i` in the finite set `s`.
|
Finset.sum_card_inter_le
theorem Finset.sum_card_inter_le :
∀ {α : Type u_2} [inst : DecidableEq α] {s : Finset α} {B : Finset (Finset α)} {n : ℕ},
(∀ a ∈ s, (Finset.filter (fun x => a ∈ x) B).card ≤ n) → (B.sum fun t => (s ∩ t).card) ≤ s.card * n
This theorem states that if every element of a finite set `s` belongs to at most `n` finite subsets from a collection `B`, then the total size of the intersections of `s` with each subset in `B` is at most `n` times the size of `s`. Here, `s` and the subsets in `B` are of some type `α` for which equality is decidable. The total size of the intersections is computed as the sum of the sizes of the individual intersections of `s` with each subset in `B`.
More concisely: If each element of a finite set `s` belongs to at most `n` subsets in a collection `B`, then the total size of `s`'s intersections with subsets in `B` is at most `n` times the size of `s`.
|
Finset.le_sum_nonempty_of_subadditive
theorem Finset.le_sum_nonempty_of_subadditive :
∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N]
(f : M → N),
(∀ (x y : M), f (x + y) ≤ f x + f y) →
∀ {s : Finset ι}, s.Nonempty → ∀ (g : ι → M), f (s.sum fun i => g i) ≤ s.sum fun i => f (g i)
This theorem states that for any subadditive function `f` from type `M` to `N`, where `f (x + y) ≤ f x + f y` for all `x` and `y`, and for any nonempty set `s` of type `ι`, the function `f` applied to the sum of a family of elements `g i` in `s` is less than or equal to the sum of `f (g i)` over all `i` in `s`. Here, `M` and `N` are types with additive commutative monoid structures, and `N` additionally has an ordered additive commutative monoid structure.
More concisely: For any subadditive function `f` from an additive commutative monoid `M` to an ordered additive commutative monoid `N`, and any nonempty family `{g i | i ∈ ι}` in `M`, we have `f (∑ i ∈ ι g i) ≤ ∑ i ∈ ι f (g i)`.
|
Finset.le_prod_of_submultiplicative
theorem Finset.le_prod_of_submultiplicative :
∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : CommMonoid M] [inst_1 : OrderedCommMonoid N] (f : M → N),
f 1 = 1 →
(∀ (x y : M), f (x * y) ≤ f x * f y) →
∀ (s : Finset ι) (g : ι → M), f (s.prod fun i => g i) ≤ s.prod fun i => f (g i)
This theorem states that if we have a function `f` from `M` to `N` that is submultiplicative, meaning that for any two elements `x` and `y` of `M`, the value of `f` at their product is less than or equal to the product of the values of `f` at `x` and `y`, and `f` at `1` equals `1`. Furthermore, if `g` is a function that maps any element `i` in a finite set `s` to an element in `M`, then the value of `f` at the product of the `g i`'s (for each `i` in `s`) is less than or equal to the product of the `f (g i)`'s (for each `i` in `s`). This is a result about submultiplicative functions over any commutative monoid `M` and any ordered commutative monoid `N`.
More concisely: If `f` is a submultiplicative function from a commutative monoid `M` to an ordered commutative monoid `N` with `f 1 = 1`, then for any finite set `s` and functions `g : s -> M`, `f (∏ i in s g i) <= ∏ i in s (f (g i))`.
|
Finset.sum_card
theorem Finset.sum_card :
∀ {α : Type u_2} [inst : DecidableEq α] {B : Finset (Finset α)} {n : ℕ} [inst_1 : Fintype α],
(∀ (a : α), (Finset.filter (fun x => a ∈ x) B).card = n) → (B.sum fun s => s.card) = Fintype.card α * n
This theorem states that for any type `α` with decidable equality, given a finite set `B` of finite sets of `α`, and a natural number `n`, if every element `a` of type `α` belongs to exactly `n` subsets of `B` (that is, the number of subsets of `B` containing the element `a` is `n` for all `a`), then the sum total of the sizes (cardinalities) of all the subsets of `B` equals `n` times the total number of elements in `α` (that is, the number of different elements that could possibly be in these subsets). In terms of mathematical notation, if $\forall a. | \{ x \in B \mid a \in x \}| = n$, then $\sum_{s \in B} |s| = |α| \times n$.
More concisely: If every element in a finite type `α` with decidable equality belongs to exactly `n` subsets of a finite set `B` of subsets of `α`, then the sum of the sizes of all subsets in `B` equals `n` times the cardinality of `α`.
|
Finset.prod_lt_prod'
theorem Finset.prod_lt_prod' :
∀ {ι : Type u_1} {M : Type u_4} [inst : OrderedCancelCommMonoid M] {f g : ι → M} {s : Finset ι},
(∀ i ∈ s, f i ≤ g i) → (∃ i ∈ s, f i < g i) → (s.prod fun i => f i) < s.prod fun i => g i
The theorem `Finset.prod_lt_prod'` states that for any types `ι` and `M`, where `M` is an ordered cancel commutative monoid, and for any functions `f` and `g` from `ι` to `M`, and any finite set `s` of type `ι`, if for every element `i` in `s`, `f(i)` is less than or equal to `g(i)`, and there exists an element `i` in `s` such that `f(i)` is strictly less than `g(i)`, then the product of `f(i)` for all `i` in `s` is strictly less than the product of `g(i)` for all `i` in `s`. In mathematical terms, if $\forall i \in s, f(i) \leq g(i)$ and $\exists i \in s, f(i) < g(i)$, then $\prod_{i \in s} f(i) < \prod_{i \in s} g(i)$.
More concisely: If `ι` is a type, `M` is an ordered cancel commutative monoid, `f` and `g` are functions from `ι` to `M`, and `s` is a finite set of type `ι` such that `∀ i ∈ s, f(i) ≤ g(i)` and `∃ i ∈ s, f(i) < g(i)`, then `∏ i ∈ s, f(i) < ∏ i ∈ s, g(i)`.
|
Finset.sum_le_sum_of_subset
theorem Finset.sum_le_sum_of_subset :
∀ {ι : Type u_1} {M : Type u_4} [inst : CanonicallyOrderedAddCommMonoid M] {f : ι → M} {s t : Finset ι},
s ⊆ t → (s.sum fun x => f x) ≤ t.sum fun x => f x
The theorem `Finset.sum_le_sum_of_subset` states that for any types `ι` and `M`, where `M` is a canonically ordered additive commutative monoid, and for any function `f` from `ι` to `M`, and any finite sets `s` and `t` of elements of type `ι`, if `s` is a subset of `t` then the sum of the function `f` evaluated at each element of `s` is less than or equal to the sum of the function `f` evaluated at each element of `t`. In other words, the sum of a function over a subset is less than or equal to the sum of the function over the whole set.
More concisely: For any additive commutative monoid M and function f from a type ι to M, if s is a finite subset of t in ι, then ∑i in s (fi) ≤ ∑i in t (fi).
|
Finset.sum_le_card_nsmul
theorem Finset.sum_le_card_nsmul :
∀ {ι : Type u_1} {N : Type u_5} [inst : OrderedAddCommMonoid N] (s : Finset ι) (f : ι → N) (n : N),
(∀ x ∈ s, f x ≤ n) → s.sum f ≤ s.card • n
This theorem, `Finset.sum_le_card_nsmul`, states that for any type `ι`, type `N` that is an ordered commutative monoid, a finite set `s` of type `ι`, a function `f` from `ι` to `N`, and a value `n` of type `N`, if for all elements `x` in the set `s` the value of the function `f` at `x` is less than or equal to `n`, then the sum of the function `f` over all elements in the set `s` is less than or equal to the cardinality of the set `s` times `n`. Here the `•` operator represents scalar multiplication, meaning the multiplication of the integer cardinality of the set `s` with the element `n` of the monoid `N`.
More concisely: For any finite set $s$ of type $\ι$, ordered commutative monoid $N$, function $f : \ι \to N$, and value $n \in N$, if $f(x) \le n$ for all $x \in s$, then $\sum_{x \in s} f(x) \le |s| \cdot n$.
|
Finset.sum_mono_set_of_nonneg
theorem Finset.sum_mono_set_of_nonneg :
∀ {ι : Type u_1} {N : Type u_5} [inst : OrderedAddCommMonoid N] {f : ι → N},
(∀ (x : ι), 0 ≤ f x) → Monotone fun s => s.sum fun x => f x
The theorem `Finset.sum_mono_set_of_nonneg` states that for any type `ι`, any ordered additive commutative monoid `N`, and any function `f` from `ι` to `N`, if `f` maps every element of `ι` to a nonnegative value (i.e., `f(x) ≥ 0` for all `x` in `ι`), then the function that maps a finite set `s` to the sum of `f(x)` for each `x` in `s` is monotone. In other words, if we have two sets `a` and `b` such that `a` is a subset of `b`, the sum of `f` evaluated at each element in `a` is less than or equal to the sum of `f` evaluated at each element in `b`. This is a statement about the preservation of order under summation in the context of nonnegative functions.
More concisely: For any ordered additive commutative monoid N and function f from a type ι to N with f(x) ≥ 0 for all x in ι, the function summing f over finite sets is monotone, i.e., the sum of f(x) over a subset is less than or equal to the sum over a superset.
|