Finite products and sums over types and sets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We define products and sums over types and subsets of types, with no finiteness hypotheses.
All infinite products and sums are defined to be junk values (i.e. one or zero).
This approach is sometimes easier to use than finset.sum,
when issues arise with finset and fintype being data.
Main definitions #
We use the following variables:
α,β- types with no structure;s,t- setsM,N- additive or multiplicative commutative monoidsf,g- functions
Definitions in this file:
-
finsum f : M: the sum off xasxranges over the support off, if it's finite. Zero otherwise. -
finprod f : M: the product off xasxranges over the multiplicative support off, if it's finite. One otherwise.
Notation #
This notation works for functions f : p → M, where p : Prop, so the following works:
∑ᶠ i ∈ s, f i, wheref : α → M,s : set α: sum over the sets;∑ᶠ n < 5, f n, wheref : ℕ → M: same asf 0 + f 1 + f 2 + f 3 + f 4;∏ᶠ (n >= -2) (hn : n < 3), f n, wheref : ℤ → M: same asf (-2) * f (-1) * f 0 * f 1 * f 2.
Implementation notes #
finsum and finprod is "yet another way of doing finite sums and products in Lean". However
experiments in the wild (e.g. with matroids) indicate that it is a helpful approach in settings
where the user is not interested in computability and wants to do reasoning without running into
typeclass diamonds caused by the constructive finiteness used in definitions such as finset and
fintype. By sticking solely to set.finite we avoid these problems. We are aware that there are
other solutions but for beginner mathematicians this approach is easier in practice.
Another application is the construction of a partition of unity from a collection of “bump” function. In this case the finite set depends on the point and it's convenient to have a definition that does not mention the set explicitly.
The first arguments in all definitions and lemmas is the codomain of the function of the big
operator. This is necessary for the heuristic in @[to_additive].
See the documentation of to_additive.attr for more information.
We did not add is_finite (X : Type) : Prop, because it is simply nonempty (fintype X).
Tags #
finsum, finprod, finite sum, finite product
Definition and relation to finset.sum and finset.prod #
Sum of f x as x ranges over the elements of the support of f, if it's finite. Zero
otherwise.
Equations
- finsum f = dite (function.support (f ∘ plift.down)).finite (λ (h : (function.support (f ∘ plift.down)).finite), h.to_finset.sum (λ (i : plift α), f i.down)) (λ (h : ¬(function.support (f ∘ plift.down)).finite), 0)
Product of f x as x ranges over the elements of the multiplicative support of f, if it's
finite. One otherwise.
Equations
- finprod f = dite (function.mul_support (f ∘ plift.down)).finite (λ (h : (function.mul_support (f ∘ plift.down)).finite), h.to_finset.prod (λ (i : plift α), f i.down)) (λ (h : ¬(function.mul_support (f ∘ plift.down)).finite), 1)
To prove a property of a finite product, it suffices to prove that the property is multiplicative and holds on the factors.
To prove a property of a finite sum, it suffices to prove that the property is additive and holds on the summands.
Distributivity w.r.t. addition, subtraction, and (scalar) multiplication #
If the multiplicative supports of f and g are finite, then the product of f i * g i equals
the product of f i multiplied by the product of g i.
If the additive supports of f and g are finite, then the sum of f i + g i
equals the sum of f i plus the sum of g i.
If the additive supports of f and g are finite, then the sum of f i - g i
equals the sum of f i minus the sum of g i.
If the multiplicative supports of f and g are finite, then the product of f i / g i
equals the product of f i divided by the product of g i.
A more general version of finprod_mem_mul_distrib that only requires s ∩ mul_support f and
s ∩ mul_support g rather than s to be finite.
A more general version of finsum_mem_add_distrib that only requires s ∩ support f
and s ∩ support g rather than s to be finite.
The product of the constant function 1 over any set equals 1.
The product of the constant function 0 over any set equals 0.
If the product of f i over i ∈ s is not equal to 1, then there is some x ∈ s such that
f x ≠ 1.
If the product of f i over i ∈ s is not equal to 0, then there is some x ∈ s
such that f x ≠ 0.
Given a finite set s, the product of f i * g i over i ∈ s equals the product of f i
over i ∈ s times the product of g i over i ∈ s.
Given a finite set s, the sum of f i + g i over i ∈ s equals the sum of f i
over i ∈ s plus the sum of g i over i ∈ s.
A more general version of monoid_hom.map_finprod_mem that requires s ∩ mul_support f rather
than s to be finite.
A more general version of add_monoid_hom.map_finsum_mem that requires
s ∩ support f rather than s to be finite.
Given a monoid homomorphism g : M →* N and a function f : α → M, the value of g at the
product of f i over i ∈ s equals the product of g (f i) over s.
Given an additive monoid homomorphism g : M →* N and a function f : α → M, the
value of g at the sum of f i over i ∈ s equals the sum of g (f i) over s.
Given a finite set s, the product of f i / g i over i ∈ s equals the product of f i
over i ∈ s divided by the product of g i over i ∈ s.
Given a finite set s, the sum of f i / g i over i ∈ s equals the sum of f i
over i ∈ s minus the sum of g i over i ∈ s.
∏ᶠ x ∈ s, f x and set operations #
Given finite sets s and t, the sum of f i over i ∈ s ∪ t plus the sum of
f i over i ∈ s ∩ t equals the sum of f i over i ∈ s plus the sum of f i over i ∈ t.
Given finite sets s and t, the product of f i over i ∈ s ∪ t times the product of
f i over i ∈ s ∩ t equals the product of f i over i ∈ s times the product of f i
over i ∈ t.
A more general version of finprod_mem_union_inter that requires s ∩ mul_support f and
t ∩ mul_support f rather than s and t to be finite.
A more general version of finsum_mem_union_inter that requires s ∩ support f and
t ∩ support f rather than s and t to be finite.
A more general version of finprod_mem_union that requires s ∩ mul_support f and
t ∩ mul_support f rather than s and t to be finite.
A more general version of finsum_mem_union that requires s ∩ support f and
t ∩ support f rather than s and t to be finite.
Given two finite disjoint sets s and t, the product of f i over i ∈ s ∪ t equals the
product of f i over i ∈ s times the product of f i over i ∈ t.
Given two finite disjoint sets s and t, the sum of f i over i ∈ s ∪ t equals
the sum of f i over i ∈ s plus the sum of f i over i ∈ t.
A more general version of finprod_mem_union' that requires s ∩ mul_support f and
t ∩ mul_support f rather than s and t to be disjoint
A more general version of finsum_mem_union' that requires s ∩ support f and
t ∩ support f rather than s and t to be disjoint
The product of f i over i ∈ {a} equals f a.
The sum of f i over i ∈ {a} equals f a.
A more general version of finsum_mem_insert that requires s ∩ support f rather
than s to be finite.
A more general version of finprod_mem_insert that requires s ∩ mul_support f rather than s
to be finite.
Given a finite set s and an element a ∉ s, the sum of f i over i ∈ insert a s
equals f a plus the sum of f i over i ∈ s.
Given a finite set s and an element a ∉ s, the product of f i over i ∈ insert a s equals
f a times the product of f i over i ∈ s.
If f a = 0 when a ∉ s, then the sum of f i over i ∈ insert a s equals the sum
of f i over i ∈ s.
If f a = 1 when a ∉ s, then the product of f i over i ∈ insert a s equals the product of
f i over i ∈ s.
If f a = 0, then the sum of f i over i ∈ insert a s equals the sum of f i
over i ∈ s.
If f a = 1, then the product of f i over i ∈ insert a s equals the product of f i over
i ∈ s.
If the multiplicative support of f is finite, then for every x in the domain of f, f x
divides finprod f.
The sum of f y over y ∈ g '' s equals the sum of f (g i) over s provided that
g is injective on s ∩ support (f ∘ g).
The product of f y over y ∈ g '' s equals the product of f (g i) over s
provided that g is injective on s ∩ mul_support (f ∘ g).
The sum of f y over y ∈ g '' s equals the sum of f (g i) over s provided that
g is injective on s.
The product of f y over y ∈ g '' s equals the product of f (g i) over s provided that
g is injective on s.
The sum of f y over y ∈ set.range g equals the sum of f (g i) over all i
provided that g is injective on support (f ∘ g).
The product of f y over y ∈ set.range g equals the product of f (g i) over all i
provided that g is injective on mul_support (f ∘ g).
The sum of f y over y ∈ set.range g equals the sum of f (g i) over all i
provided that g is injective.
The product of f y over y ∈ set.range g equals the product of f (g i) over all i
provided that g is injective.
See also finset.sum_bij.
See also finset.prod_bij.
See finprod_comp, fintype.prod_bijective and finset.prod_bij.
See finsum_comp, fintype.sum_bijective and finset.sum_bij.
See also finprod_eq_of_bijective, fintype.prod_bijective and finset.prod_bij.
See also finsum_eq_of_bijective, fintype.sum_bijective and finset.sum_bij.
A more general version of finprod_mem_mul_diff that requires t ∩ mul_support f rather than
t to be finite.
A more general version of finsum_mem_add_diff that requires t ∩ support f rather
than t to be finite.
Given a finite set t and a subset s of t, the sum of f i over i ∈ s plus
the sum of f i over t \ s equals the sum of f i over i ∈ t.
Given a finite set t and a subset s of t, the product of f i over i ∈ s
times the product of f i over t \ s equals the product of f i over i ∈ t.
Given a family of pairwise disjoint finite sets t i indexed by a finite type, the
sum of f a over the union ⋃ i, t i is equal to the sum over all indexes i of the sums of f a
over a ∈ t i.
Given a family of pairwise disjoint finite sets t i indexed by a finite type, the product of
f a over the union ⋃ i, t i is equal to the product over all indexes i of the products of
f a over a ∈ t i.
Given a family of sets t : ι → set α, a finite set I in the index type such that all sets
t i, i ∈ I, are finite, if all t i, i ∈ I, are pairwise disjoint, then the product of f a
over a ∈ ⋃ i ∈ I, t i is equal to the product over i ∈ I of the products of f a over
a ∈ t i.
Given a family of sets t : ι → set α, a finite set I in the index type such that
all sets t i, i ∈ I, are finite, if all t i, i ∈ I, are pairwise disjoint, then the sum of
f a over a ∈ ⋃ i ∈ I, t i is equal to the sum over i ∈ I of the sums of f a over
a ∈ t i.
If t is a finite set of pairwise disjoint finite sets, then the sum of f a over
a ∈ ⋃₀ t is the sum over s ∈ t of the sums of f a over a ∈ s.
If t is a finite set of pairwise disjoint finite sets, then the product of f a
over a ∈ ⋃₀ t is the product over s ∈ t of the products of f a over a ∈ s.
To prove a property of a finite product, it suffices to prove that the property is multiplicative and holds on factors.
To prove a property of a finite sum, it suffices to prove that the property is additive and holds on summands.
Note that b ∈ (s.filter (λ ab, prod.fst ab = a)).image prod.snd iff (a, b) ∈ s so
we can simplify the right hand side of this lemma. However the form stated here is more useful for
iterating this lemma, e.g., if we have f : α × β × γ → M.
Note that b ∈ (s.filter (λ ab, prod.fst ab = a)).image prod.snd iff (a, b) ∈ s so we can
simplify the right hand side of this lemma. However the form stated here is more useful for
iterating this lemma, e.g., if we have f : α × β × γ → M.
See also finsum_mem_finset_product'.
See also finprod_mem_finset_product'.