Finset.prod_sub_ordered
theorem Finset.prod_sub_ordered :
∀ {ι : Type u_1} {α : Type u_2} [inst : CommRing α] [inst_1 : LinearOrder ι] (s : Finset ι) (f g : ι → α),
(s.prod fun i => f i - g i) =
(s.prod fun i => f i) -
s.sum fun i =>
(g i * (Finset.filter (fun x => x < i) s).prod fun j => f j - g j) *
(Finset.filter (fun j => i < j) s).prod fun j => f j
This theorem, `Finset.prod_sub_ordered`, establishes a relation between function differences and certain operations on a finite set `s` of a specific type `ι`. For any two functions `f` and `g` mapping from `ι` to a commutative ring `α`, the product of the difference of `f` and `g` over all elements in `s` is equal to the difference between the product of `f` over all elements in `s` and a certain sum. This sum is over all elements `i` in `s` of `g(i)` times the product of the difference of `f` and `g` over all elements `j` in `s` less than `i`, times the product of function `f` over all elements `j` in `s` that are larger than `i`.
More concisely: For any finite set `s` and commutative ring `α`, the product of the difference between functions `f` and `g` over `s` equals the difference between the product of `f` over `s` and the sum over `i` in `s`, of `g(i)` times the product of `f` over indices `j` in `s` less than `i`, and the product of `f` over indices `j` in `s` greater than `i`.
|
Finset.prod_add
theorem Finset.prod_add :
∀ {ι : Type u_1} {α : Type u_2} [inst : CommSemiring α] [inst_1 : DecidableEq ι] (f g : ι → α) (s : Finset ι),
(s.prod fun i => f i + g i) = s.powerset.sum fun t => (t.prod fun i => f i) * (s \ t).prod fun i => g i
The theorem `Finset.prod_add` states that for any given type `ι`, another type `α` which is a commutative semiring, and a function `f` and `g` that map elements of type `ι` to `α`, and a finite set `s` of elements of type `ι`, the product of the sum of `f a` and `g a` over all elements `a` in `s` equals the sum, over the powerset of `s`, of the product of `f` over a subset `t` times the product of `g` over the set difference of `s` and `t`. This is basically an algebraic relationship involving sums, products, subsets, and set differences.
More concisely: For any commutative semiring `α`, function `f : ι -> α`, function `g : ι -> α`, and finite set `s : Finset ι`, the sum of the products of `f` and `g` over `s` equals the sum of the products of `f` over subsets of `s` and the products of `g` over the complements of those subsets.
|
Finset.prod_sum
theorem Finset.prod_sum :
∀ {ι : Type u_1} {α : Type u_2} {κ : ι → Type u_5} [inst : CommSemiring α] [inst_1 : DecidableEq ι] (s : Finset ι)
(t : (i : ι) → Finset (κ i)) (f : (i : ι) → κ i → α),
(s.prod fun a => (t a).sum fun b => f a b) = (s.pi t).sum fun p => s.attach.prod fun x => f (↑x) (p ↑x ⋯)
This theorem, `Finset.prod_sum`, states that for any type `ι`, any commutative semiring `α`, any type `κ` dependent on `ι`, any finite set `s` of `ι`, a function `t` mapping each element of `ι` to a finite set of `κ i`, and a function `f` mapping each `ι` and `κ i` to an element of `α`, the product of the sums (over each `κ i` set) of `f a b` for each `a` in `s` is equal to the sum (over all possible functions `p` from `ι` to `κ i` for each `i` in `s`) of the product of `f (↑x) (p ↑x)` for each `x` in `s`. This is essentially a statement of distributivity for finite sums and products, adapted to the type-theoretic setting.
More concisely: For any commutative semiring `α`, given a type `ι`, a finite set `s` of `ι`, functions `t` mapping each element of `ι` to a finite set of `κ i`, and `f` mapping each pair of `ι` and `κ i` to an element of `α`, the sum of the products of `f` over each `κ i` set in `s` equals the product of the sums of `f` over each `ι` in `s`.
|
Finset.sum_mul
theorem Finset.sum_mul :
∀ {ι : Type u_1} {α : Type u_2} [inst : NonUnitalNonAssocSemiring α] (s : Finset ι) (f : ι → α) (a : α),
(s.sum fun i => f i) * a = s.sum fun i => f i * a
The theorem `Finset.sum_mul` states that for any finite set `s` of a general type `ι`, any function `f` from `ι` to a type `α` equipped with a structure of `NonUnitalNonAssocSemiring` (a mathematical structure similar to the real numbers without the assumption that multiplication is associative and without a multiplicative identity element), and any element `a` of this type, the sum of the values of `f` over `s`, when multiplied by `a`, equals the sum over `s` of the products of `f` evaluated at each element of `s` and `a`. In mathematical terms, it says that for any set `s`, function `f` and scalar `a`, we have the equality $(\sum_{i \in s} f(i)) * a = \sum_{i \in s} (f(i) * a)$.
More concisely: For any finite set $s$, function $f$ from $s$ to a non-unital non-associative semiring, and scalar $a$ in the semiring, we have $\sum\_{i \in s} f(i) \cdot a = a \cdot \sum\_{i \in s} f(i)$.
|
Nat.cast_sum
theorem Nat.cast_sum :
∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoidWithOne β] (s : Finset α) (f : α → ℕ),
↑(s.sum fun x => f x) = s.sum fun x => ↑(f x)
This theorem states that for any finite set `s` of elements from an arbitrary type `α` and a function `f` that maps elements from `α` to the natural numbers (`ℕ`), the natural number cast (`↑`) of the sum of `f(x)` over all elements `x` in `s` is equal to the sum of the natural number cast of `f(x)` over all elements `x` in `s`. In other words, summing the values of `f(x)` and then applying the cast operation is the same as applying the cast operation to each `f(x)` and then summing. This theorem is applicable under the assumption that the type `β` forms an additive commutative monoid with a distinct one element.
More concisely: For any finite set `s` from type `α` and additive commutative monoid `ℙ` with identity element, the sum of the natural number casts of the function values `f(x)` over all `x` in `s` equals the natural number cast of the sum of `f(x)` over all `x` in `s`.
|
Nat.cast_prod
theorem Nat.cast_prod :
∀ {α : Type u_2} {β : Type u_3} [inst : CommSemiring β] (f : α → ℕ) (s : Finset α),
↑(s.prod fun i => f i) = s.prod fun i => ↑(f i)
The theorem `Nat.cast_prod` states that for any commutative semiring `β`, any function `f` from a type `α` to the natural numbers, and any finite set `s` of elements of type `α`, the natural number cast of the product of `f x` as `x` ranges over the set `s` is equal to the product of the natural number casts of `f x` as `x` ranges over the set `s`. In other words, casting the product of a sequence of natural numbers to a commutative semiring is the same as taking the product of the casts of the individual elements of the sequence. This theorem is a formal statement of the fact that the operation of taking products commutes with the operation of casting from natural numbers to a commutative semiring.
More concisely: For any commutative semiring β and function f from type α to natural numbers, the cast of the product of f x as x ranges over a finite set s equals the product of the casts of f x as x ranges over s.
|
Finset.sum_div
theorem Finset.sum_div :
∀ {ι : Type u_1} {α : Type u_2} [inst : DivisionSemiring α] (s : Finset ι) (f : ι → α) (a : α),
(s.sum fun i => f i) / a = s.sum fun i => f i / a
The theorem `Finset.sum_div` states that for any set `s` of elements of type `ι`, any function `f` from `ι` to a type `α` that has a division semiring structure, and any value `a` of type `α`, the division of the sum of `f x` over all elements `x` in `s` by `a` is equal to the sum over `s` of the division of `f x` by `a`. In mathematical notation, it's saying that $\frac{\sum_{x\in s} f(x)}{a} = \sum_{x\in s} \frac{f(x)}{a}$.
More concisely: For any set `s`, function `f` from `s` to a division semiring with identity element `a`, the sum of `f x / a` over all `x` in `s` is equal to the division of the sum of `f x` by `a`.
|
Int.cast_sum
theorem Int.cast_sum :
∀ {α : Type u_2} {β : Type u_3} [inst : AddCommGroupWithOne β] (s : Finset α) (f : α → ℤ),
↑(s.sum fun x => f x) = s.sum fun x => ↑(f x)
The theorem `Int.cast_sum` states that for any finite set `s` of elements of type `α` and any function `f` from `α` to integers, the cast of the sum of `f(x)` for all `x` in `s` to a type `β` (where `β` is an additive commutative group with unity) is equal to the sum of the cast of `f(x)` for all `x` in `s`. In other words, casting can be interchanged with summing over a finite set.
More concisely: For any finite set `s` and function `f` from a commutative additive group with unity to another such group, the cast of the sum of `f(x)` for all `x` in `s` is equal to the sum of the casts of `f(x)` for all `x` in `s`.
|
Finset.prod_one_sub_ordered
theorem Finset.prod_one_sub_ordered :
∀ {ι : Type u_1} {α : Type u_2} [inst : CommRing α] [inst_1 : LinearOrder ι] (s : Finset ι) (f : ι → α),
(s.prod fun i => 1 - f i) = 1 - s.sum fun i => f i * (Finset.filter (fun x => x < i) s).prod fun j => 1 - f j
This theorem states that for any commutative ring `α` and any linearly ordered type `ι`, given a finite set `s` of type `ι` and a function `f` from `ι` to `α`, the product of `(1 - f i)` for all `i` in `s` is equal to `1` subtracted by the sum of `f i` times the product of `(1 - f j)` for all `j` in `s` that are less than `i`. This formula is particularly useful in the construction of a partition of unity from a collection of "bump" functions.
More concisely: For any commutative ring `α` and linearly ordered type `ι`, the product of `(1 - f i)` for all `i` in a finite subset `s` of `ι` equals `1 - sum (i in s) (f i * product (j in s) [j < i] (1 - f j))`.
|
Finset.prod_add_ordered
theorem Finset.prod_add_ordered :
∀ {ι : Type u_1} {α : Type u_2} [inst : LinearOrder ι] [inst_1 : CommSemiring α] (s : Finset ι) (f g : ι → α),
(s.prod fun i => f i + g i) =
(s.prod fun i => f i) +
s.sum fun i =>
(g i * (Finset.filter (fun x => x < i) s).prod fun j => f j + g j) *
(Finset.filter (fun j => i < j) s).prod fun j => f j
This theorem states that for a given set "s" of elements of a certain type "ι" (where "ι" has a linear order) and for two functions "f" and "g" from "ι" to a type "α" (where "α" is a commutative semiring), the product of the elements of "s" under the function "(f i + g i)" is equal to the sum of: the product of the function "f i" over the same set "s" and the sum over "s" of each "g i" multiplied by the product of "(f j + g j)" for "j" less than "i" and the product of "f j" for "j" greater than "i". In mathematical terms, this can be expressed as
`∏ i, (f i + g i) = (∏ i, f i) + ∑ i, g i * (∏ j < i, f j + g j) * (∏ j > i, f j)`.
More concisely: The product of the function `f i + g i` over a set `s` of elements from a linearly ordered type `ι`, where `f` and `g` map `ι` to a commutative semiring `α`, equals the sum of the product of `f i` over `s` and the sum over `s` of `g i` multiplied by the product of `f j` for `j` less than `i` and `f j` for `j` greater than `i`. In mathematical notation: `∏ i, (f i + g i) = (∏ i, f i) + ∑ i, g i * (∏ j < i, f j) * (∏ j > i, f j)`.
|
Finset.mul_sum
theorem Finset.mul_sum :
∀ {ι : Type u_1} {α : Type u_2} [inst : NonUnitalNonAssocSemiring α] (s : Finset ι) (f : ι → α) (a : α),
(a * s.sum fun i => f i) = s.sum fun i => a * f i
The theorem `Finset.mul_sum` states that for any index type `ι`, any type `α` which forms a `NonUnitalNonAssocSemiring` (a type of algebraic structure with addition and multiplication operations), any finite set `s` of type `ι`, any function `f` from `ι` to `α`, and any value `a` of type `α`, the operation of multiplying `a` with the sum of the values of `f` over all elements in `s` is the same as first multiplying `a` with each value of `f(i)` for each `i` in `s` and then taking the sum of all these products. In mathematical terms, this means that `a * Σ(f(i) for i in s) = Σ(a * f(i) for i in s)`. This theorem is essentially a version of the distributive law for sums over finite sets in a non-unital, non-associative semiring.
More concisely: For any non-unital, non-associative semiring `α`, finite set `s` of index type `ι`, function `f` from `ι` to `α`, and value `a` of type `α`, we have `a * Σ(f(i): ι → α | i ∈ s) = Σ(a * f(i) | i ∈ s)`.
|
Finset.prod_add_prod_eq
theorem Finset.prod_add_prod_eq :
∀ {ι : Type u_1} {α : Type u_2} [inst : CommSemiring α] {s : Finset ι} {i : ι} {f g h : ι → α},
i ∈ s →
g i + h i = f i →
(∀ j ∈ s, j ≠ i → g j = f j) →
(∀ j ∈ s, j ≠ i → h j = f j) → ((s.prod fun i => g i) + s.prod fun i => h i) = s.prod fun i => f i
This theorem states that if you have three functions `f`, `g`, and `h` mapping from a type `ι` to a type `α` (where `α` is a commutative semiring), and a finite set `s` of `ι` including an element `i`, then if `f` equals both `g` and `h` everywhere in `s` except at `i`, where `f` at `i` equals the sum of `g` at `i` and `h` at `i`, then the total product of `f` over `s` is equal to the sum of the total products of `g` and `h` over `s`. In mathematical terms, if $\forall j \in s, j \neq i \Rightarrow f(j) = g(j) = h(j)$ and $f(i) = g(i) + h(i)$, then $\prod_{j \in s} g(j) + \prod_{j \in s} h(j) = \prod_{j \in s} f(j)$.
More concisely: If functions `f`, `g`, and `h` from a commutative semiring `ι` to a commutative semiring `α`, map `ι` to `α`, and `g(i) + h(i) = f(i)` for some `i` in a finite set `s` containing `i`, where `f`, `g`, and `h` agree on `s \ {i}`, then the total product of `g` and `h` over `s` equals the total product of `f` over `s`.
|
Finset.sum_boole
theorem Finset.sum_boole :
∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoidWithOne α] (p : ι → Prop) [inst_1 : DecidablePred p]
(s : Finset ι), (s.sum fun x => if p x then 1 else 0) = ↑(Finset.filter p s).card
The theorem `Finset.sum_boole` states that for any finite set `s` of elements of an arbitrary type `α` and a decidable predicate `p` on `α`, and given the type `β` is an additive commutative monoid with one, the sum over `s` of the function which returns 1 if `p x` holds and 0 otherwise is equal to the cardinality of the subset of `s` for which `p x` holds. In other words, it's calculating the count of elements in the set `s` that satisfy the predicate `p` by summing up 1 for each element that satisfy `p`.
More concisely: For any finite set `s` of elements from a type `α` and a decidable predicate `p` on `α`, the sum of 1 for each element in `s` for which `p` holds equals the cardinality of the subset of `s` satisfying `p`.
|
Finset.prod_univ_sum
theorem Finset.prod_univ_sum :
∀ {ι : Type u_1} {α : Type u_2} {κ : ι → Type u_5} [inst : CommSemiring α] [inst_1 : DecidableEq ι]
[inst_2 : Fintype ι] (t : (i : ι) → Finset (κ i)) (f : (i : ι) → κ i → α),
(Finset.univ.prod fun i => (t i).sum fun j => f i j) =
(Fintype.piFinset t).sum fun x => Finset.univ.prod fun i => f i (x i)
This theorem, `Finset.prod_univ_sum`, states that for every type `ι` (represented as a set), a type `α` (which forms a commutative semiring), and a function `κ` that maps each element of `ι` to a type, given the conditions that equality in `ι` is decidable and `ι` is finite, we can define a function `t` mapping each element of `ι` to a finite set of the corresponding type `κ i`, and another function `f` that maps each element `ι` and its corresponding `κ i` to an element of `α`. The theorem then asserts that the product (using the commutative semiring operation) over all elements of `ι` of the sums (using the addition of the commutative semiring) computed by `f` over each finite set `t i` is equal to the sum over all functions `x` from `ι` to the union of the sets `t i`, of the product over all elements of `ι` of `f i` evaluated at `x i`. This theorem essentially reflects the principle of distributing a product over a sum, but in the context of finite sets and functions as described.
More concisely: For every commutative semiring `α`, set `ι` (with decidable equality and finite elements), functions `κ : ι → Type`, `t : ι → Set α`, and `f : ι × κ → α`, the product of the sums of `f` over `t i` equals the sum of the products of `f` over all functions from `ι` to the union of the `t i`.
|
Finset.sum_pow_mul_eq_add_pow
theorem Finset.sum_pow_mul_eq_add_pow :
∀ {ι : Type u_1} {α : Type u_2} [inst : CommSemiring α] (a b : α) (s : Finset ι),
(s.powerset.sum fun t => a ^ t.card * b ^ (s.card - t.card)) = (a + b) ^ s.card
This theorem states that for any given set `s` in a finite set (or `Finset`), the sum of `a` to the power of the cardinality of subset `t` of set `s` times `b` to the power of the difference between the cardinality of set `s` and the cardinality of subset `t`, over all possible finite subsets `t` of the set `s`, equals `(a + b)` to the power of the cardinality of set `s`. This is true for any types `ι` and `α`, where `α` is a commutative semiring. In mathematical notation, it asserts that $\sum_{t \subseteq s} a^{|t|} \cdot b^{|s|-|t|} = (a+b)^{|s|}$.
More concisely: For any finite set `s` and commutative semiring elements `a` and `b`, the sum of the product of `a` raised to the power of the cardinality of each subset `t` of `s` and `b` raised to the power of the complementary cardinality, over all subsets `t` of `s`, equals `(a + b)` raised to the power of the cardinality of `s`.
|
Fintype.sum_pow_mul_eq_add_pow
theorem Fintype.sum_pow_mul_eq_add_pow :
∀ {α : Type u_2} [inst : CommSemiring α] (ι : Type u_6) [inst_1 : Fintype ι] (a b : α),
(Finset.univ.sum fun s => a ^ s.card * b ^ (Fintype.card ι - s.card)) = (a + b) ^ Fintype.card ι
The theorem `Fintype.sum_pow_mul_eq_add_pow` states that for any commutative semiring `α` and any finite type `ι`, the sum of `a^s.card * b^(n-s.card)` over all finite subsets `s` of `ι` equals `(a + b)^n`, where `n` is the cardinality of `ι`. Here, `a` and `b` are elements of the semiring `α`, `s.card` denotes the number of elements in `s`, and `Fintype.card ι` represents the number of elements in `ι`. The conventional proof of this theorem would involve expanding along all coordinates using the property of multilinearity of `x^n`, but since multilinear maps are currently only available over rings, an alternative proof is given that reduces the theorem to the usual binomial theorem for semirings.
More concisely: For any commutative semiring `α` and finite type `ι`, the sum of `a^(Card ι) * b^(Card ι - Card s)` over all finite subsets `s` of `ι` equals `(a + b)^(Card ι)`.
|