Finset.sum_sdiff
theorem Finset.sum_sdiff :
∀ {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f : α → β} [inst : AddCommMonoid β] [inst_1 : DecidableEq α],
s₁ ⊆ s₂ → (((s₂ \ s₁).sum fun x => f x) + s₁.sum fun x => f x) = s₂.sum fun x => f x
This theorem states that for any types `α` and `β`, any two finite sets `s₁` and `s₂` of type `α`, and any function `f` from `α` to `β`, given that `β` forms an additive commutative monoid and that equality in `α` is decidable, if `s₁` is a subset of `s₂`, then the sum of `f(x)` over all elements `x` in the set difference `s₂ \ s₁` plus the sum of `f(x)` over all elements `x` in `s₁` equals the sum of `f(x)` over all elements `x` in `s₂`. In other words, splitting the sum over `s₂` into a sum over `s₁` and a sum over `s₂ \ s₁` preserves the total sum.
More concisely: For any additive commutative monoid β, decidably equated type α, and function f : α → β, if s₁ ∋ s₂ and s₂ = s₁ ∪ (s₂ \ s₁), then ∑x ∈ s₂ (f x) = ∑x ∈ s₁ (f x) + ∑x ∈ s₂ \ s₁ (f x).
|
Finset.sum_range_succ
theorem Finset.sum_range_succ :
∀ {β : Type u_4} [inst : AddCommMonoid β] (f : ℕ → β) (n : ℕ),
((Finset.range (n + 1)).sum fun x => f x) = ((Finset.range n).sum fun x => f x) + f n
The theorem `Finset.sum_range_succ` states that for any function `f` from natural numbers `ℕ` to a type `β` which forms an additive commutative monoid, and for any natural number `n`, the sum of the function `f` applied to each element in the range from `0` to `n+1` (exclusive) is equal to the sum of the function `f` applied to each element in the range from `0` to `n` (exclusive) plus the function `f` applied to `n`. This theorem essentially describes an inductive step for proofs involving the sum of elements in a range.
More concisely: For any additive commutative monoid type `β` and natural number `n`, the sum of a function `f` from natural numbers to `β` applied to elements in the range from `0` to `n+1` (exclusive) equals the sum of the function applied to elements in the range from `0` to `n` (exclusive) plus the function applied to `n`.
|
Fintype.prod_equiv
theorem Fintype.prod_equiv :
∀ {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : CommMonoid α]
(e : ι ≃ κ) (f : ι → α) (g : κ → α),
(∀ (x : ι), f x = g (e x)) → (Finset.univ.prod fun x => f x) = Finset.univ.prod fun x => g x
The theorem `Fintype.prod_equiv` states that for any types `ι`, `κ`, and `α` with `ι` and `κ` being finite types and `α` being a type with a commutative multiplication, given a bijection `e` from `ι` to `κ`, and any two functions `f` from `ι` to `α` and `g` from `κ` to `α` such that `f` at any `x` in `ι` is equal to `g` at `e x` in `κ`, then the product of `f x` as `x` ranges over all elements of type `ι` is equal to the product of `g x` as `x` ranges over all elements of type `κ`. In other words, it says that the product of the function values over a finite set is invariant under a renaming of the elements of the set, provided the renaming is a bijection and the function is adapted accordingly.
More concisely: For finite types `ι` and `κ` and a commutative type `α` with a bijection `e` between them, if functions `f : ι → α` and `g : κ → α` satisfy `f x = g (e x)` for all `x`, then the product of `f` is equal to the product of `g`.
|
Finset.sum_induction_nonempty
theorem Finset.sum_induction_nonempty :
∀ {α : Type u_3} {s : Finset α} {M : Type u_6} [inst : AddCommMonoid M] (f : α → M) (p : M → Prop),
(∀ (a b : M), p a → p b → p (a + b)) → s.Nonempty → (∀ x ∈ s, p (f x)) → p (s.sum fun x => f x)
This theorem states that given a nonempty finite set `s` of some arbitrary type `α` and a function `f` from `α` to another type `M` (which is assumed to have an additive commutative monoid structure), if we want to prove a property `p` holds for the sum of `f(x)` for all `x` in `s`, it is sufficient to show that `p` is preserved under addition and `p` holds for each `f(x)` for all `x` in `s`. Essentially, we are proving a property for a sum by demonstrating it for each summand and showing it holds under addition.
More concisely: Given a nonempty finite set `s` and a function `f` from a type `α` to an additive commutative monoid `M`, if `p` is a property preserved under addition and `p(fx)` holds for all `x` in `s`, then `p(∑x in s, fx)` holds.
|
Finset.prod_subtype
theorem Finset.prod_subtype :
∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] {p : α → Prop} {F : Fintype (Subtype p)} (s : Finset α),
(∀ (x : α), x ∈ s ↔ p x) → ∀ (f : α → β), (s.prod fun a => f a) = Finset.univ.prod fun a => f ↑a
The theorem `Finset.prod_subtype` states that for any type `α` and `β`, given a commutative monoid structure on `β`, a property `p` on `α`, a finite type `F` of the subtype `p`, and a finite set `s` of `α`, if every element `x` in `s` satisfies the property `p`, then for any function `f` from `α` to `β`, the product of `f(a)` for all `a` in `s` is equal to the product of `f(a)` for all `a` in the universal finite set of the subtype `p`. In other words, the product over a set is equal to the product over the subtype when the property defining the subtype matches the membership in the set.
More concisely: For any commutative monoid `β`, property `p` on type `α`, finite subtype `F` of `p`, and finite set `s` of `α` consisting of elements with property `p`, the product of `f(a)` for all `a` in `s` is equal to the product of `f(a)` for all `a` in the universal finite set of `p`.
|
Finset.sum_pair
theorem Finset.sum_pair :
∀ {α : Type u_3} {β : Type u_4} {f : α → β} [inst : AddCommMonoid β] [inst_1 : DecidableEq α] {a b : α},
a ≠ b → ({a, b}.sum fun x => f x) = f a + f b
The theorem `Finset.sum_pair` states that, for any types `α` and `β`, a function `f` which maps from `α` to `β`, an instance of an additive commutative monoid `β`, an instance of decidable equality on `α`, and distinct elements `a` and `b` of type `α`, the sum of the values of the function `f` over the finite set `{a, b}` is equal to the sum of the values of `f` at `a` and `f` at `b`. In other words, if we have a set containing just two distinct elements, the sum of the function applied to those elements is equal to the sum of the function applied to each element individually.
More concisely: For any additive commutative monoid β, decidably equal types α, function f from α to β, and distinct elements a and b in α, the sum of f over the finite set {a, b} equals the sum of f(a) and f(b).
|
Finset.prod_mulIndicator_subset
theorem Finset.prod_mulIndicator_subset :
∀ {ι : Type u_1} {β : Type u_4} [inst : CommMonoid β] (f : ι → β) {s t : Finset ι},
s ⊆ t → (t.prod fun i => (↑s).mulIndicator f i) = s.prod fun i => f i
This theorem states that for any types `ι` and `β` with `β` forming a commutative monoid, given a function `f` from `ι` to `β` and two finite sets `s` and `t` of type `ι`, if `s` is a subset of `t`, then the product of the indicator function of `s` applied to `f` over `t` is the same as the product of `f` over `s`. This essentially means that the operation of taking the product of a function over a larger finset, minimizing the function to an indicator function of the smaller finset, is equivalent to directly taking the product over the smaller finset. Here, the indicator function acts like a switch, being equal to `f` on `s` and `1` elsewhere.
More concisely: For any commutative monoid type `β`, given a function `f` from type `ι` to `β`, and finite sets `s` and `t` of type `ι` with `s` a subset of `t`, the product of the indicator function of `s` and `f` is equal to the product of `f` over `s`.
|
Finset.sum_add_sum_compl
theorem Finset.sum_add_sum_compl :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] [inst_1 : Fintype α] [inst_2 : DecidableEq α]
(s : Finset α) (f : α → β), ((s.sum fun i => f i) + sᶜ.sum fun i => f i) = Finset.univ.sum fun i => f i
This theorem states that for any given finite set `s` of elements of type `α` and a function `f` mapping from `α` to another type `β` equipped with an additive commutative monoid structure, the sum of the function `f` applied to all elements in `s` combined with the sum of the function `f` applied to all elements not in `s` (i.e., in the complement of `s`) is equal to the sum of the function `f` applied to all elements of the universal set (i.e., the set of all elements of type `α`). This statement assumes that for the type `α`, we have a structure of a finite type and a decidable equality. It's essentially a statement about partitioning a set and summing over the parts.
More concisely: For any finite set `s` of elements from a type `α` with a decidable equality and a function `f` from `α` to an additive commutative monoid, the sum of `f` over `s` plus the sum of `f` over `α \ s` equals the sum of `f` over `α`.
|
Finset.prod_powersetCard
theorem Finset.prod_powersetCard :
∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] (n : ℕ) (s : Finset α) (f : ℕ → β),
((Finset.powersetCard n s).prod fun t => f t.card) = f n ^ s.card.choose n
This theorem states that for any given types `α` and `β` (where `β` is a commutative monoid), any natural number `n` and any finite set `s` of type `α`, and any function `f` from natural numbers to `β`, the product of `f` applied to the cardinals of the subsets of `s` of cardinality `n`, is equal to `f(n)` raised to the binomial coefficient "cardinal of `s` choose `n`". Essentially, if you have a product over the powerset of cardinality `n` of a given set `s` (the set of all subsets of `s` that have `n` elements), and the product only depends on the size of these subsets, it remains constant and is equal to `f(n)` raised to the number of ways to choose `n` elements from `s`.
More concisely: For any commutative monoid type `β`, given a set `α` of cardinality `|α|`, natural number `n`, finite set `s` of type `α` with `|s| = |α|`, and a function `f : ℕ → β`, the product of `f` applied to the cardinalities of `s`'s subsets of size `n` equals `f!(|s|) * (|s| choose n)`, where `f!` denotes the iterated application of `f`.
|
Finset.sum_coe_sort
theorem Finset.sum_coe_sort :
∀ {α : Type u_3} {β : Type u_4} (s : Finset α) (f : α → β) [inst : AddCommMonoid β],
(Finset.univ.sum fun i => f ↑i) = s.sum fun i => f i
This theorem states that for any type `α`, a finite set `s` of type `α`, and a function `f` from `α` to another type `β` which forms an additive commutative monoid, the sum of the function `f` applied to all elements in the universal finite set of type `α` (represented by `Finset.univ`), where each element is type-casted using the `↑` operator, is equal to the sum of the function `f` applied to all elements in the finite set `s`. In other words, summing over all possible elements (using `Finset.univ`) and summing over the elements in `s` yield the same result, provided we interpret elements of `α` as elements of `β` using the coercion function (the `↑` operator).
More concisely: For any additive commutative monoid homomorphism `f` from type `α` to type `β`, and finite set `s` of `α`, the sum of `f` applied to every element in the universal set `Finset.univ` of type `α` equals the sum of `f` applied to all elements in the finite set `s`.
|
Finset.prod_coe_sort
theorem Finset.prod_coe_sort :
∀ {α : Type u_3} {β : Type u_4} (s : Finset α) (f : α → β) [inst : CommMonoid β],
(Finset.univ.prod fun i => f ↑i) = s.prod fun i => f i
The theorem `Finset.prod_coe_sort` states that for any type `α`, a finite set `s` of type `α`, a function `f` from `α` to another type `β`, and given a commutative monoid structure on `β`, the product of `f` applied to the elements of the universal finite set of type `Finset α` (when those elements are treated as elements of `α` using type coercion) is equal to the product of `f` applied to the elements of set `s`. This theorem establishes the equality of these two products, where the product of a function over a set is defined as the product of the function values for all elements in the set.
More concisely: For any commutative monoid-valued function `f` and finite set `s` of type `α`, the product of `f` applied to the elements of the universal finite set of type `Finset α` (treated as `α` elements) equals the product of `f` applied to the elements of set `s`.
|
Finset.sum_ite_eq'
theorem Finset.sum_ite_eq' :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] [inst_1 : DecidableEq α] (s : Finset α) (a : α)
(b : α → β), (s.sum fun x => if x = a then b x else 0) = if a ∈ s then b a else 0
This theorem, `Finset.sum_ite_eq'`, states that for any finite set `s` of elements of type `α`, a given element `a` of that same type, and a function `b` from `α` to `β`, the sum over `s` of the function that maps each `x` in `s` to `b(x)` if `x` equals `a` and `0` otherwise, is equal to `b(a)` if `a` is in `s` and `0` otherwise. This is essentially the mathematical formulation of the intuitive notion that when we sum over a conditionally defined function whose value is `0` except at one specific point, the sum is either the value at that point (if the point is in the set we're summing over) or `0` (if the point isn't in the set). The difference between this theorem and `Finset.sum_ite_eq` lies in the order of the arguments to the equality test in the condition of the conditional function.
More concisely: For any finite set `s` and element `a` in type `α`, and function `b` from `α` to `β`, the sum of applying `b` to `a` if `a` is in `s`, and `0` otherwise, equals `b(a)` if `a` is a member of `s`, and `0` otherwise.
|
Finset.sum_filter
theorem Finset.sum_filter :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} [inst : AddCommMonoid β] (p : α → Prop) [inst_1 : DecidablePred p]
(f : α → β), ((Finset.filter p s).sum fun a => f a) = s.sum fun a => if p a then f a else 0
This theorem, `Finset.sum_filter`, states that for any finite set `s` of type `α`, any function `f` from `α` to `β` (where `β` is an additive commutative monoid), and any predicate `p` on `α` that is decidable, the sum of `f(a)` over all elements `a` in the subset of `s` that satisfy `p` is equal to the sum of `f(a)` over all elements `a` in `s`, where `f(a)` is taken to be 0 when `a` does not satisfy `p`. In other words, the sum of the values of a function over the elements of a filtered finite set is the same as the sum over the entire set, where the function is zero for elements not in the filter.
More concisely: For any finite set `s`, function `f` from `α` to an additive commutative monoid `β`, and decidable predicate `p` on `α`, the sum of `f(a)` over elements `a` in `s` that satisfy `p` is equal to the sum of `f(a)` over all elements in `s`, with `f(a)` being 0 for elements not satisfying `p`.
|
Finset.prod_eq_single_of_mem
theorem Finset.prod_eq_single_of_mem :
∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] {s : Finset α} {f : α → β},
∀ a ∈ s, (∀ b ∈ s, b ≠ a → f b = 1) → (s.prod fun x => f x) = f a
This theorem states that for any type `α` and `β` with `β` being a commutative monoid, given a finite set `s` of type `α` and a function `f` mapping `α` to `β`, if for an element `a` in `s` the function `f` maps all other elements `b` in `s` to the identity element of the monoid (i.e., `1`), then the product of `f x` as `x` ranges over all elements of the set `s` (denoted as `Finset.prod s fun x => f x`) is equal to `f a`.
More concisely: If `f : α → β` maps all elements in a finite set `s ⊆ α` except one to the identity element of a commutative monoid `β`, then `Finset.prod s fun x => f x = f (some x in s)`.
|
Finset.card_eq_sum_card_fiberwise
theorem Finset.card_eq_sum_card_fiberwise :
∀ {α : Type u_3} {β : Type u_4} [inst : DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β},
(∀ x ∈ s, f x ∈ t) → s.card = t.sum fun a => (Finset.filter (fun x => f x = a) s).card
This theorem states that, given two finite sets `s` of type `α` and `t` of type `β`, with a function `f` mapping from `α` to `β` such that every element in `s` maps to an element in `t`, the cardinality of `s` is equal to the sum, over all elements `a` in `t`, of the cardinality of the subset of `s` where `f` equals `a`. In other terms, the size of `s` is equal to the sum of the sizes of its "fibers" under `f` over `t`.
More concisely: Given two finite sets `s` and `t` with a function `f: s -> t` such that every element in `s` maps to an element in `t`, the cardinality of `s` equals the sum of the cardinalities of the fibers of `f`.
|
Finset.sum_erase_add
theorem Finset.sum_erase_add :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] [inst_1 : DecidableEq α] (s : Finset α) (f : α → β)
{a : α}, a ∈ s → ((s.erase a).sum fun x => f x) + f a = s.sum fun x => f x
This theorem, `Finset.sum_erase_add`, is about operations on finite sets, specifically sums over finite sets. It states that for any types `α` and `β`, where `β` forms an additive commutative monoid, and `α` has decidable equality, and for any finite set `s` of type `α`, and any function `f` from `α` to `β`, and any element `a` in `s`, the sum of the values of `f` over the elements of `s` with `a` removed, plus the value of `f` at `a`, is equal to the sum of the values of `f` over all elements of `s`. In other words, if we sum up the values of a function over a set, removing an element and adding its contribution separately does not change the total sum.
In mathematical terms, this theorem says that for a finite set $s$, a function $f : \alpha \to \beta$, and an element $a \in s$, we have
\[
\sum_{x \in s \setminus \{a\}} f(x) + f(a) = \sum_{x \in s} f(x),
\]
where the summations are over all elements in the respective sets.
More concisely: For any finite set $s$, function $f$ from a type with decidable equality to an additive commutative monoid $\beta$, and element $a$ in $s$, we have $\sum\_{x \in s \setminus \{a\}} f(x) + f(a) = \sum\_{x \in s} f(x)$.
|
Finset.prod_erase
theorem Finset.prod_erase :
∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] [inst_1 : DecidableEq α] (s : Finset α) {f : α → β} {a : α},
f a = 1 → ((s.erase a).prod fun x => f x) = s.prod fun x => f x
The theorem `Finset.prod_erase` states that for any two types `α` and `β`, where `β` has a commutative monoid structure and `α` has decidable equality, given a finite set `s` of elements of type `α`, a function `f` from `α` to `β`, and an element `a` of type `α`, if the function `f` applied at the point `a` equals 1, then the product of the function values over all elements of `s` excluding `a` (if present) is the same as the product of the function values over all elements of `s`. In other words, if the function `f` is 1 at a certain point, removing that point from the finite set does not change the total product of the function values.
More concisely: If `f` is a function from a finite set `s` of decidably equal elements of type `α` to a commutative monoid `β` with `1` such that `f(a) = 1`, then the product of `f` over `s` excluding `a` equals the product of `f` over `s`.
|
Function.Bijective.finset_prod
theorem Function.Bijective.finset_prod :
∀ {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : CommMonoid α]
(e : ι → κ),
Function.Bijective e →
∀ (f : ι → α) (g : κ → α),
(∀ (x : ι), f x = g (e x)) → (Finset.univ.prod fun x => f x) = Finset.univ.prod fun x => g x
The theorem `Function.Bijective.finset_prod` states that for any types `ι`, `κ`, and `α`, where `ι` and `κ` are finite types and `α` is a type with an associated commutative monoid, given a bijective function `e` from `ι` to `κ`, for any two functions `f` and `g` from `ι` and `κ` to `α` respectively, if for all `x` in `ι`, `f(x)` equals `g(e(x))`, then the product of the values of `f` over the universal finite set of `ι` equals the product of the values of `g` over the universal finite set of `κ`. In other words, this theorem asserts the invariance of the product operation under a bijective mapping.
More concisely: For any finite types `ι`, `κ`, and commutative monoid `α`, if `e: ι → κ` is bijective and for all `x ∈ ι`, `f(x) = g(e(x))` for functions `f: ι → α` and `g: κ → α`, then the product of `f` over `ι` equals the product of `g` over `κ`.
|
Finset.sum_sub_distrib
theorem Finset.sum_sub_distrib :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {f g : α → β} [inst : SubtractionCommMonoid β],
(s.sum fun x => f x - g x) = (s.sum fun x => f x) - s.sum fun x => g x
The theorem `Finset.sum_sub_distrib` states that for any finite set `s` of elements of an arbitrary type `α` and any two functions `f` and `g` from `α` to an arbitrary type `β` which is a commutative monoid with subtraction, the sum of the differences `f x - g x` for each `x` in `s` is equal to the difference of the sums of `f x` and `g x` over all `x` in `s`. In mathematical notation, this is equivalent to saying $\sum_{x \in s} (f(x) - g(x)) = \left( \sum_{x \in s} f(x) \right) - \left( \sum_{x \in s} g(x) \right)$.
More concisely: For any finite set `s` and functions `f` and `g` from a commutative monoid with subtraction, $\sum\_{x \in s} (f(x) - g(x)) = \left( \sum\_{x \in s} f(x) \right) - \left( \sum\_{x \in s} g(x) \right)$.
|
Finset.sum_univ_pi
theorem Finset.sum_univ_pi :
∀ {ι : Type u_1} {β : Type u_4} [inst : AddCommMonoid β] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι]
{κ : ι → Type u_6} (t : (i : ι) → Finset (κ i)) (f : ((i : ι) → i ∈ Finset.univ → κ i) → β),
((Finset.univ.pi t).sum fun x => f x) = (Fintype.piFinset t).sum fun x => f fun a x_1 => x a
This theorem states that for any finite type `ι`, any type `β` that forms an additive commutative monoid, a function `t` from `ι` to finite sets of some type `κ(i)`, and a function `f` from functions on `ι` to `β`, the sum over the `Finset (Π a ∈ univ, t a)` obtained from `univ.pi t`, using function `f`, is equal to the sum over `Finset (Π a, t a)` obtained from `Fintype.piFinset t`, using modified function `f`. Here, `univ.pi t` and `Fintype.piFinset t` are essentially the same finite set, but their elements have different types. The sum is taken over all elements of the respective finite sets. This theorem is valid when equality on `ι` is decidable, and `ι` itself is a finite type.
More concisely: For any finite type `ι`, any additive commutative monoid `β`, functions `t : ι → Set κ(i)` and `f : (ι → β) → β`, the sum over `Finset (Π a ∈ ι, t a)` using `f` equals the sum over `Finset (Π a, t a)` using the modified `f`, when `ι` has decidable equality and is finite.
|
Finset.prod_range_div
theorem Finset.prod_range_div :
∀ {M : Type u_6} [inst : CommGroup M] (f : ℕ → M) (n : ℕ),
((Finset.range n).prod fun i => f (i + 1) / f i) = f n / f 0
The theorem `Finset.prod_range_div` states that for any function `f` from natural numbers to a commutative group `M`, and for any natural number `n`, the product of the sequence `f(i + 1) / f(i)` for `i` ranging from 0 to `n - 1`, equals `f(n) / f(0)`. Essentially, this is the result of a telescoping product, where all intermediate factors cancel out, leaving only the ratio of the last and first factors.
More concisely: For any commutative group M and natural number n, the product of the ratios f(i+1)/f(i) for i from 0 to n-1 equals the ratio f(n)/f(0).
|
Finset.sum_equiv
theorem Finset.sum_equiv :
∀ {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [inst : AddCommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α}
{g : κ → α} (e : ι ≃ κ),
(∀ (i : ι), i ∈ s ↔ e i ∈ t) → (∀ i ∈ s, f i = g (e i)) → (s.sum fun i => f i) = t.sum fun i => g i
The theorem `Finset.sum_equiv` states that for any two finite sets `s` and `t` of types `ι` and `κ` respectively, and any two functions `f : ι → α` and `g : κ → α` where `α` is a type with an addition operation that is commutative and has a neutral element (an additive commutative monoid), if there exists a bijective function `e : ι ≃ κ` such that each element in `s` corresponds to an element in `t` via `e`, and `f` and `g` are the same function after applying this correspondence, then the sum of `f` over all elements in `s` is equal to the sum of `g` over all elements in `t`. In other words, under these conditions, the summation operation is invariant under the change of variables defined by `e`.
More concisely: Given finite sets $s$ and $t$ of types $\xi$ and $\kappa$, functions $f : s \to \alpha$ and $g : t \to \alpha$ with commutative additive monoid $\alpha$, and a bijective function $e : s \cong t$ such that $f \circ e = g$, then $\sum\_{x : s} f(x) = \sum\_{y : t} g(y)$.
|
Finset.prod_powerset_insert
theorem Finset.prod_powerset_insert :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} [inst : CommMonoid β] [inst_1 : DecidableEq α],
a ∉ s →
∀ (f : Finset α → β),
((insert a s).powerset.prod fun t => f t) =
(s.powerset.prod fun t => f t) * s.powerset.prod fun t => f (insert a t)
The theorem `Finset.prod_powerset_insert` states that for any types `α` and `β`, a finite set `s` of type `α`, an element `a` of type `α` not in `s`, a function `f` from finite sets of `α` to `β`, and given that `β` is a commutative monoid and `α` has decidable equality, the product of `f` over the power set of `s ∪ {a}` is equal to the product of `f` over the power set of `s` multiplied by the product of `f` over the power set of `s` where `a` is added to each subset. In other words, when calculating the product over all subsets of a set expanded by one element, we can separate it into a product over all original subsets and a product over all original subsets with the additional element.
More concisely: For any commutative monoid β and decidably equated type α, the product of a function from finite sets of α to β over the power set of a finite set s, extended with an element a not in s, equals the product of the function over the power set of s multiplied by the product over subsets of s with a added.
|
Finset.prod_fiberwise_of_maps_to
theorem Finset.prod_fiberwise_of_maps_to :
∀ {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [inst : CommMonoid α] {s : Finset ι} {t : Finset κ}
[inst_1 : DecidableEq κ] {g : ι → κ},
(∀ i ∈ s, g i ∈ t) →
∀ (f : ι → α), (t.prod fun j => (Finset.filter (fun i => g i = j) s).prod fun i => f i) = s.prod fun i => f i
This theorem states that for any types `ι`, `κ` and `α`, where `α` is a commutative monoid, given two finite sets `s` of type `ι` and `t` of type `κ`, a decidable equality on `κ`, and a function `g` mapping from `ι` to `κ` which maps every element of `s` into `t`, then for any function `f` from `ι` to `α`, the product over `t` of the function `j` mapped to the product over the filtered set of `s` where `g i = j` of the function `i` mapped to `f i` is equal to the product over `s` of the function `i` mapped to `f i`. In other words, it says that the product of each `f i` over the `i` in `s` is equal to the product of the products of each `f i` for `i` in the fiber of `j` over all `j` in `t`. This is a form of the principle of distributivity of multiplication over addition.
More concisely: Given finite sets `s` and `t`, a decidable equality on `t`, a commutative monoid `α`, a function `g` mapping `s` to `t`, and a function `f` mapping a type to `α`, the product of `f i` over `i` in `s` is equal to the product of the products of `f i` over `i` in the fibers of `g`.
|
Finset.prod_eq_zero_iff
theorem Finset.prod_eq_zero_iff :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [inst : CommMonoidWithZero β] [inst_1 : Nontrivial β]
[inst_2 : NoZeroDivisors β], (s.prod fun x => f x) = 0 ↔ ∃ a ∈ s, f a = 0
The theorem `Finset.prod_eq_zero_iff` states that for any type `α`, a second type `β` that is a commutative monoid with zero, has a nontrivial element, and has no zero divisors, a finite set `s` of type `α`, and a function `f` from `α` to `β`, the product of `f x` for all `x` in `s` is equal to zero if and only if there exists an element `a` in `s` such that `f a` equals zero.
More concisely: For any commutative monoid with zero, having a nontrivial zero and no zero divisors, a function from a finite set to this monoid, and the product of images of set elements, equals zero if and only if there exists an element in the set mapping to the zero element.
|
Finset.prod_range_succ
theorem Finset.prod_range_succ :
∀ {β : Type u_4} [inst : CommMonoid β] (f : ℕ → β) (n : ℕ),
((Finset.range (n + 1)).prod fun x => f x) = ((Finset.range n).prod fun x => f x) * f n
This theorem states that for any commutative monoid `β`, any function `f` from natural numbers to `β`, and any natural number `n`, the product of `f(x)` for each `x` in the set of natural numbers less than `n + 1` is equal to the product of `f(x)` for each `x` in the set of natural numbers less than `n` multiplied by `f(n)`. In other words, adding one more term to the range in the product changes the product by a factor of the function applied to the new term.
More concisely: For any commutative monoid `β` and function `f` from natural numbers to `β`, the product of `f(x)` for `x` in the set of natural numbers less than `n + 1` equals the product of `f(x)` for `x` in the set of natural numbers less than `n` multiplied by `f(n)`.
|
Finset.op_sum
theorem Finset.op_sum :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] {s : Finset α} (f : α → β),
MulOpposite.op (s.sum fun x => f x) = s.sum fun x => MulOpposite.op (f x)
The theorem `Finset.op_sum` states that for any additive commutative monoid `β`, any finite set `s` of type `α`, and any function `f` from `α` to `β`, moving to the opposite monoid (i.e., reversing the operation) after summing the function `f` over all elements of the set `s` is equal to summing the function `f` applied to the opposite monoid over all elements of the set `s`. In other words, the operation of summing commutes with the operation of taking the opposite in the context of additive commutative monoids.
More concisely: For any additive commutative monoid β, finite set s of type α, and function f from α to β, the opposite of the sum of f over s is equal to the sum of f over s applied to the opposite monoid.
|
Fintype.prod_bijective
theorem Fintype.prod_bijective :
∀ {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : CommMonoid α]
(e : ι → κ),
Function.Bijective e →
∀ (f : ι → α) (g : κ → α),
(∀ (x : ι), f x = g (e x)) → (Finset.univ.prod fun x => f x) = Finset.univ.prod fun x => g x
The theorem `Fintype.prod_bijective` states that for any two types `ι` and `κ` and a type `α` that forms a commutative monoid, if there exists a bijective function `e` from `ι` to `κ`, then for any two functions `f: ι → α` and `g: κ → α` such that `f x = g (e x)` for all `x` in `ι`, the product of `f x` across all elements `x` in `ι` is equal to the product of `g x` across all elements `x` in `κ`. In other words, it says that the product over a finite set remains the same under a bijective map.
More concisely: For any commutative monoid type `α`, bijective function `e: ι -> κ`, and functions `f: ι -> α` and `g: κ -> α` such that `f x = g (e x)` for all `x` in `ι`, the product of `f` over `ι` equals the product of `g` over `κ`.
|
Finset.prod_range_succ'
theorem Finset.prod_range_succ' :
∀ {β : Type u_4} [inst : CommMonoid β] (f : ℕ → β) (n : ℕ),
((Finset.range (n + 1)).prod fun k => f k) = ((Finset.range n).prod fun k => f (k + 1)) * f 0
The theorem `Finset.prod_range_succ'` states that for any commutative monoid `β` and any function `f` from natural numbers to `β`, the product of `f k` for `k` in the range `0` to `n + 1` (exclusive) is equal to the product of `f (k + 1)` for `k` in the range `0` to `n` (exclusive) times `f 0`. In other words, given a function `f` from the natural numbers to `β`, the product over the first `n + 1` natural numbers is equal to `f 0` times the product over the next `n` natural numbers.
More concisely: For any commutative monoid β and function f from natural numbers to β, the product of f(k) for k in the range 0 to n is equal to the product of f(k+1) for k in the range 0 to n-1 times f(0).
|
Finset.sum_pi_single'
theorem Finset.sum_pi_single' :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] [inst_1 : DecidableEq α] (a : α) (x : β) (s : Finset α),
(s.sum fun a' => Pi.single a x a') = if a ∈ s then x else 0
This theorem, `Finset.sum_pi_single'`, states that for any type `α`, type `β` with an associated additive commutative monoid structure, any decidable equality on `α`, any element `a` of type `α`, any element `x` of type `β`, and any finite set `s` of `α`, the sum of the function `Pi.single a x` applied to each element `a'` in the finite set `s` equals `x` if `a` is in `s`, and `0` otherwise. In other words, it expresses that the sum of the function that assigns `x` to `a` and `0` to all other elements of `s`, is equal to `x` if `a` is an element of `s`, and `0` if not.
More concisely: For any type `α`, type `β` with an additive commutative monoid structure, decidable equality relation on `α`, and finite set `s` of `α`, the function that maps each `a` in `s` to `x` and all other elements to `0` has sum equal to `x` if `a` is in `s`, and `0` otherwise.
|
Finset.prod_induction
theorem Finset.prod_induction :
∀ {α : Type u_3} {s : Finset α} {M : Type u_6} [inst : CommMonoid M] (f : α → M) (p : M → Prop),
(∀ (a b : M), p a → p b → p (a * b)) → p 1 → (∀ x ∈ s, p (f x)) → p (s.prod fun x => f x)
The theorem `Finset.prod_induction` states that, given a function `f` from a type `α` to a commutative monoid `M`, a property `p` on `M`, and a finite set `s` of elements of type `α`, if the property `p` is multiplicative (i.e., if `p(a * b)` is true whenever `p(a)` and `p(b)` are true) and the property `p` holds for the neutral element 1 and for all elements of the form `f(x)` for `x` in the set `s`, then the property `p` must also hold for the product of all `f(x)`'s where `x` is in the set `s`. In other words, to prove a property of a product, it is sufficient to prove that the property is multiplicative and holds on the factors of the product.
More concisely: If `f : α -> M` maps a finite set `s` to commutative monoid elements, `1` is neutral, `p(1)` holds, and `p` is multiplicative, then `∏x ∈ s. p(f x)` holds.
|
MonoidHom.finset_prod_apply
theorem MonoidHom.finset_prod_apply :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : MulOneClass β] [inst_1 : CommMonoid γ] (f : α → β →* γ)
(s : Finset α) (b : β), (s.prod fun x => f x) b = s.prod fun x => (f x) b
This theorem, `MonoidHom.finset_prod_apply`, is about the product of a function applied to elements of a finite set, in the context of algebraic structures called monoids. Specifically, it says that for any types `α`, `β`, and `γ`, where `β` forms a `MulOneClass` (a structure containing multiplication and one) and `γ` forms a `CommMonoid` (a commutative monoid), given a function `f` from `α` to the monoid homomorphisms from `β` to `γ`, a finite set `s` of type `α`, and an element `b` of type `β`, the product of the function `f` applied to the elements of `s` and then applied to `b` is equal to the product of the function `f` applied to the elements of `s` and `b`. This theorem is a stronger version of `Finset.prod_apply`, as it requires the function `f` to be a monoid homomorphism.
More concisely: Given a finite set `s` of type `α`, a monoid homomorphism `f` from `α` to the monoid homomorphisms from `β` to `γ`, and elements `b` of type `β` and `x₁,...,xₖ` of type `α`, the equation `∏ i in set.Ico (f x\_i) b = ∏ i in set.Ico f x\_i ∘ b` holds in the commutative monoid `γ`.
|
Finset.sum_bij
theorem Finset.sum_bij :
∀ {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [inst : AddCommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α}
{g : κ → α} (i : (a : ι) → a ∈ s → κ),
(∀ (a : ι) (ha : a ∈ s), i a ha ∈ t) →
(∀ (a₁ : ι) (ha₁ : a₁ ∈ s) (a₂ : ι) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) →
(∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b) →
(∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)) → (s.sum fun x => f x) = t.sum fun x => g x
The theorem `Finset.sum_bij` is about reordering a sum over a finite set. Given two finite sets `s` and `t`, and functions `f : ι → α` and `g : κ → α` that map elements of these sets to a type with addition (α), this theorem states that if there exists a surjective injection `i : (a : ι) → a ∈ s → κ` from `s` to `t` such that for every element `a` in `s`, `f(a)` equals `g(i(a))`, then the sum of `f` over `s` equals the sum of `g` over `t`. In simpler terms, if we have a one-to-one correspondence between the elements of two sets and the corresponding elements have the same function values, then the sums of the function values over the two sets are equal.
More concisely: If two finite sets have a surjective injection with function values having equal images under given functions, then the sums of these functions over the sets are equal.
|
Finset.prod_update_of_mem
theorem Finset.prod_update_of_mem :
∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] [inst_1 : DecidableEq α] {s : Finset α} {i : α},
i ∈ s → ∀ (f : α → β) (b : β), (s.prod fun x => Function.update f i b x) = b * (s \ {i}).prod fun x => f x
The theorem `Finset.prod_update_of_mem` asserts that for any types `α` and `β` (given that `β` forms a commutative monoid and `α` has decidable equality), for any finite set of elements `s` of type `α`, and for any element `i` of type `α` which is a member of `s`, for any function `f` from `α` to `β`, and for any `b` of type `β`, the product of the function values (where the function `f` is updated at point `i` to return `b`) over all elements of `s` is equal to `b` multiplied by the product of the original function values over all elements of `s` excluding `i`. In terms of mathematical notation, this can be expressed as $\prod_{x \in s}f_{updated}(x) = b * \prod_{x \in s \setminus \{i\}}f(x)$ where $f_{updated}(x)$ is $b$ if $x=i$ and $f(x)$ otherwise.
More concisely: For any finite set `s` of type `α` (where `α` has decidable equality), type `β` forming a commutative monoid, function `f` from `α` to `β`, element `i` of type `α` in `s`, and element `b` of type `β`, the updated function product equals the original function product multiplied by `b`: $\prod\_{x \in s} f\_{updated}(x) = b * \prod\_{x \in s \setminus \{i\}} f(x)$.
|
Finset.prod_subtype_map_embedding
theorem Finset.prod_subtype_map_embedding :
∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] {p : α → Prop} {s : Finset { x // p x }}
{f : { x // p x } → β} {g : α → β},
(∀ x ∈ s, g ↑x = f x) →
((Finset.map (Function.Embedding.subtype fun x => p x) s).prod fun x => g x) = s.prod fun x => f x
This theorem asserts that for any types `α` and `β`, and any commutative monoid structure on `β`, a predicate `p` on `α`, a finset `s` of elements of `α` satisfying `p`, and any two functions `f` from `{ x // p x }` to `β` and `g` from `α` to `β`, if the function `g` agrees with the function `f` on the elements of `s` (in the sense that for each element `x` of `s`, `g` of the inclusion of `x` equals `f` of `x`), then the product of `g` over the image of `s` in `α` (obtained by mapping `s` with the embedding of `{ x // p x }` into `α`) is the same as the product of `f` over `s`. This theorem therefore relates the product of a function over a subset of a type (defined in terms of a predicate) to the product of another function over the type itself.
More concisely: If `p` is a predicate on type `α`, `s` is a finite subset of `α` satisfying `p`, `β` is a commutative monoid, `f : {x // p x} -> β`, `g : α -> β`, and `g` agrees with `f` on `s`, then the product of `g` over the image of `s` equals the product of `f` over `s`.
|
Finset.sum_powerset
theorem Finset.sum_powerset :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] (s : Finset α) (f : Finset α → β),
(s.powerset.sum fun t => f t) =
(Finset.range (s.card + 1)).sum fun j => (Finset.powersetCard j s).sum fun t => f t
The theorem `Finset.sum_powerset` states that for any given finset `s` and a function `f` from the powerset of `s` to a commutative monoid, the sum of `f` applied to each subset in the powerset of `s` is equal to the sum, over each natural number `j` up to the cardinality of `s`, of `f` applied to each subset of `s` with cardinality `j`. This theorem connects the sum over the entire powerset of `s` to the sum over all subsets of `s` of a specific size, effectively breaking down the total sum into smaller parts.
More concisely: For any finset `s` and commutative monoid-valued function `f` on the powerset of `s`, the sum of `f` over the powerset equals the sum of `f` over all subsets of `s` indexed by their cardinality.
|
Finset.prod_range_induction
theorem Finset.prod_range_induction :
∀ {β : Type u_4} [inst : CommMonoid β] (f s : ℕ → β),
s 0 = 1 → (∀ (n : ℕ), s (n + 1) = s n * f n) → ∀ (n : ℕ), ((Finset.range n).prod fun k => f k) = s n
This theorem states that for any function `f` and `s` mapping from natural numbers to elements of a commutative monoid (an algebraic structure equipped with an associative multiplication operation and an identity element), given that the function `s` at 0 is equal to the identity element and that for any natural number `n`, the value of `s` at `n + 1` is equal to the product of `s` at `n` and `f` at `n`, then, for any natural number `n`, the product of the function `f` evaluated at each element in the set of natural numbers less than `n` (expressed as `Finset.range n`) is equal to the value of `s` at `n`.
This theorem is a discrete multiplicative analogue of the fundamental theorem of calculus, it relates the product of the values of a function over a finite set to a function describing the accumulated product up to each point.
More concisely: For any commutative monoid homomorphism `f` and identity-starting sequence `s`, the product of `f` over the finite set of natural numbers less than `n` equals `s` at `n`.
|
Finset.sum_range_succ'
theorem Finset.sum_range_succ' :
∀ {β : Type u_4} [inst : AddCommMonoid β] (f : ℕ → β) (n : ℕ),
((Finset.range (n + 1)).sum fun k => f k) = ((Finset.range n).sum fun k => f (k + 1)) + f 0
The theorem `Finset.sum_range_succ'` states that for any given function `f` from natural numbers to a type `β` with additive commutative monoid structure, and for any natural number `n`, the sum of the function `f` evaluated over the range from 0 to `n+1` is equal to the sum of the function `f` evaluated at `k+1` over the range from 0 to `n` plus the function `f` evaluated at 0. In mathematical notation, this can be expressed as:
∑_{k=0}^{n+1} f(k) = f(0) + ∑_{k=0}^n f(k+1).
More concisely: The sum of a function's values from 0 to n+1 is equal to the sum of its values from 0 to n added to the value at 0. In Lean, this is expressed as `∑(k in 0..(n+1), f k) = f 0 + ∑(k in 0..n, f (succ k))`.
|
Finset.prod_cancels_of_partition_cancels
theorem Finset.prod_cancels_of_partition_cancels :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [inst : CommMonoid β] (R : Setoid α)
[inst_1 : DecidableRel Setoid.r],
(∀ x ∈ s, ((Finset.filter (fun y => y ≈ x) s).prod fun a => f a) = 1) → (s.prod fun x => f x) = 1
This theorem, `Finset.prod_cancels_of_partition_cancels`, states that for any finite set `s` of type `α` and any function `f` from `α` to a commutative monoid `β`, if we have a decidable equivalence relation `R` on `α` and for every element `x` in `s`, the product of `f a` for all elements `a` in `s` that are equivalent to `x` according to the equivalence relation `R` is equal to `1` (the identity element of the monoid), then the product of `f x` for all elements `x` in `s` is also equal to `1`. In other words, if we can partition `s` into subsets that "cancel out" under the function `f` (i.e., their product is `1`), then the entire set `s` also "cancels out" under `f` (i.e., its product is `1`).
More concisely: If `s` is a finite set, `f : α → β` is a function from `α` to a commutative monoid `β`, and `R` is a decidable equivalence relation on `α` such that the product of `f a` for all elements `a` in `s` that are equivalent to `x` according to `R` is equal to `1`, then the product of `f x` for all elements `x` in `s` is also equal to `1`.
|
Finset.prod_bijective
theorem Finset.prod_bijective :
∀ {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [inst : CommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α}
{g : κ → α} (e : ι → κ),
Function.Bijective e →
(∀ (i : ι), i ∈ s ↔ e i ∈ t) → (∀ i ∈ s, f i = g (e i)) → (s.prod fun i => f i) = t.prod fun i => g i
The theorem `Finset.prod_bijective` states that for any types `ι`, `κ`, and `α`, given an instance of a commutative monoid `α`, finite sets `s` and `t` (with elements of type `ι` and `κ`, respectively), and functions `f : ι → α` and `g : κ → α`, if there is a bijective function `e : ι → κ` such that for every element `i` of type `ι`, `i` is in `s` if and only if `e i` is in `t`, and for every `i` in `s`, `f i` equals `g (e i)`, then the product of the elements of `s` under `f` equals the product of elements of `t` under `g`. In other words, it's a special case of `Finset.prod_bij` that provides a condition under which the product of elements in two finite sets are equal, given a bijective map between the sets and corresponding elements of the sets under two functions give the same value.
More concisely: If `ι`, `κ`, and `α` are types with `α` a commutative monoid, `s : Finset ι`, `t : Finset κ`, `f : ι → α`, `g : κ → α`, and there exists a bijective function `e : ι → κ` such that for all `i ∈ ι`, `i ∈ s` if and only if `e i ∈ t` and for all `i ∈ s`, `f i = g (e i)`, then `∏ (x : s) f x = ∏ (y : t) g y`.
|
Finset.sum_eq_single
theorem Finset.sum_eq_single :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] {s : Finset α} {f : α → β} (a : α),
(∀ b ∈ s, b ≠ a → f b = 0) → (a ∉ s → f a = 0) → (s.sum fun x => f x) = f a
The theorem `Finset.sum_eq_single` states that for any type `α`, `β` with `β` being an Additive Commutative Monoid, a finite set `s` of type `α`, a function `f` from `α` to `β`, and an element `a` of type `α`, the sum of the function `f` over all elements in `s` equals `f(a)` if and only if two conditions are satisfied: first, for every element `b` in `s` which is not equal to `a`, `f(b)` is zero; second, if `a` is not in `s`, then `f(a)` is also zero. Essentially, this theorem is saying that the sum of function values over a finite set is determined by the function value at a specific point, given that all other function values are zero or the specific point is not in the set and its function value is zero.
More concisely: For any Additive Commutative Monoid type `β`, finite set `s` of type `α`, function `f` from `α` to `β`, and `α` element `a`, if `f(b) = 0` for all `b ∈ s ∖ {a}` and `f(a) = 0` when `a ∉ s`, then `∑ₕ i in s, f i = f a`.
|
Finset.sum_const_nat
theorem Finset.sum_const_nat :
∀ {α : Type u_3} {s : Finset α} {m : ℕ} {f : α → ℕ}, (∀ x ∈ s, f x = m) → (s.sum fun x => f x) = s.card * m := by
sorry
The theorem `Finset.sum_const_nat` states that for any type `α`, any finite set `s` of type `α`, any natural number `m`, and any function `f` from `α` to `ℕ` (natural numbers), if every element `x` in `s` maps to `m` under `f` (i.e., `f(x) = m` for all `x` in `s`), then the sum of `f(x)` as `x` ranges over the elements of the finite set `s` is equal to the cardinality of `s` (number of elements in `s`) multiplied by `m`.
More concisely: For any type `α`, finite set `s` of type `α`, natural number `m`, and function `f` from `α` to `ℕ` with `f(x) = m` for all `x` in `s`, we have `∑ x in s, f x = |s| * m`, where `|s|` denotes the cardinality of `s`.
|
Finset.prod_attach
theorem Finset.prod_attach :
∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] (s : Finset α) (f : α → β),
(s.attach.prod fun x => f ↑x) = s.prod fun x => f x
The theorem `Finset.prod_attach` states that for any finite set `s` of type `α` and any function `f` from `α` to `β` (where `β` is a commutative monoid), the product of `f x` as `x` ranges over the elements of the set `s` (denoted as `(Finset.prod s fun x => f x)`) is equal to the product of `f x` where `x` ranges over the elements of the set formed by attaching each element of `s` to its membership proof in `s` (denoted as `(Finset.prod (Finset.attach s) fun x => f ↑x)`). Here, `↑x` is a way to refer back to the original element from the subset. This theorem essentially states that "attaching" each element of a finite set to its membership proof does not change the product of the set under a given function.
More concisely: For any finite set `s` and function `f` from `α` to a commutative monoid `β`, the product of `f x` over `x` in `s` is equal to the product of `f (mem_s x)` over `x` in the set formed by attaching membership proofs to elements of `s`.
|
Finset.sum_induction
theorem Finset.sum_induction :
∀ {α : Type u_3} {s : Finset α} {M : Type u_6} [inst : AddCommMonoid M] (f : α → M) (p : M → Prop),
(∀ (a b : M), p a → p b → p (a + b)) → p 0 → (∀ x ∈ s, p (f x)) → p (s.sum fun x => f x)
This theorem states that to prove a certain property of a sum over a finite set, it is sufficient to fulfill three conditions. The first condition is that this property is additive; that is, if the property holds for two elements, it also holds for their sum. The second condition is that the property holds for the additive identity (zero). The third condition is that the property holds for each element in the finite set, after it is mapped by a function. If these conditions are met, then the property holds for the sum over the finite set, where each element in the set is mapped by the function before summing.
More concisely: If a property is additive, holds for the additive identity, and holds for each element mapped by a function in a finite set, then it holds for the sum of those elements mapped by the function.
|
Finset.sum_sigma'
theorem Finset.sum_sigma' :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] {σ : α → Type u_6} (s : Finset α)
(t : (a : α) → Finset (σ a)) (f : (a : α) → σ a → β),
(s.sum fun a => (t a).sum fun s => f a s) = (s.sigma t).sum fun x => f x.fst x.snd
The theorem `Finset.sum_sigma'` states that for any types `α` and `β`, given an additive commutative monoid structure on `β`, a function `σ` from `α` to another type, a finite set `s` of elements of type `α`, a function `t` that assigns to each element of `α` a finite set of elements of type `σ a`, and a function `f` that takes an element of `α` and an element of `σ a` and returns an element of `β`, the sum over `s` of the sum over `t a` of `f(a, s)` is equal to the sum over the finite set of dependent pairs `(i, a)` such that `i` is in `s` and `a` is in `t i` of `f(i, a)`.
In other words, it proves that the sum of sums of a function over sets defined by a function over a set is equal to the sum of that function over the set of all pairs defined by the original set and function.
More concisely: For any additive commutative monoid β, given a function σ : α → *, a finite set s ⊆ α, a function t : α → Finset β, and a function f : α × σ(α) → β, the sum ∑i ∈ s ∑j ∈ t(i) f(i, j) equals the sum ∑(i, j) ∈ Finset.product s (λi => t i) f.
|
Finset.sum_disj_sum
theorem Finset.sum_disj_sum :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : AddCommMonoid β] (s : Finset α) (t : Finset γ)
(f : α ⊕ γ → β),
((s.disjSum t).sum fun x => f x) = (s.sum fun x => f (Sum.inl x)) + t.sum fun x => f (Sum.inr x)
The theorem `Finset.sum_disj_sum` states that for any two finite sets `s` and `t` with elements of types `α` and `γ` respectively, and any function `f` from the disjoint union of `α` and `γ` to a type `β` which is equipped with an additive commutative monoid structure, the sum of `f` over the disjoint union of `s` and `t` is equal to the sum of `f` over `s` (where each element is included in the left part of the union) plus the sum of `f` over `t` (where each element is included in the right part of the union).
More concisely: For any finite sets `s` and `t` and additive commutative monoid-valued function `f` on their disjoint union, the sum of `f` over the union equals the sum over `s` plus the sum over `t`.
|
Finset.prod_nbij'
theorem Finset.prod_nbij' :
∀ {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [inst : CommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α}
{g : κ → α} (i : ι → κ) (j : κ → ι),
(∀ a ∈ s, i a ∈ t) →
(∀ a ∈ t, j a ∈ s) →
(∀ a ∈ s, j (i a) = a) →
(∀ a ∈ t, i (j a) = a) → (∀ a ∈ s, f a = g (i a)) → (s.prod fun x => f x) = t.prod fun x => g x
This theorem, `Finset.prod_nbij'`, states that for any two finite sets `s` of type ι and `t` of type κ, along with a function `f` mapping elements of `s` to any Commutative Monoid `α`, and a function `g` mapping elements of `t` to the same `α`, if there exists bijective mappings `i : ι → κ` and `j : κ → ι` which are inverses of each other on the domains of `s` and `t` respectively, and the function `f` applied on any element of `s` is equal to the function `g` applied on the image of that element under `i`, then the product of `f x` as `x` ranges over the elements of `s` is equal to the product of `g x` as `x` ranges over the elements of `t`.
In simpler terms, this theorem states that if you have two finite sets and a function on each set such that the functions are equal when transformed by a bijection, then the total product of each function over its respective set is the same.
More concisely: If two functions from finite sets to a commutative monoid are related by a bijection between the sets and are equal on the images of the sets under the bijection, then their respective products over the sets are equal.
|
Finset.sum_indicator_subset
theorem Finset.sum_indicator_subset :
∀ {ι : Type u_1} {β : Type u_4} [inst : AddCommMonoid β] (f : ι → β) {s t : Finset ι},
s ⊆ t → (t.sum fun i => (↑s).indicator f i) = s.sum fun i => f i
This theorem states that if we have a function `f` from a type `ι` to a type `β`, where `β` forms an additive commutative monoid, along with two finite sets (`Finsets`) `s` and `t` of elements of type `ι` such that `s` is a subset of `t`, then the sum of the indicator function of set `s` applied to each element of `t` (where the indicator function returns `f i` if `i` belongs to `s`, and `0` otherwise) is equal to the sum of `f i` for each element `i` in `s`. In other words, if we sum the function values over a potentially larger set but ignore the elements not in our original set using the indicator function, we get the same result as just summing the function over the original set.
More concisely: If `f` is a function from a type `ι` to an additive commutative monoid `β`, and `s` is a subset of `t` in `Finsets` of type `ι`, then the sum of the indicator function of `s` applied to `t` equals the sum of `f` applied to `s`.
|
Finset.prod_image
theorem Finset.prod_image :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} {f : α → β} [inst : CommMonoid β] [inst_1 : DecidableEq α]
{s : Finset γ} {g : γ → α},
(∀ x ∈ s, ∀ y ∈ s, g x = g y → x = y) → ((Finset.image g s).prod fun x => f x) = s.prod fun x => f (g x)
This theorem, `Finset.prod_image`, states that for any types `α`, `β`, and `γ`, any function `f` from `α` to `β` where `β` is a commutative monoid, and any function `g` from `γ` to `α`, if for any `x` and `y` in a finite set `s` of type `γ`, `g x` equals `g y` implies `x` equals `y`, then the product of `f x` for `x` in the image of `s` under `g` is equal to the product of `f (g x)` for `x` in `s`. In mathematical terms, this states that the product over a set is not affected by applying a function to the set elements provided the function does not identify different elements.
More concisely: Given a commutative monoid β, if function g from γ to a set X with elements having distinct images under g, then the product of f(g(x)) over the image of a finite set s under g is equal to the product of f(x) over x in s.
|
Finset.prod_ite_one
theorem Finset.prod_ite_one :
∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] (s : Finset α) (p : α → Prop) [inst_1 : DecidablePred p],
(∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j) →
∀ (a : β), (s.prod fun i => if p i then a else 1) = if ∃ i ∈ s, p i then a else 1
The theorem `Finset.prod_ite_one` states that for any type `α` and a commutative monoid `β`, given a set `s` of type `α`, a predicate `p` on `α` that is decidable for each element in `α`, and an element `a` of type `β`, if every pair of distinct elements in `s` that satisfy `p` are equal, then the product over `s` of the function which maps each element `i` in `s` to `a` if `p i` is true and to `1` otherwise, is equal to `a` if there exists an element in `s` that satisfies `p`, and is `1` otherwise. In other words, if all the elements in the set satisfying the predicate are the same, the product is either `a` (if such an element exists) or `1`.
More concisely: Given a commutative monoid `β`, set `s` of decidable predicate `p` on type `α`, if every pair of distinct elements in `s` that satisfy `p` are equal, then the product over `s` of the function which maps each element `i` in `s` to `a` if `p i` is true and to `1` otherwise, equals `a` if there exists an element in `s` satisfying `p`, and equals `1` otherwise.
|
Finset.prod_disjiUnion
theorem Finset.prod_disjiUnion :
∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} {f : α → β} [inst : CommMonoid β] (s : Finset ι) (t : ι → Finset α)
(h : (↑s).PairwiseDisjoint t), ((s.disjiUnion t h).prod fun x => f x) = s.prod fun i => (t i).prod fun x => f x
The theorem `Finset.prod_disjiUnion` states that for any type `ι`, `α`, `β`, and a function `f` from `α` to `β` with a commutative monoid structure on `β`, given a finite set `s` of elements of type `ι`, a function `t` from `ι` to finite sets of `α` such that the images of any two distinct elements under `t` are disjoint sets, the product over the disjoint union of the sets `t i` for `i` in `s` (using the function `f`) is equal to the product over `s` of the product over `t i` (using the function `f`). In mathematical notation, this can be represented as
\[
\prod_{x \in \bigcup_{i\in s}t i} f(x) = \prod_{i\in s} \left(\prod_{x \in t i} f(x)\right)
\]
where the union in the left-hand side is a disjoint union. The theorem essentially says that when dealing with a product over a disjoint union of sets, you can distribute the product over the union.
More concisely: For any commutative monoid `β`, given a function `f` from a type `α` to `β`, and a finite set `s` of elements of type `ι` with disjoint images under a function `t` from `ι` to finite sets of `α`, the product of `f` over the disjoint union of `t i` equals the product of the products of `f` over each `t i` in `s`.
|
Finset.sum_range_induction
theorem Finset.sum_range_induction :
∀ {β : Type u_4} [inst : AddCommMonoid β] (f s : ℕ → β),
s 0 = 0 → (∀ (n : ℕ), s (n + 1) = s n + f n) → ∀ (n : ℕ), ((Finset.range n).sum fun k => f k) = s n
The theorem `Finset.sum_range_induction` states that for any function `f` and `s` from natural numbers to a type `β` that forms a commutative monoid, given that the value of `s` at `0` is the additive identity (zero), and for all natural numbers `n`, the value of `s` at `n + 1` is the sum of `s` at `n` and `f` at `n`, then for all natural numbers `n`, the sum of `f` over the set of natural numbers less than `n` (i.e., `{0, ..., n - 1}`) is equal to the value of `s` at `n`. This is a discrete version of the fundamental theorem of calculus, and the condition on `s` can be thought of as a discrete version of a definite integral from `0` to `n` of `f`.
More concisely: For any commutative monoid `β` and function `f : ℕ → β` such that `s(0) = 0` and `s(n + 1) = s(n) + f(n)` for all natural numbers `n`, the sum of `f` over the range `{0, ..., n - 1}` equals `s(n)`.
|
Finset.prod_union
theorem Finset.prod_union :
∀ {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f : α → β} [inst : CommMonoid β] [inst_1 : DecidableEq α],
Disjoint s₁ s₂ → ((s₁ ∪ s₂).prod fun x => f x) = (s₁.prod fun x => f x) * s₂.prod fun x => f x
The theorem `Finset.prod_union` states that for any types `α` and `β`, two finite sets of type `α` namely `s₁` and `s₂`, and a function `f` from `α` to `β`, given a commutative monoid structure on `β` and a way to decide equality in `α`, if `s₁` and `s₂` are disjoint (meaning that their intersection is the bottom element), then the product of `f` over the union of `s₁` and `s₂` is equal to the product of `f` over `s₁` multiplied by the product of `f` over `s₂`. In mathematical notation, this is saying $\prod_{x \in s_1 \cup s_2} f(x) = \prod_{x \in s_1} f(x) \times \prod_{x \in s_2} f(x)$, provided $s_1$ and $s_2$ are disjoint.
More concisely: Given finite sets `s₁` and `s₂` of type `α` that are disjoint and have a commutative monoid structure on type `β` with equality decidable in `α`, the product of a function `f` from `α` to `β` over the union of `s₁` and `s₂` equals the product of `f` over `s₁` multiplied by the product of `f` over `s₂`. That is, $\prod\_{x \in s\_1 \cup s\_2} f(x) = \prod\_{x \in s\_1} f(x) \times \prod\_{x \in s\_2} f(x)$.
|
Finset.prod_equiv
theorem Finset.prod_equiv :
∀ {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [inst : CommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α}
{g : κ → α} (e : ι ≃ κ),
(∀ (i : ι), i ∈ s ↔ e i ∈ t) → (∀ i ∈ s, f i = g (e i)) → (s.prod fun i => f i) = t.prod fun i => g i
The `Finset.prod_equiv` theorem states that for any types `ι`, `κ`, and `α` where `α` is a commutative monoid, given two finite sets `s` and `t` with elements from `ι` and `κ` respectively, functions `f : ι → α` and `g : κ → α`, and a bijective function `e : ι ≃ κ`, if for every element `i` in `s`, `i` maps to an element in `t` under `e`, and the function `f` applied to `i` is equal to the function `g` applied to `e(i)`, then the product of `f(i)` as `i` ranges over the elements of `s` is equal to the product of `g(i)` as `i` ranges over the elements of `t`. This theorem generalizes the idea that changing the labels of the elements does not change the product of a sequence.
More concisely: Given finite sets `s` and `t` from type `Finset ι` and `Finset κ`, bijective function `e : ι ≃ κ`, functions `f : ι → α` and `g : κ → α` such that `f i = g (e i)` for all `i` in `s`, the product of `f` over `s` equals the product of `g` over `t`.
|
Finset.sum_subtype_eq_sum_filter
theorem Finset.sum_subtype_eq_sum_filter :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} [inst : AddCommMonoid β] (f : α → β) {p : α → Prop}
[inst_1 : DecidablePred p], ((Finset.subtype p s).sum fun x => f ↑x) = (Finset.filter p s).sum fun x => f x
The theorem `Finset.sum_subtype_eq_sum_filter` states that for any finite set `s` of elements of type `α`, a function `f` from `α` to `β`, and a decidable predicate `p`, the sum of the function `f` over the elements of the subset of `s` that satisfy the predicate `p` (expressed using `Finset.subtype`) is equal to the sum of the function `f` over the elements of `s` that satisfy the predicate `p` (expressed using `Finset.filter`). Here, `β` is assumed to be an additive commutative monoid, meaning that addition is defined, associative, and commutative in `β`, and there's a zero element in `β` that doesn't change other elements when added.
More concisely: For any finite set `s` of elements from a type `α`, decidable predicate `p` on `α`, and additive commutative monoid `β`, the sum of `f` over the subset of `s` satisfying `p` using `Finset.subtype` equals the sum over the subset of `s` satisfying `p` using `Finset.filter`.
|
Finset.sum_indicator_subset_of_eq_zero
theorem Finset.sum_indicator_subset_of_eq_zero :
∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] [inst_1 : Zero α] (f : ι → α)
(g : ι → α → β) {s t : Finset ι},
s ⊆ t → (∀ (a : ι), g a 0 = 0) → (t.sum fun i => g i ((↑s).indicator f i)) = s.sum fun i => g i (f i)
This theorem states that for any types `ι`, `α`, and `β`, with `β` being an additive commutative monoid and `α` having zero, for any functions `f : ι → α` and `g : ι → α → β`, and for any finsets `s` and `t` of type `ι`, if `s` is a subset of `t` and `g` maps any element to `0` when the second argument is `0`, then the sum of `g i ((↑s).indicator f i)` over `t` equals the sum of `g i (f i)` over `s`. In other words, we can replace the finset `s` with a possibly larger finset `t` in the sum, when we replace `f` with the corresponding indicator function, without changing the value of the sum.
More concisely: For any additive commutative monoid β, functions f : ι -> α with α having zero, and g : ι -> α -> β, if s and t are finsets of type ι such that s is a subset of t and g maps any element to 0 when the second argument is 0, then the sum of g i ((up s).indicator f i) over t equals the sum of g i (f i) over s.
|
Finset.mul_prod_erase
theorem Finset.mul_prod_erase :
∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] [inst_1 : DecidableEq α] (s : Finset α) (f : α → β) {a : α},
a ∈ s → (f a * (s.erase a).prod fun x => f x) = s.prod fun x => f x
This theorem states that in a commutative monoid `β`, for any finite set `s` of type `α` with decidable equality and any function `f` mapping `α` to `β`, and for any element `a` of `α` that is in `s`, the product of the function `f` over the entire set `s` is equal to the product of the function `f` on `a` multiplied by the product over the set `s` with `a` removed. In other words, multiplying an element of a set by the product of the rest of the elements in the set is equivalent to taking the product over the entire set. This is the finite set version of a similar property in multisets.
More concisely: For any commutative monoid `β`, function `f` from a finite decidably equal set `s` of type `α` to `β`, and element `a` in `s`, we have `f (∑ i in s, a\_i) = f a * ∑ i in s, if i != a then f a\_i`.
|
Finset.eq_of_card_le_one_of_prod_eq
theorem Finset.eq_of_card_le_one_of_prod_eq :
∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] {s : Finset α},
s.card ≤ 1 → ∀ {f : α → β} {b : β}, (s.prod fun x => f x) = b → ∀ x ∈ s, f x = b
This theorem states that if a `Finset` (a finite set) `s` of some type `α` has at most one element (i.e., its cardinality is less than or equal to 1), and the product of the elements in `s` (mapped through some function `f` from `α` to another type `β`, where `β` is a commutative monoid) equals to a certain value `b`, then the function `f` applied to any element `x` in the `Finset` `s` also equals `b`. This essentially means that each element in a singleton or empty `Finset`, when put through a function `f`, results in the product of the whole `Finset`.
More concisely: If `s` is a finite set of type `α` with at most one element and the product of `f(x)` for all `x` in `s` equals `b`, then `f(x) = b` for all `x` in `s`.
|
Finset.prod_sdiff
theorem Finset.prod_sdiff :
∀ {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f : α → β} [inst : CommMonoid β] [inst_1 : DecidableEq α],
s₁ ⊆ s₂ → (((s₂ \ s₁).prod fun x => f x) * s₁.prod fun x => f x) = s₂.prod fun x => f x
This theorem is about the product of elements in finite sets using a certain function. Specifically, for any types `α` and `β`, any two finite sets `s₁` and `s₂` of type `α`, and any function `f` from `α` to `β`, given that `β` forms a commutative monoid and equality for type `α` is decidable, if `s₁` is a subset of `s₂`, the product of `f(x)` for every `x` in the difference of `s₂` and `s₁`, multiplied by the product of `f(x)` for every `x` in `s₁`, is equal to the product of `f(x)` for every `x` in `s₂`. In other words, the product over a set can be decomposed into the product over a subset and the product over the complement of the subset.
More concisely: For any commutative monoid type `β`, decidably equal types `α`, finite sets `s₁ ⊆ s₂` of `α`, and function `f` from `α` to `β`, the product of `f(x)` for all `x ∈ s₂ \ s₁` multiplied by the product of `f(x)` for all `x ∈ s₁` equals the product of `f(x)` for all `x ∈ s₂`.
|
Finset.prod_sigma
theorem Finset.prod_sigma :
∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] {σ : α → Type u_6} (s : Finset α) (t : (a : α) → Finset (σ a))
(f : Sigma σ → β), ((s.sigma t).prod fun x => f x) = s.prod fun a => (t a).prod fun s => f ⟨a, s⟩
The theorem `Finset.prod_sigma` states that for a given finite set `s` of type `α`, a function `t` mapping each element of `α` to a finite set of some type `σ a`, and a function `f` mapping each dependent pair of type `Sigma σ` to the commutative monoid `β`, the product of `f x` over the set of dependent pairs (`Finset.sigma s t`) is equal to the product of the product of `f { fst := a, snd := s }` over the set `t a` for each element `a` in `s`. In simpler terms, it asserts that the product over a sigma type equals the product of fiberwise products.
More concisely: For a finite set `s` and functions `t: α → Σ σ` and `f: Σ σ → β`, the product of `f` over `Finset.sigma s t` equals the product of the fiberwise products of `f` over each set `t a` for each `a` in `s`.
|
Finset.sum_powersetCard
theorem Finset.sum_powersetCard :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] (n : ℕ) (s : Finset α) (f : ℕ → β),
((Finset.powersetCard n s).sum fun t => f t.card) = s.card.choose n • f n
This theorem states that for any type `α`, type `β` with an additive commutative monoid structure, any natural number `n`, any finset `s` of type `α`, and any function `f` from natural numbers to `β`, the sum of the function `f` applied to the cardinality of all subsets of `s` of cardinality `n` (obtained by `Finset.powersetCard n s`) equals the binomial coefficient of the cardinality of `s` and `n` (represented as `s.card.choose n`) multiplied by the value of the function `f` at `n`. In LaTeX, the statement of the theorem would be: For all sets $s$, numbers $n$, and functions $f$, we have $\sum_{t \in \text{powersetCard}(n, s)} f(|t|) = \binom{|s|}{n} \cdot f(n)$.
More concisely: For any set $s$, function $f$ from natural numbers to a commutative additive monoid, and natural number $n$, the sum of $f$ applied to the cardinalities of all subsets of $s$ with cardinality $n$ equals the binomial coefficient of $|s|$ and $n$ times $f(n)$.
|
Finset.sum_const
theorem Finset.sum_const :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} [inst : AddCommMonoid β] (b : β), (s.sum fun _x => b) = s.card • b
The theorem `Finset.sum_const` states that for any type `α`, type `β`, a finite set `s` of type `α`, and an instance of additive commutative monoid for `β`, and any element `b` of type `β`, the sum of the constant function `b` over all elements in the set `s` is equal to the product of the cardinality of the set `s` and `b`. In other words, if we add up a constant `b` for every element in the set `s`, we get the same result as multiplying `b` by the number of elements in `s`.
More concisely: For any finite set `s` of type `α` and any additive commutative monoid `β` with an element `b`, the sum of the constant function `b` over `s` equals the product of the cardinality of `s` and `b`.
|
Finset.sum_const_zero
theorem Finset.sum_const_zero :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} [inst : AddCommMonoid β], (s.sum fun _x => 0) = 0
The theorem `Finset.sum_const_zero` states that for any finite set `s` of any type `α` and for any type `β` that forms an additive commutative monoid, the sum of the constant function that always returns zero over all elements in `s` is zero. In other words, if you sum up zero for each element in a finite set, the total sum will be zero.
More concisely: For any finite set `s` and any additive commutative monoid `β`, the sum of the constant function mapping every element of `s` to the additive identity of `β` is the additive identity of `β`.
|
Finset.prod_erase_mul
theorem Finset.prod_erase_mul :
∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] [inst_1 : DecidableEq α] (s : Finset α) (f : α → β) {a : α},
a ∈ s → ((s.erase a).prod fun x => f x) * f a = s.prod fun x => f x
This theorem, `Finset.prod_erase_mul`, states that for any finite set `s` of elements of type `α`, a function `f` from `α` to a type `β` that forms a commutative monoid, and an element `a` of type `α` that belongs to `s`, the product of `f` over all elements in `s` excluding `a`, then multiplied by `f(a)`, is equal to the product of `f` over all elements in `s`. In other words, the order of multiplication does not affect the total product in the context of a finite set, which is a reflection of the commutative property of the monoid. This theorem also requires that equality between elements of type `α` is decidable.
More concisely: For any commutative monoid homomorphism `f` from a finite set `s` of type `α` to type `β`, and any element `a` in `s`, the product of `f` over all elements in `s` excluding `a`, multiplied by `f(a)`, equals the product of `f` over all elements in `s`.
|
Finset.sum_comm
theorem Finset.sum_comm :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : AddCommMonoid β] {s : Finset γ} {t : Finset α}
{f : γ → α → β}, (s.sum fun x => t.sum fun y => f x y) = t.sum fun y => s.sum fun x => f x y
The theorem `Finset.sum_comm` states that for all types `α`, `β`, and `γ`, given an additive commutative monoid over `β`, a finite set `s` of type `γ`, a finite set `t` of type `α`, and a function `f` from `γ` to `α` to `β`, the sum over `s` of the sums over `t` of `f x y` is equal to the sum over `t` of the sums over `s` of `f x y`. In mathematical terms, this theorem is stating the commutativity of the sum, i.e., $\sum_{x \in s} \sum_{y \in t} f(x, y) = \sum_{y \in t} \sum_{x \in s} f(x, y)$.
More concisely: For all additive commutative monoids over type `β`, finite sets `s` of type `γ` and `t` of type `α`, and functions `f` from `γ` to `α` to `β`, the sum over `s` of the sums over `t` of `f x y` equals the sum over `t` of the sums over `s` of `f x y`. (Mathematically: $\sum\_{x \in s} \sum\_{y \in t} f(x, y) = \sum\_{y \in t} \sum\_{x \in s} f(x, y)$)
|
Finset.sum_eq_multiset_sum
theorem Finset.sum_eq_multiset_sum :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] (s : Finset α) (f : α → β),
(s.sum fun x => f x) = (Multiset.map f s.val).sum
This theorem states that for any given type `α` and `β`, where `β` is a commutative additive monoid, a function `f` from `α` to `β`, and a finite set `s` of type `α`, the sum of the function `f` applied to all elements in set `s` (as expressed by `Finset.sum s f`) is equal to the sum of the multiset obtained by mapping the function `f` over all the elements of `s` (as expressed by `Multiset.sum (Multiset.map f s.val)`). In other words, taking the sum over a finite set or over a multiset obtained from that set yields the same result.
More concisely: For any commutative additive monoid type `β`, function `f` from type `α` to `β`, and finite set `s` of type `α`, the sum of `Finset.sum s f` equals the sum of `Multiset.sum (Multiset.map f s.val)`.
|
Finset.sum_subset
theorem Finset.sum_subset :
∀ {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f : α → β} [inst : AddCommMonoid β],
s₁ ⊆ s₂ → (∀ x ∈ s₂, x ∉ s₁ → f x = 0) → (s₁.sum fun x => f x) = s₂.sum fun x => f x
The theorem `Finset.sum_subset` states that for any types `α` and `β`, any two finite sets `s₁` and `s₂` of type `α`, and any function `f` that maps from `α` to `β` (where `β` is an additive commutative monoid), if `s₁` is a subset of `s₂` and for all elements `x` in `s₂` that do not belong to `s₁`, `f(x)` equals zero, then the sum of the function `f` applied to the elements of `s₁` equals the sum of the function `f` applied to the elements of `s₂`. In mathematical notation, this can be written as: if $s₁ \subseteq s₂$ and $\forall x \in s₂, x \notin s₁ \rightarrow f(x) = 0$, then $\sum_{x \in s₁} f(x) = \sum_{x \in s₂} f(x)$.
More concisely: If two finite sets have the same elements with the remaining elements of one set mapping to zero under a function defined on an additive commutative monoid, then the sum of the function over the first set equals the sum over the second set.
|
Finset.sum_eq_zero
theorem Finset.sum_eq_zero :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] {f : α → β} {s : Finset α},
(∀ x ∈ s, f x = 0) → (s.sum fun x => f x) = 0
The theorem `Finset.sum_eq_zero` states that for any type `α`, any type `β` which forms an additive commutative monoid, a function `f` from `α` to `β`, and a finite set `s` of type `α`, if every element `x` in `s` maps to `0` under the function `f`, then the sum of the function `f` applied to each element in `s` equals `0`. In math terms, this could be written as: if for all $x \in s$, we have $f(x) = 0$, then $\sum_{x \in s} f(x) = 0$.
More concisely: For any additive commutative monoid type `β`, function `f` from type `α` to `β`, and finite set `s` of type `α` with all elements mapping to `0` under `f`, we have $\sum_{x \in s} f(x) = 0$.
|
Finset.sum_dite_eq'
theorem Finset.sum_dite_eq' :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] [inst_1 : DecidableEq α] (s : Finset α) (a : α)
(b : (x : α) → x = a → β), (s.sum fun x => if h : x = a then b x h else 0) = if a ∈ s then b a ⋯ else 0
This theorem is about the sum of a function over a finite set in Lean. It states that for any given type `α`, type `β` that is an additive commutative monoid, a finite set `s` of elements of type `α`, and any specific element `a` of type `α`, when we have a function `b` that maps an element `x` and a proof that `x = a` to `β`, the sum of function values over set `s` where each function value is determined by an if-then-else expression (`b x h` if `x = a` otherwise `0`) is equal to the value of `b a` if `a` belongs to the set `s` and `0` otherwise. This theorem is particularly useful when we want to compute the sum of a function at a specific point in a finite set, effectively isolating the contribution of a particular element to the sum.
More concisely: For any additive commutative monoid type `β`, finite set `s` of type `α`, and function `b : α → β`, the sum of `b x <| x ∈ s` equals `b a` if `a ∈ s`, and `0` otherwise.
|
Finset.sum_disjUnion
theorem Finset.sum_disjUnion :
∀ {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f : α → β} [inst : AddCommMonoid β] (h : Disjoint s₁ s₂),
((s₁.disjUnion s₂ h).sum fun x => f x) = (s₁.sum fun x => f x) + s₂.sum fun x => f x
This theorem is stating that for any two disjoint finite sets `s₁` and `s₂` of type `α`, and any function `f` from `α` to `β` where `β` is an additive commutative monoid, the sum of the function `f` over the disjoint union of `s₁` and `s₂` is equal to the sum of `f` over `s₁` plus the sum of `f` over `s₂`. In other words, when computing the sum of `f` over the elements of the disjoint union of `s₁` and `s₂`, we can instead compute the sum of `f` over the elements of `s₁` and `s₂` separately and then add the results together. This is analogous to the principle of inclusion-exclusion in mathematics.
More concisely: For any additive commutative monoid β and disjoint finite sets s₁ and s₂ of type α, the sum of a function f from α to β over the disjoint union of s₁ and s₂ equals the sum of f over s₁ plus the sum of f over s₂.
|
Finset.prod_subtype_eq_prod_filter
theorem Finset.prod_subtype_eq_prod_filter :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} [inst : CommMonoid β] (f : α → β) {p : α → Prop}
[inst_1 : DecidablePred p], ((Finset.subtype p s).prod fun x => f ↑x) = (Finset.filter p s).prod fun x => f x
This theorem states that for any finite set `s` of elements of type `α`, a commutative monoid `β`, a function `f` from `α` to `β`, and a decidable predicate `p` on `α`, the product of the function `f` applied to elements of the subtype of `s` satisfying the predicate `p` is equal to the product of `f` applied to elements of `s` that satisfy the predicate `p`. In simpler terms, it says that the product remains the same whether we calculate it over a subtype or over a filtered set, as long as the filtering condition is the same.
More concisely: For any finite set `s` in type `α`, commutative monoid `β`, function `f` from `α` to `β`, and decidable predicate `p` on `α`, the product of `f` over `s` restricted to elements satisfying `p` equals the product of `f` over all elements of `s` satisfying `p`.
|
Equiv.prod_comp'
theorem Equiv.prod_comp' :
∀ {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : CommMonoid α]
(e : ι ≃ κ) (f : ι → α) (g : κ → α),
(∀ (x : ι), f x = g (e x)) → (Finset.univ.prod fun x => f x) = Finset.univ.prod fun x => g x
The theorem `Equiv.prod_comp'` states that for any types ι, κ and α, where ι and κ are finite types and α is a commutative monoid, given a bijective function `e` from ι to κ, and functions `f : ι → α` and `g : κ → α` such that `f(x) = g(e(x))` for all `x` in ι, the product of the function `f` over the universal set of ι equals the product of the function `g` over the universal set of κ. This theorem is a specialization of `Finset.prod_bij` that automatically fills in most arguments, and it is an alias of `Fintype.prod_equiv`. There is a version of the theorem, `Equiv.prod_comp`, that doesn't require the hypothesis `h : ∀ (x : ι), f x = g (e x)`.
More concisely: For finite types ι, κ and a commutative monoid α, if there is a bijective function e from ι to κ and functions f and g such that f(x) = g(e(x)) for all x in ι, then the product of f over ι equals the product of g over κ.
|
Finset.sum_filter_add_sum_filter_not
theorem Finset.sum_filter_add_sum_filter_not :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] (s : Finset α) (p : α → Prop) [inst_1 : DecidablePred p]
[inst_2 : (x : α) → Decidable ¬p x] (f : α → β),
(((Finset.filter p s).sum fun x => f x) + (Finset.filter (fun x => ¬p x) s).sum fun x => f x) =
s.sum fun x => f x
This theorem, named `Finset.sum_filter_add_sum_filter_not`, states that for any finite set `s` of elements of type `α`, a property `p` that can be decided for each element, and a function `f` from `α` to `β` (where `β` is a type with an associated commutative addition operation), the sum of `f(x)` over elements `x` in `s` that satisfy property `p`, added to the sum of `f(x)` over elements `x` in `s` that do not satisfy property `p`, equals to the sum of `f(x)` over all elements `x` in `s`. This theorem is essentially expressing the partition of a finite sum into two parts according to whether elements satisfy a certain property or not.
More concisely: For any finite set `s` and function `f` from a type with commutative addition, the sum of `f` applied to elements in `s` satisfying a property equals the sum of `f` applied to all elements in `s`, partitioned by elements satisfying or not satisfying the property.
|
Finset.prod_insert
theorem Finset.prod_insert :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [inst : CommMonoid β] [inst_1 : DecidableEq α],
a ∉ s → ((insert a s).prod fun x => f x) = f a * s.prod fun x => f x
The theorem `Finset.prod_insert` states that for any types `α` and `β`, a finite set `s` of type `α`, an element `a` of type `α`, and a function `f` from `α` to `β`, given that `β` forms a commutative monoid and `α` has decidable equality, if `a` is not an element of `s`, then the product of the function `f` evaluated over the set resulting from the insertion of `a` into `s` is equal to the product of `f` evaluated at `a` and the product of `f` evaluated over `s`. In mathematical terms, if $a \notin s$, then $\prod_{x \in s \cup \{a\}} f(x) = f(a) \cdot \prod_{x \in s} f(x)$.
More concisely: For any commutative monoid β and type α with decidable equality, if a is not an element of finite set s and f is a function from α to β, then f(a) * ∏x∈s f(x) = ∏x∈s∪{a} f(x).
|
List.prod_toFinset
theorem List.prod_toFinset :
∀ {α : Type u_3} {M : Type u_6} [inst : DecidableEq α] [inst_1 : CommMonoid M] (f : α → M) {l : List α},
l.Nodup → l.toFinset.prod f = (List.map f l).prod
This theorem states that for any type `α` with a decidable equality, and any type `M` that forms a commutative monoid, given a function `f` mapping elements of `α` to `M` and a list `l` of type `α` with no duplicate elements (i.e., `List.Nodup l`), the product of the function `f` applied to each element in the finset created from `l` (i.e., `Finset.prod (List.toFinset l) f`) is equal to the product of the list created by mapping the function `f` onto each element in `l` (i.e., `List.prod (List.map f l)`). In other words, removing duplicates and applying a function before multiplying (in a commutative monoid sense) is the same as applying the function and then multiplying.
More concisely: For any decidably equal type `α` and commutative monoid `M`, the product of a function from `α` to `M` applied to the unique elements of a list from `α`, equals the product of the list of the function applications.
|
Finset.sum_congr_set
theorem Finset.sum_congr_set :
∀ {α : Type u_6} [inst : AddCommMonoid α] {β : Type u_7} [inst_1 : Fintype β] (s : Set β)
[inst_2 : DecidablePred fun x => x ∈ s] (f : β → α) (g : ↑s → α),
(∀ (x : β) (h : x ∈ s), f x = g ⟨x, h⟩) → (∀ x ∉ s, f x = 0) → Finset.univ.sum f = Finset.univ.sum g
This theorem, `Finset.sum_congr_set`, states that for any types `α` (which is an additive commutative monoid) and `β` (which is a finite type), a set `s` of elements of type `β`, a predicate to decide membership in `s`, and two functions `f : β → α` and `g : ↑s → α`, the sum of all values of `g` over the set `s` is equal to the sum of all values of `f` over the entire universe if two conditions are met: Firstly, `f` and `g` must agree on `s`, meaning for every element `x` in `s`, `f(x)` must be equal to `g(x)`. Secondly, `f(x)` must be equal to zero for all `x` not in `s`. In other words, if the function `f` behaves like `g` on the set `s` and is zero everywhere else, the total sum of the function `f` over the universe is the same as the sum of `g` over the set `s`.
More concisely: If `f : β → α` agrees with a function `g : s → α` on a finite set `s` of type `β` and `f(x) = 0` for all `x ∉ s`, then `∑ x in β, f x = ∑ x in s, g x`.
|
map_sum
theorem map_sum :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : AddCommMonoid β] [inst_1 : AddCommMonoid γ] {G : Type u_6}
[inst_2 : FunLike G β γ] [inst_3 : AddMonoidHomClass G β γ] (g : G) (f : α → β) (s : Finset α),
g (s.sum fun x => f x) = s.sum fun x => g (f x)
This theorem, `map_sum`, states that for any types `α`, `β`, `γ` and `G`, with `β` and `γ` being additive commutative monoids, and `G` being a function-like type from `β` to `γ` with a additive monoid homomorphism, and for any function `g : G`, function `f : α → β` and finite set `s : Finset α`, applying the function `g` to the sum of the results of applying `f` to each element in `s` is the same as first applying `f` to each element in `s`, then applying `g` to each result, and finally summing these results. In mathematical terms, this can be represented as $g(\sum_{x\in s} f(x)) = \sum_{x\in s} g(f(x))$. This is a property of homomorphisms in the context of additive commutative monoids.
More concisely: For any additive commutative monoids β and γ, additive monoid homomorphism G: β -> γ, and function f: α -> β, the map G o (∑ x in s. f x) equals ∑ x in s. (G o f x), where s is a finite set and ∑ denotes summation.
|
Finset.sum_erase
theorem Finset.sum_erase :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] [inst_1 : DecidableEq α] (s : Finset α) {f : α → β}
{a : α}, f a = 0 → ((s.erase a).sum fun x => f x) = s.sum fun x => f x
The theorem `Finset.sum_erase` states that for any type `α`, type `β` that forms an additive commutative monoid, a function `f` from `α` to `β`, and a `Finset` `s` of `α` elements, if the function `f` evaluated at a specific point `a` of `α` equals zero, then the sum of the function values over the `Finset` `s` remains unchanged when the point `a` is removed from the `Finset`. In other words, if $f(a)=0$, then $\sum_{x \in s \setminus \{a\}}f(x) = \sum_{x \in s}f(x)$, where $s$ is a finite set.
More concisely: If `α` is a type, `β` an additive commutative monoid, `f` a function from `α` to `β`, and `s` a `Finset` of `α`, then removing an element `a` from `s` with `f(a) = 0` leaves the sum of function values over `s` unchanged: $\sum\_{x \in s \setminus \{a\}} f(x) = \sum\_{x \in s} f(x)$.
|
Finset.sum_sigma
theorem Finset.sum_sigma :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] {σ : α → Type u_6} (s : Finset α)
(t : (a : α) → Finset (σ a)) (f : Sigma σ → β),
((s.sigma t).sum fun x => f x) = s.sum fun a => (t a).sum fun s => f ⟨a, s⟩
The theorem `Finset.sum_sigma` states that for any finset `s` of elements of type `α`, and for any function `t` producing a finset of type `σ a` for each `a` in `α`, the sum over the finset of dependent pairs (sigma type) obtained from `s` and `t` of a function `f` is equal to the sum of the fiberwise sums over `s` and `t`. This means that the total sum of `f` applied to each pair is the same whether we first sum over each fiber (`t a`) for a fixed `a` in `s`, and then sum over `s`, or if we flatten all pairs into a single finset and then sum over it.
More concisely: For any finset `s` and function `t` that maps each element of `s` to a finset of type `σ a`, the sum of `f` applied to the dependent pairs of `s` and `t` is equal to the sum of fiberwise sums of `f` over `s` and `t`.
|
Finset.prod_induction_nonempty
theorem Finset.prod_induction_nonempty :
∀ {α : Type u_3} {s : Finset α} {M : Type u_6} [inst : CommMonoid M] (f : α → M) (p : M → Prop),
(∀ (a b : M), p a → p b → p (a * b)) → s.Nonempty → (∀ x ∈ s, p (f x)) → p (s.prod fun x => f x)
This theorem, `Finset.prod_induction_nonempty`, states that if you want to prove a property about a product of elements in a non-empty finite set, it is enough to show two things: First, that the property is multiplicative, meaning that if the property holds for two elements `a` and `b`, then it also holds for their product `a * b`. Second, that the property holds for every element in the set. In more specific terms, given a finite set `s` of an arbitrary type `α`, a function `f` from `α` to another type `M` which forms a commutative monoid, and a property `p` that `M` elements may satisfy, if `p` is multiplicative and `p (f x)` holds for all `x` in `s`, then `p` also holds for the product of `f x` over all `x` in `s`.
More concisely: If a property is multiplicative and holds for all elements in a non-empty finite set, then it holds for the product of those elements in the set.
|
Equiv.sum_comp'
theorem Equiv.sum_comp' :
∀ {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : AddCommMonoid α]
(e : ι ≃ κ) (f : ι → α) (g : κ → α),
(∀ (x : ι), f x = g (e x)) → (Finset.univ.sum fun x => f x) = Finset.univ.sum fun x => g x
The theorem `Equiv.sum_comp'` states that for any types `ι`, `κ`, and `α` with `ι` and `κ` being finite types and `α` being an additive commutative monoid, given an equivalence `e` from `ι` to `κ`, and functions `f` from `ι` to `α` and `g` from `κ` to `α`, if for each element `x` of type `ι`, `f(x)` is equal to `g(e(x))`, then the sum of `f` over all elements in the universal finite set of `ι` is equal to the sum of `g` over all elements in the universal finite set of `κ`. In other words, this theorem guarantees the equality of sums under an equivalent transformation that respects the function mapping.
More concisely: For finite types `ι` and `κ` and an additive commutative monoid `α`, if there exists an equivalence `e` from `ι` to `κ` such that `f(x) = g(e(x))` for all `x` in `ι`, then the sum of `f` over `ι` equals the sum of `g` over `κ`.
|
Finset.sum_dite_eq
theorem Finset.sum_dite_eq :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] [inst_1 : DecidableEq α] (s : Finset α) (a : α)
(b : (x : α) → a = x → β), (s.sum fun x => if h : a = x then b x h else 0) = if a ∈ s then b a ⋯ else 0
This theorem, `Finset.sum_dite_eq`, states that for any types `α` and `β` (with `β` being an additive commutative monoid), given a decidable equality on `α`, a finite set `s` of type `α`, an element `a` of type `α`, and a function `b` from `α` (and a proof that `a` equals that element of `α`) to `β`, the sum over `s` of the function that equals `b x` if `a` equals `x` and `0` otherwise, equals `b a` if `a` is in `s` and `0` otherwise. Essentially, it's stating that in a summation over a set, if we're adding up a function that is zero except at one particular point, the sum just equals the function's value at that point (if the point is in the set) or zero (if the point isn't in the set).
More concisely: For any additive commutative monoid type `β`, given a decidable equality on type `α`, a finite set `s` of type `α`, an element `a` of type `α`, and a function `b` from `α` to `β` with `b a` defined when `a` is in `s`, the sum of `b x` over `s` equals `b a` if `a` is in `s`, and zero otherwise.
|
Finset.sum_insert
theorem Finset.sum_insert :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [inst : AddCommMonoid β]
[inst_1 : DecidableEq α], a ∉ s → ((insert a s).sum fun x => f x) = f a + s.sum fun x => f x
The theorem `Finset.sum_insert` states that for any type `α` and `β`, a finite set `s` of type `α`, an element `a` of type `α`, and a function `f` mapping `α` to `β`, given an additive commutative monoid structure on `β` and a decidable equality on `α`, if `a` is not an element of `s`, then the sum of the function `f` over the elements of the set obtained by inserting `a` into `s` is equal to `f(a)` plus the sum of `f` over the elements of `s`. In other words, inserting an element into a finite set and then summing a function over the elements of the set is the same as summing the function over the original set and then adding the function applied to the inserted element.
More concisely: For any additive commutative monoid `β` with decidable equality, and given a finite set `s` of type `α`, an element `a` not in `s`, and a function `f` from `α` to `β`, we have `Sum(f, s ++ {a}) = Sum(f, s) + f a`.
|
Finset.sum_range_zero
theorem Finset.sum_range_zero :
∀ {β : Type u_4} [inst : AddCommMonoid β] (f : ℕ → β), ((Finset.range 0).sum fun k => f k) = 0
The theorem `Finset.sum_range_zero` states that for all type `β` which has an `AddCommMonoid` instance, and for any function `f` from natural numbers to the type `β`, the sum of the function `f` over the range 0 (i.e., the set of natural numbers less than 0) equals to 0. Since there are no natural numbers less than 0, the sum is over an empty set and is therefore 0, as per the default property of addition in an `AddCommMonoid`.
More concisely: For any type `β` with an `AddCommMonoid` instance and any function `f : ℕ -> β`, the sum of `f` over the empty natural number set is 0.
|
Finset.prod_cons
theorem Finset.prod_cons :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [inst : CommMonoid β] (h : a ∉ s),
((Finset.cons a s h).prod fun x => f x) = f a * s.prod fun x => f x
The theorem `Finset.prod_cons` states that for any types `α` and `β`, any finite set `s` of elements of type `α`, any element `a` of type `α`, and any function `f` from `α` to `β`, where `β` is a commutative monoid, if `a` is not an element of `s`, then the product of `f x` for every `x` in the set `{a} ∪ s` (constructed by cons function) is equal to `f a` multiplied by the product of `f x` for every `x` in `s`. In mathematical terms, this theorem states that $\prod_{x \in \{a\} \cup s} f(x) = f(a) \cdot \prod_{x \in s} f(x)$.
More concisely: For any commutative monoid β, finite set s of α, function f from α to β, and a not in s, we have f a * ∏x∈s (fx) = ∏x∈{a} ∪ s (fx).
|
Finset.prod_subset
theorem Finset.prod_subset :
∀ {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f : α → β} [inst : CommMonoid β],
s₁ ⊆ s₂ → (∀ x ∈ s₂, x ∉ s₁ → f x = 1) → (s₁.prod fun x => f x) = s₂.prod fun x => f x
The `Finset.prod_subset` theorem states that for any two finite sets `s₁` and `s₂` of type `α`, and a function `f` mapping `α` to `β`, in the context of a commutative monoid structure on `β`, if `s₁` is a subset of `s₂` and for every element `x` in `s₂` that is not in `s₁`, the function `f` maps `x` to the identity element `1`, then the product of `f(x)` as `x` ranges over `s₁` is equal to the product of `f(x)` as `x` ranges over `s₂`. In mathematical notation, given $s_1 \subseteq s_2$ and $\forall x \in s_2, x \notin s_1 \Rightarrow f(x) = 1$, we have $\prod_{x \in s_1} f(x) = \prod_{x \in s_2} f(x)$.
More concisely: If `s₁` is a subset of `s₂`, and for every `x` in `s₂` not in `s₁`, `f(x)` equals the identity element `1`, then the product of `f(x)` over `s₁` equals the product of `f(x)` over `s₂`.
|
Finset.sum_union
theorem Finset.sum_union :
∀ {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f : α → β} [inst : AddCommMonoid β] [inst_1 : DecidableEq α],
Disjoint s₁ s₂ → ((s₁ ∪ s₂).sum fun x => f x) = (s₁.sum fun x => f x) + s₂.sum fun x => f x
The theorem `Finset.sum_union` states that for any types `α` and `β`, given two finite sets `s₁` and `s₂` of type `α` and a function `f` from `α` to `β`, if `β` is an additive commutative monoid and there is a decidable equality on `α`, and if `s₁` and `s₂` are disjoint (i.e., their intersection is the empty set), then the sum of the function `f` applied to each element of the union of `s₁` and `s₂` is equal to the sum of the function `f` applied to each element of `s₁` plus the sum of the function `f` applied to each element of `s₂`. In mathematical terms, if $s_1$ and $s_2$ are disjoint sets and $f$ is a function, then $\sum_{x \in s_1 \cup s_2} f(x) = \sum_{x \in s_1} f(x) + \sum_{x \in s_2} f(x)$.
More concisely: If `α` is a type with decidable equality, `β` is an additive commutative monoid, `f : α → β`, and `s₁` and `s₂` are disjoint finite sets of type `α`, then `∑ x in s₁ ∪ s₂, f x = ∑ x in s₁, f x + ∑ x in s₂, f x`.
|
Finset.prod_mul_prod_compl
theorem Finset.prod_mul_prod_compl :
∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] [inst_1 : Fintype α] [inst_2 : DecidableEq α] (s : Finset α)
(f : α → β), ((s.prod fun i => f i) * sᶜ.prod fun i => f i) = Finset.univ.prod fun i => f i
This theorem states that for any types `α` and `β`, where `β` is a commutative monoid, `α` has finite elements, and a decidable equality exists for all `α`, given a finite set `s` of type `α` and a function `f` from `α` to `β`, the product of the function `f` over the elements of `s` times the product of function `f` over the elements of the complement of `s` equals the product of function `f` over all elements of `α`. In other words, it asserts that the total product of a function over a set and its complement gives the product over the whole universe. For a version of this theorem that uses subtypes, refer to `Fintype.prod_subtype_mul_prod_subtype`.
More concisely: For any commutative monoid β, any type α with finite elements and decidable equality, and any function f from α to β, the product of f over a finite subset s of α and the product of f over the complement of s equal the product of f over all elements of α.
|
Finset.prod_empty
theorem Finset.prod_empty :
∀ {α : Type u_3} {β : Type u_4} {f : α → β} [inst : CommMonoid β], (∅.prod fun x => f x) = 1
This theorem states that for any types `α` and `β`, and any function `f` from `α` to `β` under the condition that `β` forms a commutative monoid, the product of `f x` as `x` ranges over the elements of an empty set is equal to the identity element of the monoid, which is 1. This is akin to saying that the product of an empty list of numbers is 1, in the sense of multiplication of numbers.
More concisely: For any commutative monoid type `β` and function `f` from type `α` to `β`, the empty product of `f x` over an empty set equals the identity element of `β`.
|
Finset.prod_powerset
theorem Finset.prod_powerset :
∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] (s : Finset α) (f : Finset α → β),
(s.powerset.prod fun t => f t) =
(Finset.range (s.card + 1)).prod fun j => (Finset.powersetCard j s).prod fun t => f t
The theorem `Finset.prod_powerset` states that for any given set `s` and a function `f` from subsets of `s` to a commutative monoid `β`, the product of `f` over the power set of `s` is equal to the double product over the set of subsets of `s` with cardinalities ranging from `1` to the cardinality of `s`. Here, the double product means we first take the product over subsets of a particular cardinality, and then take the product over all such cardinalities.
More concisely: For any set `s` and commutative monoid `β`, the product of a function from subsets of `s` to `β` over the power set of `s` equals the double product over subsets of `s` with cardinalities ranging from 1 to the cardinality of `s`.
|
Finset.sum_multiset_map_count
theorem Finset.sum_multiset_map_count :
∀ {α : Type u_3} [inst : DecidableEq α] (s : Multiset α) {M : Type u_6} [inst_1 : AddCommMonoid M] (f : α → M),
(Multiset.map f s).sum = s.toFinset.sum fun m => Multiset.count m s • f m
The theorem `Finset.sum_multiset_map_count` states that for any multiset `s` of type `α` with a decidable equality structure, and any function `f` from `α` to a type `M` equipped with a commutative additive monoid structure, the sum of the multiset obtained by mapping `f` over `s` is equal to the sum, over the finset obtained by removing duplicates from `s`, of the product of the count of each element `m` in `s` and the value of `f` at `m`. In other words, it provides a relationship between the sum of the transformed multiset and the weighted sum of the finset, where weights are the multiplicities of the elements in the original multiset.
More concisely: For any decidable multiset `s` of type `α` and commutative additive monoid-valued function `f` on `α`, the sum of `f` applied to the elements of `s` equals the sum of the counts of each element in `s` multiplied by the corresponding image under `f`.
|
Equiv.prod_comp
theorem Equiv.prod_comp :
∀ {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : CommMonoid α]
(e : ι ≃ κ) (g : κ → α), (Finset.univ.prod fun i => g (e i)) = Finset.univ.prod fun i => g i
The theorem `Equiv.prod_comp` states that for any two types `ι` and `κ`, both of finite size, equipped with a total bijective function (equivalence) `e : ι ≃ κ`, and a function `g : κ → α` where `α` is a type with commutative monoid structure, the product of `g (e i)` over all elements `i` in the universal set of `ι` is equal to the product of `g i` over all elements `i` in the universal set of `κ`. In other words, applying an equivalence to the elements before taking the product does not change the overall product.
More concisely: For any finite types `ι ≃ κ` with a bijective function `e : ι → κ` and a commutative monoid `α`, the product of `g (e i)` over all `i` in `ι` equals the product of `g i` over all `i` in `κ`.
|
Finset.sum_eq_single_of_mem
theorem Finset.sum_eq_single_of_mem :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] {s : Finset α} {f : α → β},
∀ a ∈ s, (∀ b ∈ s, b ≠ a → f b = 0) → (s.sum fun x => f x) = f a
This theorem, `Finset.sum_eq_single_of_mem`, states that for any given type `α` and `β`, if `β` is an additive commutative monoid, and 's' is a finite set of type `α`, and `f` is a function from `α` to `β`, then for any element `a` in set 's', if for all other elements `b` in 's' that are not equal to `a`, the function `f` maps `b` to the zero element of `β`, then the summation of the function values of the elements in set 's' is equal to the function value of `a`. In other words, if all the other elements of the set are mapped to zero by `f`, the sum over the entire set is just the value of `f` at the single non-zero element `a`.
More concisely: If `f : α → β` is a function from a finite set `s : Finset α` to an additive commutative monoid `β`, such that for all `b ∈ s \{a}`, `f b = 0`, then `∑ x in s, f x = f a`.
|
Finset.prod_eq_single
theorem Finset.prod_eq_single :
∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] {s : Finset α} {f : α → β} (a : α),
(∀ b ∈ s, b ≠ a → f b = 1) → (a ∉ s → f a = 1) → (s.prod fun x => f x) = f a
This theorem, `Finset.prod_eq_single`, states that for any types `α` and `β`, given a commutative monoid instance on `β`, a finite set `s` of `α`, a function `f` from `α` to `β`, and an element `a` of `α`, if it holds that the function `f` maps any element `b` in the set `s` not equal to `a` to the identity element `1`, and if `a` is not in the set `s`, then `f a` is also `1`, then the product of the function `f` over all elements `x` in `s`, denoted `(Finset.prod s fun x => f x)`, is equal to `f a`. In other words, the product of `f x` across all `x` in `s` collapses to `f a` under these conditions.
More concisely: Given a commutative monoid `β`, a finite set `s` of `α`, a function `f` from `α` to `β` such that `f x = 1` for all `x in s` except possibly `x = a not in s`, then `(∏ x ∈ s. f x) = f a`.
|
Finset.prod_univ_pi
theorem Finset.prod_univ_pi :
∀ {ι : Type u_1} {β : Type u_4} [inst : CommMonoid β] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι]
{κ : ι → Type u_6} (t : (i : ι) → Finset (κ i)) (f : ((i : ι) → i ∈ Finset.univ → κ i) → β),
((Finset.univ.pi t).prod fun x => f x) = (Fintype.piFinset t).prod fun x => f fun a x_1 => x a
This theorem, `Finset.prod_univ_pi`, states that for any types `ι`, `β`, and an indexed type `κ`, given a function `t` from `ι` to a `Finset` of `κ` and a function `f` from a function from `ι` to `κ` to `β`, the product over the function `f` applied to each element of the finset `univ.pi t` is equal to the product over the function `f` applied to each element of the `Fintype.piFinset t`. Here, `univ.pi t` is a finset of functions from `ι` to elements in `κ`, where each function maps an element `i` to an element in `t i`. Similarly, `Fintype.piFinset t` is a finset of functions from `ι` to `κ`. The theorem highlights that although `univ.pi t` and `Fintype.piFinset t` may have different types of elements, taking the product over these finsets using the function `f` yields the same result.
More concisely: For any types `ι`, `β`, and an indexed type `κ`, the product of `f` applied to the functions in `univ.pi t` is equal to the product of `f` applied to the functions in `Fintype.piFinset t`, where `t` is a function from `ι` to a `Finset` of `κ`.
|
Finset.prod_pair
theorem Finset.prod_pair :
∀ {α : Type u_3} {β : Type u_4} {f : α → β} [inst : CommMonoid β] [inst_1 : DecidableEq α] {a b : α},
a ≠ b → ({a, b}.prod fun x => f x) = f a * f b
The theorem `Finset.prod_pair` states that for any types `α` and `β`, a function `f` from `α` to `β`, a commutative monoid instance for `β`, a decidable equality instance for `α`, and any two distinct elements `a` and `b` of type `α`, the product of `f` applied to all elements in the finite set containing just `a` and `b` is equal to the product of `f a` and `f b`. In other words, if `a` and `b` are different, then applying `f` to each element of the set `{a, b}` and taking the product is the same as simply multiplying `f a` by `f b`.
More concisely: For any commutative monoid `β`, decidably equal types `α` with distinct elements `a, b`, and a function `f` from `α` to `β`, the product of `f` applied to the finite set `{a, b}` is equal to the product of `f a` and `f b`.
|
Finset.prod_bij
theorem Finset.prod_bij :
∀ {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [inst : CommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α}
{g : κ → α} (i : (a : ι) → a ∈ s → κ),
(∀ (a : ι) (ha : a ∈ s), i a ha ∈ t) →
(∀ (a₁ : ι) (ha₁ : a₁ ∈ s) (a₂ : ι) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) →
(∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b) →
(∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)) → (s.prod fun x => f x) = t.prod fun x => g x
This theorem, `Finset.prod_bij`, is about reordering a product over a finite set (a `Finset`). Given two finite sets `s` of type `ι` and `t` of type `κ`, and two functions `f : ι → α` and `g : κ → α` that map elements of these sets to a commutative monoid `α`, it establishes conditions under which the product of `f` over `s` equals the product of `g` over `t`. Key to this are a surjective injection `i : (a : ι) → a ∈ s → κ`, proving that every element of `t` has a pre-image in `s`, and an equality condition ensuring that `f` and `g` map corresponding elements to the same value. Compared to similar theorems `Finset.prod_bij'` and `Finset.prod_nbij`, `Finset.prod_bij` allows `i` to be dependent on membership in `s` and does not require specifying an inverse function.
More concisely: Given two finite sets `s` and `t`, two functions `f : ι -> α` and `g : κ -> α` from their elements to a commutative monoid `α`, and a surjective injection `i : ι -> s -> κ`, if for all `a in s` and `b in t`, `f a = g (i a)`, then `∏(x in s) f x = ∏(y in t) g y`.
|
Finset.add_sum_erase
theorem Finset.add_sum_erase :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] [inst_1 : DecidableEq α] (s : Finset α) (f : α → β)
{a : α}, a ∈ s → (f a + (s.erase a).sum fun x => f x) = s.sum fun x => f x
The theorem `Finset.add_sum_erase` states that for any given finite set `s` of a type `α` and a function `f` from `α` to a type `β` (where `β` has an additive commutative monoid structure), and any element `a` of the set `s` (which equality can be decided), the sum of the function `f` over the set `s` is the same as the sum of the function `f` over the set `s` with `a` removed, plus the value of the function `f` at `a`. In mathematical terms, if $\sum_{x \in s} f(x)$ is the sum of `f(x)` for all `x` in `s`, then $\sum_{x \in s} f(x) = f(a) + \sum_{x \in s \setminus \{a\}} f(x)$, where `a` is in `s`.
More concisely: For a finite set `s` of type `α` and a function `f` from `α` to an additive commutative monoid `β`, the sum of `f` over `s` equals the sum of `f` over `s` without the element `a` in `s`, plus `f(a)`. In mathematical notation, $\sum\_{x \in s} f(x) = f(a) + \sum\_{x \in s \setminus \{a\}} f(x)$.
|
Finset.prod_mulIndicator_subset_of_eq_one
theorem Finset.prod_mulIndicator_subset_of_eq_one :
∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] [inst_1 : One α] (f : ι → α) (g : ι → α → β)
{s t : Finset ι},
s ⊆ t → (∀ (a : ι), g a 1 = 1) → (t.prod fun i => g i ((↑s).mulIndicator f i)) = s.prod fun i => g i (f i)
This theorem states that if you have a function `g` such as `n ↦ (· ^ n)`, which maps a second argument of `1` to `1`, and a function `f` from a type `ι` to a type `α`, then for any two finite sets `s` and `t` of type `ι` such that `s` is a subset of `t`, the product of `g i (f i)` over the finite set `s` is equal to the product of `g i ((↑s).mulIndicator f i)` over the finite set `t`. This means that you can replace `f` with the corresponding multiplicative indicator function and `s` with a possibly larger set `t` without changing the value of the product.
More concisely: For any function `f : ι → α` and finite sets `s` and `t` of type `ι` with `s` a subset of `t`, the product of `(∏ i ∈ s, g i (f i))` equals the product of `(∏ i ∈ t, g i (↑s .mulIndicator f i))`, where `g : ℕ → α → α`, `↑s` is the upper set of `s`, and `mulIndicator` is the multiplicative indicator function.
|
Finset.sum_bij'
theorem Finset.sum_bij' :
∀ {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [inst : AddCommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α}
{g : κ → α} (i : (a : ι) → a ∈ s → κ) (j : (a : κ) → a ∈ t → ι) (hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t)
(hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s),
(∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a) →
(∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a) →
(∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)) → (s.sum fun x => f x) = t.sum fun x => g x
This theorem, named `Finset.sum_bij'`, states that for two finite sets `s` and `t` with elements of type `ι` and `κ` respectively, and two functions `f : ι → α` and `g : κ → α` where `α` is a type with an additive commutative monoid structure, if there exist functions `i : ι → κ` and `j : κ → ι` that form a bijection between elements of `s` and `t` (taking into account their membership in `s` and `t`), and if for each element `a` in `s`, `f a` equals `g` of the image of `a` under `i`, then the sum of `f` over all elements of `s` equals the sum of `g` over all elements of `t`.
In simpler terms, you can rearrange the elements of a finite sum without changing the total, as long as you have a function that correctly maps elements from one set to another and vice versa, preserving the behavior of the original functions under the sum.
More concisely: Given finite sets `s` and `t` with types `ι` and `κ`, functions `f : ι → α` and `g : κ → α` on an additive commutative monoid `α`, and bijections `i : ι ↔ κ` and `j : κ ↔ ι` between their elements, if `f a = g (i a)` for all `a ∈ s`, then `∑ i in s, f i = ∑ j in t, g j`.
|
Finset.sum_filter_of_ne
theorem Finset.sum_filter_of_ne :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [inst : AddCommMonoid β] {p : α → Prop}
[inst_1 : DecidablePred p],
(∀ x ∈ s, f x ≠ 0 → p x) → ((Finset.filter p s).sum fun x => f x) = s.sum fun x => f x
The theorem `Finset.sum_filter_of_ne` states that for any type `α`, any type `β` with an additive commutative monoid structure, any finite set `s` of `α`, any function `f` from `α` to `β`, and any decidable predicate `p` on `α`, if every element `x` of `s` for which `f(x)` is not zero satisfies the predicate `p`, then the sum over the filtered set, where the filter is given by `p`, is equal to the sum over the entire set `s`. In mathematical terms, if for all `x` in `s`, `f(x) ≠ 0` implies `p(x)` then the equation ∑_{x in {p(x) | x in s}} f(x) = ∑_{x in s} f(x) holds.
More concisely: If `p` is a decidable predicate on a finite set `s` of `α` such that `f(x) neq 0` implies `p(x)` for all `x` in `s`, then the sum of `f(x)` over the filtered set `{x in s | p(x)}` equals the sum over the entire set `s`.
|
Finset.sum_comm'
theorem Finset.sum_comm' :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : AddCommMonoid β] {s : Finset γ} {t : γ → Finset α}
{t' : Finset α} {s' : α → Finset γ},
(∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t') →
∀ {f : γ → α → β}, (s.sum fun x => (t x).sum fun y => f x y) = t'.sum fun y => (s' y).sum fun x => f x y
This theorem, `Finset.sum_comm'`, generalizes the `Finset.sum_comm` to the case where the inner `Finset`s depend on the outer variable. Given two types `α` and `γ`, and a function `f` from `γ` to `α` to `β` (where `β` is an AddCommMonoid), the condition for the equality of two different sums is defined. The first sum is over `s` (a `Finset` of `γ`), and for each element `x` in `s`, it sums over `t x` (a `Finset` of `α`), applying the function `f` to `x` and `y`. The second sum is similarly defined but with roles of `α` and `γ` reversed. The exact condition is that for all `x` in `γ` and `y` in `α`, `x` belongs to `s` and `y` belongs to `t x` if and only if `x` belongs to `s' y` and `y` belongs to `t'`.
More concisely: Given functions `f : γ -> α -> β` from `γ` to an additive commutative monoid `β`, and `s : Finset γ` and `t, t' : (α -> Finset β)`, if for all `x in γ` and `y in α`, `x in s` and `y in t x` if and only if `x in s' y` and `y in t' x`, then `∑x in s. ∑y in t x. f x y = ∑x in s'. ∑y in t' x. f x y`.
|
Finset.prod_insert_of_eq_one_if_not_mem
theorem Finset.prod_insert_of_eq_one_if_not_mem :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [inst : CommMonoid β] [inst_1 : DecidableEq α],
(a ∉ s → f a = 1) → ((insert a s).prod fun x => f x) = s.prod fun x => f x
The theorem `Finset.prod_insert_of_eq_one_if_not_mem` states that for any given types `α` and `β`, a finite set `s` of type `α`, an element `a` of type `α`, and a function `f` from `α` to `β`, under the conditions that `β` forms a commutative monoid and `α` has decidable equality, if `a` is not a member of `s` then `f(a)` must be 1. With these conditions, the product of `f` over the set obtained by inserting `a` into `s` is the same as the product of `f` over `s`. In simpler terms, inserting an element that maps to the identity (1, in this case) into the set doesn't change the overall product.
More concisely: If `α` has decidable equality and `β` is a commutative monoid, then for any finite set `s` of type `α`, element `a` not in `s`, and function `f` from `α` to `β`, `f(a) = 1` implies `∏ (x : α) in s. f x = ∏ (x : α) in s. f x * f a`.
|
Finset.sum_neg_distrib
theorem Finset.sum_neg_distrib :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [inst : SubtractionCommMonoid β],
(s.sum fun x => -f x) = -s.sum fun x => f x
The theorem `Finset.sum_neg_distrib` states that for any finite set `s` of type `α`, and for any function `f` from `α` to `β` where `β` is a subtraction commutative monoid, the sum over `s` of the negation of `f(x)` (i.e., `∑ x in s, -f x`) is equal to the negation of the sum over `s` of `f(x)` (i.e., `- ∑ x in s, f x`). This is a distributive property of the sum operation over the negative operation.
More concisely: For any finite set `s` and function `f` from a subtraction commutative monoid to itself, the sum of the negations of `f(x)` over `s` is equal to the negation of the sum of `f(x)` over `s`.
|
Finset.prod_mul_distrib
theorem Finset.prod_mul_distrib :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {f g : α → β} [inst : CommMonoid β],
(s.prod fun x => f x * g x) = (s.prod fun x => f x) * s.prod fun x => g x
The theorem `Finset.prod_mul_distrib` in Lean 4 states that for any given type `α`, another type `β` under a commutative monoid structure, a finite set `s` of `α`, and two functions `f` and `g` from `α` to `β`, the product of the values obtained by multiplying the outputs of `f` and `g` for each element in the set `s` is equal to the product of the outputs of `f` for each element in the set `s`, multiplied by the product of the outputs of `g` for each element in the set `s`. In mathematical terms, this theorem represents the distributive property of multiplication over addition in a commutative monoid: $\prod_{x\in s}(f(x)g(x)) = \left(\prod_{x\in s}f(x)\right)\left(\prod_{x\in s}g(x)\right)$.
More concisely: For any commutative monoid `β` and functions `f` and `g` from a finite set `s` of a type `α` to `β`, the product of the element-wise products of `f` and `g` equals the product of the `f`-values and the product of the `g`-values over all elements in `s`.
|
Finset.sum_subtype
theorem Finset.sum_subtype :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] {p : α → Prop} {F : Fintype (Subtype p)} (s : Finset α),
(∀ (x : α), x ∈ s ↔ p x) → ∀ (f : α → β), (s.sum fun a => f a) = Finset.univ.sum fun a => f ↑a
This theorem, `Finset.sum_subtype`, states that for any types `α` and `β`, and given an additive commutative monoid over `β`, a predicate `p` on `α`, and a finite type of the subtype of `α` satisfying `p`, then for any finite set `s` of `α` such that an element `x` of `α` is in `s` if and only if `p x` is true, and any function `f` from `α` to `β`, the sum of `f x` over all elements `x` in `s` is equal to the sum of `f x` over all elements `x` in the universal set of the subtype. In other words, summing `f x` over a set `s` where `s` precisely contains the elements of `α` satisfying a property `p` is the same as summing `f x` over all elements of the subtype of `α` defined by `p`.
More concisely: For any additive commutative monoid over `β`, given a finite subtype of type `α` defined by a predicate `p`, and a function `f` from `α` to `β`, the sum of `f x` over all elements `x` in the subtype equals the sum of `f x` over all elements in the universal set of the subtype.
|
Finset.sum_disjiUnion
theorem Finset.sum_disjiUnion :
∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} {f : α → β} [inst : AddCommMonoid β] (s : Finset ι)
(t : ι → Finset α) (h : (↑s).PairwiseDisjoint t),
((s.disjiUnion t h).sum fun x => f x) = s.sum fun i => (t i).sum fun x => f x
This theorem, `Finset.sum_disjiUnion`, states that for any types `ι`, `α`, and `β`, along with a function `f` from `α` to `β` and given an additive commutative monoid structure on `β`, the sum of the function `f` over the disjoint union of a collection of finite sets `t` indexed by elements of another finite set `s` (with the guarantee that these sets `t i` are pairwise disjoint) equals the sum, over each element `i` of `s`, of the sum of `f` over the elements `x` of `t i`. In mathematical notation, this could be written as $\sum_{x \in \bigsqcup_{i \in s} t_i} f(x) = \sum_{i \in s} \sum_{x \in t_i} f(x)$, where $\bigsqcup$ denotes a disjoint union.
More concisely: The sum of a function over the disjoint union of a collection of finite sets is equal to the sum of the function over each set in the collection.
|
Finset.card_biUnion_le
theorem Finset.card_biUnion_le :
∀ {α : Type u_3} {β : Type u_4} [inst : DecidableEq β] {s : Finset α} {t : α → Finset β},
(s.biUnion t).card ≤ s.sum fun a => (t a).card
This theorem is stating that for any two types, `α` and `β`, where `β` has a decidable equality, and for any finite set `s` of type `α` and a function `t` that maps elements of `α` to finite sets of `β`, the cardinality (or size) of the biUnion of `s` and `t` is less than or equal to the sum of the cardinalities of the sets `t a` for each `a` in `s`. In other words, the size of the union of the sets `t a` for each `a` in `s` is less than or equal to the sum of the sizes of these sets. This is an application of the general principle that the size of a union of sets is less than or equal to the sum of the sizes of the sets.
More concisely: For any finite set `s` of type `α` and function `t` from `α` to finite sets of type `β` with decidable equality, the cardinality of the biUnion of `s` and the image of `t` is less than or equal to the sum of the cardinalities of the images of `t` on each element of `s`.
|
Finset.sum_add_distrib
theorem Finset.sum_add_distrib :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {f g : α → β} [inst : AddCommMonoid β],
(s.sum fun x => f x + g x) = (s.sum fun x => f x) + s.sum fun x => g x
The theorem `Finset.sum_add_distrib` states that for any finite set `s` of any type `α`, and any two functions `f` and `g` from `α` to another type `β` where `β` is an additive commutative monoid, the sum over `s` of `f(x) + g(x)` equals the sum of `f(x)` over `s` plus the sum of `g(x)` over `s`. This is the distributive property of summation over a finite set in the context of additive commutative monoids. In terms of mathematical notation, this can be represented as $\sum_{x \in s} (f(x) + g(x)) = \sum_{x \in s} f(x) + \sum_{x \in s} g(x)$.
More concisely: For any finite set `s` and additive commutative monoid-valued functions `f` and `g` on a type `α`, the sum of `f(x) + g(x)` over `s` equals the sum of `f(x)` over `s` plus the sum of `g(x)` over `s`. (Mathematically: $\sum\_{x \in s} (f(x) + g(x)) = \sum\_{x \in s} f(x) + \sum\_{x \in s} g(x)$)
|
Finset.sum_nsmul
theorem Finset.sum_nsmul :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] (s : Finset α) (n : ℕ) (f : α → β),
(s.sum fun x => n • f x) = n • s.sum fun x => f x
This theorem, named `Finset.sum_nsmul`, states that for any finite set `s` of elements of an arbitrary type `α`, any natural number `n`, and any function `f` from `α` to a type `β` that forms an additive commutative monoid, the sum over `s` where each element is multiplied by `n` after being mapped by `f` (`Finset.sum s fun x => n • f x`) is equal to `n` times the sum over `s` of the elements mapped by `f` (`n • Finset.sum s fun x => f x`). This theorem essentially expresses a property of distributivity of scalar multiplication over a finite sum in the context of additive commutative monoids.
More concisely: For any finite set `s`, natural number `n`, and additive commutative monoid homomorphism `f` from a type `α` to a type `β`, we have `Finset.sum s fun x => n • f x = n * Finset.sum s fun x => f x`.
|
Finset.prod_ite_eq'
theorem Finset.prod_ite_eq' :
∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] [inst_1 : DecidableEq α] (s : Finset α) (a : α) (b : α → β),
(s.prod fun x => if x = a then b x else 1) = if a ∈ s then b a else 1
This theorem states that for any given types `α` and `β`, where `β` has a Commutative Monoid structure and `α` has a Decidable Equality structure, and for any finite set `s` of type `α`, any element `a` of type `α`, and a function `b` from `α` to `β`, the product of the function values (where the function is defined such that if an element `x` of the set `s` is equal to `a`, the value is `b(x)`, otherwise it's `1`) over the set `s` is equal to `b(a)` if `a` belongs to `set s` and `1` otherwise. In simpler terms, it says that the product over the set `s` will be `b(a)` if `a` is present in `s` and `1` if it's not. The only difference from `Finset.prod_ite_eq` is the swapping of the arguments to `Eq`.
More concisely: For any commutative monoid β, decidable equality α, finite set s of α, and function f : α → β such that f(x) = b if x ∈ s and x = a, and x = a if and only if x ∈ s, we have ∏(x ∈ s, f(x)) = if h : a ∈ s then b else 1.
|
Fintype.sum_unique
theorem Fintype.sum_unique :
∀ {α : Type u_9} {β : Type u_10} [inst : AddCommMonoid β] [inst_1 : Unique α] [inst_2 : Fintype α] (f : α → β),
(Finset.univ.sum fun x => f x) = f default
The theorem `Fintype.sum_unique` states that for all types `α` and `β`, given that `β` is an additive commutative monoid, `α` is a unique type and a finite type, and a function `f` from `α` to `β`, the sum of `f x` as `x` ranges over all elements of the universal (i.e., total) finite set of `α` is equal to the value of function `f` at the default element of `α`. In other words, if there is only one element in type `α` (due to the `Unique` instance), summing over all elements of `α` is the same as applying `f` to the lone element.
More concisely: If `α` is a finite, unique type and `β` is an additive commutative monoid, then the sum of `f(x)` over all `x` in `α` equals `f(default α)`.
|
Finset.sum_range_tsub
theorem Finset.sum_range_tsub :
∀ {α : Type u_3} [inst : CanonicallyOrderedAddCommMonoid α] [inst_1 : Sub α] [inst_2 : OrderedSub α]
[inst_3 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {f : ℕ → α},
Monotone f → ∀ (n : ℕ), ((Finset.range n).sum fun i => f (i + 1) - f i) = f n - f 0
This theorem states that for any function `f` from natural numbers `ℕ` to some type `α` that is equipped with a canonically ordered addition-commutative monoid, subtraction operation, and an ordered subtraction, if the function `f` is monotone, then the sum of the differences `f (i + 1) - f i` over the range `{0, ..., n-1}` is equal to `f n - f 0`. In simpler terms, this theorem is about the "telescoping" property of sums in a sequence generated by a monotone function: many terms in the sequence cancel out when we sum up the differences, leaving us with just the difference between the final and initial terms. This theorem is a formalization of the concept of "telescoping series" from mathematics.
More concisely: If `f : ℕ → α` is a monotone function on the naturally ordered additive commutative monoid, then Σ(i in 0..
|
Finset.dvd_prod_of_mem
theorem Finset.dvd_prod_of_mem :
∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] (f : α → β) {a : α} {s : Finset α},
a ∈ s → f a ∣ s.prod fun i => f i
This theorem states that for any types `α` and `β`, where `β` is a commutative monoid, any function `f` from `α` to `β`, and any element `a` of type `α` and finite set `s` of elements of type `α`, if `a` is an element of `s`, then the value of `f` at `a` divides the product of `f` evaluated at every element in `s`. In mathematical terms, for $f : \alpha \to \beta$, $a \in \alpha$, $s \subseteq \alpha$ such that $a \in s$, we have $f(a) | \prod_{i \in s} f(i)$.
More concisely: For any commutative monoid type `β`, function `f` from type `α` to `β`, element `a` of type `α` in a finite set `s` of type `α` that includes `a`, we have `f(a) | ∏(i ∈ s) f(i)`.
|
Finset.sum_attach
theorem Finset.sum_attach :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] (s : Finset α) (f : α → β),
(s.attach.sum fun x => f ↑x) = s.sum fun x => f x
The `Finset.sum_attach` theorem asserts that for any finite set `s` of type `α` and any function `f` from `α` to `β` (where `β` is an additive commutative monoid), the sum of `f x` over all elements `x` in the attached form of `s` (i.e., `Finset.attach s`, which is a set of elements of the subtype `{x // x ∈ s}`) is equal to the sum of `f x` over all elements `x` in `s` itself. This theorem essentially states that attaching a finite set does not change the sum of the function applied to the elements of the set.
More concisely: For any finite set `s` of type `α` and any additive commutative monoid `β`, the sum of a function `f` from `α` to `β` over the attached form of `s` is equal to the sum over `s` itself.
|
Finset.eq_of_card_le_one_of_sum_eq
theorem Finset.eq_of_card_le_one_of_sum_eq :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] {s : Finset α},
s.card ≤ 1 → ∀ {f : α → β} {b : β}, (s.sum fun x => f x) = b → ∀ x ∈ s, f x = b
This theorem states that, for any types α and β, given a commutative monoid on β, a finite set 's' of type α with a maximum cardinality of one, a function 'f' from α to β, and a value 'b' of type β, if the sum of the function 'f' applied to all the elements of 's' equals 'b', then the function 'f' applied to each element in 's' will also equal 'b'. In other words, if the total sum of all elements in a set of size at most one equals a certain value, each element in that set must also equal that same value.
More concisely: If $f:\alpha \to \beta$ is a function, $b \in \beta$, $s \subseteq \alpha$ is finite with $|s| \leq 1$, and $\sum_{x \in s} f(x) = b$, then $f(x) = b$ for all $x \in s$.
|
Finset.sum_range_succ_comm
theorem Finset.sum_range_succ_comm :
∀ {β : Type u_4} [inst : AddCommMonoid β] (f : ℕ → β) (n : ℕ),
((Finset.range (n + 1)).sum fun x => f x) = f n + (Finset.range n).sum fun x => f x
The theorem `Finset.sum_range_succ_comm` states that for any given type `β` that forms an additive commutative monoid, and any function `f` from natural numbers to `β`, the sum of the function `f` applied to each element in the set of natural numbers less than `n+1` is equal to the value of the function `f` at `n` plus the sum of the function `f` applied to each element in the set of natural numbers less than `n`. In mathematical notation, this can be written as $\sum_{x=0}^{n} f(x) = f(n) + \sum_{x=0}^{n-1} f(x)$.
More concisely: The sum of a function's values over the set of natural numbers up to `n` is equal to the function value at `n` plus the sum of its values over the set of natural numbers up to `n-1`.
|
Finset.sum_image
theorem Finset.sum_image :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} {f : α → β} [inst : AddCommMonoid β] [inst_1 : DecidableEq α]
{s : Finset γ} {g : γ → α},
(∀ x ∈ s, ∀ y ∈ s, g x = g y → x = y) → ((Finset.image g s).sum fun x => f x) = s.sum fun x => f (g x)
The theorem `Finset.sum_image` states that for any types α, β, and γ, a function `f` from α to β, a finite set `s` of elements of type γ, a function `g` from γ to α, as long as `g` sends different elements in `s` to different elements, the sum of `f` over the image of `s` under `g` equals to the sum of `f` after applying `g` over the elements of `s`. In simpler terms, the sum of the function values at the images is the same as the sum of the function values at the originals, provided that the mapping function maintains distinctness among elements.
More concisely: For any functions `f: α -> β`, `g: γ -> α` with `g(s)` injective for a finite set `s` in γ, the sum of `f` over `g(s)` equals the sum of `f` applied to `s`.
|
Finset.sum_empty
theorem Finset.sum_empty :
∀ {α : Type u_3} {β : Type u_4} {f : α → β} [inst : AddCommMonoid β], (∅.sum fun x => f x) = 0
The theorem `Finset.sum_empty` states that for any type `α`, any type `β` that forms an additive commutative monoid, and any function `f` from `α` to `β`, the sum of `f x` over the elements of an empty finite set is zero. In other words, if you try to compute the sum of elements from an empty set, where the elements are obtained by applying some function `f` to each element of the set, the result is zero. This is because there are no elements in the set to apply the function to and sum up.
More concisely: For any additive commutative monoid type `β` and function `f` from type `α` to `β`, the sum of `f x` over an empty finite set `α` is the zero element of `β`.
|
Finset.sum_range_one
theorem Finset.sum_range_one :
∀ {β : Type u_4} [inst : AddCommMonoid β] (f : ℕ → β), ((Finset.range 1).sum fun k => f k) = f 0
This theorem states that for any given type `β` with an additive commutative monoid structure, and any given function `f` that maps from natural numbers to `β`, the sum of the function values over the range less than 1 (i.e., the set of natural numbers less than 1) is equal to the function value at 0. In mathematical terms, it asserts that the sum of `f(k)` as `k` ranges over the natural numbers less than 1 equals `f(0)`.
More concisely: For any additive commutative monoid type `β` and function `f` from natural numbers to `β`, the sum of `f` over the natural numbers less than 1 equals `f` applied to 0.
|
Finset.sum_product
theorem Finset.sum_product :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : AddCommMonoid β] {s : Finset γ} {t : Finset α}
{f : γ × α → β}, ((s ×ˢ t).sum fun x => f x) = s.sum fun x => t.sum fun y => f (x, y)
The theorem `Finset.sum_product` states that for any types `α`, `β`, and `γ`, and given an addition-commutative monoid structure on `β`, any finite sets `s` of type `γ` and `t` of type `α`, and any function `f` from the Cartesian product of `γ` and `α` to `β`, the sum of `f` over the Cartesian product of `s` and `t` is equal to the sum of the sums of `f` over the elements of `t` for each element of `s`. In mathematical notation, this is ∑_{(x,y) ∈ s × t} f(x,y) = ∑_{x ∈ s} ∑_{y ∈ t} f(x,y). This theorem is expressing a property of summing over a product of sets.
More concisely: For any addition-commutative monoid β, given finite sets s of type γ and t of type α, and a function f from the Cartesian product s × t to β, the sum of f over the Cartesian product s × t is equal to the sum of the sums of f over the elements of t for each element of s. (i.e., ∑_{(x,y) ∈ s × t} f(x,y) = ∑_{x ∈ s} ∑_{y ∈ t} f(x,y)).
|
Finset.prod_comp
theorem Finset.prod_comp :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Finset α} [inst : CommMonoid β] [inst_1 : DecidableEq γ]
(f : γ → β) (g : α → γ),
(s.prod fun a => f (g a)) = (Finset.image g s).prod fun b => f b ^ (Finset.filter (fun a => g a = b) s).card
This theorem states that for any finite set `s` of elements of type `α`, a function `f` from `γ` to `β` (where `β` is a commutative monoid), and a function `g` from `α` to `γ`, the product of `f` applied to `g` over all elements of `s` is equal to the product over all elements `b` in the image of `s` under `g` of `f b` raised to the power of the cardinality of the preimage of `b` under `g`. In other words, it's a statement about rearranging the terms in a product, where the terms are given by a function composition and the grouping of terms is determined by another function.
More concisely: For any finite set `s` of elements from type `α`, function `f` from `γ` to `β` (β being a commutative monoid), and function `g` from `α` to `γ`, the following equality holds:
`∏ x ∈ s (f ∘ g x) = ∏ b ∈ range g (∏ x ∈ g⁻¹{b} f x)^(cardinality (g⁻¹{b}))`
|
Finset.prod_ite
theorem Finset.prod_ite :
∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] {s : Finset α} {p : α → Prop} {hp : DecidablePred p}
(f g : α → β),
(s.prod fun x => if p x then f x else g x) =
((Finset.filter p s).prod fun x => f x) * (Finset.filter (fun x => ¬p x) s).prod fun x => g x
The theorem `Finset.prod_ite` states that for any type `α` and a commutative monoid `β`, given a finite set `s` of type `α`, a decidable predicate `p`, and two functions `f, g` from `α` to `β`, the product of the set `s` where each element `x` is mapped to `f x` if `p x` is true and `g x` if `p x` is false, is equal to the product of the elements of the set that satisfy `p` mapped to `f x` times the product of the elements that do not satisfy `p` mapped to `g x`. In mathematical terms, we have $\prod_{x \in s} (if\ p(x)\ then\ f(x)\ else\ g(x)) = \prod_{x \in s,\ p(x)} f(x) * \prod_{x \in s,\ ¬p(x)} g(x)$.
More concisely: For any commutative monoid β and finite set s of type α with a decidable predicate p and functions f, g from α to β, the product of s mapped to f using p is equal to the product of elements of s satisfying p mapped to f multiplied by the product of elements of s not satisfying p mapped to g: $\prod\_{x \in s} (if\ p(x)\ then\ f(x)\ else\ g(x)) = \prod\_{x \in s,\ p(x)} f(x) * \prod\_{x \in s,\ ¬p(x)} g(x)$.
|
Finset.sum_partition
theorem Finset.sum_partition :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [inst : AddCommMonoid β] (R : Setoid α)
[inst_1 : DecidableRel Setoid.r],
(s.sum fun x => f x) =
(Finset.image Quotient.mk'' s).sum fun xbar => (Finset.filter (fun x => ⟦x⟧ = xbar) s).sum fun y => f y
This theorem, named `Finset.sum_partition`, states that for any given finite set `s` of elements of type `α`, a function `f` from `α` to `β`, an additive commutative monoid structure on `β`, and an equivalence relation `R` on `α`, the sum of the function `f` applied to each element of `s` is equal to the sum, over all equivalence classes `xbar` of `α` under `R`, of the sum of `f` applied to each element `y` in `s` that belongs to the equivalence class `xbar`. Here, the equivalence class of an element `x` of `α` is represented as ⟦x⟧ in Lean 4. The theorem requires the decidability of the equivalence relation `R`.
More concisely: For any finite set `s` of elements from a type `α`, an additive commutative monoid `β`, a function `f` from `α` to `β`, and a decidable equivalence relation `R` on `α`, the sum of `f` applied to each element of `s` equals the sum of `f` applied to representatives of each equivalence class of `s` under `R`.
|
Finset.prod_multiset_map_count
theorem Finset.prod_multiset_map_count :
∀ {α : Type u_3} [inst : DecidableEq α] (s : Multiset α) {M : Type u_6} [inst_1 : CommMonoid M] (f : α → M),
(Multiset.map f s).prod = s.toFinset.prod fun m => f m ^ Multiset.count m s
The theorem `Finset.prod_multiset_map_count` states that for any multiset `s` of elements from an arbitrary type `α` (which has a decidable equality) and a function `f` that maps from `α` to a type `M` (which is equipped with a commutative monoid structure), the product of the mapped multiset elements is equal to the product of the unique elements of the multiset (obtained by converting the multiset to a finset) each raised to the power of its multiplicity in the original multiset. In simpler terms, it justifies the ability to interchange the order of mapping a function over a multiset and taking the product, with taking the product over the unique elements of the multiset where each element is raised to the power of its count in the multiset.
More concisely: For any multiset `s` of decidably equal elements from type `α` and any commutative monoid `M` with a function `f` from `α` to `M`, the multiset product of `f` applied to the elements of `s` equals the product of `f` applied to each unique element in `s` raised to the power of its multiplicity in `s`.
|
Finset.sum_product_right'
theorem Finset.sum_product_right' :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : AddCommMonoid β] {s : Finset γ} {t : Finset α}
{f : γ → α → β}, ((s ×ˢ t).sum fun x => f x.1 x.2) = t.sum fun y => s.sum fun x => f x y
This theorem states that for any two finite sets (`s` and `t`) and a function `f` from the product of the sets into an additive commutative monoid `β`, the sum over the product of `s` and `t` of applying `f` to each pair is equal to the sum over `t` of the sum over `s` of applying `f` to each pair in the nested sum. In mathematical terms, it says that for a finite sets `s` and `t` and a function `f : γ → α → β`, we have the equality:
∑_{(x,y) in s×t} f(x, y) = ∑_{y in t} (∑_{x in s} f(x, y))
This theorem thus states a kind of 'exchange of summation'.
More concisely: For any finite sets `s` and `t` and a function `f : γ → α → β`, the sum of `f` applied to all pairs in the product of `s` and `t` is equal to the sum of the sums of `f` applied to each element in `s` for each element in `t`. In symbols, ∑_{(x,y) ∈ s × t} `f`(x, y) = ∑\_{y ∈ t} ∑\_{x ∈ s} `f`(x, y).
|
Finset.sum_indicator_eq_sum_filter
theorem Finset.sum_indicator_eq_sum_filter :
∀ {ι : Type u_1} {β : Type u_4} [inst : AddCommMonoid β] {κ : Type u_6} (s : Finset ι) (f : ι → κ → β)
(t : ι → Set κ) (g : ι → κ) [inst_1 : DecidablePred fun i => g i ∈ t i],
(s.sum fun i => (t i).indicator (f i) (g i)) = (Finset.filter (fun i => g i ∈ t i) s).sum fun i => f i (g i)
The theorem `Finset.sum_indicator_eq_sum_filter` states that for any types `ι`, `β`, and `κ`, any additive commutative monoid `β`, any finite set `s` of type `ι`, any functions `f : ι → κ → β`, `t : ι → Set κ`, and `g : ι → κ`, under the condition that the predicate "the image of `g` is in the image of `t`" is decidable, the sum over `s` of the indicator function of `t i` applied to `f i` and `g i` is equal to the sum over the subset of `s` satisfying the predicate "the image of `g` is in the image of `t`" of `f i` applied to `g i`.
In other words, this theorem compares two methods of summing a function over a finite set: one method uses an indicator function to assign zero to elements outside a set, and the other filters out those elements before the sum. It asserts that these two methods yield the same result.
More concisely: For any additive commutative monoid β, finite set s of type ι, functions f : ι → κ → β, t : ι → Set κ, and g : ι → κ, if the predicate "the image of g is in the image of t" is decidable, then the sum of indicator functions of t i applied to fi and gi over s equals the sum of fi applied to gi over the subset of s where the image of g is in the image of t.
|
Finset.sum_insert_of_eq_zero_if_not_mem
theorem Finset.sum_insert_of_eq_zero_if_not_mem :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [inst : AddCommMonoid β]
[inst_1 : DecidableEq α], (a ∉ s → f a = 0) → ((insert a s).sum fun x => f x) = s.sum fun x => f x
This theorem states that for any types `α` and `β`, for any finite set `s` of type `α`, for any element `a` of type `α`, and for any function `f` from `α` to `β`, given that `β` forms an additive commutative monoid and that equality in `α` is decidable, if `a` does not belong to `s` implies `f a` equals zero, then the sum of `f` over the set formed by inserting `a` into `s` is the same as the sum of `f` over `s`. In mathematical terms, if $a \notin s$ implies $f(a) = 0$, then $\sum_{x \in s \cup \{a\}} f(x) = \sum_{x \in s} f(x)$.
More concisely: If `α` is a type with decidable equality and `β` is an additive commutative monoid, for any finite set `s` of type `α`, function `f` from `α` to `β`, and element `a` not in `s`, if `f a = 0`, then the sum of `f` over `s` and `a` is equal.
|
Finset.prod_comm'
theorem Finset.prod_comm' :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : CommMonoid β] {s : Finset γ} {t : γ → Finset α}
{t' : Finset α} {s' : α → Finset γ},
(∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t') →
∀ {f : γ → α → β}, (s.prod fun x => (t x).prod fun y => f x y) = t'.prod fun y => (s' y).prod fun x => f x y
This theorem, `Finset.prod_comm'`, is a generalization of `Finset.prod_comm`. It states that for any types `α`, `β`, and `γ`, given a commutative monoid structure on `β`, a `Finset` `s` of elements of type `γ`, a function `t` mapping elements of `γ` to `Finset`s of `α`, a `Finset` `t'` of elements of type `α`, a function `s'` mapping elements of `α` to `Finset`s of `γ`, and a condition such that for any `x` in `γ` and `y` in `α`, `x` is in `s` and `y` is in `t x` if and only if `x` is in `s' y` and `y` is in `t'`, then for any function `f` from `γ` and `α` to `β`, the product over `s` of the product over `t x` of `f x y` is equal to the product over `t'` of the product over `s' y` of `f x y`. In simpler terms, it states that under certain conditions, the order in which we take products over nested `Finset`s doesn't matter.
More concisely: Given commutative monoids `β`, functions `t : γ → Finset α` and `s' : α → Finset γ`, a `Finset` `s` of `γ`, and functions `t' : Finset α → Finset γ`, `s' : Finset γ → Finset α`, and `f : γ × α → β`, if for all `x ∈ γ` and `y ∈ α`, `x ∈ s` if and only if `y ∈ t x` if and only if `x ∈ s' y` and `y ∈ t' x`, then `∏(s, ∏(xi, to x)) = ∏(t' xi, ∏(y, so y))`, where `∏` denotes the product over a `Finset`.
|
Finset.prod_filter_mul_prod_filter_not
theorem Finset.prod_filter_mul_prod_filter_not :
∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] (s : Finset α) (p : α → Prop) [inst_1 : DecidablePred p]
[inst_2 : (x : α) → Decidable ¬p x] (f : α → β),
(((Finset.filter p s).prod fun x => f x) * (Finset.filter (fun x => ¬p x) s).prod fun x => f x) =
s.prod fun x => f x
This theorem states that for any given type `α` and `β` where `β` is a Commutative Monoid, a finite set `s` of type `α`, a predicate `p` on `α` which is decidable, a function `f` from `α` to `β`, and for all elements of `α` the negation of predicate `p` is decidable, the product of `f x` for every `x` in the set of elements of `s` that satisfy `p`, multiplied by the product of `f x` for every `x` in the set of elements of `s` that do not satisfy `p`, is equal to the product of `f x` for every `x` in the set `s`. In other words, it's saying that the product over a set is the same as the product over the partition of the set by a certain decidable predicate.
More concisely: Given a type `α`, a Commutative Monoid `β`, a finite set `s` of type `α`, a decidable predicate `p` on `α`, and a function `f` from `α` to `β` such that the negation of `p` is also decidable, the product of `f` applied to elements of `s` that satisfy `p` is equal to the product of `f` applied to elements of `s` that satisfy `p` and the product of `f` applied to elements of `s` that do not satisfy `p`.
|
Finset.card_biUnion
theorem Finset.card_biUnion :
∀ {α : Type u_3} {β : Type u_4} [inst : DecidableEq β] {s : Finset α} {t : α → Finset β},
(∀ x ∈ s, ∀ y ∈ s, x ≠ y → Disjoint (t x) (t y)) → (s.biUnion t).card = s.sum fun u => (t u).card
This theorem states that for any two types `α` and `β`, given a finite set `s` of type `α` and a function `t` from `α` to a finite set of type `β`, if for all distinct elements `x` and `y` in `s`, the finite sets `t(x)` and `t(y)` are disjoint (meaning that their infimum is the bottom element), then the cardinality of the biUnion of `s` and `t` (which is the union of `t(a)` for all `a` in `s`) equals the sum of the cardinalities of `t(u)` for all `u` in `s`. In other words, the size of the union of all the sets `t(x)` for `x` in `s` is the sum of the sizes of these sets, provided that these sets are pairwise disjoint.
More concisely: Given a finite set `s` and a function `t` from a type `α` to finite sets of type `β`, if the images `t(x)` and `t(y)` are disjoint for all distinct `x` and `y` in `s`, then the cardinality of the union of `s` and the biUnion of `t` equals the sum of the cardinalities of the images `t(x)` for all `x` in `s`.
|
Finset.sum_ite
theorem Finset.sum_ite :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] {s : Finset α} {p : α → Prop} {hp : DecidablePred p}
(f g : α → β),
(s.sum fun x => if p x then f x else g x) =
((Finset.filter p s).sum fun x => f x) + (Finset.filter (fun x => ¬p x) s).sum fun x => g x
The theorem `Finset.sum_ite` asserts that for any finite set `s` of elements of type `α`, a decidable predicate `p` on `α`, and two functions `f` and `g` from `α` to `β` (where `β` forms an additive commutative monoid), the sum over all elements of `s` of `f(x)` if `p(x)` holds and `g(x)` otherwise, is equal to the sum of `f(x)` over elements of `s` that satisfy `p`, plus the sum of `g(x)` over elements of `s` that do not satisfy `p`. In other words, it splits the sum over a condition into two separate sums over the subsets where the condition is true and false, respectively.
More concisely: For any finite set `s`, decidable predicate `p` on a type `α`, and functions `f` and `g` from `α` to an additive commutative monoid `β`, the sum of `f(x)` over elements `x` in `s` that satisfy `p` is equal to the sum of `f(x)` for `x` in `s` plus the sum of `g(x)` for `x` in `s` where `p` does not hold.
|
Fintype.sum_bijective
theorem Fintype.sum_bijective :
∀ {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : AddCommMonoid α]
(e : ι → κ),
Function.Bijective e →
∀ (f : ι → α) (g : κ → α),
(∀ (x : ι), f x = g (e x)) → (Finset.univ.sum fun x => f x) = Finset.univ.sum fun x => g x
The theorem `Fintype.sum_bijective` states that for any two types `ι` and `κ` that have a finite number of elements (i.e., they are both instances of `Fintype`), and for any type `α` that is an instance of `AddCommMonoid` (meaning it behaves like a set of numbers with addition defined), if there is a bijective function `e` from `ι` to `κ`, then for any two functions `f : ι → α` and `g : κ → α` such that `f x` equals `g (e x)` for all `x` in `ι`, the sum of `f x` over all elements `x` in the universal finite set of type `ι` equals the sum of `g x` over all elements `x` in the universal finite set of type `κ`. Essentially, it says that if we re-label the elements of the finite set and apply the respective function, the sum remains the same.
More concisely: For any finite types `ι` and `κ` and functions `f : ι → α` and `g : κ → α` such that there exists a bijective function `e : ι ≃ κ` with `f x = g (e x)` for all `x`, the sum of `f x` over `ι` equals the sum of `g x` over `κ`.
|
Finset.prod_powerset_cons
theorem Finset.prod_powerset_cons :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} [inst : CommMonoid β] (ha : a ∉ s) (f : Finset α → β),
((Finset.cons a s ha).powerset.prod fun t => f t) =
(s.powerset.prod fun t => f t) * s.powerset.attach.prod fun t => f (Finset.cons a ↑t ⋯)
The theorem `Finset.prod_powerset_cons` states that for all types `α` and `β`, a set `s` of type `α`, an element `a` of type `α` not in `s`, and a function `f` from sets of type `α` to `β`, the product of the function `f` applied to each subset of the set formed by adding `a` to `s` (i.e., `s ∪ {a}`) is equal to the product of `f` applied to each subset of `s` multiplied by the product of `f` applied to each subset of `s` to which `a` is added. Here, the product is defined within a commutative monoid context. This theorem highlights a way to break down the product over a larger set into products over smaller sets.
More concisely: For all types `α` and `β`, sets `s` of `α`, elements `a ∉ s`, and functions `f` from sets of `α` to `β`, the product of `f` over subsets of `s ∪ {a}` equals the product of `f` over subsets of `s` multiplied by the product of `f` over subsets of `s` with `a` added.
|
AddMonoidHom.finset_sum_apply
theorem AddMonoidHom.finset_sum_apply :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : AddZeroClass β] [inst_1 : AddCommMonoid γ] (f : α → β →+ γ)
(s : Finset α) (b : β), (s.sum fun x => f x) b = s.sum fun x => (f x) b
This theorem, `AddMonoidHom.finset_sum_apply`, states that for any types `α`, `β`, and `γ`, where `β` is an additive monoid (AddZeroClass) and `γ` is a commutative additive monoid (AddCommMonoid), and given a function `f : α → β →+ γ` from type `α` to the type of additive monoid homomorphisms from `β` to `γ`, and a finite set (`Finset`) `s` of elements of type `α` and an element `b` of type `β`, the sum over `s` of `f(x)(b)` for each `x` in `s` is the same as the function application of the sum over `s` of `f(x)` for each `x` in `s` to `b`.
In other words, it's a rearrangement property of the sum operation over a finite set in the context of additive monoid homomorphisms, stating that summing the results of applying each function to a fixed element is the same as applying the sum of the functions to the fixed element.
More concisely: For any additive monoids β and γ, commutative additive monoid γ, and additive monoid homomorphism f from a type α to β →+ γ, the sum over a finite set s of α of f(x)(b) for each x in s equals the application of the sum over s of f(x) to b.
|
Finset.prod_eq_multiset_prod
theorem Finset.prod_eq_multiset_prod :
∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] (s : Finset α) (f : α → β),
(s.prod fun x => f x) = (Multiset.map f s.val).prod
The theorem `Finset.prod_eq_multiset_prod` states that for any given finite set `s` of type `α` and a function `f` from `α` to `β` where `β` forms a commutative monoid, the product of `f(x)` for each `x` in the set `s` (represented as `Finset.prod s f`) is equal to the product of the multiset obtained by mapping the function `f` over the underlying multiset of the finite set `s` (represented as `Multiset.prod (Multiset.map f s.val)`). In other words, calculating the product over a finite set using a function is equivalent to mapping the function over the set first and then taking the product.
More concisely: For any commutative monoid type `β` and a finite set `s` of type `α` along with a function `f` from `α` to `β`, the product of `f(x)` for all `x` in `s` equals the product of the multiset obtained by mapping `f` over the underlying multiset of `s`.
|
Finset.sum_fiberwise_of_maps_to
theorem Finset.sum_fiberwise_of_maps_to :
∀ {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [inst : AddCommMonoid α] {s : Finset ι} {t : Finset κ}
[inst_1 : DecidableEq κ] {g : ι → κ},
(∀ i ∈ s, g i ∈ t) →
∀ (f : ι → α), (t.sum fun j => (Finset.filter (fun i => g i = j) s).sum fun i => f i) = s.sum fun i => f i
This theorem states that for any types `ι`, `κ`, and `α`, where `α` is an additive commutative monoid, any finite sets `s` of type `ι` and `t` of type `κ`, any function `g` from `ι` to `κ` that maps each element of `s` into `t`, and any function `f` from `ι` to `α`, the sum of the values of `f` over `s` equals the sum of the sums of the values of `f` over the elements of `s` that map to each element of `t` under `g`. In other words, it's asserting that you can rearrange the terms in the sum over `s` of `f` by grouping together the terms that correspond to elements of `s` that map to the same element of `t` under `g`, and this rearrangement does not change the sum's value.
More concisely: For any additive commutative monoid α, given finite sets s:ι and t:κ, function g:ι -> κ mapping s into t, and function f:ι -> α, the sum ∑i in s. f i equals the sum ∑j in t. (∑i in g ^-1 {j}. f i).
|
Equiv.sum_comp
theorem Equiv.sum_comp :
∀ {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : AddCommMonoid α]
(e : ι ≃ κ) (g : κ → α), (Finset.univ.sum fun i => g (e i)) = Finset.univ.sum fun i => g i
The theorem `Equiv.sum_comp` states that for any types `ι`, `κ`, and `α`, where `ι` and `κ` are finite types and `α` is a type with an additive commutative monoid structure, for any equivalence `e` between `ι` and `κ`, and any function `g` from `κ` to `α`, the sum of `g (e i)` over all elements `i` in the universal finite set of type `ι` is equal to the sum of `g i` over all elements `i` in the universal finite set of type `κ`. In other words, summing over a set of values transformed by an equivalence function gives the same result as summing over the original set of values.
More concisely: For any equivolution `e` between finite types `ι` and `κ` and any additive commutative monoid `α`, and for any function `g` from `κ` to `α`, the sum of `g (e i)` over all elements `i` in `ι` equals the sum of `g i` over all elements `i` in `κ`.
|
Finset.prod_bij'
theorem Finset.prod_bij' :
∀ {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [inst : CommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α}
{g : κ → α} (i : (a : ι) → a ∈ s → κ) (j : (a : κ) → a ∈ t → ι) (hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t)
(hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s),
(∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a) →
(∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a) →
(∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)) → (s.prod fun x => f x) = t.prod fun x => g x
This theorem, `Finset.prod_bij'`, states that for any two finite sets `s` of type `ι` and `t` of type `κ` and for any two functions `f : ι → α` and `g : κ → α` defined on these sets with values in a commutative monoid `α`, if there exists a pair of functions `i : ι → κ` and `j : κ → ι` that forms a bijection between the sets `s` and `t` (with the property that each function `i` maps elements in `s` to elements in `t` and `j` maps elements in `t` to elements in `s`, and the compositions `j ∘ i` and `i ∘ j` are identity mappings on `s` and `t` respectively), and if `f` and `g` are equivalent under this bijection (meaning that applying `f` to any element `a` of `s` gives the same result as applying `g` to the image of `a` under `i`), then the product of `f` over all elements in `s` is equal to the product of `g` over all elements in `t`. This theorem is useful for switching between different indexes in a product without changing the final result.
More concisely: If two functions with the same domain and codomain, defined on finite sets with a bijection between them, have equivalent values under this bijection, then their respective products over their respective sets are equal.
|
Finset.sum_bijective
theorem Finset.sum_bijective :
∀ {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [inst : AddCommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α}
{g : κ → α} (e : ι → κ),
Function.Bijective e →
(∀ (i : ι), i ∈ s ↔ e i ∈ t) → (∀ i ∈ s, f i = g (e i)) → (s.sum fun i => f i) = t.sum fun i => g i
The theorem `Finset.sum_bijective` states that for all types `ι`, `κ`, `α` where `α` is an additive commutative monoid, given two finite sets `s` and `t` of types `ι` and `κ` respectively, and two functions `f : ι → α` and `g : κ → α`, if there exists a bijective function `e : ι → κ` such that every `i` in `s` maps to `t` through `e`, and the value of `f` at any `i` in `s` equals to the value of `g` at `e(i)`, then the sum of all elements in `s` under `f` equals the sum of all elements in `t` under `g`. In mathematical terms, this theorem is saying $\sum_{i \in s} f(i) = \sum_{i \in t} g(i)$ under the given conditions.
More concisely: Given finite sets $s$ and $t$ of types $\ι$ and $\κ$ respectively, and functions $f : ι \rightarrow \alpha$ and $g : κ \rightarrow \alpha$ from an additive commutative monoid $\alpha$, if there exists a bijective function $e : ι \rightarrow κ$ such that $f(i) = g(e(i))$ for all $i$ in $s$, then $\sum\_{i \in s} f(i) = \sum\_{i \in t} g(i)$.
|
Finset.prod_partition
theorem Finset.prod_partition :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [inst : CommMonoid β] (R : Setoid α)
[inst_1 : DecidableRel Setoid.r],
(s.prod fun x => f x) =
(Finset.image Quotient.mk'' s).prod fun xbar => (Finset.filter (fun x => ⟦x⟧ = xbar) s).prod fun y => f y
This theorem states that given a finset `s` and a function `f` from the elements of `s` to a commutative monoid, it's possible to reorganize the total product of `f` over `s` into a product of products, where each sub-product is over a partition of `s`. These partitions are determined by an equivalence relation on the elements of `s`, represented by a setoid `R`. Specifically, each partition consists of all elements `x` in `s` that are equivalent under `R` to a given representative `xbar`. The representative `xbar` is the equivalence class of `x` under `R`, denoted as `⟦x⟧`.
More concisely: Given a finset `s`, an equivalence relation `R` on its elements, and a function `f` from `s` to a commutative monoid, the total product of `f` over `s` is equal to the product of products of `f` over partitions of `s` determined by `R`.
|
Finset.prod_disjUnion
theorem Finset.prod_disjUnion :
∀ {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f : α → β} [inst : CommMonoid β] (h : Disjoint s₁ s₂),
((s₁.disjUnion s₂ h).prod fun x => f x) = (s₁.prod fun x => f x) * s₂.prod fun x => f x
This theorem states that for all types `α` and `β`, all `α`-typed finite sets `s₁` and `s₂`, and all functions `f` mapping from `α` to `β`, under the commutative monoid structure of `β`, if `s₁` and `s₂` are disjoint, then the product of `f x` (where `x` ranges over the elements) over the disjoint union of `s₁` and `s₂` equals the product of `f x` over `s₁` times the product of `f x` over `s₂`. In other words, the product over the disjoint union of two sets is equal to the product of the individual products over the sets, assuming that the sets are disjoint.
More concisely: For all types `α`, `β`, finite sets `s₁` and `s₂` of type `α`, and functions `f : α → β`, if `s₁` and `s₂` are disjoint, then the product of `f x` over the disjoint union of `s₁` and `s₂` equals the product of the product of `f x` over `s₁` and the product of `f x` over `s₂`.
|
Finset.prod_nbij
theorem Finset.prod_nbij :
∀ {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [inst : CommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α}
{g : κ → α} (i : ι → κ),
(∀ a ∈ s, i a ∈ t) →
Set.InjOn i ↑s → Set.SurjOn i ↑s ↑t → (∀ a ∈ s, f a = g (i a)) → (s.prod fun x => f x) = t.prod fun x => g x
This theorem, `Finset.prod_nbij`, states that in the context of a commutative monoid, for any sets `s` of type `ι` and `t` of type `κ`, and any functions `f : ι → α` and `g : κ → α`, given a function `i : ι → κ` that maps every element of `s` into `t`, is an injective function on `s`, and is a surjective function from `s` to `t`, if `f` and the composition of `g` with `i` are equal for all elements in `s`, then the product of the elements of `s` under `f` is equal to the product of the elements of `t` under `g`. This theorem demonstrates a way to reorder a product in the context of a commutative monoid by providing a bijection specified as a surjective injection, without using an inverse function or using membership of the domain of the product.
More concisely: If `f : ι → α`, `g : κ → α`, `i : ι → κ` are functions in a commutative monoid such that `i` is an injection from `s` to `t`, `f` and `g ∘ i` agree on `s`, then `∏ x ∈ s f x = ∏ y ∈ t g y`.
|
Finset.sum_powerset_cons
theorem Finset.sum_powerset_cons :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} [inst : AddCommMonoid β] (ha : a ∉ s) (f : Finset α → β),
((Finset.cons a s ha).powerset.sum fun t => f t) =
(s.powerset.sum fun t => f t) + s.powerset.attach.sum fun t => f (Finset.cons a ↑t ⋯)
The theorem `Finset.sum_powerset_cons` states the following:
For every type `α` and `β` and for every finite set `s` of type `α` and for any element `a` of type `α` that is not in `s`, given an additive commutative monoid `β` and a function `f` mapping from a finite set of type `α` to `β`, the sum of the function `f` over all subsets of the set `s` union the singleton set `{a}` is equal to the sum of the function `f` over all subsets of `s`, plus the sum of the function `f` over all subsets of `s` to which the element `a` is added. This theorem essentially describes a partition of the sum over the powerset of `s ∪ {a}` into two separate sums over subsets of `s`.
More concisely: For any finite set $S$ and element $a \notin S$, in an additive commutative monoid $\beta$, the sum of a function $f$ over all subsets of $S \cup \{a\}$ is equal to the sum over subsets of $S$ plus the sum over subsets of $S$ with $a$ added.
|
Finset.prod_subtype_of_mem
theorem Finset.prod_subtype_of_mem :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} [inst : CommMonoid β] (f : α → β) {p : α → Prop}
[inst_1 : DecidablePred p], (∀ x ∈ s, p x) → ((Finset.subtype p s).prod fun x => f ↑x) = s.prod fun x => f x
This theorem states that for any finite set `s` of elements with type `α` and a function `f` from `α` to `β` where `β` is a commutative monoid, if a predicate `p` is true for all elements in `s`, then the product of the function `f` evaluated at each of the elements in the subtype of `s` determined by `p` is equal to the product of `f` evaluated at each element in `s`. In other words, filtering `s` based on `p` and taking the product doesn't change the result if `p` is true for all elements in `s`.
More concisely: For any commutative monoid `β`, finite set `s` of elements of type `α`, and function `f` from `α` to `β`, if `p` is a predicate true for all elements in `s`, then the product of `f` over the subtype of `s` determined by `p` equals the product of `f` over `s`.
|
Function.Bijective.sum_comp
theorem Function.Bijective.sum_comp :
∀ {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : AddCommMonoid α]
{e : ι → κ},
Function.Bijective e → ∀ (g : κ → α), (Finset.univ.sum fun i => g (e i)) = Finset.univ.sum fun i => g i
This theorem, named `Function.Bijective.sum_comp`, states that for all types ι, κ, and α where ι and κ are finite types and α is a type with a commutative addition operation, for any bijective function `e` mapping elements of type ι to κ, and for any function `g` mapping elements of type κ to α, the sum of function `g` applied to the image of each element in the universal set of ι under `e` is equal to the sum of function `g` applied to each element in the universal set of κ. In other words, when `e` is a bijection, rearranging the elements of the finite sets using `e` doesn't change the total sum when applying the function `g`.
More concisely: For any bijective function between finite types and a commutative additive type, the sum of the function applied to the images of the elements under the bijection equals the sum of the function applied to the elements themselves.
|
Multiset.toFinset_sum_count_nsmul_eq
theorem Multiset.toFinset_sum_count_nsmul_eq :
∀ {α : Type u_3} [inst : DecidableEq α] (s : Multiset α), (s.toFinset.sum fun a => Multiset.count a s • {a}) = s
This theorem states that for any multiset `s` of a type `α` that has decidable equality, the sum over the finset obtained from `s` through the function `Multiset.toFinset`, of the product of the count of each element `a` in `s` and the singleton set containing `a` (`Multiset.count a s • {a}`), is equal to the original multiset `s`.
In other words, if we convert a multiset to a finset, which removes any duplicate elements, and then for each element in the finset, we multiply the count of that element in the original multiset by a singleton set containing that element, and sum all these results, we get back the original multiset.
More concisely: For any decidably equal multiset `s` of type `α`, the sum over its corresponding finset of the count of each element multiplied by the singleton set is equal to the multiset itself: `∑ x ∈ Multiset.toFinset s, Multiset.count x s • {x} = s`.
|
Finset.prod_eq_zero
theorem Finset.prod_eq_zero :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [inst : CommMonoidWithZero β],
a ∈ s → f a = 0 → (s.prod fun x => f x) = 0
The theorem `Finset.prod_eq_zero` states that for any types `α` and `β`, a finite set `s` of type `α`, an element `a` of type `α`, and a function `f` mapping elements from `α` to `β`, given the condition that `β` is a commutative monoid with zero, if `a` is an element of `s` and `f(a)` equals zero, then the product of `f(x)` for all `x` in the set `s`, denoted as `∏ x in s, f x`, is zero. This theorem captures the idea that if you multiply a set of numbers and one of those numbers is zero, then the whole product becomes zero.
More concisely: If `β` is a commutative monoid with zero, then for any finite set `s` of type `α`, element `a` of type `α`, and function `f` from `α` to `β` with `a` in `s` and `f(a)` equal to zero, it follows that `∏ x in s, f x` equals zero.
|
Finset.prod_const_one
theorem Finset.prod_const_one :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} [inst : CommMonoid β], (s.prod fun _x => 1) = 1
The theorem `Finset.prod_const_one` states that for any finite set `s` of elements of some type `α` and for any commutative monoid `β`, the product of the constant function `1` over all elements of `s` is `1`. In other words, if you take the product of the number `1` for each element in a finite set, the overall product will always be `1`.
More concisely: For any finite set `s` and commutative monoid `β`, the product of the constant function `1` over all elements of `s` equals `1`.
|
Finset.prod_congr
theorem Finset.prod_congr :
∀ {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f g : α → β} [inst : CommMonoid β],
s₁ = s₂ → (∀ x ∈ s₂, f x = g x) → s₁.prod f = s₂.prod g
The theorem `Finset.prod_congr` states that for any two sets `s₁` and `s₂` of the same type `α`, and any two functions `f` and `g` from `α` to another type `β` (where `β` is a commutative monoid), if `s₁` and `s₂` are the same, and `f(x)` equals `g(x)` for every element `x` in `s₂`, then the product of `f(x)` over all elements `x` in `s₁` is equal to the product of `g(x)` over all elements `x` in `s₂`. In mathematical terms, if $s_1 = s_2$ and $f(x) = g(x)$ for all $x \in s_2$, then $\prod_{x \in s_1} f(x) = \prod_{x \in s_2} g(x)$.
More concisely: If two sets have the same elements and every element maps the same way under two functions to a commutative monoid, then the products of the functions over the sets are equal.
|
Finset.sum_map
theorem Finset.sum_map :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : AddCommMonoid β] (s : Finset α) (e : α ↪ γ) (f : γ → β),
((Finset.map e s).sum fun x => f x) = s.sum fun x => f (e x)
The theorem `Finset.sum_map` states that for any finite set `s` of a type `α`, an embedding function `e` from `α` to another type `γ`, and any function `f` from `γ` to a type `β` that has additive commutative monoid structure, the sum of the function `f` applied over the image set of `s` under the embedding `e` is equal to the sum of the function `f` composed with `e` applied over the set `s`. In simpler terms, when you map each element of a finite set to another set using an embedding and then perform a sum operation, it is the same as if you first apply the function to each element of the original set via the embedding and then sum the results.
More concisely: For any finite set `s` of type `α`, embedding function `e` from `α` to type `γ`, and additive commutative monoid homomorphism `f` from `γ` to type `β`, the sum of `f` applied to the images of `s` under `e` equals the sum of `f` composed with `e` applied to `s`.
|
Finset.prod_disj_sum
theorem Finset.prod_disj_sum :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : CommMonoid β] (s : Finset α) (t : Finset γ) (f : α ⊕ γ → β),
((s.disjSum t).prod fun x => f x) = (s.prod fun x => f (Sum.inl x)) * t.prod fun x => f (Sum.inr x)
The `Finset.prod_disj_sum` theorem states that for any two finite sets `s` and `t`, and any function `f` from the disjoint union of `s` and `t` to a commutative monoid, the product of `f` over the disjoint union of `s` and `t` equals the product of the restrictions of `f` to `s` and `t`, separately. Here, the restriction of `f` to `s` or `t` is calculated by applying `f` to an element from `s` or `t`, respectively, and then taking the sum of the left or right, respectively. This theorem articulates a form of distributivity for the product operation over finite sets.
More concisely: For any commutative monoid M and finite sets s and t, the function product of a function from the disjoint union of s and t to M equals the function product of the restrictions of the function to s and t.
|
Finset.sum_subtype_of_mem
theorem Finset.sum_subtype_of_mem :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} [inst : AddCommMonoid β] (f : α → β) {p : α → Prop}
[inst_1 : DecidablePred p], (∀ x ∈ s, p x) → ((Finset.subtype p s).sum fun x => f ↑x) = s.sum fun x => f x
The theorem `Finset.sum_subtype_of_mem` states that if all elements of a finite set `s` of type `α` satisfy a certain predicate `p`, then the sum of the function `f` applied to all elements in the `subtype` of `s` with respect to `p` is the same as the sum of `f` applied to all elements in `s` itself. Here, `f` is a function that maps elements of type `α` to elements of type `β`, where `β` is an additive commutative monoid, and `p` is a decidable predicate on `α`.
More concisely: If `s` is a finite set of type `α` and `p` is a decidable predicate on `α` such that `p(x)` holds for all `x` in `s`, then the sum of `f(x)` for `x` in the subtype of `s` with respect to `p` equals the sum of `f(x)` for all `x` in `s`.
|
Finset.sum_flip
theorem Finset.sum_flip :
∀ {β : Type u_4} [inst : AddCommMonoid β] {n : ℕ} (f : ℕ → β),
((Finset.range (n + 1)).sum fun r => f (n - r)) = (Finset.range (n + 1)).sum fun k => f k
The theorem `Finset.sum_flip` states that for any type `β` that is an additive commutative monoid, and for any natural number `n` and function `f` from natural numbers to `β`, the sum of `f(n - r)` for each `r` in the set of natural numbers less than `n + 1` equals the sum of `f(k)` for each `k` in the set of natural numbers less than `n + 1`. In other words, summing the values of the function `f` applied to each number up to `n` is the same as summing the values of `f` applied to `n` minus each number up to `n`. This theorem essentially states that the order of summation does not matter in an additive commutative monoid.
More concisely: For any additive commutative monoid type `β` and function `f` from natural numbers to `β`, the sum of `f(n - r)` for `r` in the set of natural numbers less than `n + 1` equals the sum of `f(k)` for `k` in the same set, i.e., the order of summation does not matter.
|
Finset.prod_product'
theorem Finset.prod_product' :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : CommMonoid β] {s : Finset γ} {t : Finset α} {f : γ → α → β},
((s ×ˢ t).prod fun x => f x.1 x.2) = s.prod fun x => t.prod fun y => f x y
This theorem, `Finset.prod_product'`, provides an uncurried version of the `Finset.prod_product` theorem. It states that for any types `α`, `β`, and `γ`, and given a commutative monoid for type `β`, a finite set `s` of type `γ`, a finite set `t` of type `α`, and a function `f` mapping an element of `γ` and `α` to `β`, the product of `f` over the Cartesian product of `s` and `t` is equal to the product of `f` over each element in `s` and `t`. That is, it expresses the distributive property of the product operation over Cartesian product of finite sets.
More concisely: For any commutative monoid β, given finite sets s:Γ and t:α, and a function f:γ × α → β, the product of f over the Cartesian product of s and t is equal to the product of f over each element in s and the product of f over each element in t. In other words, (∏ i in s ∏ j in t) f i j = ∏ i in s ∏ j in t f i j.
|
Finset.prod_div_distrib
theorem Finset.prod_div_distrib :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {f g : α → β} [inst : DivisionCommMonoid β],
(s.prod fun x => f x / g x) = (s.prod fun x => f x) / s.prod fun x => g x
This theorem, `Finset.prod_div_distrib`, states that for any finite set `s` of elements of type `α` and for any two functions `f` and `g` from `α` to `β`, where `β` possesses a commutative division monoid structure, the product over `s` of the function values of `f` divided by `g` is equal to the product over `s` of the function values of `f` divided by the product over `s` of the function values of `g`. In mathematical notation, this is equivalent to the statement $\prod_{x \in s} \frac{f(x)}{g(x)} = \frac{\prod_{x \in s} f(x)}{\prod_{x \in s} g(x)}$.
More concisely: For any finite set `s` and functions `f` and `g` from a commutative division monoid to itself, the product of `f` over `s` divided by the product of `g` over `s` is equal to the product of `f(x) / g(x)` for all `x` in `s`.
|
map_prod
theorem map_prod :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : CommMonoid β] [inst_1 : CommMonoid γ] {G : Type u_6}
[inst_2 : FunLike G β γ] [inst_3 : MonoidHomClass G β γ] (g : G) (f : α → β) (s : Finset α),
g (s.prod fun x => f x) = s.prod fun x => g (f x)
This theorem, named `map_prod`, states that for any types `α`, `β`, `γ`, and `G`, given that `β` and `γ` are commutative monoids, `G` is a function-like structure from `β` to `γ`, and `G` also forms a monoid homomorphism from `β` to `γ`. If we have a function `g : G`, a function `f : α → β`, and a finite set `s : Finset α`, then applying `g` to the product of the elements in `s` mapped by `f` is the same as the product of the elements in `s` mapped by `g` composed with `f`. In mathematical terms, it states that $g(\prod_{x \in s} f(x)) = \prod_{x \in s} g(f(x))$. This is essentially a property of homomorphisms in the context of commutative monoids.
More concisely: Given commutative monoids `β` and `γ`, a monoid homomorphism `G : β → γ`, and `f : α → β` and `g : G`, `g(∏ₓ x ∈ s. f x) = ∏ₓ x ∈ s. g(f x)`, where `s : Finset α`.
|
Finset.prod_congr_set
theorem Finset.prod_congr_set :
∀ {α : Type u_6} [inst : CommMonoid α] {β : Type u_7} [inst_1 : Fintype β] (s : Set β)
[inst_2 : DecidablePred fun x => x ∈ s] (f : β → α) (g : ↑s → α),
(∀ (x : β) (h : x ∈ s), f x = g ⟨x, h⟩) → (∀ x ∉ s, f x = 1) → Finset.univ.prod f = Finset.univ.prod g
The theorem `Finset.prod_congr_set` states that for any types `α` and `β`, where `α` is a commutative monoid and `β` is a finite type, given a set `s` of type `β`, a decidable predicate that determines set membership, and functions `f : β → α` and `g : ↑s → α`, if `f` and `g` agree on all elements `x` in set `s`, and `f` maps all elements not in `s` to the identity element `1` of the commutative monoid `α`, then the product of `f` over all elements of the finite type `β` is equal to the product of `g` over all elements in set `s`.
More concisely: If `α` is a commutative monoid, `β` is a finite type, `s` is a set of `β`, `P` is a decidable subset membership predicate for `s`, `f : β → α`, and `g : s → α` agree on all elements in `s` and map all other elements to the identity `1` in `α`, then `∏ x : β, f x = ∏ x in s, g x`.
|
Finset.exists_ne_zero_of_sum_ne_zero
theorem Finset.exists_ne_zero_of_sum_ne_zero :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [inst : AddCommMonoid β],
(s.sum fun x => f x) ≠ 0 → ∃ a ∈ s, f a ≠ 0
This theorem states that for any types α and β, and for any finite set `s` of type α and function `f` from α to β, if the sum of the values of `f` over all elements in `s` is not equal to zero (where the sum and zero are defined with respect to an additive commutative monoid structure on β), then there exists an element `a` in `s` such that the value of `f` at `a` is not equal to zero.
More concisely: If `f` is a function from a finite set `s` in type α to type β with non-zero sum, then there exists an element `a` in `s` such that `f a ≠ 0`.
|
Finset.sum_range_sub
theorem Finset.sum_range_sub :
∀ {M : Type u_6} [inst : AddCommGroup M] (f : ℕ → M) (n : ℕ),
((Finset.range n).sum fun i => f (i + 1) - f i) = f n - f 0
The theorem `Finset.sum_range_sub` states that for any function `f` from natural numbers to an additive commutative group `M`, and any natural number `n`, the sum over the range `{0, ..., n - 1}` of the difference `f (i + 1) - f i` equals the difference `f n - f 0`. In simpler terms, it asserts the "telescoping property" where most terms in the sum cancel each other out, leaving only the difference of the last term `f n` and the first term `f 0`.
More concisely: For any additive commutative group M and natural number n, the sum of the differences between consecutive applications of a function f from natural numbers to M from i = 0 to i = n - 1 equals the difference between f(n) and f(0).
|
Finset.sum_powerset_insert
theorem Finset.sum_powerset_insert :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} [inst : AddCommMonoid β] [inst_1 : DecidableEq α],
a ∉ s →
∀ (f : Finset α → β),
((insert a s).powerset.sum fun t => f t) =
(s.powerset.sum fun t => f t) + s.powerset.sum fun t => f (insert a t)
The theorem `Finset.sum_powerset_insert` states that for any type `α` and `β`, a finite set `s` of type `α`, an element `a` of type `α`, additive commutative monoid structure on `β`, and decidable equality on `α`, if `a` is not an element of `s`, then for any function `f` from finite sets of `α` to `β`, the sum (under the operation of `β`) of the function `f` applied over the powerset of the set obtained by inserting `a` into `s` is equal to the sum of `f` applied over the powerset of `s`, plus the sum of `f` applied to the sets obtained by inserting `a` into each subset of the powerset of `s`. This can be seen as a specific version of the principle of inclusion-exclusion in combinatorics.
More concisely: For any additive commutative monoid `β`, finite set `s` of type `α` with decidable equality, and function `f` from finite sets of `α` to `β`, the sum of `f` over the powerset of `s ∪ {a}` equals the sum over the powerset of `s` plus the sum over the sets obtained by inserting `a` into each subset of `s`.
|
Finset.prod_product_right'
theorem Finset.prod_product_right' :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : CommMonoid β] {s : Finset γ} {t : Finset α} {f : γ → α → β},
((s ×ˢ t).prod fun x => f x.1 x.2) = t.prod fun y => s.prod fun x => f x y
The theorem `Finset.prod_product_right'` is an uncurried version of the theorem `Finset.prod_product_right`. Given types `α`, `β`, and `γ`, with `β` being a commutative monoid, a finite set `s` of type `γ`, a finite set `t` of type `α`, and a function `f` from `γ` and `α` to `β`, it states that the product over the cartesian product of `s` and `t` applied to function `f` is equal to the product over `t` of the product over `s` applied to function `f`. This is about rearranging the order of computation in the product of a cartesian product of two finite sets.
More concisely: For commutative monoids β, finite sets s of type γ and t of type α, and a function f from γ × α to β, the product ∏(s × t) (f) = ∏t (∏s (f)).
|
Finset.sum_singleton
theorem Finset.sum_singleton :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] (f : α → β) (a : α), ({a}.sum fun x => f x) = f a := by
sorry
The theorem `Finset.sum_singleton` states that for any types `α` and `β`, given an addition-commutative monoid on `β`, a function `f` from `α` to `β` and a value `a` of type `α`, the sum over the singleton set `{a}` (i.e., a set containing only `a`) of the function `f` is equal to the function `f` applied to `a`. In mathematical terms, for a given function `f: α → β` and a single element `a` of `α`, this theorem states that `∑_{x in {a}} f(x) = f(a)`.
More concisely: For any addition-commutative monoid β, function f : α → β, and element a of α, the sum of the function f over the singleton set {a} equals f(a).
|
Finset.sum_ite_eq
theorem Finset.sum_ite_eq :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] [inst_1 : DecidableEq α] (s : Finset α) (a : α)
(b : α → β), (s.sum fun x => if a = x then b x else 0) = if a ∈ s then b a else 0
The theorem `Finset.sum_ite_eq` states that for any type `α`, type `β` with an addition commutative monoid structure, a finset `s` of `α`, an element `a` of `α`, and a function `b` mapping `α` to `β`, the sum over the finset `s` of the function which applies `b` to `x` if `x` equals `a` and otherwise returns zero, is equal to `b(a)` if `a` is an element of `s` and is otherwise zero. This can be interpreted as saying that the sum of a set of conditionally defined elements equals the value of the element if the condition is met in the set or zero if it isn't.
More concisely: For any commutative monoid type `β`, finset `s` of type `α`, element `a` of `α`, and function `b` from `α` to `β`, the sum of `b` applied to elements of `s` that equal `a` equals `b(a)` if `a` is in `s`, and is zero otherwise.
|
Fintype.sum_equiv
theorem Fintype.sum_equiv :
∀ {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : AddCommMonoid α]
(e : ι ≃ κ) (f : ι → α) (g : κ → α),
(∀ (x : ι), f x = g (e x)) → (Finset.univ.sum fun x => f x) = Finset.univ.sum fun x => g x
The theorem `Fintype.sum_equiv` states that for any two types `ι` and `κ`, both having a `Fintype` instance, and for any type `α` with an `AddCommMonoid` instance, given an equivalence `e` between `ι` and `κ`, a function `f` from `ι` to `α`, and a function `g` from `κ` to `α`, if for each element `x` of `ι`, `f x` equals `g` of the image of `x` under `e`, then the sum of `f x` for all `x` in the universal finite set of `ι` equals the sum of `g x` for all `x` in the universal finite set of `κ`. This theorem shows that the sum of the elements of a function over a finite set remains the same after a bijective transformation.
More concisely: Given types `ι` and `κ` with `Fintype` instances, an equivalence `e` between them, and functions `f: ι → α` and `g: κ → α` such that `f x = g (e x)` for all `x`, the sum of `f` over the universal finite set of `ι` equals the sum of `g` over the universal finite set of `κ`.
|
Finset.eq_zero_of_sum_eq_zero
theorem Finset.eq_zero_of_sum_eq_zero :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] {s : Finset α} {f : α → β} {a : α},
(s.sum fun x => f x) = 0 → (∀ x ∈ s, x ≠ a → f x = 0) → ∀ x ∈ s, f x = 0
The theorem `Finset.eq_zero_of_sum_eq_zero` states that, given a finite set `s` of some type `α` and a function `f : α → β` from `α` to some additive commutative monoid `β`, if the sum of the function values over all elements in `s` equals zero and the function is zero at all points in `s` except possibly at one point `a`, then the function must be zero at all points in `s`. In simpler terms, if all the values of a function over a finite set add up to zero, and the function is zero everywhere except possibly one point, then it must be zero even at that point.
More concisely: If a function from a finite set to an additive commutative monoid has zero sum over the set and is zero at all but one point, then it is zero at that remaining point.
|
Finset.sum_comp
theorem Finset.sum_comp :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Finset α} [inst : AddCommMonoid β] [inst_1 : DecidableEq γ]
(f : γ → β) (g : α → γ),
(s.sum fun a => f (g a)) = (Finset.image g s).sum fun b => (Finset.filter (fun a => g a = b) s).card • f b
The theorem `Finset.sum_comp` states that for any finite set `s` of elements of type `α`, a function `f` from `γ` to `β`, and a function `g` from `α` to `γ`, the sum of `f` composed with `g` over all elements of `s` is equal to the sum over all elements `b` in the image of `s` under `g`, of the product of `f b` and the cardinality of the preimage of `b` under `g` in `s`. This is also known as summing over the distinct values of `g`, with each value weighted by the number of times it appears in `s`. This requires `β` to have a commutative additive monoid structure and `γ` to have decidable equality.
More concisely: For any finite set `s` of elements from type `α`, functions `f: γ → β` and `g: α → γ`, and given that `β` has a commutative additive monoid structure and `γ` has decidable equality, the sum of `f` composed with `g` over `s` equals the sum of the products of `f` applied to elements in the image of `g` in `s` and the cardinality of the preimage of those elements under `g` in `s`.
|
Finset.sum_cancels_of_partition_cancels
theorem Finset.sum_cancels_of_partition_cancels :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [inst : AddCommMonoid β] (R : Setoid α)
[inst_1 : DecidableRel Setoid.r],
(∀ x ∈ s, ((Finset.filter (fun y => y ≈ x) s).sum fun a => f a) = 0) → (s.sum fun x => f x) = 0
The theorem `Finset.sum_cancels_of_partition_cancels` states that for any given finite set `s` of elements of type `α` and any given function `f` from `α` to `β` where `β` is a type with an associated additive commutative monoid structure, if we have a decidable equivalence relation `R` on `α` that partitions our set into subsets and the sum of the function `f` applied to each of these subsets equals zero, then the sum of the function `f` applied to the entire set `s` is also zero. In other words, if we can break a set into smaller subsets such that the sum of the function applied to each subset is zero, then the sum of the function applied to the entire set will also be zero.
More concisely: If `f` is a function from a finite set `s` to an additive commutative monoid with the property that the sum of `f` over each subset of `s` determined by a decidable equivalence relation that partitions `s` is zero, then the sum of `f` over `s` is also zero.
|
Finset.sum_congr
theorem Finset.sum_congr :
∀ {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f g : α → β} [inst : AddCommMonoid β],
s₁ = s₂ → (∀ x ∈ s₂, f x = g x) → s₁.sum f = s₂.sum g
The theorem `Finset.sum_congr` states that for any two finite sets `s₁` and `s₂` of type `α`, and any two functions `f` and `g` from `α` to `β`, where `β` is a type with an addition operation that is commutative and associative, if `s₁` is equal to `s₂` and `f` is equal to `g` for all elements in `s₂`, then the sum of the function `f` evaluated over the set `s₁` is equal to the sum of the function `g` evaluated over the set `s₂`. In mathematical terms, this can be written as: if $s_1 = s_2$ and $f(x) = g(x)$ for all $x \in s_2$, then $\sum_{x \in s_1} f(x) = \sum_{x \in s_2} g(x)$.
More concisely: If two finite sets have the same elements and a function maps them equivalently to another type with commutative and associative addition, then the sum of the function over the first set equals the sum over the second set.
|
Finset.prod_ne_zero_iff
theorem Finset.prod_ne_zero_iff :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [inst : CommMonoidWithZero β] [inst_1 : Nontrivial β]
[inst_2 : NoZeroDivisors β], (s.prod fun x => f x) ≠ 0 ↔ ∀ a ∈ s, f a ≠ 0
The theorem `Finset.prod_ne_zero_iff` states that for any type `α`, a type `β` that has a commutative monoid structure with zero, is nontrivial and has no zero divisors, a finite set `s` of type `α`, and a function `f` from `α` to `β`, the product of `f(x)` for all `x` in `s` is non-zero if and only if `f(a)` is non-zero for all elements `a` in `s`. Essentially, this theorem asserts that the product of a function's values over a finite set is non-zero if every value produced by the function for elements in the set is non-zero.
More concisely: For any commutative monoid with zero, having no zero divisors, and a finite set and function, the product of the function values on the set is non-zero if and only if every value is non-zero.
|
Finset.prod_singleton
theorem Finset.prod_singleton :
∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] (f : α → β) (a : α), ({a}.prod fun x => f x) = f a
The theorem `Finset.prod_singleton` asserts that for every type `α` and `β`, given `β` forms a commutative monoid, and given a function `f` from `α` to `β`, as well as an element `a` of type `α`, the product of the function `f` over the singleton finite set containing only `a` (notated as `Finset.prod {a} f`) is equal to the function `f` applied to `a` (notated as `f a`). In other words, the product of a single-element set under any function is just the function applied to that element.
More concisely: For any type `α` and commutative monoid `β`, and given a function `f` from `α` to `β` and an element `a` of type `α`, the product of `f` over the singleton finite set `{a}` is equal to the application of `f` to `a`, i.e., `Finset.prod {a} f = f a`.
|
Finset.prod_eq_one
theorem Finset.prod_eq_one :
∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] {f : α → β} {s : Finset α},
(∀ x ∈ s, f x = 1) → (s.prod fun x => f x) = 1
This theorem states that for any type `α` and any commutative monoid `β`, given a function `f` from `α` to `β` and a finite set `s` of type `α`, if all the elements in `s` when mapped by `f` equals to the identity element of `β` (which is `1` for a commutative monoid), then the product of all these mapped elements (denoted as `Finset.prod s f`) is also equal to the identity element of `β`. In other words, the product over a finite set of all `1`'s in a commutative monoid is `1`.
More concisely: For any commutative monoid `β` and finite set `s` of a type `α`, if for all `x ∈ s`, `f(x) = 1_β`, then `Finset.prod s f = 1_β`.
|
Finset.sum_ite_zero
theorem Finset.sum_ite_zero :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] (s : Finset α) (p : α → Prop) [inst_1 : DecidablePred p],
(∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j) →
∀ (a : β), (s.sum fun i => if p i then a else 0) = if ∃ i ∈ s, p i then a else 0
The `Finset.sum_ite_zero` theorem in Lean 4 is about summation over a finite set. It states that for any types `α` and `β`, where `β` has an additive commutative monoid structure, given a finite set `s` of `α` and a decidable predicate `p` on `α`, if for all `i` and `j` in `s`, if `p i` and `p j` are true then `i` equals `j`. Then for any element `a` of `β`, the sum over `s` of the function which assigns `a` if `p i` is true and 0 otherwise, equals `a` if there exists an element `i` in `s` for which `p i` is true, and 0 otherwise. This theorem is a generalization of the principle that the sum of a constant over a set is equal to the size of the set times the constant, but with the size of the set replaced by the number of elements satisfying the predicate `p`.
More concisely: For any type `α`, additive commutative monoid `β`, finite set `s` of `α`, decidable predicate `p` on `α`, if for all `i`, `j` in `s` with `i ≠ j` imply `¬p i ∨ ¬p j`, then the sum of the function `a ↦ if p i then a else 0 over `s` equals `a` if there exists `i` in `s` with `p i`, and 0 otherwise.
|
Finset.sum_cons
theorem Finset.sum_cons :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [inst : AddCommMonoid β] (h : a ∉ s),
((Finset.cons a s h).sum fun x => f x) = f a + s.sum fun x => f x
The theorem `Finset.sum_cons` states that for any types `α` and `β`, a finite set `s` of type `α`, an element `a` of type `α`, a function `f` from `α` to `β`, and an additive commutative monoid instance on `β`, if `a` is not an element of `s`, then the sum of the function `f` applied to each element of the set formed by adding `a` to `s` (`Finset.cons a s h`) is equal to the sum of `f` applied to `a` plus the sum of `f` applied to each element of `s`. In other words, the sum over the set `{a} ∪ s` is the same as `f(a)` plus the sum over the set `s`. This is an expression of the distributive property of addition over a finite set.
More concisely: For any additive commutative monoid `β` and function `f` from a finite set `s` of type `α` to `β`, along with an element `a` not in `s`, the sum of `f` applied to `a` and the sum of `f` applied to `s` is equal to the sum of `f` applied to the set `{a} ∪ s`.
|
Finset.sum_nbij'
theorem Finset.sum_nbij' :
∀ {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [inst : AddCommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α}
{g : κ → α} (i : ι → κ) (j : κ → ι),
(∀ a ∈ s, i a ∈ t) →
(∀ a ∈ t, j a ∈ s) →
(∀ a ∈ s, j (i a) = a) →
(∀ a ∈ t, i (j a) = a) → (∀ a ∈ s, f a = g (i a)) → (s.sum fun x => f x) = t.sum fun x => g x
This theorem, named `Finset.sum_nbij'`, states that for any two finite sets `s` and `t`, each element of `s` and `t` are associated with a function `f: ι → α` and `g: κ → α`, respectively, where `ι` and `κ` are the types of elements in `s` and `t` respectively, and `α` is a set equipped with an addition and a zero element (an additive commutative monoid). If there exist two functions `i: ι → κ` and `j: κ → ι` such that `i` maps each element of `s` into `t`, `j` maps each element of `t` into `s`, the composition of `j` and `i` is the identity on `s`, the composition of `i` and `j` is the identity on `t`, and `f` and `g ∘ i` are equal on `s`, then the sum of the values of `f` over `s` equals the sum of the values of `g` over `t`.
This theorem is a variant of other similar theorems about reordering the sum over a finite set, with the key difference being the specific way in which the bijection between the sets is specified and the requirements for the bijection's properties.
More concisely: If two finite sets `s` and `t` have a bijection `i: s ≃ t` such that the functions `f: s → α` and `g: t → α` satisfy `f = g ∘ i` and the bijection properties hold, then `∑ x in s, f x = ∑ y in t, g y`.
|
Finset.sum_subtype_map_embedding
theorem Finset.sum_subtype_map_embedding :
∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] {p : α → Prop} {s : Finset { x // p x }}
{f : { x // p x } → β} {g : α → β},
(∀ x ∈ s, g ↑x = f x) →
((Finset.map (Function.Embedding.subtype fun x => p x) s).sum fun x => g x) = s.sum fun x => f x
This theorem states that for any types `α` and `β` with `β` being an additive commutative monoid, a predicate `p` on `α`, a finite set `s` of elements of `α` satisfying `p`, and two functions `f` and `g` from the subtype and the main type to `β` respectively, if the function `g` applied to the elements of `s` is equal to the function `f` applied to those elements, then the sum of `g` applied to the elements of `s` when viewed in the main type via embedding is equal to the sum of `f` applied to the elements of `s` in the subtype. In more informal terms, it says that the sum over a finset doesn't change if you pass from a subset to the main set via an embedding, provided the functions agree on the subset.
More concisely: For any additive commutative monoid `β`, type `α`, predicate `p` on `α`, finite set `s` of `α` satisfying `p`, and functions `f : s → β` and `g : {x : α | p x} → β`, if `∑i in s, f i = ∑i in s, g i`, then `∑i in s, g i = ∑x in {x : α | p x}, g x`.
|
Finset.prod_eq_mul_prod_diff_singleton
theorem Finset.prod_eq_mul_prod_diff_singleton :
∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] [inst_1 : DecidableEq α] {s : Finset α} {i : α},
i ∈ s → ∀ (f : α → β), (s.prod fun x => f x) = f i * (s \ {i}).prod fun x => f x
This theorem states that for any type `α`, and a commutative monoid `β`, given a function `f` from `α` to `β` and a finite set `s` of type `α` with decidable equality, if an element `i` belongs to `s`, then the product of `f(x)` for each `x` in the set `s` is equal to `f(i)` times the product of `f(x)` for each `x` in the set `s` excluding `i`. In mathematical terms, it's asserting that $\prod_{x \in s} f(x) = f(i) * \prod_{x \in s \setminus \{i\}} f(x)$.
More concisely: For any commutative monoid `β`, given a function `f` from type `α` to `β`, and a finite set `s` of type `α` with decidable equality, the product of `f(x)` for all `x` in `s` equals `f(i)` times the product of `f(x)` for all `x` in `s` except `i`. In symbolic form: $\prod\_{x \in s} f(x) = f(i) * \prod\_{x \in s \setminus \{i\}} f(x)$.
|
Finset.card_eq_sum_ones
theorem Finset.card_eq_sum_ones : ∀ {α : Type u_3} (s : Finset α), s.card = s.sum fun x => 1
The theorem `Finset.card_eq_sum_ones` states that for any finite set `s` of type `α`, the cardinality of `s` (i.e., the number of elements in `s`) is equal to the sum of `1` for each element in `s`. In other words, if you were to take each element in the finite set `s` and map it to the number `1`, then add up all those ones, you would get the same count as the total number of elements in the set `s`.
More concisely: For any finite set `s` of type `α`, the cardinality of `s` equals the sum of ones over its elements.
|
Finset.sum_insert_zero
theorem Finset.sum_insert_zero :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [inst : AddCommMonoid β]
[inst_1 : DecidableEq α], f a = 0 → ((insert a s).sum fun x => f x) = s.sum fun x => f x
The theorem `Finset.sum_insert_zero` states that for any types `α` and `β`, any finite set `s` of type `α`, any element `a` of type `α`, and any function `f` from `α` to `β`, given that `β` has an additive commutative monoid structure and `α` has decidable equality, if the function `f` evaluated at `a` is zero, then the sum of `f` over the set obtained by inserting `a` into `s` is the same as the sum of `f` over `s`. In other words, if `f(a) = 0`, then adding `a` to the set does not change the total sum when `f` is applied to every element of the set and the results are added together.
More concisely: If `f` is a function from a finite set `s` to an additive commutative monoid with neutral element `0`, and `a` is an element of the set such that `f(a) = 0`, then the sum of `f` over `s` is equal to the sum of `f` over `s ∪ {a}`.
|
Finset.prod_map
theorem Finset.prod_map :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : CommMonoid β] (s : Finset α) (e : α ↪ γ) (f : γ → β),
((Finset.map e s).prod fun x => f x) = s.prod fun x => f (e x)
This theorem, `Finset.prod_map`, states that for any type `α`, `β`, and `γ`, with `β` being a commutative monoid, given a finite set `s` of type `α`, an embedding `e` from `α` to `γ`, and a function `f` from `γ` to `β`, the product of `f x` for every `x` in the image set `Finset.map e s` (that is, the set obtained by applying the embedding `e` to each element of `s`) is equal to the product of `f (e x)` for every `x` in the original set `s`. In other words, it's asserting that mapping a function over a set and then taking the product is the same as first applying the map to each element and then taking the product, for a specific map that is an embedding. This is an instance of a very general principle in mathematics, often referred to as changing the order of operations, or more formally, as the interchange of limit processes.
More concisely: For any commutative monoid β, finite set s of type α, embedding e from α to γ, and function f from γ to β, the product of f (e x) for each x in s equals the product of f (e (s.map x)).
|
Finset.prod_const
theorem Finset.prod_const :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} [inst : CommMonoid β] (b : β), (s.prod fun _x => b) = b ^ s.card
The theorem `Finset.prod_const` states that for any finite set `s` of a certain type `α`, and for any element `b` of a type `β` that forms a commutative monoid, the product of the constant function `b` as `x` ranges over all the elements of the set `s` equals `b` to the power of the size of the set `s`. In mathematical terms, this is expressing that the product over a set of a constant equals that constant raised to the size of the set: $\prod_{x \in s} b = b^{|s|}$ where |s| denotes the size or cardinality of the set `s`.
More concisely: For any finite set `s` and commutative monoid element `b`, the product of `b` over `s` equals `b` raised to the power of `s`'s size: `∏(x : s) b = b^( card s)`.
|
Finset.prod_insert_one
theorem Finset.prod_insert_one :
∀ {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [inst : CommMonoid β] [inst_1 : DecidableEq α],
f a = 1 → ((insert a s).prod fun x => f x) = s.prod fun x => f x
This theorem states that for any given types `α` and `β`, a finite set `s` of type `α`, an element `a` of type `α`, and a function `f` from `α` to `β`, if the structure `β` is a commutative monoid and the equality in `α` is decidable, then if the function `f` evaluated at `a` equals the identity element of the monoid `β`, the product of `f` over the set obtained by inserting `a` into `s` is the same as the product of `f` over `s`. In other words, inserting an element into the set that maps to the identity of the monoid does not change the overall product.
More concisely: For any commutative monoid β with decidable equality, function f : α → β, finite set s ⊆ α, and element a ∈ α such that f(a) = id\_β (the identity element of β), the product of f over s with a added (f(s) * f(a)) is equal to the product of f over just s (f(s)).
|
Finset.eq_one_of_prod_eq_one
theorem Finset.eq_one_of_prod_eq_one :
∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] {s : Finset α} {f : α → β} {a : α},
(s.prod fun x => f x) = 1 → (∀ x ∈ s, x ≠ a → f x = 1) → ∀ x ∈ s, f x = 1
This theorem states that given a function `f` from an arbitrary type `α` to a commutative monoid `β`, and a finite set `s` of elements from `α`; if the product of the function values (when applied to each element in the set) equals one and the function yields one for every element in the set except possibly one element `a`, then the function actually yields one for every element in the set.
More concisely: If `f` is a function from type `α` to commutative monoid `β`, `s ⊆ α` is finite, and the product of `f` applied to `s` equals one and `f(a)` may not be one for some `a ∈ s`, then `f(x) = 1` for all `x ∈ s`.
|
Finset.prod_comm
theorem Finset.prod_comm :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : CommMonoid β] {s : Finset γ} {t : Finset α} {f : γ → α → β},
(s.prod fun x => t.prod fun y => f x y) = t.prod fun y => s.prod fun x => f x y
The theorem `Finset.prod_comm` states that for all types `α`, `β`, and `γ`, given a commutative monoid over `β`, and given finite sets `s` of type `γ` and `t` of type `α`, and a function `f` that maps each pair of elements from `s` and `t` to `β`, the product over `s` of the function which itself is the product over `t` of `f`, is equal to the product over `t` of the function which itself is the product over `s` of `f`. In other words, the order of taking product over two finite sets does not affect the result, which mirrors the commutative property of multiplication in mathematics.
More concisely: For all commutative monoids over type `β`, and finite sets `s` of type `γ` and `t` of type `α`, the function `f` mapping pairs of elements from `s` and `t` to `β` satisfies `∏(s, f ∘ ∏(t, f)) = ∏(t, f ∘ ∏(s, f))`.
|
Finset.sum_nbij
theorem Finset.sum_nbij :
∀ {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [inst : AddCommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α}
{g : κ → α} (i : ι → κ),
(∀ a ∈ s, i a ∈ t) →
Set.InjOn i ↑s → Set.SurjOn i ↑s ↑t → (∀ a ∈ s, f a = g (i a)) → (s.sum fun x => f x) = t.sum fun x => g x
The theorem `Finset.sum_nbij` states that if we have two finite sets `s` and `t`, and a function `i` from elements of `s` to elements of `t` such that `i` is injective when restricted to `s` (meaning no two distinct elements in `s` are mapped to the same element in `t`), and surjective from `s` to `t` (meaning every element of `t` is the image of some element in `s`), and for any element `a` in `s`, the function `f` at `a` equals the function `g` at `i(a)`, then the sum of `f` over all elements of `s` equals the sum of `g` over all elements of `t`.
In simpler terms, this theorem allows us to "reorder" a sum over a finite set by establishing a bijection (a one-to-one correspondence) between the elements of the original set and the elements of the new set, and adjusting the function being summed accordingly.
More concisely: If two finite sets have an injective and surjective function between them, with corresponding elements having equal images under the functions, then the sum of the functions is equal.
|
Finset.sum_product'
theorem Finset.sum_product' :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : AddCommMonoid β] {s : Finset γ} {t : Finset α}
{f : γ → α → β}, ((s ×ˢ t).sum fun x => f x.1 x.2) = s.sum fun x => t.sum fun y => f x y
The theorem `Finset.sum_product'` states that for all types `α`, `β`, and `γ`, given an additive commutative monoid `β`, a finite set `s` of type `γ`, a finite set `t` of type `α`, and a function `f` from `γ` and `α` to `β`, the sum of the function `f` applied to each element in the product set of `s` and `t` (i.e., all combinations of elements from `s` and `t`), is equal to the sum of the function `f` applied to each element in `s` and each element in `t`. In mathematical terms, it asserts that summing over the product set is the same as summing over each set individually, i.e., $\sum_{(x,y) \in s \times t} f(x,y) = \sum_{x \in s} \sum_{y \in t} f(x,y)$. This is an instance of the distributive property of summation over set products.
More concisely: The theorem asserts that for an additive commutative monoid β, the sum of a function applied to all combinations of elements from two finite sets and the function applied to each element in one set and then summed over the other set, are equal. In other words, $\sum_{(x,y) \in s \times t} f(x,y) = \sum_{x \in s} \sum_{y \in t} f(x,y)$.
|