finprod_mem_mul_distrib
theorem finprod_mem_mul_distrib :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f g : α → M} {s : Set α},
s.Finite →
(finprod fun i => finprod fun h => f i * g i) =
(finprod fun i => finprod fun h => f i) * finprod fun i => finprod fun h => g i
The theorem `finprod_mem_mul_distrib` states that for any given finite set `s` of type `α`, and functions `f` and `g` mapping from `α` to `M` where `M` is a type with a commutative monoid structure, the product of the function values `f(i) * g(i)` for each `i` in set `s` is equal to the product of the function values `f(i)` times the product of the function values `g(i)` for all `i` in set `s`. In other words, the product over a finite set distributes over the multiplication of functions.
More concisely: For any finite set `S` and functions `f` and `g` from `S` to a commutative monoid `M`, the product of `f(i) * g(i)` for all `i` in `S` equals the product of `f(i)` and the product of `g(i)` for all `i` in `S`. In other words, the function product distributes over the set product.
|
finsum_induction
theorem finsum_induction :
∀ {M : Type u_2} {α : Sort u_4} [inst : AddCommMonoid M] {f : α → M} (p : M → Prop),
p 0 → (∀ (x y : M), p x → p y → p (x + y)) → (∀ (i : α), p (f i)) → p (finsum fun i => f i)
This theorem, named `finsum_induction`, states that in order to prove a property `p` about a finite sum, we need to show three things:
1. The property `p` holds for the number zero.
2. The property `p` is preserved under addition, i.e., if `p` holds for two numbers `x` and `y`, then it also holds for their sum `x + y`.
3. The property `p` holds for all the terms of the sum (i.e., for all `f i` where `i` is an element from the set `α`).
If these three conditions are met, then the property `p` holds for the entire finite sum. In other words, `p (finsum fun i => f i)` is true. Here, `finsum` is a function that computes the sum of `f x` as `x` ranges over the elements of the support of `f`, if it's finite. Otherwise, it returns zero.
More concisely: The theorem `finsum_induction` asserts that a property `p` holds for a finite sum `finsum (fun i => f i)` if it holds for the sum of all terms `f i` when `i` ranges over a finite set `α`, and for the number zero, and is preserved under addition.
|
finprod_mem_singleton
theorem finprod_mem_singleton :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {a : α},
(finprod fun i => finprod fun h => f i) = f a
The theorem `finprod_mem_singleton` states that for any given types `α` and `M`, where `M` is a commutative monoid, and for any function `f` mapping from `α` to `M`, the product of `f i` over the singleton set `{a}` equals `f a`. In other words, when you apply the `finprod` operation over a singleton set, you essentially get the function value at that single element.
More concisely: For any commutative monoid M and function f from type α to M, the product of f over the singleton set {a} equals f a.
|
nonempty_of_finsum_mem_ne_zero
theorem nonempty_of_finsum_mem_ne_zero :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s : Set α},
(finsum fun i => finsum fun h => f i) ≠ 0 → s.Nonempty
The theorem `nonempty_of_finsum_mem_ne_zero` states that for any types `α` and `M`, where `M` is an additive commutative monoid, and any function `f` from `α` to `M`, if the two-fold finite sum of `f` over some index set is not equal to zero, then the set `s` of elements in `α` is nonempty. Here, the two-fold finite sum refers to the sum of `f i` for every element `i` in the support of `f`, and this sum is taken twice. If this double sum is not zero, then the set `s` must contain at least one element.
More concisely: If `f` is a function from a nonempty set `α` to an additive commutative monoid `M`, and the two-fold finite sum of `f` over `α` is not zero, then `α` is nonempty.
|
finsum_add_distrib
theorem finsum_add_distrib :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f g : α → M},
(Function.support f).Finite →
(Function.support g).Finite → (finsum fun i => f i + g i) = (finsum fun i => f i) + finsum fun i => g i
This theorem states that for any given types `α` and `M`, with `M` being an additive commutative monoid, and any two functions `f` and `g` from `α` to `M`, if both the additive supports of `f` and `g` are finite, then the total sum over all `i` of `f(i) + g(i)` is equal to the sum of `f(i)` for all `i` added to the sum of `g(i)` for all `i`. In other words, the sum of the combined function `f + g` over its finite support is equal to the sum of `f` over its finite support added to the sum of `g` over its finite support. This is analogous to the distributive property in arithmetic.
More concisely: For additive commutative monoids M and functions f and g from type α to M with finite additive supports, the sum of (f + g) over their supports equals the sum of f over the supports plus the sum of g over the supports.
|
finsum_congr_Prop
theorem finsum_congr_Prop :
∀ {M : Type u_2} [inst : AddCommMonoid M] {p q : Prop} {f : p → M} {g : q → M} (hpq : p = q),
(∀ (h : q), f ⋯ = g h) → finsum f = finsum g
This theorem, `finsum_congr_Prop`, states that for any type `M` that is equipped with an additive commutative monoid structure, for any two propositions `p` and `q`, and for any functions `f : p → M` and `g : q → M`, if `p` is equal to `q` and for every element `h` of `q`, `f` applied to a certain argument (which depends on `h`) is equal to `g h`, then the sum of `f x` over all `x` in the support of `f` (as defined by `finsum`) is equal to the sum of `g x` over all `x` in the support of `g`. This theorem essentially states that under these conditions, the finitary sums of `f` and `g` are equal.
More concisely: For any additive commutative monoid-structured type M and propositions p and q, if the functions f from p to M and g from q to M satisfy p = q and ∀h ∈ q, f(x h) = g h for some x, then ∑x ∈ supp(f) f x = ∑x ∈ supp(g) g x.
|
finprod_eq_of_bijective
theorem finprod_eq_of_bijective :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {g : β → M} (e : α → β),
Function.Bijective e → (∀ (x : α), f x = g (e x)) → (finprod fun i => f i) = finprod fun j => g j
This theorem states that for any types `α`, `β`, and `M` where `M` is a commutative monoid, if `f` is a function from `α` to `M` and `g` is a function from `β` to `M`, and `e` is a bijective function from `α` to `β`, then if for all `x` in `α`, `f(x)` is equal to `g(e(x))`, the product of `f` over its finite multiplicative support is equal to the product of `g` over its finite multiplicative support. This essentially says that under these conditions, changing the elements of the domain using a bijective function doesn't change the product over the multiplicative support of the function.
More concisely: If `f : α → M` and `g : β → M` are commutative monoid homomorphisms with the same finite multiplicative support, and `e : α ≃ β` is a bijective function such that `f(x) = g(e(x))` for all `x` in `α`, then `∏_{i ∈ I} f(a\_i) = ∏_{i ∈ I} g(b\_i)`, where `{a\_i : α | i ∈ I}` and `{b\_i : β | i ∈ I}` are the finite multiplicative supports of `f` and `g`, respectively.
|
finprod_mem_mul_diff'
theorem finprod_mem_mul_diff' :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s t : Set α},
s ⊆ t →
(t ∩ Function.mulSupport f).Finite →
((finprod fun i => finprod fun h => f i) * finprod fun i => finprod fun h => f i) =
finprod fun i => finprod fun h => f i
The theorem `finprod_mem_mul_diff'` is a general version of `finprod_mem_mul_diff` that states the following: for any types `α` and `M` where `M` is a commutative monoid, for any function `f : α → M`, and for any sets `s` and `t` of type `α`, if `s` is a subset of `t` and the intersection of `t` and the multiplicative support of `f` (the set of points `x` such that `f(x) ≠ 1`) is finite, then the product of `f(i)` over all elements `i` in the intersection of `t` and the multiplicative support of `f`, times the product of `f(i)` over all elements `i` in the difference between `t` and `s`, is equal to the product of `f(i)` over all elements `i` in `t`. In mathematical notation, if `s ⊆ t` and `(t ∩ {x | f(x) ≠ 1})` is finite, then `∏_{i in (t ∩ {x | f(x) ≠ 1}) ∪ (t \ s)} f(i) = ∏_{i in t} f(i)`.
More concisely: If `s` is a subset of `t` and the intersection of `t` with the multiplicative support of `f` is finite, then the product of `f(i)` over all `i` in `t` is equal to the product of `f(i)` over all `i` in `s` and the product of `f(i)` over all `i` in `t \ s`, where `f` is a function from type `α` to a commutative monoid `M` with `{x | f(x) ≠ 1}` being its multiplicative support.
|
finsum_sub_distrib
theorem finsum_sub_distrib :
∀ {α : Type u_1} {G : Type u_4} [inst : SubtractionCommMonoid G] {f g : α → G},
(Function.support f).Finite →
(Function.support g).Finite → (finsum fun i => f i - g i) = (finsum fun i => f i) - finsum fun i => g i
The theorem `finsum_sub_distrib` states that for any types `α` and `G` where `G` is a commutative monoid under subtraction, if we have two functions `f` and `g` from `α` to `G`, such that the supports of both `f` and `g` (i.e., the sets of points `x` for which `f(x)` and `g(x)` are non-zero, respectively) are finite, then the sum of the differences `f(i) - g(i)` over all `i` in `α` is equal to the difference between the sum of `f(i)` over all `i` in `α` and the sum of `g(i)` over all `i` in `α`. In other words, taking the sum of the differences is equivalent to taking the difference of the sums when the supports of `f` and `g` are finite.
More concisely: For functions `f` and `g` from a type `α` to a commutative monoid under subtraction `G` with finite supports, the sum of the differences `f(i) - g(i)` for all `i` in `α` equals the difference of the sums of `f` and `g` over `α`.
|
finsum_mem_of_eqOn_zero
theorem finsum_mem_of_eqOn_zero :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s : Set α},
Set.EqOn f 0 s → (finsum fun i => finsum fun h => f i) = 0
This theorem states that if a function `f` is equal to `0` for all elements `i` in a set `s`, then the sum of `f(i)` for all `i` in `s` is `0`. More formally, for any types `α` and `M` where `M` is an additive commutative monoid, and any function `f` from `α` to `M` and set `s` of `α`, if `f(i)` equals `0` for all `i` in `s`, then the sum of `f(i)` for each `i` in `s` is `0`.
More concisely: If a function from a set to an additive commutative monoid is equal to 0 for all elements in the set, then the sum of the function's values over that set is equal to 0.
|
AddMonoidHom.map_finsum_mem
theorem AddMonoidHom.map_finsum_mem :
∀ {α : Type u_1} {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] {s : Set α}
(f : α → M) (g : M →+ N),
s.Finite → g (finsum fun j => finsum fun h => f j) = finsum fun i => finsum fun h => g (f i)
This theorem states that for a given additive monoid homomorphism `g` mapping from `M` to `N` and a function `f` from some set `s` in `α` to `M`, the value of `g` at the sum of `f(i)` for each `i` in `s` is equal to the sum of `g(f(i))` for each `i` in `s`, given that `s` is finite. In other words, the mapping of the sum under `g` is equivalent to the sum of the mappings under `g`. This is a property of additive monoid homomorphisms and it's often referred to as the property of preserving finite sums.
More concisely: For any additive monoid homomorphism `g` and finite set `s`, the value of `g` applied to the sum of elements in `s` under the function `f` equals the sum of `g` applied to each element in `s` under the function `f`.
|
finprod_mem_eq_of_bijOn
theorem finprod_mem_eq_of_bijOn :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] {s : Set α} {t : Set β} {f : α → M} {g : β → M}
(e : α → β),
Set.BijOn e s t →
(∀ x ∈ s, f x = g (e x)) → (finprod fun i => finprod fun h => f i) = finprod fun j => finprod fun h => g j
The theorem `finprod_mem_eq_of_bijOn` states that for any types `α`, `β` and `M` with `M` being a commutative monoid, given sets `s` of type `α` and `t` of type `β`, and functions `f : α → M` and `g : β → M`. If there exists another function `e: α → β` that is bijective from `s` to `t` (meaning it maps each element in `s` to a unique element in `t` and covers all elements in `t`), and for every element `x` in `s`, `f(x)` equals `g(e(x))`. Then, the product over elements of the function `f` in the set `s` equals the product over elements of the function `g` in the set `t`. Here each of the products is computed by taking the product of `f(x)` for each `x` in `s` (respectively, `g(y)` for each `y` in `t`).
More concisely: If `f : α -> M`, `g : β -> M`, `α` and `β` are types, `M` is a commutative monoid, `s : set α`, `t : set β`, `e : α -> β` is a bijection from `s` to `t`, and `f(x) = g(e(x))` for all `x in s`, then `∏ x in s, f(x) = ∏ y in t, g(y)`.
|
finsum_mem_union_inter'
theorem finsum_mem_union_inter' :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s t : Set α},
(s ∩ Function.support f).Finite →
(t ∩ Function.support f).Finite →
((finsum fun i => finsum fun h => f i) + finsum fun i => finsum fun h => f i) =
(finsum fun i => finsum fun h => f i) + finsum fun i => finsum fun h => f i
This theorem states that for any type `α`, commutative additive monoid `M`, and a function `f` from `α` to `M`, given two sets `s` and `t` of type `α`, if the intersection of `s` and the support of `f` is finite, and the intersection of `t` and the support of `f` is also finite, then the sum of `f(i)` over `i` in `s` union `t` plus the sum of `f(i)` over `i` in `s` intersect `t` equals the sum of `f(i)` over `i` in `s` plus the sum of `f(i)` over `i` in `t`. Here, the sum over a set is defined to be 0 if the set is infinite. The support of a function is the set of points where the function is not 0. The proof of this theorem is omitted.
More concisely: For any commutative additive monoid M, function f from type α to M, and finite sets s and t of α, the sum of f(i) over i in s ∪ t is equal to the sum of f(i) over i in s plus the sum of f(i) over i in t.
|
finsum_mem_add_distrib'
theorem finsum_mem_add_distrib' :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f g : α → M} {s : Set α},
(s ∩ Function.support f).Finite →
(s ∩ Function.support g).Finite →
(finsum fun i => finsum fun h => f i + g i) =
(finsum fun i => finsum fun h => f i) + finsum fun i => finsum fun h => g i
The theorem `finsum_mem_add_distrib'` states that for any type `α`, any type `M` that forms an additive commutative monoid, any two functions `f` and `g` from `α` to `M`, and any set `s` of type `α`, if the intersection of `s` with the support of `f` and the intersection of `s` with the support of `g` are both finite, then the `finsum` (finite sum) across `i` of the `finsum` across `h` of `f i + g i` is equal to the sum of the `finsum` across `i` of the `finsum` across `h` of `f i` and the `finsum` across `i` of the `finsum` across `h` of `g i`.
In mathematical terms, it states that if we have two functions `f` and `g` and a set `s` such that the set of all points in `s` where `f` and `g` are non-zero (i.e., their supports) are finite, then the sum (over all points in the support) of the sums (for each point) of `f` and `g` is equal to the sum of the sum (over all points in the support) of `f` and the sum (over all points in the support) of `g`. This is a sort of "distributive law" for finite sums.
More concisely: For any additive commutative monoid M, given functions f and g from a finite set s to M with finite intersections of s with the supports of f and g, the finite sum of the sums of f and g over their common finite support equals the sum of the finite sums of f and g over their individual finite supports.
|
finsum_mem_union
theorem finsum_mem_union :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s t : Set α},
Disjoint s t →
s.Finite →
t.Finite →
(finsum fun i => finsum fun h => f i) =
(finsum fun i => finsum fun h => f i) + finsum fun i => finsum fun h => f i
This theorem, "finsum_mem_union", states that for any two finite disjoint sets `s` and `t` of type `α`, and a function `f` from `α` to type `M` (where `M` is an additively commutative monoid), the sum of `f(i)` over all elements `i` in the union of `s` and `t` is equal to the sum of `f(i)` over all elements `i` in `s` plus the sum of `f(i)` over all elements `i` in `t`. In other words, the sum of the function values over the union of the sets is the sum of the function values over each set, provided the sets are disjoint and finite.
In mathematical notation, this theorem states that for finite disjoint sets `s` and `t`, $\sum_{i \in s \cup t} f(i) = \sum_{i \in s} f(i) + \sum_{i \in t} f(i)$.
More concisely: For finite disjoint sets $s$ and $t$ and a function $f$ from a set to an additively commutative monoid, $\sum\_{i \in s \cup t} f(i) = \sum\_{i \in s} f(i) + \sum\_{i \in t} f(i)$.
|
MonoidHom.map_finprod_plift
theorem MonoidHom.map_finprod_plift :
∀ {M : Type u_2} {N : Type u_3} {α : Sort u_4} [inst : CommMonoid M] [inst_1 : CommMonoid N] (f : M →* N)
(g : α → M),
(Function.mulSupport (g ∘ PLift.down)).Finite → f (finprod fun x => g x) = finprod fun x => f (g x)
This theorem states that for any commutative monoids `M` and `N`, a monoid homomorphism `f` from `M` to `N`, and a function `g` from an arbitrary type `α` to `M`, if the multiplicative support of the function `g ∘ PLift.down` (i.e., the set of points `x` such that `g(PLift.down(x)) ≠ 1`) is finite, then the image of the finprod (product of `g x` as `x` ranges over the elements of the multiplicative support of `g`, or `1` if this set is infinite) under `f` is equal to the finprod of the images of `g x` under `f`. In other words, the monoid homomorphism `f` preserves the finprod over the multiplicative support of the function `g`.
More concisely: For any commutative monoids M, N, monoid homomorphism f from M to N, and function g from type α to M with finite multiplicative support of g ∘ PLift.down, the image of the finite product of g x under f is equal to the finite product of the images of g x under f.
|
exists_ne_one_of_finprod_mem_ne_one
theorem exists_ne_one_of_finprod_mem_ne_one :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s : Set α},
(finprod fun i => finprod fun h => f i) ≠ 1 → ∃ x ∈ s, f x ≠ 1
This theorem states that for any types `α` and `M`, where `M` is a commutative monoid, and any function `f` from `α` to `M`, if the product of `f(i)` for each `i` in a set `s` does not equal to `1` (which is the multiplicative identity), then there must exist an element `x` in the set `s` such that `f(x)` is not equal to `1`. In other words, if the product of all function values over a set is not the identity, then there is at least one function value over that set which is not the identity.
More concisely: If `f` is a function from a set `α` to a commutative monoid `M` such that the product of `f(i)` for all `i` in a set `s` does not equal the identity `1_M`, then there exists an `x` in `s` with `f(x) ≠ 1_M`.
|
finsum_mem_finset_product
theorem finsum_mem_finset_product :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] (s : Finset (α × β)) (f : α × β → M),
(finsum fun ab => finsum fun x => f ab) = finsum fun a => finsum fun b => finsum fun x => f (a, b)
This theorem, `finsum_mem_finset_product`, states that for any types `α`, `β`, and `M`, where `M` is an additive commutative monoid, and any finite set `s` of pairs of elements from `α` and `β`, and any function `f` from such a pair to `M`, the sum of function `f` over all elements of the set is equal to the sum of `f` of each pair `(a, b)`, where the sum is taken over all `a` and `b`. More formally, in mathematical notation, it states that:
\[
\sum_{(a,b) \in s} f(a, b) = \sum_a \sum_b f(a, b)
\]
The theorem essentially changes the order of summation, which is possible due to the commutativity of addition.
More concisely: For any additive commutative monoid M and finite set s of pairs (α × β) of elements from types α and β, the sum of a function from s to M over all pairs is equal to the sum of the function applied to each pair, where the sum is taken over all elements a from α and b from β. In other words, ∑((a, b) ∈ s) f(a, b) = ∑a ∑b f(a, b).
|
finprod_mem_eq_prod_of_inter_mulSupport_eq
theorem finprod_mem_eq_prod_of_inter_mulSupport_eq :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) {s : Set α} {t : Finset α},
s ∩ Function.mulSupport f = ↑t ∩ Function.mulSupport f →
(finprod fun i => finprod fun h => f i) = t.prod fun i => f i
This theorem states that for any type `α` and any type `M` that forms a commutative monoid, given a function `f` from `α` to `M`, a set `s` of `α` and a finite set `t` of `α`, if the intersection of `s` with the multiplicative support of `f` (the set of points `x` such that `f(x) ≠ 1`) is equal to the intersection of `t` with the multiplicative support of `f`, then the product of `f(x)` for each `x` in `s` (given by `finprod (finprod f)`) is equal to the product of `f(x)` for each `x` in `t` (given by `Finset.prod t f`). This theorem is essentially about the equality of two different types of product operations under certain conditions concerning the multiplicative support of a function.
More concisely: If `f` is a function from type `α` to a commutative monoid `M`, `s` and `t` are finite sets of `α`, and the intersection of `s` and the multiplicative support of `f` equals the intersection of `t` and the multiplicative support of `f`, then `finprod (finprod f) (set.toList s)` equals `Finset.prod t f`.
|
finprod_congr
theorem finprod_congr :
∀ {M : Type u_2} {α : Sort u_4} [inst : CommMonoid M] {f g : α → M},
(∀ (x : α), f x = g x) → finprod f = finprod g
This theorem, `finprod_congr`, states that for any type `M` with a commutative monoid structure and a function `α → M`, if we have two such functions `f` and `g` that map each element `x` of type `α` to the same element in `M`, then the finitely supported product (or `finprod`) of `f` equals the `finprod` of `g`. In other words, if two functions are pointwise equal, then their products over their multiplicative support are also equal.
More concisely: For commutative monoids M and functions f and g from type α to M that agree pointwise, their finitely supported products are equal: f ⊗₋ fin {x : α} (x ∈ s) = g ⊗₋ s, where s is a finite set and ⊗₋ denotes the finitely supported product.
|
AddMonoidHom.map_finsum_plift
theorem AddMonoidHom.map_finsum_plift :
∀ {M : Type u_2} {N : Type u_3} {α : Sort u_4} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] (f : M →+ N)
(g : α → M), (Function.support (g ∘ PLift.down)).Finite → f (finsum fun x => g x) = finsum fun x => f (g x)
This theorem states that for any two types `M` and `N` that form additive commutative monoids, and any type `α`, given an additive monoid homomorphism `f` from `M` to `N` and a function `g` from `α` to `M`, if the support of the composition `g ∘ PLift.down` is finite (i.e., there are only finitely many elements `x` in `α` such that `(g ∘ PLift.down)(x) ≠ 0`), then the value of `f` applied to the finite sum of `g(x)` over all `x` in `α` is equal to the finite sum of `f(g(x))` over all `x` in `α`.
This means that we can interchange the order of the sum and the application of the homomorphism `f` when summing over the elements of the support of `g ∘ PLift.down`.
More concisely: Given additive commutative monoids M and N, an additive monoid homomorphism f from M to N, and a function g from a set α to M with finite support, the sum of f(g(x)) over x in α equals the application of f to the sum of g(x) over x in α.
|
finsum_mem_pair
theorem finsum_mem_pair :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {a b : α},
a ≠ b → (finsum fun i => finsum fun h => f i) = f a + f b
This theorem states that for any two distinct elements `a` and `b` of a type `α`, and for any function `f` from `α` to a type `M` that forms an additive commutative monoid, the sum of `f i` over the set consisting of `a` and `b` is equal to `f a + f b`. In other words, if we compute `f` for both `a` and `b` and then add the results together, we get the same value as if we added the values of `f` computed over the entire two-element set `{a, b}`. This is the finiteness sum property of the function `f` over the pair `{a, b}`.
More concisely: For any additive commutative monoid-valued function `f` and distinct elements `a, b` of type `α`, we have `f a + f b = ∑ i in {a, b}, f i`.
|
finsum_comp
theorem finsum_comp :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {g : β → M} (e : α → β),
Function.Bijective e → (finsum fun i => g (e i)) = finsum fun j => g j
The theorem `finsum_comp` states that for all types `α`, `β`, and `M` such that `M` is an additive commutative monoid, a function `g` from `β` to `M` and a bijective function `e` from `α` to `β`, the sum of `g` applied to `e i` for all `i` in the domain of `e` (`finsum fun i => g (e i)`) is equal to the sum of `g j` for all `j` in the domain of `g` (`finsum fun j => g j`). In simpler terms, changing the domain of the summation using a bijective function does not change the sum.
More concisely: For all additive commutative monoids M, functions g from β to M, and bijective functions e from α to β, the sum of g (e i) over i in the domain of e equals the sum of g j over j in the domain of g.
|
finsum_mem_image
theorem finsum_mem_image :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s : Set β} {g : β → α},
Set.InjOn g s → (finsum fun i => finsum fun h => f i) = finsum fun j => finsum fun h => f (g j)
This theorem states that given a type `α` with an additive commutative monoid structure `M`, a function `f` from `α` to `M`, a set `s` of a type `β`, and a function `g` from `β` to `α`, if `g` is injective on the set `s`, then the sum of `f(y)` for each `y` in the image of `s` under `g` equals the sum of `f(g(i))` for each `i` in `s`. That is, we can sum over the image of `s` under `g` or sum over `s` itself with `g` applied to each element, and we get the same result as long as `g` is injective on `s`.
More concisely: Given a commutative additive monoid `M` over type `α`, a function `f : α → M`, an injective function `g : β → α` from a set `s ⊆ β`, the sum of `f(g(i))` for all `i ∈ s` equals the sum of `f(y)` for all `y ∈ g[s]`, where `g[s]` is the image of `s` under `g`.
|
finprod_mem_comm
theorem finprod_mem_comm :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] {s : Set α} {t : Set β} (f : α → β → M),
s.Finite →
t.Finite →
(finprod fun i => finprod fun h => finprod fun j => finprod fun h => f i j) =
finprod fun j => finprod fun h => finprod fun i => finprod fun h => f i j
This theorem states that, given two finite sets `s` of type `α` and `t` of type `β`, along with a function `f` that maps an element of `α` and an element of `β` to a `CommMonoid M`, the total product taken over `s` then `t` is equal to the total product taken over `t` then `s`. In other words, it means that the order of taking the product does not matter, this is a property of commutativity applied to products over finite sets. In mathematical terms, we can express this as $\prod_{i \in s}\prod_{j \in t} f(i, j) = \prod_{j \in t}\prod_{i \in s} f(i, j)$, where the product is taken over all elements `i` in set `s` and all elements `j` in set `t`.
More concisely: The theorem asserts the commutativity of finite product over finite sets, that is, $\prod\_{i \in s}\prod\_{j \in t} f(i, j) = \prod\_{j \in t}\prod\_{i \in s} f(i, j)$.
|
finprod_mem_induction
theorem finprod_mem_induction :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s : Set α} (p : M → Prop),
p 1 → (∀ (x y : M), p x → p y → p (x * y)) → (∀ x ∈ s, p (f x)) → p (finprod fun i => finprod fun h => f i)
This theorem states that to prove a property of a finite product, it suffices to demonstrate that the property is multiplicative and holds on factors. More formally, given a type `α`, a commutative monoid `M`, a function `f` mapping `α` to `M`, and a set `s` of `α`, if we have a property `p` such that `p` holds for the multiplicative identity `1`, `p` is closed under multiplication (i.e., for any `x, y` in `M`, if `p(x)` and `p(y)` hold, then `p(x*y)` also holds), and `p` holds for all `f(x)` where `x` belongs to `s`, then `p` holds for the finite product of `f(i)` across all `i`. The finite product is represented by `finprod (λ i, finprod (λ h, f i))`.
More concisely: If `f : α → M` maps a set `s` of `α` to a commutative monoid `M`, and `p` is a property that holds for the multiplicative identity `1`, is closed under multiplication, and holds for all `f(x)` with `x` in `s`, then `p` holds for the finite product `∏i∈I f i`, where `I` is the finite indexing set.
|
finprod_eq_prod_of_mulSupport_toFinset_subset
theorem finprod_eq_prod_of_mulSupport_toFinset_subset :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) (hf : (Function.mulSupport f).Finite)
{s : Finset α}, hf.toFinset ⊆ s → (finprod fun i => f i) = s.prod fun i => f i
The theorem `finprod_eq_prod_of_mulSupport_toFinset_subset` states that for any type `α` and `M`, where `M` is a commutative monoid, given a function `f : α → M`, if the set of points `x` such that `f(x) ≠ 1` (also known as the multiplicative support of `f`) is finite, then for any finite set `s` of type `α`, if the finite set corresponding to the multiplicative support of `f` is a subset of `s`, then the product of `f(x)` as `x` ranges over all elements of type `α` (denoted as `finprod f`) is equal to the product of `f(x)` as `x` ranges over the elements of the finite set `s` (denoted as `Finset.prod s f`). In other words, it shows that the infinite product over all elements is the same as the finite product over a superset of the multiplicative support.
More concisely: Given a commutative monoid `M` and a function `f : α → M` with finite multiplicative support, if the multiplicative support of `f` is a subset of a finite set `s`, then `finprod f = Finset.prod s f`.
|
finsum_mem_sUnion
theorem finsum_mem_sUnion :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {t : Set (Set α)},
t.PairwiseDisjoint id →
t.Finite →
(∀ x ∈ t, x.Finite) →
(finsum fun a => finsum fun h => f a) =
finsum fun s => finsum fun h => finsum fun a => finsum fun h => f a
This theorem states that if `t` is a finite collection of finite sets where every pair of sets in `t` are disjoint, then the sum of the function `f a` over all elements `a` in the union of all sets in `t` is equal to the sum over each set `s` in `t` of the sums of `f a` over all elements `a` in `s`. Here, `f` is a function from some type `α` to another type `M` where `M` is a type with an addition operation that is commutative and associative. Basically, this theorem is expressing a property of finite sums over disjoint finite sets.
More concisely: If `t` is a finite collection of finite, pairwise disjoint sets, then the sum of `f` over all elements in the union of `t` equals the sum of the sums of `f` over each set in `t`. Here, `f` is a function from some type to a commutative and associative additive semigroup.
|
finsum_mem_iUnion
theorem finsum_mem_iUnion :
∀ {α : Type u_1} {ι : Type u_3} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} [inst_1 : Finite ι]
{t : ι → Set α},
Pairwise (Disjoint on t) →
(∀ (i : ι), (t i).Finite) →
(finsum fun a => finsum fun h => f a) = finsum fun i => finsum fun a => finsum fun h => f a
The theorem `finsum_mem_iUnion` states that, for a given family of pairwise disjoint finite sets `t i` indexed by a finite type, the sum of `f a` over the union of these sets is equal to the sum over all indexes `i` of the sums of `f a` over the members of each `t i`. Here, `f` is a function from `α` to `M` where `M` is a type equipped with an addition operation that is commutative and associative. In other words, the sum over the union of these sets is the same as the sum of sums over each individual set. This theorem generalizes the principle of including each element exactly once when summing over a union of disjoint sets.
More concisely: For a family of pairwise disjoint finite sets indexed by a finite type and a commutative and associative type `M` with addition, the sum of a function `f` over the union of the sets equals the sum of the functions' sums over each individual set.
|
finprod_mem_range'
theorem finprod_mem_range' :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {g : β → α},
Set.InjOn g (Function.mulSupport (f ∘ g)) → (finprod fun i => finprod fun h => f i) = finprod fun j => f (g j)
This theorem states that for any types `α`, `β`, and `M` (with `M` being a commutative monoid), and any functions `f : α → M` and `g : β → α`, if `g` is injective on the set of points where `f ∘ g` is not equal to 1 (the multiplicative support of `f ∘ g`), then the product of `f x` for all `x` in the range of `g` is equal to the product of `f (g y)` for all `y`. In mathematical terms, if $g$ is injective on the set where $f \circ g \neq 1$, then $\prod_{y \in \text{range } g} f(y) = \prod_{i} f(g(i))$.
More concisely: If a function `g : β => alpha` is injective on the domain where `f ∘ g` is not the identity, then the product of `f` applied to the range of `g` equals the product of `f` applied to `g`'s image. In other words, if `g` is injective on the support of `f ∘ g`, then `∏(f ∘ g) = ∏(f o g)`.
|
finprod_mem_pair
theorem finprod_mem_pair :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {a b : α},
a ≠ b → (finprod fun i => finprod fun h => f i) = f a * f b
The theorem `finprod_mem_pair` states that for any types `α` and `M`, where `M` is a commutative monoid, and for any function `f` from `α` to `M`, and any distinct elements `a` and `b` of `α`, the total product of `f i` as `i` ranges over the set `{a, b}` is equal to the product of `f a` and `f b`. Here, `finprod` function represents the product of `f x` as `x` ranges over the elements of the multiplicative support of `f`. It's important to note that, `a` and `b` must be distinct elements (`a ≠ b`).
More concisely: For any commutative monoid M, function f from type α to M, and distinct elements a and b of α, the product of f a and f b is equal to the total product of f over the set {a, b}.
|
finsum_mem_def
theorem finsum_mem_def :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (s : Set α) (f : α → M),
(finsum fun a => finsum fun h => f a) = finsum fun a => s.indicator f a
The theorem `finsum_mem_def` states that for any set `s` of some type `α` and any function `f` from `α` to a type `M` which is an additive commutative monoid, the double finite sum of `f a` over all `a` is equal to the finite sum of the indicator function of `s` applied to `f` and `a`. In other words, summing `f a` over all `a` in a double finite sum is the same as summing the indicator function of `s` applied to `f` and `a`. This essentially means it's summing `f a` for `a` in `s` and 0 otherwise. This theorem connects the concept of finite sums and indicator functions in the context of set theory and additive commutative monoids.
More concisely: For any set `s` and additive commutative monoid-valued function `f`, the double finite sum of `f a` over all `a` is equal to the finite sum of the indicator function of `s` applied to `f` and `a`.
|
finsum_mem_comm
theorem finsum_mem_comm :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {s : Set α} {t : Set β} (f : α → β → M),
s.Finite →
t.Finite →
(finsum fun i => finsum fun h => finsum fun j => finsum fun h => f i j) =
finsum fun j => finsum fun h => finsum fun i => finsum fun h => f i j
The theorem `finsum_mem_comm` states that for any two finite sets `s` of type `α` and `t` of type `β`, the order of summation over these sets does not matter. More specifically, given a function `f` mapping elements of `s` and `t` to an additive commutative monoid `M`, the sum of `f` over all elements in `s`, for each element in `t`, is equal to the sum of `f` over all elements in `t`, for each element in `s`. In mathematical terms, this theorem formalises the property of double summation over finite sets that the order of summation can be interchanged.
More concisely: For any finite sets `s` and `t`, and any additive commutative monoid `M` with a function `f` mapping `s x t` to `M`, the sum of `f` over all pairs `(x, y)` in `s x t` where `x` is in `s` and `y` is in `t` is equal to the sum of `f` over all pairs `(x, y)` in `s x t` where `y` is in `t` and `x` is in `s`.
|
finprod_mem_union_inter'
theorem finprod_mem_union_inter' :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s t : Set α},
(s ∩ Function.mulSupport f).Finite →
(t ∩ Function.mulSupport f).Finite →
((finprod fun i => finprod fun h => f i) * finprod fun i => finprod fun h => f i) =
(finprod fun i => finprod fun h => f i) * finprod fun i => finprod fun h => f i
This theorem, named `finprod_mem_union_inter'`, is a more general version of `finprod_mem_union_inter`. It is defined over an arbitrary type `α`, a type `M` which is a commutative monoid, and a function `f` from `α` to `M`. Given two arbitrary sets `s` and `t` of type `α`, if the intersection of `s` and the multiplicative support of `f`, and the intersection of `t` and the multiplicative support of `f` are both finite, then the product over the elements of `s` and `t` of the finproduct of `f` equals the product of the finproduct over the elements of `s` of `f` and the finproduct over the elements of `t` of `f`. Here, the multiplicative support of a function `f` refers to the set of points `x` such that `f(x) ≠ 1`, and the finproduct of a function `f` refers to the product of `f(x)` as `x` ranges over the elements of the multiplicative support of `f`, if it is finite; otherwise it is one.
More concisely: If `s` and `t` are two finite sets and `f` is a function from an arbitrary type `α` to a commutative monoid `M` such that the intersections of `s` and `f`'s multiplicative support, and `t` and `f`'s multiplicative support are finite, then the product of `f` over the elements in `s ∪ t` equals the product of the product over `s` and the product over `t` of `f`.
|
finsum_mem_singleton
theorem finsum_mem_singleton :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {a : α},
(finsum fun i => finsum fun h => f i) = f a
This theorem states that for any given type `α` and `M` with `M` being an additive commutative monoid, and any function `f` mapping from `α` to `M`, and any element `a` of type `α`, the sum of the function `f` evaluated at `i` for each `i` in the singleton set `{a}` is equal to the function `f` evaluated at `a`. In other words, the finite sum over a singleton set is just the function evaluated at that single element.
More concisely: For any additive commutative monoid M, function f from type α to M, and element a of α, the sum of f evaluated at the singleton set {a} equals f evaluated at a. In mathematical notation, ∏i ∈ {a} f i = f a.
|
finprod_mem_insert_of_eq_one_if_not_mem
theorem finprod_mem_insert_of_eq_one_if_not_mem :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {a : α} {s : Set α},
(a ∉ s → f a = 1) → (finprod fun i => finprod fun h => f i) = finprod fun i => finprod fun h => f i
This theorem states that for any types `α` and `M`, with `M` being a commutative monoid, for a function `f` from `α` to `M`, an element `a` of type `α`, and a set `s` of type `α`, if the function `f` maps `a` to the identity element of `M` (in this case, `1`) whenever `a` is not an element of `s`, then the product of `f i` for all `i` in the set obtained by inserting `a` into `s` is equal to the product of `f i` for all `i` in `s`. Here, the product over a set is defined as the product of `f x` as `x` ranges over the elements of the set, with the product being `1` if the set is empty.
More concisely: If `f` is a function from type `α` to a commutative monoid `M` such that `f(a) = 1` for all `a` in the complement of a set `s`, then `∏_{i ∈ s⋃{a}} f(i) = ∏_{i ∈ s} f(i)`.
|
finprod_mem_range
theorem finprod_mem_range :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {g : β → α},
Function.Injective g → (finprod fun i => finprod fun h => f i) = finprod fun j => f (g j)
This theorem states that given two types `α` and `β`, and a commutative monoid `M`, if you have a function `f : α → M` and an injective function `g : β → α`, then the product of `f y` over all `y` in the range of `g` is equal to the product of `f (g i)` over all `i`. In other words, taking the product over the range of `g` is the same as taking the product over the original domain and then applying `g`. This is assuming that the product operation is commutative, i.e., the order does not matter.
More concisely: Given commutative monoids `M` and types `α` and `β`, if `f : α → M`, `g : β → α` is injective, then the product of `f (g y)` over all `y` in the range of `g` equals the product of `f x` over all `x` in `α`.
|
finsum_mem_induction
theorem finsum_mem_induction :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s : Set α} (p : M → Prop),
p 0 → (∀ (x y : M), p x → p y → p (x + y)) → (∀ x ∈ s, p (f x)) → p (finsum fun i => finsum fun h => f i)
This theorem states that to prove a property `p` holds for a finite sum of elements from a set, three conditions must be satisfied. First, the property `p` holds for the zero element of the additive commutative monoid `M`. Second, the property `p` is additive, that is, if `p` holds for elements `x` and `y` of `M`, then it also holds for their sum `x + y`. Finally, the property `p` holds for every element of the set `s` mapped through function `f`. If these conditions are met, then the property `p` holds for the sum of all elements of `f`, summed over all elements of `s`. Here, `Set α` is a set of elements of some type `α`, `AddCommMonoid M` is an additive commutative monoid of some type `M`, and `f : α → M` is a function from `α` to `M`. `finsum` denotes finite sum over the elements of `f`.
More concisely: If a property holds for the zero element of an additive commutative monoid and is additive, then it holds for the finite sum of elements mapped through the function if and only if it holds for each element of the domain.
|
finsum_eq_sum_plift_of_support_subset
theorem finsum_eq_sum_plift_of_support_subset :
∀ {M : Type u_2} {α : Sort u_4} [inst : AddCommMonoid M] {f : α → M} {s : Finset (PLift α)},
Function.support (f ∘ PLift.down) ⊆ ↑s → (finsum fun i => f i) = s.sum fun i => f i.down
This theorem, `finsum_eq_sum_plift_of_support_subset`, states that for any given type `M`, which is an additive commutative monoid, and for any type `α`, given a function `f` from `α` to `M` and a finite set `s` of lifted elements of `α`, if the support of the function `f` composed with the "down" operation on `PLift α` (i.e. the set of points where `f` does not evaluate to zero) is a subset of `s`, then the sum of `f` over all elements `i` (in the sense of `finsum`) is equal to the sum of `f` applied to the "down" of each element `i` in the finite set `s`. The "down" operation on `PLift α` is used to extract a value from a lifted type. The sum over a finite set is simply the addition of `f x` for all `x` in the set.
More concisely: For any additive commutative monoid M and function f from type α to M, if the support of f composed with the down operation on PLift α is a subset of a finite set s of lifted elements, then the sum of f over all elements in the domain equals the sum of f applied to the down of each element in s.
|
finprod_mem_div_distrib
theorem finprod_mem_div_distrib :
∀ {α : Type u_1} {G : Type u_4} {s : Set α} [inst : DivisionCommMonoid G] (f g : α → G),
s.Finite →
(finprod fun i => finprod fun h => f i / g i) =
(finprod fun i => finprod fun h => f i) / finprod fun i => finprod fun h => g i
This theorem states that for a finite set `s` of elements of type `α`, and a `DivisionCommMonoid` `G` which gives us our division operation, if we have two functions `f` and `g` that map each element of `s` to `G`, then the product of the division of `f(i)` by `g(i)` for each `i` in `s` is equal to the product of `f(i)` for each `i` in `s` divided by the product of `g(i)` for each `i` in `s`. This theorem essentially expresses the distributive property of division over multiplication for finite products.
More concisely: For a finite set `s` and functions `f` and `g` mapping each element of `s` to a `DivisionCommMonoid`, the product of `f(i) / g(i)` for all `i` in `s` equals the quotient of the product of `f(i)` for all `i` in `s` by the product of `g(i)` for all `i` in `s`.
|
finprod_mem_def
theorem finprod_mem_def :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (s : Set α) (f : α → M),
(finprod fun a => finprod fun h => f a) = finprod fun a => s.mulIndicator f a
The theorem `finprod_mem_def` states that for any set `s` of a certain type `α` and any function `f` from `α` to a type `M` (where `M` has a `CommMonoid` structure), the product of `f(x)` for each `x` in `s` is the same as the product of `f(x)` if `x` is in `s` and `1` otherwise. In other words, the finite product over the set `s` (using the function `f`) is equal to the finite product over all elements, where each element not in `s` contributes a multiplicative identity (`1`) to the product. This is computed using the `Set.mulIndicator` function, which returns the value of the function `f` at a point if the point is in the set, and `1` otherwise.
More concisely: For any set `s` and function `f` from a type `α` to a commutative monoid `M`, the finite product of `f(x)` over `s` equals the product of `f(x)` for `x` in `s` and `1` for `x` not in `s`.
|
finprod_induction
theorem finprod_induction :
∀ {M : Type u_2} {α : Sort u_4} [inst : CommMonoid M] {f : α → M} (p : M → Prop),
p 1 → (∀ (x y : M), p x → p y → p (x * y)) → (∀ (i : α), p (f i)) → p (finprod fun i => f i)
The theorem `finprod_induction` states that to prove a property `p` holds for the finite product of a function `f` mapping from type `α` to a commutative monoid `M`, it is sufficient to prove three things:
1. The property `p` holds for the identity element `1` of the commutative monoid `M`.
2. The property `p` is stable under multiplication, that is, if `p` holds for two elements `x` and `y` of the monoid `M`, then it also holds for their product `x * y`.
3. The property `p` holds for every value `f i` where `i` is an element of `α`.
If these three conditions are met, then the property `p` holds for the finite product, represented as `finprod fun i => f i`.
More concisely: If `f` is a function from type `α` to a commutative monoid `M`, and `p` is a property stable under multiplication such that `p` holds for the identity element `1` of `M` and for every `f i` where `i` is an element of `α`, then `p` holds for the finite product `finprod fun i => f i`.
|
finprod_mem_mul_distrib'
theorem finprod_mem_mul_distrib' :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f g : α → M} {s : Set α},
(s ∩ Function.mulSupport f).Finite →
(s ∩ Function.mulSupport g).Finite →
(finprod fun i => finprod fun h => f i * g i) =
(finprod fun i => finprod fun h => f i) * finprod fun i => finprod fun h => g i
This theorem, named `finprod_mem_mul_distrib'`, is a more general version of `finprod_mem_mul_distrib`. It states that for any commutative monoid `M`, any two functions `f` and `g` from a type `α` to `M`, and any set `s` of elements of type `α`, if the intersection of `s` with the multiplicative support of `f` (i.e., the set of points `x` such that `f(x) ≠ 1`) is finite, and likewise the intersection of `s` with the multiplicative support of `g` is finite, then the function defined by `i` ranging over all elements and `h` ranging over all elements such that `f(i)*g(i)` is equal to the product of two functions defined by `i` ranging over all elements and `h` ranging over all elements such that `f(i)` and `g(i)`, respectively. In other words, we can distribute the `finprod` operation over multiplication, under certain finiteness conditions.
More concisely: For any commutative monoid M and functions f, g from type α to M with finite intersections of their multiplicative supports with a set s, the function defined by i ∈ s mapping to f(i) * g(i) is equal to the product of the functions defined by i ∈ s mapping to f(i) and g(i), respectively.
|
finsum_mem_union'
theorem finsum_mem_union' :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s t : Set α},
Disjoint s t →
(s ∩ Function.support f).Finite →
(t ∩ Function.support f).Finite →
(finsum fun i => finsum fun h => f i) =
(finsum fun i => finsum fun h => f i) + finsum fun i => finsum fun h => f i
This theorem, `finsum_mem_union'`, is a more general version of `finsum_mem_union` and it states that for any two sets `s` and `t` of type `α` and a function `f` from `α` to `M` under addition-commutative monoid setting, if `s` and `t` are disjoint, and if the intersection of `s` and `t` with the support of `f` are both finite, then the sum of `f` over all elements in the union of `s` and `t` is equal to the sum of `f` over all elements in `s` added to the sum of `f` over all elements in `t`. Here, the 'support' of a function refers to the set of points where the function is non-zero, and 'finsum' refers to the sum over a finite set (or zero if the set is not finite).
More concisely: For disjoint, finite subsets $S, T$ of a set $\alpha$ and a commutative monoid $(M, +)$ with finite supports $S \cap \operatorname{supp}(f)$ and $T \cap \operatorname{supp}(f)$, the sum $\sum\_{x \in S \cup T} f(x)$ equals $\sum\_{x \in S} f(x) + \sum\_{x \in T} f(x)$.
|
finsum_eq_sum
theorem finsum_eq_sum :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) (hf : (Function.support f).Finite),
(finsum fun i => f i) = hf.toFinset.sum fun i => f i
This theorem states that for any type `α` and `M`, given that `M` has an addition that is both commutative and associative, and a function `f : α → M`, if the set of elements `α` for which `f` is non-zero (the support of `f`) is finite, then the sum of `f(x)` for all `x` in the domain is equal to the sum of `f(x)` for all `x` in the finite set that represents the support of `f`. In mathematical terms, this theorem says that ∑ f(x) (where the sum ranges over all x) equals ∑ f(x) (where the sum only ranges over x in the support of f), provided the support of f is a finite set.
More concisely: If `α` is a finite type with a commutative and associative addition, and `f : α → M` is a function with finite support, then the sum of `f(x)` over all `x` in `α` equals the sum of `f(x)` over the finite support of `f`.
|
finsum_mem_range'
theorem finsum_mem_range' :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {g : β → α},
Set.InjOn g (Function.support (f ∘ g)) → (finsum fun i => finsum fun h => f i) = finsum fun j => f (g j)
This theorem states that for any two types `α` and `β`, and any type `M` that forms an additive commutative monoid, given a function `f` from `α` to `M`, and a function `g` from `β` to `α`, if `g` is injective on the set of points where the composition `f ∘ g` is not zero (the support of `f ∘ g`), then the sum of `f y` for all `y` in the range of `g` is equal to the sum of `f (g i)` for all `i`. In other words, if we first apply `g` to each element and then apply `f`, or if we directly apply `f` to each element in the range of `g`, the total sum will be the same, as long as `g` doesn't map different non-zero values of `f ∘ g` to the same place.
More concisely: If `f: α → M` is a function from type `α` to an additive commutative monoid `M`, `g: β → α` is an injective function, and the support of `f ∘ g` is contained in the image of `g`, then the sum of `f (g i)` for all `i` is equal to the sum of `f y` for all `y` in the image of `g`.
|
finsum_smul
theorem finsum_smul :
∀ {ι : Sort u_6} {R : Type u_7} {M : Type u_8} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : NoZeroSMulDivisors R M] (f : ι → R) (x : M), (finsum fun i => f i) • x = finsum fun i => f i • x
The theorem `finsum_smul` states that, for any sort `ι`, any ring `R`, and any additive commutative group `M` that's also a module over `R`, and under the condition that there are no zero scalar-multiplication-divisors in `R` and `M`, the scalar multiplication of the `finsum` of a function `f` from `ι` to `R` and an element `x` from `M` is equal to the `finsum` of the function `i` maps to the scalar multiplication of `f i` and `x`. In other words, assuming that scalar multiplication by zero is not a division operation in the module, the sum of the results of `f` over its domain, multiplied by `x`, is equal to the sum of the scalar products of `f i` and `x` over `i` in the domain of `f`. This theorem holds even when the support of `f` is infinite. For a similar theorem that assumes a finite support of `f`, see `finsum_smul'`.
More concisely: For any additive commutative group `M` that's a module over a ring `R` with no zero scalar-multiplication-divisors, and for any function `f` from a sort `ι` to `R`, the finitary sum of the scalar multiplications of `f i` and `x` over `i` is equal to the scalar multiplication of the finitary sum of `f` and `x`.
|
finprod_mul_distrib
theorem finprod_mul_distrib :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f g : α → M},
(Function.mulSupport f).Finite →
(Function.mulSupport g).Finite → (finprod fun i => f i * g i) = (finprod fun i => f i) * finprod fun i => g i
This theorem, `finprod_mul_distrib`, states that for any types `α` and `M`, with `M` being a commutative monoid, and any two functions `f` and `g` from `α` to `M`, if the multiplicative supports of `f` and `g` (that is, the sets of points `x` such that `f(x)` and `g(x)` are not equal to 1, respectively) are finite, then the finite product of the values `f(i) * g(i)` for all `i` in `α` (denoted as `finprod (fun i => f i * g i)`) is equal to the product of the finite product of the values `f(i)` for all `i` (denoted as `finprod (fun i => f i)`) and the finite product of the values `g(i)` for all `i` (denoted as `finprod (fun i => g i)`). In other words, when the multiplicative supports of `f` and `g` are finite, the finite product over a function that multiplies the outputs of `f` and `g` is the same as the product of the finite products over `f` and `g` separately.
More concisely: If `f` and `g` are functions from a type `α` to a commutative monoid `M` with finite multiplicative supports, then `finprod (fun i => f i * g i) = finprod (fun i => f i) * finprod (fun i => g i)`.
|
finsum_mem_insert_of_eq_zero_if_not_mem
theorem finsum_mem_insert_of_eq_zero_if_not_mem :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {a : α} {s : Set α},
(a ∉ s → f a = 0) → (finsum fun i => finsum fun h => f i) = finsum fun i => finsum fun h => f i
The theorem `finsum_mem_insert_of_eq_zero_if_not_mem` states that for any types `α` and `M`, where `M` is an additive commutative monoid, any function `f` from `α` to `M`, any element `a` of type `α`, and any set `s` of elements of type `α`, if the function `f` applied to `a` equals zero whenever `a` is not in the set `s`, then the sum of `f i` for all `i` in the set obtained by inserting `a` into `s` equals the sum of `f i` for all `i` in the set `s` itself. This essentially means that inserting an element into a set does not change the total sum according to the function `f`, if the function value of that element is zero when it's not already present in the set.
More concisely: If `f : α -> M` is a function from type `α` to an additive commutative monoid `M`, `a : α`, and `s : set α` such that `f a = 0` for all `a' in α \ s, then `∑ i in s. f i = ∑ i in s ∪ {a}. f i`.
|
finsum_zero
theorem finsum_zero : ∀ {M : Type u_2} {α : Sort u_4} [inst : AddCommMonoid M], (finsum fun x => 0) = 0
This theorem, `finsum_zero`, states that for any type `M` with an additive commutative monoid structure, and any type `α`, the finite sum (`finsum`) of the constant zero function (i.e., a function that maps every element of `α` to zero in `M`) is zero. In other words, adding up all the zeroes gives you zero, regardless of the set you're summing over.
More concisely: For any additive commutative monoid `M` and type `α`, the finitesum of the constant zero function from `α` to `M` is the zero element of `M`.
|
finprod_mem_finset_product
theorem finprod_mem_finset_product :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] (s : Finset (α × β)) (f : α × β → M),
(finprod fun ab => finprod fun x => f ab) = finprod fun a => finprod fun b => finprod fun x => f (a, b)
This theorem, `finprod_mem_finset_product`, states that for any given types `α`, `β`, and `M` (where `M` has a Commutative Monoid structure), and a function `f` from the product of `α` and `β` to `M`, the finite product (denoted by `finprod`) over all pairs `(a, b)` in a given finite set `s` of `f(a, b)` equals to the finite product over all `a` of the finite product over all `b` of `f(a, b)`. This theorem showcases how we can interchange the order of finite products when they are over a Commutative Monoid.
More concisely: For any Commutative Monoid M, function f from the product of types α and β to M, and finite set s of pairs (α × β), the finite product of f over s is equal to the finite product of the finite products of f over the first coordinate for each element in s.
|
finprod_mem_insert'
theorem finprod_mem_insert' :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {a : α} {s : Set α} (f : α → M),
a ∉ s →
(s ∩ Function.mulSupport f).Finite →
(finprod fun i => finprod fun h => f i) = f a * finprod fun i => finprod fun h => f i
This theorem, `finprod_mem_insert'`, provides a more generalized version of `finprod_mem_insert`. It operates under the context of a set `s` of type `α`, a function `f` from `α` to `M` where `M` is a commutative monoid, and an element `a` of type `α` that is not a member of `s`. The theorem states that if the intersection of `s` with the multiplicative support of `f` (the set of points `x` such that `f(x) ≠ 1`) is finite, then the product of `f(i)` across all `i` (where the inner product is defined only when `i` lies in `s`) equals the product of `f(a)` and the product of `f(i)` across all `i` (where the inner product is defined only when `i` lies in `s` and `i ≠ a`).
More concisely: If `s` is a finite subset of `α` and `f:` `α` → `M` maps `s` (excluding one element `a`) to non-identity elements in the commutative monoid `M`, then `∥f∥(s) = f(a) * ∥f∥(s \ {a})`, where `∥f∥(s)` denotes the product of `f(i)` over all `i` in `s`.
|
finsum_mem_insert
theorem finsum_mem_insert :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {a : α} {s : Set α} (f : α → M),
a ∉ s → s.Finite → (finsum fun i => finsum fun h => f i) = f a + finsum fun i => finsum fun h => f i
The theorem `finsum_mem_insert` states that given a finite set `s` of elements of some type `α` and an element `a` of the same type that does not belong to `s`, the sum of the function `f` applied to each element `i` in the set obtained by inserting `a` into `s` is equal to the value of `f` at `a` plus the sum of `f` applied to each element `i` in `s`. This is, of course, under the assumption that the codomain of `f` is a type `M` which forms an additive commutative monoid. The finiteness of `s` is necessary to ensure that the sums are well-defined.
More concisely: Given a finite set `s` of elements from a type `α` and an element `a ∈ α \ s`, the sum of the function `f : α → M` evaluated at each element in `s ∪ {a}` equals the sum of `f a` and the sum of `f` over `s`.
|
MonoidHom.map_finprod_mem'
theorem MonoidHom.map_finprod_mem' :
∀ {α : Type u_1} {M : Type u_5} {N : Type u_6} [inst : CommMonoid M] [inst_1 : CommMonoid N] {s : Set α} {f : α → M}
(g : M →* N),
(s ∩ Function.mulSupport f).Finite →
g (finprod fun j => finprod fun h => f j) = finprod fun i => finprod fun h => g (f i)
This theorem, `MonoidHom.map_finprod_mem'`, states a more generalized version of `MonoidHom.map_finprod_mem`. It says that for any types `α`, `M`, `N`, given two commutative monoids `M` and `N`, a set `s` of type `α`, a function `f` from `α` to `M`, and a monoid homomorphism `g` from `M` to `N`, if the intersection of `s` and the multiplicative support of `f` (the set of points `x` where `f(x)` is not equal to `1`) is finite, then the monoid homomorphism `g` applied to the double infinite product `finprod` (product of `f(x)` as `x` ranges over the elements of the multiplicative support, if it's finite; otherwise, it equals to one) of function `f` is equal to the double infinite product of the monoid homomorphism `g` applied to `f(i)`.
In mathematical terms, given $s \subseteq \alpha$, function $f: \alpha \rightarrow M$ and monoid homomorphism $g: M \rightarrow N$, if $s \cap \{x : f(x) \neq 1\}$ is finite, then $g \left( \prod_{j \in s} \prod_{h \in \{x : f(x) \neq 1\}} f(j) \right) = \prod_{i \in s} \prod_{h \in \{x : f(x) \neq 1\}} g(f(i))$. This theorem generalizes the concept of mapping the infinite product of a function's values over a set under a monoid homomorphism in the context where the set and the function's multiplicative support intersect finitely.
More concisely: Given sets $s \subseteq \alpha$, a function $f: \alpha \rightarrow M$ from a type to a commutative monoid $M$, and a monoid homomorphism $g: M \rightarrow N$, if the intersection of $s$ and the multiplicative support of $f$ is finite, then $g(\prod\_{j \in s} \prod\_{h \in \{x : f(x) \neq 1\}} f(j)) = \prod\_{i \in s} \prod\_{h \in \{x : f(x) \neq 1\}} g(f(i))$.
|
finsum_eq_indicator_apply
theorem finsum_eq_indicator_apply :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (s : Set α) (f : α → M) (a : α),
(finsum fun x => f a) = s.indicator f a
The theorem `finsum_eq_indicator_apply` states that for any set `s` of type `α`, any function `f` from `α` to `M`, and any element `a` of `α`, the sum (`finsum`) of `f a` over all `x` is equal to the `Set.indicator` of `s`, `f`, and `a`. In more detail, `Set.indicator` is a function that returns `f a` if `a` is in the set `s`, and `0` otherwise. Therefore, if you sum `f a` over all `x`, you get the same result as using the `Set.indicator` function on `s`, `f`, and `a`. This theorem essentially connects the concepts of summing over a function and using an indicator function in the context of a set.
More concisely: For any set `s`, function `f` from `s` to `M`, and element `a` in `s`, the sum of `f a` over all `x` in `s` equals the value of `Set.indicator s f a`.
|
finprod_cond_eq_prod_of_cond_iff
theorem finprod_cond_eq_prod_of_cond_iff :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) {p : α → Prop} {t : Finset α},
(∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)) → (finprod fun i => finprod fun x => f i) = t.prod fun i => f i
This theorem states that for any types `α` and `M` with `M` a commutative monoid, and any function `f` from `α` to `M`, given a predicate `p` on `α` and a finite set `t` of elements of type `α`, if for all `x` in `α`, `f x` is not equal to `1` implies that `p x` if and only if `x` is in `t`, then the product of `f x` over all `x` in the multiplicative support of `f`, where the product is defined by `finprod`, is equal to the product of `f i` over all `i` in the finite set `t`, where the product is defined by `Finset.prod`. In mathematical terms, this theorem is saying that under the conditions specified, the infinite product `∏ (f x : ∀ x)` is equal to the finite product `∏ₜ (f i : ∀ i ∈ t)`.
More concisely: Given a commutative monoid M, a function f from type α to M, a predicate p on α, and a finite set t of elements in α such that for all x in α, if f x ≠ 1 then p(x) if and only if x is in t, the infinite product ∏(fx) over all x in the multiplicative support of f is equal to the finite product ∏i∈t(fi).
|
finsum_mem_sub_distrib
theorem finsum_mem_sub_distrib :
∀ {α : Type u_1} {G : Type u_4} {s : Set α} [inst : SubtractionCommMonoid G] (f g : α → G),
s.Finite →
(finsum fun i => finsum fun h => f i - g i) =
(finsum fun i => finsum fun h => f i) - finsum fun i => finsum fun h => g i
The theorem `finsum_mem_sub_distrib` states that for any finite set `s` of a certain type `α` and any functions `f` and `g` from `α` to a type `G` which forms a subtraction-commutative monoid, the sum of the differences `f i - g i` for all `i` in `s` equals the difference of the sum of `f i` for all `i` in `s` and the sum of `g i` for all `i` in `s`. In other words, it states that the sum of the differences is equal to the difference of the sums over the same finite set.
More concisely: For any finite set `s` and functions `f` and `g` from `s` to a subtraction-commutative monoid `G`, the sum of the differences `f i - g i` for all `i` in `s` equals the difference of the sums `∑ i in s, f i` and `∑ i in s, g i`.
|
finsum_mem_biUnion
theorem finsum_mem_biUnion :
∀ {α : Type u_1} {ι : Type u_3} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {I : Set ι} {t : ι → Set α},
I.PairwiseDisjoint t →
I.Finite →
(∀ i ∈ I, (t i).Finite) →
(finsum fun a => finsum fun h => f a) =
finsum fun i => finsum fun h => finsum fun j => finsum fun h => f j
The theorem `finsum_mem_biUnion` states that for a family of sets `t : ι → Set α` indexed by `ι`, and a finite set `I` in this index type such that all sets `t i` for `i ∈ I` are finite, and are pairwise disjoint, then the sum of a function `f` over all elements `a` in union of these sets is equal to the sum of sums of `f a` over each set `t i` for `i ∈ I`. In mathematical terms, it says $\sum_{a \in \bigcup_{i \in I} t_i} f(a) = \sum_{i \in I} \sum_{a \in t_i} f(a)$. This is essentially a statement about rearranging the order of a finite summation.
More concisely: For a family of finite, pairwise disjoint sets `t : ι → Set α` indexed by `ι`, the sum of a function over the union equals the sum of the functions' sums over each set: $\sum\_{a \in \bigcup\_{i \in I} t\_i} f(a) = \sum\_{i \in I} \sum\_{a \in t\_i} f(a)$.
|
finprod_eq_mulIndicator_apply
theorem finprod_eq_mulIndicator_apply :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (s : Set α) (f : α → M) (a : α),
(finprod fun x => f a) = s.mulIndicator f a
The theorem `finprod_eq_mulIndicator_apply` states that for any given set `s` of type `α`, any function `f` from `α` to a commutative monoid `M`, and any element `a` of type `α`, the product of `f a` over all elements of the multiplicative support of `f` (`finprod fun x => f a`) is equal to `f a` if `a` belongs to the set `s`, and `1` otherwise. This latter operation is defined by `Set.mulIndicator s f a`. In other words, this theorem connects the concepts of finitary product and set-valued multiplication indicator function in the context of a commutative monoid.
More concisely: For any set `s`, function `f` from a commutative monoid to itself, and element `a` of the set, `finprod fun x => f x = f a` if `a` is in `s`, and `finprod fun x => f x = 1` otherwise, equivalent to `Set.mulIndicator s f a`.
|
AddMonoidHom.map_finsum
theorem AddMonoidHom.map_finsum :
∀ {α : Type u_1} {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] {f : α → M}
(g : M →+ N), (Function.support f).Finite → g (finsum fun i => f i) = finsum fun i => g (f i)
The `AddMonoidHom.map_finsum` theorem states that for any two types `α` and `M`, and another type `N`, all of which are under the context of additive commutative monoids, given a function `f` from `α` to `M`, and an additive monoid homomorphism `g` from `M` to `N`, if the support of the function `f` is finite, then the sum of the function `f` over its support, after being mapped by `g`, is equal to the sum, over the same support, of `f` mapped by `g`. In other words, the operation of summing over a finite support commutes with the operation of applying an additive monoid homomorphism. This can be represented in mathematical notation as: if the set $\{x | f(x) \neq 0\}$ is finite, then $g(\sum f(i)) = \sum g(f(i))$.
More concisely: Given a function from a finite set to an additive commutative monoid, and an additive monoid homomorphism, the sum of the function mapped by the homomorphism is equal to the homomorphism of the sum of the function.
|
finsum_mem_union''
theorem finsum_mem_union'' :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s t : Set α},
Disjoint (s ∩ Function.support f) (t ∩ Function.support f) →
(s ∩ Function.support f).Finite →
(t ∩ Function.support f).Finite →
(finsum fun i => finsum fun h => f i) =
(finsum fun i => finsum fun h => f i) + finsum fun i => finsum fun h => f i
This theorem, `finsum_mem_union''`, is a generalized version of `finsum_mem_union'`. It states that for any type `α`, a commutative monoid `M`, a function `f` from `α` to `M`, and two sets `s` and `t` of `α`, if the intersection of `s` and the support of `f` is disjoint from the intersection of `t` and the support of `f`, and if these intersections are finite, then the sum of `f i` as `i` ranges over the elements of the union of `s` and `t` (the `finsum` operation) equals to the sum of `f i` as `i` ranges over `s`, plus the sum of `f i` as `i` ranges over `t`. Here, the support of `f` is the set of points `x` such that `f x ≠ 0`.
More concisely: For any commutative monoid M, function f from type α to M, and finite sets s and t of α with disjoint intersections and support of f, the sum of f i over i in the union of s and t equals the sum over i in s plus the sum over i in t.
|
finprod_mem_mul_diff
theorem finprod_mem_mul_diff :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s t : Set α},
s ⊆ t →
t.Finite →
((finprod fun i => finprod fun h => f i) * finprod fun i => finprod fun h => f i) =
finprod fun i => finprod fun h => f i
This theorem states that for a given finite set `t` and a subset `s` of `t`, the product of `f(i)` for each `i` in `s`, multiplied by the product of `f(i)` for each `i` in `t` but not in `s`, is equal to the product of `f(i)` for each `i` in `t`. Here `f` is a function from an arbitrary type `α` to a commutative monoid `M`. The subset relationship is denoted as `s ⊆ t`. The "product of `f(i)` over a set" is represented by `finprod` function in the theorem statement.
More concisely: For a finite set `t`, function `f` from type `α` to a commutative monoid `M`, and subset `s ⊆ t`, the theorem states that `finprod (map f s) * finprod (map (lambda i, f i) (set.difference t s)) = finprod (map f t)`.
|
AddMonoidHom.map_finsum_mem'
theorem AddMonoidHom.map_finsum_mem' :
∀ {α : Type u_1} {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] {s : Set α}
{f : α → M} (g : M →+ N),
(s ∩ Function.support f).Finite →
g (finsum fun j => finsum fun h => f j) = finsum fun i => finsum fun h => g (f i)
This theorem states a more general version of the `AddMonoidHom.map_finsum_mem` property, but with a modified requirement that the intersection of set `s` and the support of function `f` should be finite. In this context, the support of a function `f` is defined as the set of points where `f` is non-zero.
Given any types `α`, `M`, and `N`, along with two additive commutative monoids `M` and `N`, a set `s` of type `α`, and a function `f` mapping from `α` to `M`, the theorem asserts that for any additive monoid homomorphism `g` from `M` to `N`, if the intersection of set `s` and the support of `f` is finite, then the homomorphism of the double finite sum of `f` is equal to the double finite sum of the homomorphism of `f`. That is, in mathematical terms, we have
\[ g \left( \sum_{j} \sum_{h} f(j) \right) = \sum_{i} \sum_{h} g(f(i)) \]
This equality holds under the premise that the intersection of `s` and the set of all `x` such that `f(x) ≠ 0` is finite.
More concisely: Given additive commutative monoids M and N, set s, function f from α to M, and additive monoid homomorphism g from M to N, if the intersection of s and the support of f is finite, then g(∑j ∑h f(j)) = ∑i ∑h g(f(i)).
|
finprod_mem_union'
theorem finprod_mem_union' :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s t : Set α},
Disjoint s t →
(s ∩ Function.mulSupport f).Finite →
(t ∩ Function.mulSupport f).Finite →
(finprod fun i => finprod fun h => f i) =
(finprod fun i => finprod fun h => f i) * finprod fun i => finprod fun h => f i
This theorem, `finprod_mem_union'`, states a more generalized version of the `finprod_mem_union` theorem. It states that for any two disjoint sets `s` and `t` of a type `α`, and any function `f` from `α` to a commutative monoid `M`, if the intersection of `s` and the multiplicative support of `f`, and the intersection of `t` and the multiplicative support of `f` are both finite, then the finite product (denoted by `finprod`) over all elements considering both `s` and `t` is equal to the product of the finite product over elements of `s` and the finite product over elements of `t`. Here, the multiplicative support of `f` is the set of points `x` such that `f(x) ≠ 1`.
More concisely: For disjoint sets `s` and `t` of a type `α` and a function `f` from `α` to a commutative monoid `M` with finite intersections of `s` and `f`'s multiplicative support, and `t` and `f`'s multiplicative support, `finprod (s ∪ t) f = finprod s f ⊓ finprod t f`, where `⊓` denotes the finite product.
|
finprod_mem_image
theorem finprod_mem_image :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s : Set β} {g : β → α},
Set.InjOn g s → (finprod fun i => finprod fun h => f i) = finprod fun j => finprod fun h => f (g j)
The theorem `finprod_mem_image` states that for a given types `α`, `β`, and `M`, where `M` is a commutative monoid, and given a function `f : α → M`, a set `s` of type `β` and a function `g : β → α` that is injective on `s`, the product of `f y` over `y` in the image of `g` applied over `s` is equal to the product of `f (g i)` over `i` in `s`. In other words, the theorem says that when you first apply the function `g` to each element in `s` and then take the product of the function `f` applied to each of these results, it is the same as first taking the product of `f` applied to each element in the image of `g` over `s`.
More concisely: For injective function `g : β → α` and commutative monoid `M`, if `f : α → M` and `s` is a subset of `β`, then the product of `f (g y)` over `y` in the image of `g` equals the product of `f x` over `x` in `s`, i.e., the product of `f (g i)` over `i` in `s`.
|
finprod_mem_iUnion
theorem finprod_mem_iUnion :
∀ {α : Type u_1} {ι : Type u_3} {M : Type u_5} [inst : CommMonoid M] {f : α → M} [inst_1 : Finite ι]
{t : ι → Set α},
Pairwise (Disjoint on t) →
(∀ (i : ι), (t i).Finite) →
(finprod fun a => finprod fun h => f a) = finprod fun i => finprod fun a => finprod fun h => f a
The theorem `finprod_mem_iUnion` establishes a property of the product of a function over a union of pairwise disjoint finite sets. More specifically, given a function `f` mapping elements of some type `α` to a commutative monoid `M`, and a family of pairwise disjoint finite sets `t i` indexed by a finite type `ι`, the product of `f a` over the union of these sets is equal to the product over all indexes `i` of the products of `f a` over each `a` in `t i`. This theorem generalizes the principle of distributing multiplication over addition in the context of set union and product of function values.
More concisely: Given a commutative monoid `M`, a function `f` from a type `α` to `M`, and a family of pairwise disjoint finite sets `t i` indexed by a finite type `ι`, the product of `f` over the union of the `t i`'s equals the product over all `i` of the products of `f` over each element in `t i`.
|
Mathlib.Algebra.BigOperators.Finprod._auxAddLemma.6
theorem Mathlib.Algebra.BigOperators.Finprod._auxAddLemma.6 :
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α → M} {x : α}, (x ∈ Function.support f) = (f x ≠ 0) := by
sorry
This theorem states that for any type `α` and any type `M` that has a zero element, given a function `f` from `α` to `M` and an element `x` of type `α`, `x` is in the support of the function `f` if and only if the value of `f` at `x` is not equal to zero. In terms of mathematics, if we consider `f` as a function and `x` as a point, this theorem asserts that `x` belongs to the support of `f` precisely when `f(x)` is non-zero.
More concisely: The support of a function `f` from type `α` to type `M` with zero element, equals the set `{x : α | f x ≠ 0}`.
|
finprod_mem_union''
theorem finprod_mem_union'' :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s t : Set α},
Disjoint (s ∩ Function.mulSupport f) (t ∩ Function.mulSupport f) →
(s ∩ Function.mulSupport f).Finite →
(t ∩ Function.mulSupport f).Finite →
(finprod fun i => finprod fun h => f i) =
(finprod fun i => finprod fun h => f i) * finprod fun i => finprod fun h => f i
This theorem, `finprod_mem_union''`, states that for any commutative monoid `M`, a function `f` from a type `α` to `M`, and two sets `s` and `t` of type `α`, if the intersection of `s` and the multiplicative support of `f` is disjoint with the intersection of `t` and the multiplicative support of `f`, and if both these intersections are finite, then the product of `f i` for `i` in the union of `s` and `t` (where `f i` is not identically one) equals the product of `f i` for `i` in `s` (where `f i` is not identically one) times the product of `f i` for `i` in `t` (where `f i` is not identically one).
In other words, the theorem generalizes the principle that the total product over a union of disjoint sets is the product of the total products over each set, but the disjointness condition is specifically applied to the elements where the function `f` is not identically one.
More concisely: For any commutative monoid `M`, function `f` from a type `α` to `M`, and finite disjoint sets `s` and `t` of type `α` such that the multiplicative support of `f` intersects neither `s` nor `t` in elements where `f` is not identically one, the product of `f i` for `i` in `s ∪ t` (where `f i` is not identically one) equals the product of `f i` for `i` in `s` (where `f i` is not identically one) times the product of `f i` for `i` in `t` (where `f i` is not identically one).
|
finprod_mem_insert
theorem finprod_mem_insert :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {a : α} {s : Set α} (f : α → M),
a ∉ s → s.Finite → (finprod fun i => finprod fun h => f i) = f a * finprod fun i => finprod fun h => f i
This theorem states that for a finite set `s` of some type `α` and an element `a` of type `α` that is not in `s`, along with a function `f` from `α` to another type `M` with a commutative monoid structure, the total product of `f(i)` for each `i` in the set obtained by inserting `a` into `s` equals the product of `f(a)` and the total product of `f(i)` for each `i` in `s`. In mathematical notation, this can be written as \(\prod_{i \in s \cup \{a\}} f(i) = f(a) \prod_{i \in s} f(i)\), assuming that the product is defined as `1` for an empty set.
More concisely: For a finite set `s` of type `α`, an element `a` not in `s`, and a commutative monoid homomorphism `f` from `α` to another type `M`, we have \(\prod_{i \in s \cup \{a\}} f(i) = f(a) \prod_{i \in s} f(i)\).
|
finsum_congr
theorem finsum_congr :
∀ {M : Type u_2} {α : Sort u_4} [inst : AddCommMonoid M] {f g : α → M},
(∀ (x : α), f x = g x) → finsum f = finsum g
The theorem `finsum_congr` states that for any type `M` having addition that's commutative and associative, and any type `α`, if two functions `f` and `g` from `α` to `M` are such that they are equal at every point in `α`, then the sum of `f(x)` as `x` ranges over the elements of the support of `f`, if it's finite, is equal to the sum of `g(x)` as `x` ranges over the elements of the support of `g`, if it's finite. In other words, if two functions are equal pointwise, their finite sums over their supports are also equal.
More concisely: If `f` and `g` are two functions from a set `α` to a commutative and associative additive semigroup `M` with finite supports, and `f(x) = g(x)` for all `x ∈ α`, then `∑ (x : α) f x = ∑ (x : α) g x`.
|
AddMonoidHom.map_finsum_of_injective
theorem AddMonoidHom.map_finsum_of_injective :
∀ {M : Type u_2} {N : Type u_3} {α : Sort u_4} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] (g : M →+ N),
Function.Injective ⇑g → ∀ (f : α → M), g (finsum fun i => f i) = finsum fun i => g (f i)
This theorem states that for any types `M`, `N` and `α` (where `M` and `N` are commutative additive monoids), if we have an additive monoid homomorphism `g` from `M` to `N` that is injective, then for any function `f` from `α` to `M`, the value of `g` applied to the finite sum of `f` over all elements `i` of `α` is equal to the finite sum of `g(f(i))` over all elements `i` of `α`. In mathematical terms, this theorem is saying that the map `g` commutes with the finite sum operation.
More concisely: If `g` is an injective additive monoid homomorphism from commutative additive monoid `M` to commutative additive monoid `N`, then for any function `f` from set `α` to `M`, `g(∑ i in α f i) = ∑ i in α g(f i)`.
|
finsum_eq_of_bijective
theorem finsum_eq_of_bijective :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {g : β → M} (e : α → β),
Function.Bijective e → (∀ (x : α), f x = g (e x)) → (finsum fun i => f i) = finsum fun j => g j
This theorem, titled `finsum_eq_of_bijective`, states that for any two types `α` and `β`, and a type `M` that has an additive commutative monoid structure, given two functions `f : α → M` and `g : β → M`, and a third function `e : α → β` that is bijective (i.e., it is both injective and surjective), if for every `x` in `α`, `f(x)` is equal to `g(e(x))`, then the finite sum (`finsum`) of `f` over all `i` in `α` is equal to the finite sum (`finsum`) of `g` over all `j` in `β`. In other words, if we have a bijective function that transforms `α`s to `β`s and preserves the values of `f` and `g`, then the finite sums of `f` and `g` are equal.
More concisely: If `f : α → M`, `g : β → M`, and `e : α → β` is a bijective function such that `f(x) = g(e(x))` for all `x` in `α`, then `∑i∈α f i = ∑j∈β g j`.
|
finsum_mem_add_diff
theorem finsum_mem_add_diff :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s t : Set α},
s ⊆ t →
t.Finite →
((finsum fun i => finsum fun h => f i) + finsum fun i => finsum fun h => f i) =
finsum fun i => finsum fun h => f i
This theorem states that for any finite set `t` and any subset `s` of `t` in some type `α`, and given a function `f : α → M` where `M` is a type with addition and zero, the sum of the function `f` evaluated at each element `i` in `s` combined with the sum of the function `f` evaluated at each element `i` in `t \ s` (the set difference of `t` and `s`, i.e., elements in `t` but not in `s`) is equal to the sum of the function `f` evaluated at each element `i` in `t`. In mathematical notation, we can express this as $\sum_{i \in s} f(i) + \sum_{i \in t \setminus s} f(i) = \sum_{i \in t} f(i)$. Essentially, this theorem is the formalization of the intuitive idea of splitting a sum over a set into a sum over a subset and a sum over the complement of the subset.
More concisely: For any finite set `t` and subset `s` of type `α`, and any function `f : α → M` where `M` has addition and zero, the sum of `f` over `s` and the sum of `f` over `t \ s` equals the sum of `f` over `t`. That is, $\sum_{i \in s} f(i) + \sum_{i \in t \setminus s} f(i) = \sum_{i \in t} f(i)$.
|
finsum_mem_add_distrib
theorem finsum_mem_add_distrib :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f g : α → M} {s : Set α},
s.Finite →
(finsum fun i => finsum fun h => f i + g i) =
(finsum fun i => finsum fun h => f i) + finsum fun i => finsum fun h => g i
This theorem states that, for any finite set `s` of elements from some type `α`, and for any two functions `f` and `g` mapping from `α` to some type `M` where `M` is an additive commutative monoid, the sum of `f(i) + g(i)` for all `i` in the set `s` is equal to the sum of `f(i)` for all `i` in `s` plus the sum of `g(i)` for all `i` in `s`. This captures the distributive property of addition over finite sums.
More concisely: For any finite set `s` and functions `f` and `g` from a set `α` to an additive commutative monoid `M`, the sum of `f(i) + g(i)` for all `i` in `s` equals the sum of `f(i)` plus the sum of `g(i)`, i.e., ∑(`i` ∈ `s`).(`f(i)`) = ∑(`i` ∈ `s`).(`f(i)`) + ∑(`i` ∈ `s`).(`g(i)`).
|
finprod_mem_dvd
theorem finprod_mem_dvd :
∀ {α : Type u_1} {N : Type u_6} [inst : CommMonoid N] {f : α → N} (a : α),
(Function.mulSupport f).Finite → f a ∣ finprod f
This theorem states that given any type `α` and a type `N` that forms a commutative monoid, if the multiplicative support of a function `f` from `α` to `N` is finite, then for any element `a` of `α`, the value `f(a)` divides the finite product of `f` (denoted as `finprod f`). The multiplicative support of `f` is the set of points `x` where `f(x)` is not equal to the identity element of the monoid. The finiteness condition ensures that the product `finprod f` is well-defined. The symbol `∣` denotes the divisibility relation: `b ∣ a` means that there exists some `c` such that `a = b * c`.
More concisely: Given a commutative monoid `N` and a function `f` from type `α` to `N` with finite multiplicative support, for all `a` in `α`, `f(a)` divides the finite product `finprod f`.
|
finprod_mem_of_eqOn_one
theorem finprod_mem_of_eqOn_one :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s : Set α},
Set.EqOn f 1 s → (finprod fun i => finprod fun h => f i) = 1
The theorem `finprod_mem_of_eqOn_one` states that for any types `α` and `M`, with `M` being a commutative monoid, if a function `f` from `α` to `M` equals `1` on a set `s` of type `α` (i.e., `f(i) = 1` for all `i` in `s`), then the product of `f(i)` over all `i` in `s` is `1`. In mathematical notation, if $f(i) = 1$ for all $i \in s$, then $\prod_{i \in s}f(i) = 1$.
More concisely: If `f` is a function from a type `α` to a commutative monoid `M` such that `f(i) = 1` for all `i` in a set `s` of type `α`, then `∏ (i : s) f i = 1`.
|
finsum_cond_eq_sum_of_cond_iff
theorem finsum_cond_eq_sum_of_cond_iff :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) {p : α → Prop} {t : Finset α},
(∀ {x : α}, f x ≠ 0 → (p x ↔ x ∈ t)) → (finsum fun i => finsum fun x => f i) = t.sum fun i => f i
This theorem states that, for any types `α` and `M` where `M` is an additive commutative monoid, and for any function `f` from `α` to `M`, a predicate `p` on `α`, and a finite set `t` of `α`, if for all `x` from `α`, `f(x)` is not zero implies that `p(x)` is true if and only if `x` is in `t`, then the sum of `f(i)` for `i` ranging over all elements in the support of `f` is equal to the sum of `f(i)` for `i` ranging over all elements of `t`. This sum is calculated using the `finsum` function for the left side and the `Finset.sum` function for the right side.
More concisely: For any additive commutative monoid M, function f from type α to M, predicate p on α, and finite set t of α, if for all x in α, f(x) is non-zero implies p(x) holds if and only if x is in t, then the sum of f(x) for x in the support of f is equal to the sum of f(x) for x in t.
|
finprod_eq_prod
theorem finprod_eq_prod :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) (hf : (Function.mulSupport f).Finite),
(finprod fun i => f i) = hf.toFinset.prod fun i => f i
The theorem `finprod_eq_prod` states that for any type `α`, a type `M` that is a commutative monoid, and a function `f` from `α` to `M`, given the finite set condition `hf` which states that the set of elements `x` such that `f(x)` is not equal to 1 is finite (`Set.Finite (Function.mulSupport f)`), the product of `f(x)` as `x` ranges over the elements of the multiplicative support of `f` (`finprod fun i => f i`) equals the product of `f(x)` as `x` ranges over the elements of the finite set (`Finset.prod (Set.Finite.toFinset hf) fun i => f i`). In other words, when the multiplicative support of the function `f` is finite, the unrestricted product over the whole domain `α` is equal to the finite product over the finite set of points where `f` is not equal to 1.
More concisely: Given a commutative monoid M, a type α, and a function f from α to M with finite multiplicative support, the product of f(x) over the finite set of elements x where f(x) is not equal to 1 is equal to the product of f(x) over the entire domain α.
|
finprod_one
theorem finprod_one : ∀ {M : Type u_2} {α : Sort u_4} [inst : CommMonoid M], (finprod fun x => 1) = 1
The theorem `finprod_one` states that for any type `M` with a commutative monoid structure and any type `α`, the product, as determined by the `finprod` function, of the constant function that always yields 1 (i.e., `(fun x => 1)`) is 1. This is akin to stating that the product of 1, taken over any number of elements (possibly infinite), remains 1 in the context of a commutative monoid.
More concisely: For any commutative monoid `M` and type `α`, the constant function `(fun x => 1)` has a product of 1 according to the `finprod` function.
|
smul_finsum
theorem smul_finsum :
∀ {ι : Sort u_6} {R : Type u_7} {M : Type u_8} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : NoZeroSMulDivisors R M] (c : R) (f : ι → M), (c • finsum fun i => f i) = finsum fun i => c • f i
This theorem, `smul_finsum`, describes the interaction between scalar multiplication and finite summation in the context of a Ring and an Additive Commutative Group with a Module structure, assuming that there are no zero scalar multiplication divisors. It states that for any scalar `c` and any function `f` mapping from an arbitrary type `ι` to the group `M`, the scalar multiplication of `c` with the finite sum of `f` over its support equals the finite sum of the scalar multiplication of `c` with `f(i)` for each `i` in the support of `f`. This result holds even when the support of `f` is infinite due to the `NoZeroSMulDivisors` assumption. For a more conventional version assuming finite support of `f`, one can refer to the theorem `smul_finsum'`.
More concisely: For any ring R, additive commutative group G with a module structure over R, function f from an arbitrary type ι to G, and scalar c in R with no zero divisors, the scalar multiplication of c with the finite sum (or infinite sum under NoZeroSMulDivisors assumption) of f is equal to the finite (or infinite) sum of the scalar multiplications of c with f(i) over the support of f.
|
finprod_mem_one
theorem finprod_mem_one :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (s : Set α), (finprod fun i => finprod fun h => 1) = 1 := by
sorry
This theorem states that the product of the constant function `1`, computed over any set of any type, is equal to `1`. In other words, if you take the function that always returns `1` and compute its product using the `finprod` function over all elements of any given set, you always get `1` as the result. This holds for any types `α` and `M`, where `M` is a type that has a commutative monoid structure.
More concisely: For any commutative monoid `M` and type `α`, the product of the constant function mapping to `1` over all elements of `M` is equal to `1`.
|
smul_finsum'
theorem smul_finsum' :
∀ {ι : Type u_3} {R : Type u_7} {M : Type u_8} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(c : R) {f : ι → M}, (Function.support f).Finite → (c • finsum fun i => f i) = finsum fun i => c • f i
The theorem `smul_finsum'` states that for every index set `ι`, and for types `R` and `M` where `R` forms a semiring and `M` forms an additive commutative monoid with a module structure over `R`, given any scalar `c` from `R` and a function `f` from `ι` to `M` (which has finite support), the scalar multiplication of `c` with the finsum (the sum over the support of `f`) is equal to the finsum of the scalar multiplication of `c` with each `f i`. This means that you can 'move' a scalar multiplication outside of a finsum, as long as the support of `f` is finite. This is a version of the generalized distributive law for finsums.
More concisely: For any semiring `R`, additive commutative monoid `M` with an `R`-module structure, index set `ι`, scalar `c` in `R`, and function `f` from `ι` to `M` with finite support, we have `c * (∑ i in ι, f i) = ∑ i in ι, c * f i`.
|
finsum_mem_insert'
theorem finsum_mem_insert' :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {a : α} {s : Set α} (f : α → M),
a ∉ s →
(s ∩ Function.support f).Finite →
(finsum fun i => finsum fun h => f i) = f a + finsum fun i => finsum fun h => f i
This theorem, named `finsum_mem_insert'`, states that for any type `α` and `M` where `M` is an additive commutative monoid, a function `f` from `α` to `M`, a set `s` of type `α`, and an element `a` of type `α` that does not belong to `s`, if the intersection of `s` and the support of `f` is finite (where the support of `f` is the set of elements `x` such that `f(x) ≠ 0`), then the sum of `f(x)` over all elements `x` in the union of `s` and `{a}` (i.e. `s` with `a` inserted) is equal to `f(a)` plus the sum of `f(x)` over all elements `x` in `s`.
In mathematical notation, this theorem would read as follows: if `a ∉ s` and `s ∩ {x | f(x) ≠ 0}` is finite, then `∑_{x in s ∪ {a}} f(x) = f(a) + ∑_{x in s} f(x)`.
More concisely: For any additive commutative monoid `M`, function `f` from a set `α` to `M` with finite intersection of `α \ s` and support of `f`, and `a` not in `s`, we have `∑(x in s ∪ {a}) f(x) = f(a) + ∑(x in s) f(x)`.
|
finprod_eq_prod_of_mulSupport_subset
theorem finprod_eq_prod_of_mulSupport_subset :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) {s : Finset α},
Function.mulSupport f ⊆ ↑s → (finprod fun i => f i) = s.prod fun i => f i
The theorem `finprod_eq_prod_of_mulSupport_subset` states that for any type `α` and any commutative monoid `M`, given a function `f` from `α` to `M` and a finite set `s` of `α`, if the multiplicative support of `f` (the set of points `x` such that `f(x)` is not equal to the identity element `1`) is a subset of `s`, then the finprod of `f` (the product of `f(x)` as `x` ranges over the elements of the multiplicative support of `f`, if it's finite; `1` otherwise) is equal to the product of `f(x)` as `x` ranges over the elements of the finite set `s`. In mathematical notation, if $\{x | f(x) \neq 1\} \subseteq s$, then $\prod_{i \in \text{mulSupport}(f)} f(i) = \prod_{i \in s} f(i)$.
More concisely: If a function's multiplicative support is a subset of a finite set, then the product of the function over its multiplicative support is equal to the product of the function over that finite set.
|
finsum_mem_eq_of_bijOn
theorem finsum_mem_eq_of_bijOn :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {s : Set α} {t : Set β} {f : α → M}
{g : β → M} (e : α → β),
Set.BijOn e s t →
(∀ x ∈ s, f x = g (e x)) → (finsum fun i => finsum fun h => f i) = finsum fun j => finsum fun h => g j
This theorem states that for any types `α`, `β`, and `M` (with `M` being an additive commutative monoid), given two sets `s` of type `α` and `t` of type `β`, two functions `f : α → M` and `g : β → M`, and a function `e : α → β` that is bijective from `s` to `t`, if `f x` equals `g (e x)` for all `x` in `s`, then the sum of `f x` for each element `x` in the support of `f` equals the sum of `g y` for each element `y` in the support of `g`. The support of a function is the set of points where the function is not zero. The sum is zero if the support is not finite. This theorem mirrors the `Finset.sum_bij` theorem, which states a similar result for finite sets.
More concisely: If `s` and `t` are two sets with a bijective function `e` from `s` to `t`, `f` and `g` are functions from `s` and `t` to an additive commutative monoid `M` respectively, and `f(x) = g(e(x))` for all `x` in `s`, then the sum of `f(x)` for `x` in the support of `f` equals the sum of `g(y)` for `y` in the support of `g`.
|
finprod_div_distrib
theorem finprod_div_distrib :
∀ {α : Type u_1} {G : Type u_4} [inst : DivisionCommMonoid G] {f g : α → G},
(Function.mulSupport f).Finite →
(Function.mulSupport g).Finite → (finprod fun i => f i / g i) = (finprod fun i => f i) / finprod fun i => g i
The theorem `finprod_div_distrib` states that for any two functions `f` and `g` from a type `α` to a type `G`, where `G` is a division commutative monoid, if the multiplicative supports of `f` and `g` are both finite, then the total product of the ratios `f i / g i` for each `i` in `α` is equal to the total product of `f i` for each `i` in `α` divided by the total product of `g i` for each `i` in `α`. In other words, it states that the product of ratios equals the ratio of products when the multiplicative supports are finite.
More concisely: If `f` and `g` are functions from a finite type `α` to a commutative division monoid `G`, then `∏i∈α (fi / gi) = ∏i∈α fi / ∏i∈α gi`.
|
finsum_mem_finset_product'
theorem finsum_mem_finset_product' :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] [inst_1 : DecidableEq α]
[inst_2 : DecidableEq β] (s : Finset (α × β)) (f : α × β → M),
(finsum fun ab => finsum fun x => f ab) = finsum fun a => finsum fun b => finsum fun x => f (a, b)
This theorem, `finsum_mem_finset_product'`, states that for any types `α`, `β`, and `M` (with `M` being an additive commutative monoid), and given decidable equality on `α` and `β`, for any finite set `s` of pairs `(α, β)` and any function `f` from the pair `(α, β)` to `M`, the sum of `f` over all elements `ab` of the set is equal to the sum of `f(a, b)` over all `a` and `b`.
In other words, it's stating that we can rearrange the sums in a certain way without changing the total sum. This form of the theorem is particularly useful for iteration, for instance when we have a function `f` that is a function of multiple variables, like `α × β × γ → M`.
More concisely: Given a decidable equality on types `α` and `β`, an additive commutative monoid `M`, a finite set `s` of pairs `(α, β)`, and a function `f : α × β → M`, the sum of `f(a, b)` over all pairs `(a, b)` in `s` equals the sum of the values of `f` over all elements `ab` in the Cartesian product `∏(a ∈ s.to_list) α ⊛ ∏(b ∈ s.to_list) β`, where `⊛` denotes the Cartesian product.
|
finprod_mem_image'
theorem finprod_mem_image' :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s : Set β} {g : β → α},
Set.InjOn g (s ∩ Function.mulSupport (f ∘ g)) →
(finprod fun i => finprod fun h => f i) = finprod fun j => finprod fun h => f (g j)
The theorem `finprod_mem_image'` states that for any types `α`, `β` and `M` and a commutative monoid structure on `M`, given a function `f : α → M`, a set `s : Set β` and a function `g : β → α`, if `g` is injective on the intersection of `s` and the multiplicative support of the composition `(f ∘ g)` (which is the set of points `x` such that `(f ∘ g)(x) ≠ 1`), then the product of `f y` for `y` in the image of `g` applied to `s` equals the product of `f (g i)` for `i` in `s`.
In other words, rearranging the terms of a product according to an injective function does not change the product, as long as we only consider elements for which `f` applied to their image under `g` is not the identity of the monoid.
More concisely: Given commutative monoids type `M`, types `α` and `β`, an injective function `g : β → α`, and a function `f : α → M` such that `(f ∘ g)` has non-identity elements only on the image of `s : Set β`, then `∏[y ∈ g""(s)] f (g y) = ∏[i ∈ s] f (g i)`.
|
finprod_def
theorem finprod_def :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M)
[inst_1 : Decidable (Function.mulSupport f).Finite],
(finprod fun i => f i) = if h : (Function.mulSupport f).Finite then h.toFinset.prod fun i => f i else 1
The theorem `finprod_def` states that for any types `α` and `M`, where `M` forms a commutative monoid, and a function `f` from `α` to `M`, given that it is decidable whether the set of points where `f` does not equal one is finite (the multiplicative support of `f`), then the product of `f i` for all `i` (denoted `finprod fun i => f i`) is equivalent to: if the multiplicative support of `f` is finite, then the product of `f i` for all `i` in the finite set that represents the multiplicative support of `f`; otherwise, the result is one. In other words, the product over the entire domain is equivalent to the product over the multiplicative support when it's finite; otherwise, the result is the multiplicative identity.
More concisely: Given a function `f` from a type `α` to a commutative monoid `M` with a decidable finite multiplicative support, the product of `f i` over all `i` is equal to the product over the finite support set or the multiplicative identity if the support is infinite.
|
finsum_smul'
theorem finsum_smul' :
∀ {ι : Type u_3} {R : Type u_7} {M : Type u_8} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{f : ι → R}, (Function.support f).Finite → ∀ (x : M), (finsum fun i => f i) • x = finsum fun i => f i • x
This theorem, `finsum_smul'`, states that for any type `ι`, semiring `R`, type `M` which forms an `R`-module, and any function `f` from `ι` to `R` with finite support, the scalar multiplication of the sum of the function `f(i)` over all `i` and any element `x` from `M` is equal to the sum over all `i` of the scalar multiplication of `f(i)` and `x`. In simpler terms, it's about the interchangeability of summation and scalar multiplication in the context of `R`-modules, provided the function has finite support. This statement comes with a companion theorem `finsum_smul` that does not require finite support but imposes slightly stronger conditions.
More concisely: For any semiring `R`, type `ι`, `R`-module `M`, function `f` from `ι` to `R` with finite support, and `x` in `M`, the scalar multiplication of the sum of `f(i)` over all `i` and `x` is equal to the sum over all `i` of the scalar multiplication of `f(i)` and `x`.
|
finprod_comp
theorem finprod_comp :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] {g : β → M} (e : α → β),
Function.Bijective e → (finprod fun i => g (e i)) = finprod fun j => g j
This theorem, `finprod_comp`, states that for any types `α`, `β`, and `M`, where `M` is a commutative monoid, a function `g` from `β` to `M`, and a bijective function `e` from `α` to `β`, the finitely defined product (or `finprod`) over the function `g` composed with `e` (taking an element `i` from `α`, applying `e` to get an element of `β`, and then applying `g` to get an element of `M`) is equal to the `finprod` over the function `g` alone. In other words, the bijective function `e` doesn't affect the finitely defined product of the function `g`.
More concisely: For any commutative monoid M, bijective function e from α to β, and function g from β to M, the finite product of g and the composition of e and g is equal to the finite product of g.
|
finprod_mem_insert_one
theorem finprod_mem_insert_one :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {a : α} {s : Set α},
f a = 1 → (finprod fun i => finprod fun h => f i) = finprod fun i => finprod fun h => f i
This theorem states that if we have a function `f` from a type `α` to a type `M` (where `M` is a commutative monoid), a specific element `a` from type `α`, and a set `s` of elements of type `α`, then if `f(a)` equals 1, the product of `f(i)` for `i` in the set obtained by inserting `a` into `s` is equal to the product of `f(i)` for `i` in `s`. In other words, inserting an element that maps to the identity of the monoid does not change the product. The product is calculated using the `finprod` function, which calculates the product of `f(x)` as `x` ranges over the elements of the finite multiplicative support of `f`.
More concisely: If `f` is a function from type `α` to a commutative monoid `M` such that `f(a) = 1` for some `a` in `α`, then `∏(i ∈ s : f i) = ∏(i ∈ s ∪ {a} : f i)`, where the products are taken using the `finprod` function.
|
finsum_mem_union_inter
theorem finsum_mem_union_inter :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s t : Set α},
s.Finite →
t.Finite →
((finsum fun i => finsum fun h => f i) + finsum fun i => finsum fun h => f i) =
(finsum fun i => finsum fun h => f i) + finsum fun i => finsum fun h => f i
This theorem, `finsum_mem_union_inter`, states that for any finite sets `s` and `t` and any function `f` from a type `α` to a type `M` that forms an additive commutative monoid, the sum of the function `f` evaluated at each element in the union of `s` and `t` plus the sum of `f` evaluated at each element in the intersection of `s` and `t` is equal to the sum of `f` evaluated at each element in `s` plus the sum of `f` evaluated at each element in `t`. This can be written in mathematical notation as:
\[ \sum_{i \in s \cup t} f(i) + \sum_{i \in s \cap t} f(i) = \sum_{i \in s} f(i) + \sum_{i \in t} f(i) \]
This theorem provides a property about the summation over sets and their unions and intersections, which can be useful in various mathematical computations and proofs.
More concisely: For any finite sets $s$ and $t$ and additive commutative monoid $M$-valued function $f$ on a type, $\sum\_{i \in s \cup t} f(i) + \sum\_{i \in s \cap t} f(i) = \sum\_{i \in s} f(i) + \sum\_{i \in t} f(i)$.
|
finsum_mem_range
theorem finsum_mem_range :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {g : β → α},
Function.Injective g → (finsum fun i => finsum fun h => f i) = finsum fun j => f (g j)
The theorem `finsum_mem_range` states that for any two types `α` and `β`, and a third type `M` that forms an additive commutative monoid, given a function `f : α → M` and another function `g : β → α` which is injective, the sum of `f y` over all `y` in the range of `g` is equal to the sum of `f (g i)` over all `i`. In other words, when we apply `f` to each value in the range of `g` and add those up, it's the same as if we had applied `f` to `g i` for each `i` directly and added those up. This theorem is a statement about the rearrangement of terms in a sum, and how it doesn't affect the final result, provided that the function `g` used for indexing is injective.
More concisely: For injective functions `g : β -> α` and additive commutative monoids `M`, if `f : α -> M` is a function, then the sum of `f (g y)` over all `y` in the range of `g` equals the sum of `f y` over all `y` in the range of `g`.
|
MonoidHom.map_finprod_mem
theorem MonoidHom.map_finprod_mem :
∀ {α : Type u_1} {M : Type u_5} {N : Type u_6} [inst : CommMonoid M] [inst_1 : CommMonoid N] {s : Set α} (f : α → M)
(g : M →* N), s.Finite → g (finprod fun j => finprod fun h => f j) = finprod fun i => finprod fun h => g (f i)
This theorem states that given a monoid homomorphism `g` from `M` to `N` and a function `f` from `α` to `M`, the value of `g` at the product of `f i` for all `i` in `s` is equal to the product of `g (f i)` for all `i` in `s`, provided `s` is a finite set. In mathematical terms, if `g : M → N` is a monoid homomorphism and `f : α → M` is a function, then `g (∏_{i ∈ s} f i) = ∏_{i ∈ s} g (f i)`, when `s` is finite. This is a statement about the preservation of finite products under a monoid homomorphism.
More concisely: Given a monoid homomorphism `g: M -> N` and a finite set `s`, the product `g (∏_{i ∈ s} f i)` equals the product `∏_{i ∈ s} g (f i)`, where `f: α -> M` is a function.
|
exists_ne_zero_of_finsum_mem_ne_zero
theorem exists_ne_zero_of_finsum_mem_ne_zero :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s : Set α},
(finsum fun i => finsum fun h => f i) ≠ 0 → ∃ x ∈ s, f x ≠ 0
This theorem states that for any types `α` and `M` with `M` being an additive commutative monoid, and given a function `f` from `α` to `M` and a set `s` of elements of type `α`, if the sum (denoted by `finsum`) of `f(i)` for all `i` in the support of `f` is not zero, then there exists at least one element `x` in the set `s` such that `f(x)` is not zero. The support of a function is the set of points where the function is non-zero. Thus, this theorem makes an assertion about the existence of a non-zero value of the function over the set `s` under certain conditions.
More concisely: If `f` is a function from a type `α` to an additive commutative monoid `M` with non-empty support, and `s` is a subset of `α`, then there exists an `x` in `s` such that `f(x) ≠ 0`.
|
finprod_eq_prod_plift_of_mulSupport_subset
theorem finprod_eq_prod_plift_of_mulSupport_subset :
∀ {M : Type u_2} {α : Sort u_4} [inst : CommMonoid M] {f : α → M} {s : Finset (PLift α)},
Function.mulSupport (f ∘ PLift.down) ⊆ ↑s → (finprod fun i => f i) = s.prod fun i => f i.down
This theorem states that for any function `f` mapping from a type `α` to a commutative monoid `M`, and any finite set `s` of plifted values from `α`, if the multiplicative support of `f` composed with the plift lowering function (`PLift.down`) is a subset of the set `s`, then the infinite product (given by `finprod`) of `f i` as `i` ranges over the domain of `f` equals the finite product (`Finset.prod`) of `f i.down` as `i` ranges over the elements in `s`.
In simpler terms, this theorem provides a condition under which the infinite product of a function over its entire domain can be reduced to a finite product over a subset of the domain. The condition is that the set of points where the function doesn't produce the identity element (i.e., the multiplicative support of `f`) must be a subset of the finite set `s` considered for the finite product.
More concisely: If `f` is a function from type `α` to a commutative monoid `M`, `s` is a finite set of plifted values from `α`, and the multiplicative support of `f` composed with the plifting lowering function is a subset of `s`, then `finprod (f i) i in domain(f)` equals `Finset.prod (f i.down) i in s`.
|
finprod_mem_sUnion
theorem finprod_mem_sUnion :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {t : Set (Set α)},
t.PairwiseDisjoint id →
t.Finite →
(∀ x ∈ t, x.Finite) →
(finprod fun a => finprod fun h => f a) =
finprod fun s => finprod fun h => finprod fun a => finprod fun h => f a
This theorem states that given `t`, a finite set of pairwise disjoint finite sets, and `f` a function from a type `α` to a type `M` (where `M` forms a commutative monoid), the product of `f(a)` for all `a` in the union of `t` is equivalent to the product, over each set `s` in `t`, of the product of `f(a)` over all `a` in `s`. In essence, this theorem is expressing a rule of rearrangement for the finite product operation (denoted as `finprod`) under certain conditions.
More concisely: Given a finite set of pairwise disjoint sets `t` and a function `f` from a type to a commutative monoid, the finite product of `f(a)` over all `a` in the union of `t` is equivalent to the finite product, over each set `s` in `t`, of the finite product of `f(a)` over all `a` in `s`.
|
nonempty_of_finprod_mem_ne_one
theorem nonempty_of_finprod_mem_ne_one :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s : Set α},
(finprod fun i => finprod fun h => f i) ≠ 1 → s.Nonempty
This theorem states that for any set `s` of some type `α`, and any function `f` that maps `α` to a type `M` (where `M` forms a commutative monoid), if the product of `f(x)` over all `x` in the multiplicative support of `f` is not equal to `1`, then the set `s` is nonempty. In other words, it tells us that if the product of the function values for elements in the set is not equal to the multiplicative identity, then there must be at least one element in the set.
More concisely: If `f` is a function from a nonempty set `s` to a commutative monoid `M` such that the product of `f(x)` for all `x` in the multiplicative support of `f` is not equal to the multiplicative identity, then `s` is nonempty.
|
finprod_congr_Prop
theorem finprod_congr_Prop :
∀ {M : Type u_2} [inst : CommMonoid M] {p q : Prop} {f : p → M} {g : q → M} (hpq : p = q),
(∀ (h : q), f ⋯ = g h) → finprod f = finprod g
This theorem states that for any type `M` that forms a commutative monoid, given two propositions `p` and `q` and two functions `f` from `p` to `M` and `g` from `q` to `M`, if `p` is equivalent to `q`, and for every truth of `q` the value of `f` and `g` are equal, then the "finite product" (as defined by the `finprod` function) of `f` over its multiplicative support is equal to the "finite product" of `g` over its multiplicative support. In simpler terms, if we have two functions that are essentially defined on the same domain and take the same values, their products over their respective domains (calculated by the `finprod` function) are equal.
More concisely: Given two functions `f` and `g` from propositions `p` and `q` to a commutative monoid `M` respectively, if `p` is equivalent to `q` and for all `q', g(q') = f(q')`, then the finite products of `f` and `g` over their multiplicative supports are equal.
|
finsum_mem_empty
theorem finsum_mem_empty :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M}, (finsum fun i => finsum fun h => f i) = 0
This theorem states that the sum of any function over an empty set equals zero. In more detail, given any function `f` from a type `α` to another type `M` where `M` is an additive commutative monoid, the finite sum (`finsum`) of `f` over all elements in the empty set is zero. This is consistent with the mathematical concept that the sum of an empty set of numbers is defined to be zero.
More concisely: The sum of a function over an empty set equals zero in an additive commutative monoid.
|
finsum_eq_sum_of_support_toFinset_subset
theorem finsum_eq_sum_of_support_toFinset_subset :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) (hf : (Function.support f).Finite)
{s : Finset α}, hf.toFinset ⊆ s → (finsum fun i => f i) = s.sum fun i => f i
This theorem states that for any type `α` and `M`, where `M` is an additive commutative monoid, and any function `f` from `α` to `M`, if the support of `f` (the set of points `x` where `f(x) ≠ 0`) is a finite set, then for any finite set `s` of type `α`, if the finite set derived from the support of `f` is a subset of `s`, the sum of `f(x)` for all `x` (denoted as `finsum f`) is equal to the sum of `f(x)` for all `x` in `s` (denoted as `Finset.sum s f`). Essentially, the theorem connects the sum of a function over its support to the sum of the function over a finite set that contains the support.
More concisely: For any additive commutative monoid M, function f from type α to M with finite support, and finite set s of type α containing the support of f, the sum of f over s equals the sum of f over its support. (i.e., Finset.sum s f = finsum f)
|
finprod_mem_finset_product'
theorem finprod_mem_finset_product' :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] [inst_1 : DecidableEq α]
[inst_2 : DecidableEq β] (s : Finset (α × β)) (f : α × β → M),
(finprod fun ab => finprod fun x => f ab) = finprod fun a => finprod fun b => finprod fun x => f (a, b)
The theorem `finprod_mem_finset_product'` states that for all types `α`, `β`, and `M`, where `M` forms a commutative monoid and `α` and `β` have decidable equality, given a finite set `s` of ordered pairs of elements from `α` and `β`, and a function `f` from these pairs to `M`, the product of each `f` of `ab` (where `ab` ranges over all elements in `s`) is equal to the product over all `a` and `b`, of the product of `f` applied to the pair `(a, b)`. This implies that the finite product over the set can be iteratively computed by computing the finite product over each element in the pairs.
More concisely: For any commutative monoid M and decidably equal types α and β, the product of a function over all ordered pairs in a finite set of pairs from α x β is equal to the product of the function applied to each pair, then iteratively computed over all pairs in the set.
|
finprod_mem_union
theorem finprod_mem_union :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s t : Set α},
Disjoint s t →
s.Finite →
t.Finite →
(finprod fun i => finprod fun h => f i) =
(finprod fun i => finprod fun h => f i) * finprod fun i => finprod fun h => f i
The theorem `finprod_mem_union` states that, for any two finite and disjoint sets `s` and `t` of a certain type `α`, and for a function `f` that maps elements of `α` to elements of a commutative monoid `M`, the product of `f(i)` for all `i` in the union of `s` and `t` is equal to the product of `f(i)` for all `i` in `s` times the product of `f(i)` for all `i` in `t`. This is a generalization of the rule of product in multiplicative arithmetic where the product over the union of two disjoint sets is equal to the product of the individual sets.
More concisely: For finite, disjoint sets `s` and `t` of type `α` and a commutative monoid `M`, the function `f : α → M` satisfies `∏ i in s ⨝ i ∈ t : f i = (∏ i in s : f i) ⨝ (∏ i in t : f i)`.
|
finsum_def'
theorem finsum_def' :
∀ {M : Type u_7} {α : Sort u_8} [inst : AddCommMonoid M] (f : α → M),
finsum f = if h : (Function.support (f ∘ PLift.down)).Finite then h.toFinset.sum fun i => f i.down else 0
This theorem states that for any function `f` from a given sort `α` to a type `M` that forms an additive commutative monoid, the finite sum of `f x` for `x` in the support of `f` is defined as follows: if the support of the function `f`, when considering `x` as a lifted proposition, is a finite set, then the sum is the total of `f x.down` for `x` in the finite set equivalent to the support of `f`; otherwise, if the set is not finite, the sum is defined to be zero. Here, the `support` of a function is the set of points where the function is non-zero, `PLift.down` is a function that extracts a value from a lifted proposition, and `Finset.sum` sums up all the values of a function at points in a finite set.
More concisely: For any additive commutative monoid-valued function `f` on a sort `α`, if the support of `f` is finite, then the sum of `f x` over the support is equal to the sum of `f x.down`; otherwise, the sum is zero.
|
finprod_mem_biUnion
theorem finprod_mem_biUnion :
∀ {α : Type u_1} {ι : Type u_3} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {I : Set ι} {t : ι → Set α},
I.PairwiseDisjoint t →
I.Finite →
(∀ i ∈ I, (t i).Finite) →
(finprod fun a => finprod fun h => f a) =
finprod fun i => finprod fun h => finprod fun j => finprod fun h => f j
This theorem states that given a family of sets `t : ι → Set α` and a finite set `I` within the index type such that all sets `t i` for `i ∈ I` are finite, if all `t i` for `i ∈ I` are pairwise disjoint, then the product of `f a` for `a` in the union of all `t i` with `i ∈ I` is equal to the product over `i ∈ I` of the products of `f a` for `a` in `t i`. In mathematical terms, this is expressing the principle that the product of a function over a union of disjoint sets is equal to the product of the products over each individual set.
More concisely: Given a family of finite sets `t : ι → Set α` and a finite index set `I`, if all sets `t i` for `i ∈ I` are pairwise disjoint, then `∏(a ∈ ∪(i ∈ I) t i) f a = ∏(i ∈ I) (∏(a ∈ t i) f a)`.
|
finprod_mem_empty
theorem finprod_mem_empty :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M}, (finprod fun i => finprod fun h => f i) = 1 := by
sorry
The theorem `finprod_mem_empty` states that for any type `α`, and any type `M` where `M` has a commutative monoid structure, and any function `f` from `α` to `M`, the finitary product (denoted by `finprod`) of `f` over an empty set is `1`. In other words, when you multiply together the values of `f` for all elements in an empty set, the result is the multiplicative identity in `M`, which is `1`.
In terms of mathematical formulation, if `α` is a type, `M` is a type with a commutative monoid structure, and `f` is a function from `α` to `M`, then $\prod_{i \in \emptyset} (f(i)) = 1$.
More concisely: For any commutative monoid `M` and function `f` from a type `α` to `M`, the finitary product of `f` over the empty set equals the multiplicative identity `1` in `M`.
|
finsum_mem_zero
theorem finsum_mem_zero :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (s : Set α), (finsum fun i => finsum fun h => 0) = 0 := by
sorry
The theorem `finsum_mem_zero` states that for any given set of elements of type `α` and for any type `M` that forms an additive commutative monoid, the sum of the constant function `0` over any set equals `0`. In more formal terms, if we compute a `finsum` (finite sum) where each element of the set contributes `0` to the sum, the total sum will always be `0`, regardless of the specific types `α` and `M` or the elements of the set.
More concisely: For any set and any additive commutative monoid, the sum of the constant function mapping to 0 over that set equals 0.
|
Mathlib.Algebra.BigOperators.Finprod._auxLemma.6
theorem Mathlib.Algebra.BigOperators.Finprod._auxLemma.6 :
∀ {α : Type u_1} {M : Type u_5} [inst : One M] {f : α → M} {x : α}, (x ∈ Function.mulSupport f) = (f x ≠ 1) := by
sorry
This theorem states that for any types `α` and `M`, where `M` is a type with a one-element (`1`), and any function `f` from `α` to `M`, and any element `x` of type `α`, the element `x` is in the `mulSupport` of `f` if and only if `f(x)` is not equal to `1`. In other words, `mulSupport f` is precisely the set of points `x` in `α` such that `f(x) ≠ 1`.
More concisely: For any type `α` and function `f` from `α` to a one-element type `M`, `x` in `α` is in the support of `f` (denoted `mulSupport f`) if and only if `f(x)` is not equal to the unique element of `M`.
|
finsum_mem_eq_sum_of_inter_support_eq
theorem finsum_mem_eq_sum_of_inter_support_eq :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) {s : Set α} {t : Finset α},
s ∩ Function.support f = ↑t ∩ Function.support f → (finsum fun i => finsum fun h => f i) = t.sum fun i => f i
The theorem `finsum_mem_eq_sum_of_inter_support_eq` states that for any type `α`, `M`, any function `f` mapping from `α` to `M`, a set `s` of type `α`, and a finset `t` of type `α`, given that the intersection of `s` and the support of `f` is equal to the intersection of `t` and the support of `f`, the sum of `f(i)` for each `i` in the domain (calculated using the `finsum` function) is equal to the sum of `f(i)` for each `i` in the finset `t` (calculated using the `Finset.sum` function). Here, the support of a function `f` is the set of elements `x` such that `f(x)` is not zero. The `finsum` function calculates the sum over the support of `f` if it's finite and gives zero otherwise, while the `Finset.sum` function calculates the sum over a finite set.
More concisely: For any function `f` from type `α` to `M` and finite sets `s` and `t` of type `α` with `s ∩ supp(f) = t ∩ supp(f)`, we have `finsum f = Finset.sum (map f t)`, where `supp(f)` denotes the support of `f`.
|
finsum_mem_image'
theorem finsum_mem_image' :
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s : Set β} {g : β → α},
Set.InjOn g (s ∩ Function.support (f ∘ g)) →
(finsum fun i => finsum fun h => f i) = finsum fun j => finsum fun h => f (g j)
This theorem states that for any types `α`, `β`, and `M` (where `M` is an additive commutative monoid), a function `f` from `α` to `M`, a set `s` of type `β`, and a function `g` from `β` to `α`, if `g` is injective on the intersection of set `s` and the support of the function `f ∘ g` (where `f ∘ g` is the composition of `f` and `g`), then the sum of the values `f y` for `y` in the image of `s` under `g` is equal to the sum of the values `f (g i)` for `i` in `s`.
In mathematical terms, this can be expressed as: if $g$ is a function that is injective on $s \cap \{x | (f \circ g)(x) \neq 0\}$, then $\sum_{y \in g(s)} f(y) = \sum_{i \in s} f(g(i))$, where the sums are assumed to be finite.
More concisely: If a function `g` is injective on the intersection of its image and the support of the composition of `f` and `g` for functions `f: α -> M (M being an additive commutative monoid)` and `g: β -> α`, then the sum of `f` applied to elements in `g`'s image equals the sum of `f` applied to the images under `g` of the original set.
|
finprod_def'
theorem finprod_def' :
∀ {M : Type u_7} {α : Sort u_8} [inst : CommMonoid M] (f : α → M),
finprod f = if h : (Function.mulSupport (f ∘ PLift.down)).Finite then h.toFinset.prod fun i => f i.down else 1
The theorem `finprod_def'` states that for any type `M` with a commutative monoid structure and any function `f` from an arbitrary type `α` to `M`, the finitary product `finprod f` is defined as follows: If the multiplicative support of the function `f` composed with the function that extracts a value from a `PLift` object (i.e., `f ∘ PLift.down`) is a finite set (i.e., there exists a natural number `n` and an equivalence between this set and `Fin n`), then `finprod f` is the product of `f x` for `x` ranging over the elements of this finite set. This product is computed using the function `Finset.prod`, which takes a finite set and a function, and computes the product of the function values over the elements of the finite set. We obtain a finite set from the finite multiplicative support using the `Set.Finite.toFinset` function. On the other hand, if the multiplicative support of `f ∘ PLift.down` is not a finite set, then `finprod f` is defined to be `1` (the multiplicative identity in the commutative monoid `M`).
More concisely: If the multiplicative support of a function from an arbitrary type to a commutative monoid with a finite multiplicative support has a finite image under the extraction function, then the finitary product is the product of the function values on those images; otherwise, the finitary product is the identity element.
|
finsum_eq_sum_of_support_subset
theorem finsum_eq_sum_of_support_subset :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) {s : Finset α},
Function.support f ⊆ ↑s → (finsum fun i => f i) = s.sum fun i => f i
This theorem states that for any type `α` and `M` where `M` is an additive commutative monoid, and any function `f` from `α` to `M`, if the support of the function `f` is a subset of the elements in the finset `s`, then the sum of `f x` for all `x` in the support of `f` (denoted by `finsum`) is equal to the sum of `f x` for all `x` in the finset `s` (denoted by `Finset.sum`). Here, the support of a function is the set of points where the function is non-zero.
More concisely: For any additive commutative monoid M, type α, and function f from α to M with finite support contained in a finset s, the sum of f x over the support equals the sum of f x over s.
|
finsum_mem_insert_zero
theorem finsum_mem_insert_zero :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {a : α} {s : Set α},
f a = 0 → (finsum fun i => finsum fun h => f i) = finsum fun i => finsum fun h => f i
The theorem `finsum_mem_insert_zero` states that for any set `s` of elements of some type `α`, an element `a` of the same type, and a function `f` from `α` to another type `M` (under the condition that `M` is an additive commutative monoid), if the value of `f` at `a` is zero, then the sum of `f i` for all `i` in the set obtained by inserting `a` into `s` is the same as the sum of `f i` for all `i` in `s`. In other words, inserting a zero element under `f` doesn't affect the total sum.
More concisely: Let `s` be a set, `α` be a type, `f : α → M` a function from `α` to an additive commutative monoid `M`, and `a ∈ α` such that `f a = 0`. Then, `∑ i ∈ s.insert a (f i) = ∑ i ∈ s (f i)`.
|
finsum_mem_add_diff'
theorem finsum_mem_add_diff' :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s t : Set α},
s ⊆ t →
(t ∩ Function.support f).Finite →
((finsum fun i => finsum fun h => f i) + finsum fun i => finsum fun h => f i) =
finsum fun i => finsum fun h => f i
This theorem, `finsum_mem_add_diff'`, states that for any type `α`, a type `M` that forms an additive commutative monoid, a function `f` from `α` to `M`, and sets `s` and `t` of `α`, if `s` is a subset of `t` and the intersection of `t` and the support of `f` (the set of points `x` for which `f(x)` is not zero) is finite, then the sum of `f(x)` over all `x` in the union of `s` and `t` (disregarding repetitions) is equal to the sum of `f(x)` over all `x` in `s` plus the sum of `f(x)` over all `x` in `t` minus `s`. Here, the sums are defined as zero if the sets we are summing over are not finite.
More concisely: For any additive commutative monoid M, function f from a set α to M, finite intersections of sets s and t in α with the support of f, if s is a subset of t, then the sum of f(x) over x in s ∪ t equals the sum over x in s plus the sum over x in t minus the sum over x in s.
|
finprod_mem_union_inter
theorem finprod_mem_union_inter :
∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s t : Set α},
s.Finite →
t.Finite →
((finprod fun i => finprod fun h => f i) * finprod fun i => finprod fun h => f i) =
(finprod fun i => finprod fun h => f i) * finprod fun i => finprod fun h => f i
The theorem `finprod_mem_union_inter` states that for any two finite sets `s` and `t` of any type `α`, and a function `f` from `α` to a commutative monoid `M`, the product of `f i` over all elements `i` in the union of `s` and `t` multiplied by the product of `f i` over all elements `i` in the intersection of `s` and `t` is equal to the product of `f i` over all elements `i` in `s` multiplied by the product of `f i` over all elements `i` in `t`. In mathematical terms, it states that $\prod_{i \in s \cup t} f(i) \cdot \prod_{i \in s \cap t} f(i) = \prod_{i \in s} f(i) \cdot \prod_{i \in t} f(i)$.
More concisely: For any finite sets $s$ and $t$ and function $f$ from a commutative monoid to itself, $\prod\_{i \in s \cup t} f(i) \cdot \prod\_{i \in s \cap t} f(i) = \prod\_{i \in s} f(i) \cdot \prod\_{i \in t} f(i)$.
|