Finite products and sums over types and sets #
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 IsFinite (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 #
Equations
- One or more equations did not get rendered due to their size.
Instances For
∑ᶠ x, f x is notation for finsum f. It is the sum of f x, where x ranges over the
support of f, if it's finite, zero otherwise. Taking the sum over multiple arguments or
conditions is possible, e.g. ∏ᶠ (x) (y), f x y and ∏ᶠ (x) (h: x ∈ s), f x
Equations
- One or more equations did not get rendered due to their size.
Instances For
∏ᶠ x, f x is notation for finprod f. It is the sum of f x, where x ranges over the
multiplicative support of f, if it's finite, one otherwise. Taking the product over multiple
arguments or conditions is possible, e.g. ∏ᶠ (x) (y), f x y and ∏ᶠ (x) (h: x ∈ s), f x
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
To prove a property of a finite sum, it suffices to prove that the property is additive and holds on the summands.
To prove a property of a finite product, it suffices to prove that the property is multiplicative and holds on the factors.
The NoZeroSMulDivisors makes sure that the result holds even when the support of f is
infinite. For a more usual version assuming (support f).Finite instead, see finsum_smul'.
The NoZeroSMulDivisors makes sure that the result holds even when the support of f is
infinite. For a more usual version assuming (support f).Finite instead, see smul_finsum'.
Distributivity w.r.t. addition, subtraction, and (scalar) multiplication #
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 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 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 finsum_mem_add_distrib that only requires s ∩ support f
and s ∩ support g rather than s to be finite.
A more general version of finprod_mem_mul_distrib that only requires s ∩ mulSupport f and
s ∩ mulSupport g rather than s to be finite.
The product of the constant function 0 over any set equals 0.
The product of the constant function 1 over any set equals 1.
If a function f equals 0 on a set s, then the product of f i over i ∈ s
equals 0.
If a function f equals 1 on a set s, then the product of f i over i ∈ s equals 1.
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.
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.
See also finsum_smul for a version that works even when the support of f is not finite,
but with slightly stronger typeclass requirements.
See also smul_finsum for a version that works even when the support of f is not finite,
but with slightly stronger typeclass requirements.
A more general version of AddMonoidHom.map_finsum_mem that requires
s ∩ support f rather than s to be finite.
A more general version of MonoidHom.map_finprod_mem that requires s ∩ mulSupport f rather
than s to be finite.
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 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 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.
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.
∏ᶠ x ∈ s, f x and set operations #
The sum of any function over an empty set is 0.
The product of any function over an empty set is 1.
A set s is nonempty if the sum of some function over s is not equal to 0.
A set s is nonempty if the product of some function over s is not equal to 1.
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 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_inter that requires s ∩ mulSupport f and
t ∩ mulSupport 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.
A more general version of finprod_mem_union that requires s ∩ mulSupport f and
t ∩ mulSupport f rather than s and t to be finite.
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.
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.
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
A more general version of finprod_mem_union' that requires s ∩ mulSupport f and
t ∩ mulSupport f rather than s and t to be disjoint
The sum of f i over i ∈ {a} equals f a.
The product 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 ∩ mulSupport 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 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 i over i ∈ {a, b}, a ≠ b, is equal to f a + f b.
The product of f i over i ∈ {a, b}, a ≠ b, is equal to f a * f b.
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 ∩ mulSupport (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 mulSupport (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 finsum_comp, Fintype.sum_bijective and Finset.sum_bij.
See finprod_comp, Fintype.prod_bijective and Finset.prod_bij.
See also finsum_eq_of_bijective, Fintype.sum_bijective and Finset.sum_bij.
See also finprod_eq_of_bijective, Fintype.prod_bijective and Finset.prod_bij.
A more general version of finsum_mem_add_diff that requires t ∩ support f rather
than t to be finite.
A more general version of finprod_mem_mul_diff that requires t ∩ mulSupport 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
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.
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.
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.
If s : Set α and t : Set β are finite sets, then summing over s commutes with
summing over t.
If s : Set α and t : Set β are finite sets, then taking the product over s commutes with
taking the product over t.
To prove a property of a finite sum, it suffices to prove that the property is additive and holds on summands.
To prove a property of a finite product, it suffices to prove that the property is multiplicative and holds on factors.
Note that b ∈ (s.filter (fun 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 (fun 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'.