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 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), ∑ (i : plift α) in h.to_finset, 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), ∏ (i : plift α) in h.to_finset, f i.down) (λ (h : ¬(function.mul_support (f ∘ plift.down)).finite), 1)
theorem
finsum_eq_sum_plift_of_support_to_finset_subset
{M : Type u_1}
{α : Sort u_3}
[add_comm_monoid M]
{f : α → M}
(hf : (function.support (f ∘ plift.down)).finite)
{s : finset (plift α)}
(hs : hf.to_finset ⊆ s) :
theorem
finprod_eq_prod_plift_of_mul_support_to_finset_subset
{M : Type u_1}
{α : Sort u_3}
[comm_monoid M]
{f : α → M}
(hf : (function.mul_support (f ∘ plift.down)).finite)
{s : finset (plift α)}
(hs : hf.to_finset ⊆ s) :
theorem
finsum_eq_sum_plift_of_support_subset
{M : Type u_1}
{α : Sort u_3}
[add_comm_monoid M]
{f : α → M}
{s : finset (plift α)}
(hs : function.support (f ∘ plift.down) ⊆ ↑s) :
theorem
finprod_eq_prod_plift_of_mul_support_subset
{M : Type u_1}
{α : Sort u_3}
[comm_monoid M]
{f : α → M}
{s : finset (plift α)}
(hs : function.mul_support (f ∘ plift.down) ⊆ ↑s) :
@[simp]
@[simp]
theorem
finprod_of_is_empty
{M : Type u_1}
{α : Sort u_3}
[comm_monoid M]
[is_empty α]
(f : α → M) :
∏ᶠ (i : α), f i = 1
theorem
finsum_of_is_empty
{M : Type u_1}
{α : Sort u_3}
[add_comm_monoid M]
[is_empty α]
(f : α → M) :
∑ᶠ (i : α), f i = 0
@[simp]
@[simp]
theorem
finsum_eq_single
{M : Type u_1}
{α : Sort u_3}
[add_comm_monoid M]
(f : α → M)
(a : α)
(ha : ∀ (x : α), x ≠ a → f x = 0) :
∑ᶠ (x : α), f x = f a
theorem
finprod_eq_single
{M : Type u_1}
{α : Sort u_3}
[comm_monoid M]
(f : α → M)
(a : α)
(ha : ∀ (x : α), x ≠ a → f x = 1) :
∏ᶠ (x : α), f x = f a
@[simp]
@[simp]
theorem
finsum_congr
{M : Type u_1}
{α : Sort u_3}
[add_comm_monoid M]
{f g : α → M}
(h : ∀ (x : α), f x = g x) :
theorem
finprod_congr
{M : Type u_1}
{α : Sort u_3}
[comm_monoid M]
{f g : α → M}
(h : ∀ (x : α), f x = g x) :
theorem
finsum_congr_Prop
{M : Type u_1}
[add_comm_monoid M]
{p q : Prop}
{f : p → M}
{g : q → M}
(hpq : p = q)
(hfg : ∀ (h : q), f _ = g h) :
theorem
finprod_congr_Prop
{M : Type u_1}
[comm_monoid M]
{p q : Prop}
{f : p → M}
{g : q → M}
(hpq : p = q)
(hfg : ∀ (h : q), f _ = g h) :
theorem
finprod_induction
{M : Type u_1}
{α : Sort u_3}
[comm_monoid M]
{f : α → M}
(p : M → Prop)
(hp₀ : p 1)
(hp₁ : ∀ (x y : M), p x → p y → p (x * y))
(hp₂ : ∀ (i : α), p (f i)) :
p (∏ᶠ (i : α), f i)
To prove a property of a finite product, it suffices to prove that the property is multiplicative and holds on multipliers.
theorem
finsum_induction
{M : Type u_1}
{α : Sort u_3}
[add_comm_monoid M]
{f : α → M}
(p : M → Prop)
(hp₀ : p 0)
(hp₁ : ∀ (x y : M), p x → p y → p (x + y))
(hp₂ : ∀ (i : α), p (f i)) :
p (∑ᶠ (i : α), f i)
To prove a property of a finite sum, it suffices to prove that the property is additive and holds on summands.
theorem
finprod_nonneg
{α : Sort u_3}
{R : Type u_1}
[ordered_comm_semiring R]
{f : α → R}
(hf : ∀ (x : α), 0 ≤ f x) :
0 ≤ ∏ᶠ (x : α), f x
theorem
finsum_nonneg
{α : Sort u_3}
{M : Type u_1}
[ordered_add_comm_monoid M]
{f : α → M}
(hf : ∀ (i : α), 0 ≤ f i) :
0 ≤ ∑ᶠ (i : α), f i
theorem
one_le_finprod'
{α : Sort u_3}
{M : Type u_1}
[ordered_comm_monoid M]
{f : α → M}
(hf : ∀ (i : α), 1 ≤ f i) :
1 ≤ ∏ᶠ (i : α), f i
theorem
monoid_hom.map_finprod_plift
{M : Type u_1}
{N : Type u_2}
{α : Sort u_3}
[comm_monoid M]
[comm_monoid N]
(f : M →* N)
(g : α → M)
(h : (function.mul_support (g ∘ plift.down)).finite) :
theorem
add_monoid_hom.map_finsum_plift
{M : Type u_1}
{N : Type u_2}
{α : Sort u_3}
[add_comm_monoid M]
[add_comm_monoid N]
(f : M →+ N)
(g : α → M)
(h : (function.support (g ∘ plift.down)).finite) :
theorem
add_monoid_hom.map_finsum_Prop
{M : Type u_1}
{N : Type u_2}
[add_comm_monoid M]
[add_comm_monoid N]
{p : Prop}
(f : M →+ N)
(g : p → M) :
theorem
monoid_hom.map_finprod_Prop
{M : Type u_1}
{N : Type u_2}
[comm_monoid M]
[comm_monoid N]
{p : Prop}
(f : M →* N)
(g : p → M) :
theorem
monoid_hom.map_finprod_of_preimage_one
{M : Type u_1}
{N : Type u_2}
{α : Sort u_3}
[comm_monoid M]
[comm_monoid N]
(f : M →* N)
(hf : ∀ (x : M), ⇑f x = 1 → x = 1)
(g : α → M) :
theorem
add_monoid_hom.map_finsum_of_preimage_zero
{M : Type u_1}
{N : Type u_2}
{α : Sort u_3}
[add_comm_monoid M]
[add_comm_monoid N]
(f : M →+ N)
(hf : ∀ (x : M), ⇑f x = 0 → x = 0)
(g : α → M) :
theorem
monoid_hom.map_finprod_of_injective
{M : Type u_1}
{N : Type u_2}
{α : Sort u_3}
[comm_monoid M]
[comm_monoid N]
(g : M →* N)
(hg : function.injective ⇑g)
(f : α → M) :
theorem
add_monoid_hom.map_finsum_of_injective
{M : Type u_1}
{N : Type u_2}
{α : Sort u_3}
[add_comm_monoid M]
[add_comm_monoid N]
(g : M →+ N)
(hg : function.injective ⇑g)
(f : α → M) :
theorem
mul_equiv.map_finprod
{M : Type u_1}
{N : Type u_2}
{α : Sort u_3}
[comm_monoid M]
[comm_monoid N]
(g : M ≃* N)
(f : α → M) :
theorem
add_equiv.map_finsum
{M : Type u_1}
{N : Type u_2}
{α : Sort u_3}
[add_comm_monoid M]
[add_comm_monoid N]
(g : M ≃+ N)
(f : α → M) :
theorem
finsum_smul
{ι : Sort u_5}
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
[no_zero_smul_divisors R M]
(f : ι → R)
(x : M) :
theorem
smul_finsum
{ι : Sort u_5}
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
[no_zero_smul_divisors R M]
(c : R)
(f : ι → M) :
theorem
finprod_eq_mul_indicator_apply
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
(s : set α)
(f : α → M)
(a : α) :
∏ᶠ (h : a ∈ s), f a = s.mul_indicator f a
theorem
finsum_eq_indicator_apply
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
(s : set α)
(f : α → M)
(a : α) :
@[simp]
@[simp]
theorem
finprod_mem_def
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
(s : set α)
(f : α → M) :
∏ᶠ (a : α) (H : a ∈ s), f a = ∏ᶠ (a : α), s.mul_indicator f a
theorem
finsum_eq_sum_of_support_subset
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
(f : α → M)
{s : finset α}
(h : function.support f ⊆ ↑s) :
∑ᶠ (i : α), f i = ∑ (i : α) in s, f i
theorem
finprod_eq_prod_of_mul_support_subset
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
(f : α → M)
{s : finset α}
(h : function.mul_support f ⊆ ↑s) :
∏ᶠ (i : α), f i = ∏ (i : α) in s, f i
theorem
finsum_eq_sum_of_support_to_finset_subset
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
(f : α → M)
(hf : (function.support f).finite)
{s : finset α}
(h : hf.to_finset ⊆ s) :
∑ᶠ (i : α), f i = ∑ (i : α) in s, f i
theorem
finprod_eq_prod_of_mul_support_to_finset_subset
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
(f : α → M)
(hf : (function.mul_support f).finite)
{s : finset α}
(h : hf.to_finset ⊆ s) :
∏ᶠ (i : α), f i = ∏ (i : α) in s, f i
theorem
finprod_def
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
(f : α → M)
[decidable (function.mul_support f).finite] :
∏ᶠ (i : α), f i = dite (function.mul_support f).finite (λ (h : (function.mul_support f).finite), ∏ (i : α) in h.to_finset, f i) (λ (h : ¬(function.mul_support f).finite), 1)
theorem
finsum_def
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
(f : α → M)
[decidable (function.support f).finite] :
∑ᶠ (i : α), f i = dite (function.support f).finite (λ (h : (function.support f).finite), ∑ (i : α) in h.to_finset, f i) (λ (h : ¬(function.support f).finite), 0)
theorem
finsum_of_infinite_support
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
(hf : (function.support f).infinite) :
∑ᶠ (i : α), f i = 0
theorem
finprod_of_infinite_mul_support
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
(hf : (function.mul_support f).infinite) :
∏ᶠ (i : α), f i = 1
theorem
finsum_eq_sum
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
(f : α → M)
(hf : (function.support f).finite) :
theorem
finprod_eq_prod
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
(f : α → M)
(hf : (function.mul_support f).finite) :
theorem
finprod_eq_prod_of_fintype
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
[fintype α]
(f : α → M) :
∏ᶠ (i : α), f i = ∏ (i : α), f i
theorem
finsum_eq_sum_of_fintype
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
[fintype α]
(f : α → M) :
∑ᶠ (i : α), f i = ∑ (i : α), f i
theorem
finsum_cond_eq_sum_of_cond_iff
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
(f : α → M)
{p : α → Prop}
{t : finset α}
(h : ∀ {x : α}, f x ≠ 0 → (p x ↔ x ∈ t)) :
∑ᶠ (i : α) (hi : p i), f i = ∑ (i : α) in t, f i
theorem
finprod_cond_eq_prod_of_cond_iff
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
(f : α → M)
{p : α → Prop}
{t : finset α}
(h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)) :
∏ᶠ (i : α) (hi : p i), f i = ∏ (i : α) in t, f i
theorem
finsum_cond_ne
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
(f : α → M)
(a : α)
[decidable_eq α]
(hf : (function.support f).finite) :
theorem
finprod_cond_ne
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
(f : α → M)
(a : α)
[decidable_eq α]
(hf : (function.mul_support f).finite) :
theorem
finsum_mem_eq_sum_of_inter_support_eq
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
(f : α → M)
{s : set α}
{t : finset α}
(h : s ∩ function.support f = ↑t ∩ function.support f) :
theorem
finprod_mem_eq_prod_of_inter_mul_support_eq
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
(f : α → M)
{s : set α}
{t : finset α}
(h : s ∩ function.mul_support f = ↑t ∩ function.mul_support f) :
theorem
finsum_mem_eq_sum_of_subset
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
(f : α → M)
{s : set α}
{t : finset α}
(h₁ : s ∩ function.support f ⊆ ↑t)
(h₂ : ↑t ⊆ s) :
theorem
finprod_mem_eq_prod_of_subset
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
(f : α → M)
{s : set α}
{t : finset α}
(h₁ : s ∩ function.mul_support f ⊆ ↑t)
(h₂ : ↑t ⊆ s) :
theorem
finsum_mem_eq_sum
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
(f : α → M)
{s : set α}
(hf : (s ∩ function.support f).finite) :
theorem
finprod_mem_eq_prod
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
(f : α → M)
{s : set α}
(hf : (s ∩ function.mul_support f).finite) :
theorem
finsum_mem_eq_sum_filter
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
(f : α → M)
(s : set α)
[decidable_pred (λ (_x : α), _x ∈ s)]
(hf : (function.support f).finite) :
∑ᶠ (i : α) (H : i ∈ s), f i = ∑ (i : α) in finset.filter (λ (_x : α), _x ∈ s) hf.to_finset, f i
theorem
finprod_mem_eq_prod_filter
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
(f : α → M)
(s : set α)
[decidable_pred (λ (_x : α), _x ∈ s)]
(hf : (function.mul_support f).finite) :
∏ᶠ (i : α) (H : i ∈ s), f i = ∏ (i : α) in finset.filter (λ (_x : α), _x ∈ s) hf.to_finset, f i
theorem
finprod_mem_eq_to_finset_prod
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
(f : α → M)
(s : set α)
[fintype ↥s] :
theorem
finsum_mem_eq_to_finset_sum
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
(f : α → M)
(s : set α)
[fintype ↥s] :
theorem
finprod_mem_eq_finite_to_finset_prod
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
(f : α → M)
{s : set α}
(hs : s.finite) :
theorem
finsum_mem_eq_finite_to_finset_sum
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
(f : α → M)
{s : set α}
(hs : s.finite) :
theorem
finprod_mem_finset_eq_prod
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
(f : α → M)
(s : finset α) :
theorem
finsum_mem_finset_eq_sum
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
(f : α → M)
(s : finset α) :
theorem
finprod_mem_coe_finset
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
(f : α → M)
(s : finset α) :
theorem
finsum_mem_coe_finset
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
(f : α → M)
(s : finset α) :
theorem
finsum_mem_eq_zero_of_infinite
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
{s : set α}
(hs : (s ∩ function.support f).infinite) :
theorem
finprod_mem_eq_one_of_infinite
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
{s : set α}
(hs : (s ∩ function.mul_support f).infinite) :
theorem
finprod_mem_eq_one_of_forall_eq_one
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
{s : set α}
(h : ∀ (x : α), x ∈ s → f x = 1) :
theorem
finsum_mem_eq_zero_of_forall_eq_zero
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
{s : set α}
(h : ∀ (x : α), x ∈ s → f x = 0) :
theorem
finprod_mem_inter_mul_support
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
(f : α → M)
(s : set α) :
∏ᶠ (i : α) (H : i ∈ s ∩ function.mul_support f), f i = ∏ᶠ (i : α) (H : i ∈ s), f i
theorem
finsum_mem_inter_support
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
(f : α → M)
(s : set α) :
∑ᶠ (i : α) (H : i ∈ s ∩ function.support f), f i = ∑ᶠ (i : α) (H : i ∈ s), f i
theorem
finprod_mem_inter_mul_support_eq
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
(f : α → M)
(s t : set α)
(h : s ∩ function.mul_support f = t ∩ function.mul_support f) :
theorem
finsum_mem_inter_support_eq
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
(f : α → M)
(s t : set α)
(h : s ∩ function.support f = t ∩ function.support f) :
theorem
finprod_mem_inter_mul_support_eq'
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
(f : α → M)
(s t : set α)
(h : ∀ (x : α), x ∈ function.mul_support f → (x ∈ s ↔ x ∈ t)) :
theorem
finsum_mem_inter_support_eq'
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
(f : α → M)
(s t : set α)
(h : ∀ (x : α), x ∈ function.support f → (x ∈ s ↔ x ∈ t)) :
theorem
finprod_mem_congr
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f g : α → M}
{s t : set α}
(h₀ : s = t)
(h₁ : ∀ (x : α), x ∈ t → f x = g x) :
theorem
finsum_mem_congr
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{f g : α → M}
{s t : set α}
(h₀ : s = t)
(h₁ : ∀ (x : α), x ∈ t → f x = g x) :
theorem
finprod_eq_one_of_forall_eq_one
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
(h : ∀ (x : α), f x = 1) :
∏ᶠ (i : α), f i = 1
theorem
finsum_eq_zero_of_forall_eq_zero
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
(h : ∀ (x : α), f x = 0) :
∑ᶠ (i : α), f i = 0
Distributivity w.r.t. addition, subtraction, and (scalar) multiplication #
theorem
finprod_mul_distrib
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f g : α → M}
(hf : (function.mul_support f).finite)
(hg : (function.mul_support g).finite) :
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 over g i.
theorem
finsum_add_distrib
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{f g : α → M}
(hf : (function.support f).finite)
(hg : (function.support g).finite) :
theorem
finsum_sub_distrib
{α : Type u_1}
{G : Type u_2}
[add_comm_group G]
{f g : α → G}
(hf : (function.support f).finite)
(hg : (function.support g).finite) :
theorem
finprod_div_distrib
{α : Type u_1}
{G : Type u_2}
[comm_group G]
{f g : α → G}
(hf : (function.mul_support f).finite)
(hg : (function.mul_support g).finite) :
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 over g i.
theorem
finprod_div_distrib₀
{α : Type u_1}
{G : Type u_2}
[comm_group_with_zero G]
{f g : α → G}
(hf : (function.mul_support f).finite)
(hg : (function.mul_support g).finite) :
theorem
finprod_mem_mul_distrib'
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f g : α → M}
{s : set α}
(hf : (s ∩ function.mul_support f).finite)
(hg : (s ∩ function.mul_support g).finite) :
A more general version of finprod_mem_mul_distrib that requires s ∩ mul_support f and
s ∩ mul_support g instead of s to be finite.
theorem
finsum_mem_add_distrib'
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{f g : α → M}
{s : set α}
(hf : (s ∩ function.support f).finite)
(hg : (s ∩ function.support g).finite) :
The product of constant one over any set equals one.
theorem
finprod_mem_of_eq_on_one
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
{s : set α}
(hf : set.eq_on f 1 s) :
If a function f equals one on a set s, then the product of f i over i ∈ s equals one.
theorem
finsum_mem_of_eq_on_zero
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
{s : set α}
(hf : set.eq_on f 0 s) :
theorem
exists_ne_one_of_finprod_mem_ne_one
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
{s : set α}
(h : ∏ᶠ (i : α) (H : i ∈ s), f i ≠ 1) :
If the product of f i over i ∈ s is not equal to one, then there is some x ∈ s
such that f x ≠ 1.
theorem
exists_ne_zero_of_finsum_mem_ne_zero
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
{s : set α}
(h : ∑ᶠ (i : α) (H : i ∈ s), f i ≠ 0) :
theorem
finprod_mem_mul_distrib
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f g : α → M}
{s : set α}
(hs : s.finite) :
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.
theorem
add_monoid_hom.map_finsum
{α : Type u_1}
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
{f : α → M}
(g : M →+ N)
(hf : (function.support f).finite) :
theorem
monoid_hom.map_finprod
{α : Type u_1}
{M : Type u_4}
{N : Type u_5}
[comm_monoid M]
[comm_monoid N]
{f : α → M}
(g : M →* N)
(hf : (function.mul_support f).finite) :
theorem
monoid_hom.map_finprod_mem'
{α : Type u_1}
{M : Type u_4}
{N : Type u_5}
[comm_monoid M]
[comm_monoid N]
{s : set α}
{f : α → M}
(g : M →* N)
(h₀ : (s ∩ function.mul_support f).finite) :
A more general version of monoid_hom.map_finprod_mem that requires s ∩ mul_support f and
instead of s to be finite.
theorem
add_monoid_hom.map_finsum_mem'
{α : Type u_1}
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
{s : set α}
{f : α → M}
(g : M →+ N)
(h₀ : (s ∩ function.support f).finite) :
theorem
monoid_hom.map_finprod_mem
{α : Type u_1}
{M : Type u_4}
{N : Type u_5}
[comm_monoid M]
[comm_monoid N]
{s : set α}
(f : α → M)
(g : M →* N)
(hs : s.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.
theorem
add_monoid_hom.map_finsum_mem
{α : Type u_1}
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
{s : set α}
(f : α → M)
(g : M →+ N)
(hs : s.finite) :
theorem
mul_equiv.map_finprod_mem
{α : Type u_1}
{M : Type u_4}
{N : Type u_5}
[comm_monoid M]
[comm_monoid N]
(g : M ≃* N)
(f : α → M)
{s : set α}
(hs : s.finite) :
theorem
add_equiv.map_finsum_mem
{α : Type u_1}
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
(g : M ≃+ N)
(f : α → M)
{s : set α}
(hs : s.finite) :
theorem
finprod_mem_inv_distrib
{α : Type u_1}
{s : set α}
{G : Type u_2}
[comm_group G]
(f : α → G)
(hs : s.finite) :
theorem
finsum_mem_neg_distrib
{α : Type u_1}
{s : set α}
{G : Type u_2}
[add_comm_group G]
(f : α → G)
(hs : s.finite) :
theorem
finprod_mem_inv_distrib₀
{α : Type u_1}
{s : set α}
{G : Type u_2}
[comm_group_with_zero G]
(f : α → G)
(hs : s.finite) :
theorem
finprod_mem_div_distrib
{α : Type u_1}
{s : set α}
{G : Type u_2}
[comm_group G]
(f g : α → G)
(hs : s.finite) :
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 product of any function over an empty set is one.
theorem
nonempty_of_finprod_mem_ne_one
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
{s : set α}
(h : ∏ᶠ (i : α) (H : i ∈ s), f i ≠ 1) :
s.nonempty
A set s is not empty if the product of some function over s is not equal to one.
theorem
nonempty_of_finsum_mem_ne_zero
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
{s : set α}
(h : ∑ᶠ (i : α) (H : i ∈ s), f i ≠ 0) :
s.nonempty
theorem
finprod_mem_union_inter
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
{s t : set α}
(hs : s.finite)
(ht : t.finite) :
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.
theorem
finprod_mem_union_inter'
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
{s t : set α}
(hs : (s ∩ function.mul_support f).finite)
(ht : (t ∩ function.mul_support f).finite) :
A more general version of finprod_mem_union_inter that requires s ∩ mul_support f and
t ∩ mul_support f instead of s and t to be finite.
theorem
finsum_mem_union_inter'
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
{s t : set α}
(hs : (s ∩ function.support f).finite)
(ht : (t ∩ function.support f).finite) :
theorem
finprod_mem_union'
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
{s t : set α}
(hst : disjoint s t)
(hs : (s ∩ function.mul_support f).finite)
(ht : (t ∩ function.mul_support f).finite) :
A more general version of finprod_mem_union that requires s ∩ mul_support f and
t ∩ mul_support f instead of s and t to be finite.
theorem
finsum_mem_union'
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
{s t : set α}
(hst : disjoint s t)
(hs : (s ∩ function.support f).finite)
(ht : (t ∩ function.support f).finite) :
theorem
finprod_mem_union
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
{s t : set α}
(hst : disjoint s t)
(hs : s.finite)
(ht : t.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.
theorem
finprod_mem_union''
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
{s t : set α}
(hst : disjoint (s ∩ function.mul_support f) (t ∩ function.mul_support f))
(hs : (s ∩ function.mul_support f).finite)
(ht : (t ∩ function.mul_support f).finite) :
A more general version of finprod_mem_union' that requires s ∩ mul_support f and
t ∩ mul_support f instead of s and t to be disjoint
theorem
finsum_mem_union''
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
{s t : set α}
(hst : disjoint (s ∩ function.support f) (t ∩ function.support f))
(hs : (s ∩ function.support f).finite)
(ht : (t ∩ function.support f).finite) :
The product of f i over i ∈ {a} equals f a.
theorem
finsum_mem_singleton
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
{a : α} :
@[simp]
@[simp]
@[simp]
@[simp]
theorem
finsum_cond_eq_right
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
{a : α} :
theorem
finsum_mem_insert'
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{a : α}
{s : set α}
(f : α → M)
(h : a ∉ s)
(hs : (s ∩ function.support f).finite) :
theorem
finprod_mem_insert'
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{a : α}
{s : set α}
(f : α → M)
(h : a ∉ s)
(hs : (s ∩ function.mul_support f).finite) :
A more general version of finprod_mem_insert that requires s ∩ mul_support f instead of
s to be finite.
theorem
finprod_mem_insert
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{a : α}
{s : set α}
(f : α → M)
(h : a ∉ s)
(hs : s.finite) :
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.
theorem
finsum_mem_insert_of_eq_zero_if_not_mem
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
{a : α}
{s : set α}
(h : a ∉ s → f a = 0) :
theorem
finprod_mem_insert_of_eq_one_if_not_mem
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
{a : α}
{s : set α}
(h : a ∉ s → f a = 1) :
If f a = 1 for all a ∉ s, then the product of f i over i ∈ insert a s equals the
product of f i over i ∈ s.
theorem
finsum_mem_insert_zero
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
{a : α}
{s : set α}
(h : f a = 0) :
theorem
finprod_mem_insert_one
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
{a : α}
{s : set α}
(h : f a = 1) :
If f a = 1, then the product of f i over i ∈ insert a s equals the product of f i over
i ∈ s.
theorem
finprod_mem_dvd
{α : Type u_1}
{N : Type u_5}
[comm_monoid N]
{f : α → N}
(a : α)
(hf : (function.mul_support f).finite) :
If the multiplicative support of f is finite, then for every x in the domain of f,
f x divides finprod f.
theorem
finprod_mem_pair
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
{a b : α}
(h : a ≠ b) :
The product of f i over i ∈ {a, b}, a ≠ b, is equal to f a * f b.
theorem
finsum_mem_pair
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
{a b : α}
(h : a ≠ b) :
theorem
finsum_mem_image'
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
{s : set β}
{g : β → α}
(hg : set.inj_on g (s ∩ function.support (f ∘ g))) :
theorem
finprod_mem_image'
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
{s : set β}
{g : β → α}
(hg : set.inj_on g (s ∩ function.mul_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).
theorem
finsum_mem_image
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
{β : Type u_2}
{s : set β}
{g : β → α}
(hg : set.inj_on g s) :
theorem
finprod_mem_image
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
{β : Type u_2}
{s : set β}
{g : β → α}
(hg : set.inj_on g 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.
theorem
finsum_mem_range'
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
{g : β → α}
(hg : set.inj_on g (function.support (f ∘ g))) :
theorem
finprod_mem_range'
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
{g : β → α}
(hg : set.inj_on g (function.mul_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).
theorem
finsum_mem_range
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
{g : β → α}
(hg : function.injective g) :
theorem
finprod_mem_range
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
{g : β → α}
(hg : function.injective 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.
theorem
finsum_mem_eq_of_bij_on
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[add_comm_monoid M]
{s : set α}
{t : set β}
{f : α → M}
{g : β → M}
(e : α → β)
(he₀ : set.bij_on e s t)
(he₁ : ∀ (x : α), x ∈ s → f x = g (e x)) :
theorem
finprod_mem_eq_of_bij_on
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[comm_monoid M]
{s : set α}
{t : set β}
{f : α → M}
{g : β → M}
(e : α → β)
(he₀ : set.bij_on e s t)
(he₁ : ∀ (x : α), x ∈ s → f x = g (e x)) :
The product of f i over s : set α is equal to the product of g j over t : set β
if there exists a function e : α → β such that e is bijective from s to t and for all
x in s we have f x = g (e x).
See also finset.prod_bij.
theorem
finprod_eq_of_bijective
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
{g : β → M}
(e : α → β)
(he₀ : function.bijective e)
(he₁ : ∀ (x : α), f x = g (e x)) :
∏ᶠ (i : α), f i = ∏ᶠ (j : β), g j
The product of f i is equal to the product of g j if there exists a bijective function
e : α → β such that for all x we have f x = g (e x).
See finprod_comp, fintype.prod_bijective and finset.prod_bij
theorem
finsum_eq_of_bijective
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
{g : β → M}
(e : α → β)
(he₀ : function.bijective e)
(he₁ : ∀ (x : α), f x = g (e x)) :
∑ᶠ (i : α), f i = ∑ᶠ (j : β), g j
theorem
finprod_comp
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[comm_monoid M]
{g : β → M}
(e : α → β)
(he₀ : function.bijective e) :
∏ᶠ (i : α), g (e i) = ∏ᶠ (j : β), g j
Given a bijective function e the product of g i is equal to the product of g (e i).
See also finprod_eq_of_bijective, fintype.prod_bijective and finset.prod_bij
theorem
finsum_comp
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[add_comm_monoid M]
{g : β → M}
(e : α → β)
(he₀ : function.bijective e) :
∑ᶠ (i : α), g (e i) = ∑ᶠ (j : β), g j
theorem
finsum_set_coe_eq_finsum_mem
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
(s : set α) :
theorem
finprod_set_coe_eq_finprod_mem
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
(s : set α) :
theorem
finsum_subtype_eq_finsum_cond
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
(p : α → Prop) :
theorem
finprod_subtype_eq_finprod_cond
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
(p : α → Prop) :
theorem
finprod_mem_inter_mul_diff'
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
{s : set α}
(t : set α)
(h : (s ∩ function.mul_support f).finite) :
theorem
finsum_mem_inter_add_diff'
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
{s : set α}
(t : set α)
(h : (s ∩ function.support f).finite) :
theorem
finprod_mem_mul_diff'
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
{s t : set α}
(hst : s ⊆ t)
(ht : (t ∩ function.mul_support f).finite) :
A more general version of finprod_mem_mul_diff that requires t ∩ mul_support f instead of
t to be finite.
theorem
finsum_mem_add_diff'
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
{s t : set α}
(hst : s ⊆ t)
(ht : (t ∩ function.support f).finite) :
theorem
finprod_mem_mul_diff
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
{s t : set α}
(hst : s ⊆ t)
(ht : t.finite) :
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.
theorem
finprod_mem_Union
{α : Type u_1}
{ι : Type u_3}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
[fintype ι]
{t : ι → set α}
(h : pairwise (disjoint on t))
(ht : ∀ (i : ι), (t i).finite) :
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.
theorem
finprod_mem_bUnion
{α : Type u_1}
{ι : Type u_3}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
{I : set ι}
{t : ι → set α}
(h : I.pairwise_disjoint t)
(hI : I.finite)
(ht : ∀ (i : ι), i ∈ I → (t i).finite) :
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.
theorem
finsum_mem_bUnion
{α : Type u_1}
{ι : Type u_3}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
{I : set ι}
{t : ι → set α}
(h : I.pairwise_disjoint t)
(hI : I.finite)
(ht : ∀ (i : ι), i ∈ I → (t i).finite) :
theorem
finprod_mem_sUnion
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
{t : set (set α)}
(h : t.pairwise_disjoint id)
(ht₀ : t.finite)
(ht₁ : ∀ (x : set α), x ∈ t → x.finite) :
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.
theorem
mul_finprod_cond_ne
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
(a : α)
(hf : (function.mul_support f).finite) :
theorem
add_finsum_cond_ne
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
(a : α)
(hf : (function.support f).finite) :
theorem
finprod_mem_comm
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[comm_monoid M]
{s : set α}
{t : set β}
(f : α → β → M)
(hs : s.finite)
(ht : t.finite) :
If s : set α and t : set β are finite sets, then the product over s commutes
with the product over t.
theorem
finprod_mem_induction
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{f : α → M}
{s : set α}
(p : M → Prop)
(hp₀ : p 1)
(hp₁ : ∀ (x y : M), p x → p y → p (x * y))
(hp₂ : ∀ (x : α), x ∈ s → p (f x)) :
p (∏ᶠ (i : α) (H : i ∈ s), f i)
To prove a property of a finite product, it suffices to prove that the property is multiplicative and holds on multipliers.
theorem
finsum_mem_induction
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{f : α → M}
{s : set α}
(p : M → Prop)
(hp₀ : p 0)
(hp₁ : ∀ (x y : M), p x → p y → p (x + y))
(hp₂ : ∀ (x : α), x ∈ s → p (f x)) :
p (∑ᶠ (i : α) (H : i ∈ s), f i)
theorem
finprod_cond_nonneg
{α : Type u_1}
{R : Type u_2}
[ordered_comm_semiring R]
{p : α → Prop}
{f : α → R}
(hf : ∀ (x : α), p x → 0 ≤ f x) :
0 ≤ ∏ᶠ (x : α) (h : p x), f x
theorem
single_le_finsum
{α : Type u_1}
{M : Type u_2}
[ordered_add_comm_monoid M]
(i : α)
{f : α → M}
(hf : (function.support f).finite)
(h : ∀ (j : α), 0 ≤ f j) :
f i ≤ ∑ᶠ (j : α), f j
theorem
single_le_finprod
{α : Type u_1}
{M : Type u_2}
[ordered_comm_monoid M]
(i : α)
{f : α → M}
(hf : (function.mul_support f).finite)
(h : ∀ (j : α), 1 ≤ f j) :
f i ≤ ∏ᶠ (j : α), f j
theorem
finprod_eq_zero
{α : Type u_1}
{M₀ : Type u_2}
[comm_monoid_with_zero M₀]
(f : α → M₀)
(x : α)
(hx : f x = 0)
(hf : (function.mul_support f).finite) :
∏ᶠ (x : α), f x = 0
theorem
finsum_sum_comm
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[add_comm_monoid M]
(s : finset β)
(f : α → β → M)
(h : ∀ (b : β), b ∈ s → (function.support (λ (a : α), f a b)).finite) :
∑ᶠ (a : α), ∑ (b : β) in s, f a b = ∑ (b : β) in s, ∑ᶠ (a : α), f a b
theorem
finprod_prod_comm
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[comm_monoid M]
(s : finset β)
(f : α → β → M)
(h : ∀ (b : β), b ∈ s → (function.mul_support (λ (a : α), f a b)).finite) :
∏ᶠ (a : α), ∏ (b : β) in s, f a b = ∏ (b : β) in s, ∏ᶠ (a : α), f a b
theorem
sum_finsum_comm
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[add_comm_monoid M]
(s : finset α)
(f : α → β → M)
(h : ∀ (a : α), a ∈ s → (function.support (f a)).finite) :
∑ (a : α) in s, ∑ᶠ (b : β), f a b = ∑ᶠ (b : β), ∑ (a : α) in s, f a b
theorem
prod_finprod_comm
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[comm_monoid M]
(s : finset α)
(f : α → β → M)
(h : ∀ (a : α), a ∈ s → (function.mul_support (f a)).finite) :
∏ (a : α) in s, ∏ᶠ (b : β), f a b = ∏ᶠ (b : β), ∏ (a : α) in s, f a b
theorem
mul_finsum
{α : Type u_1}
{R : Type u_2}
[semiring R]
(f : α → R)
(r : R)
(h : (function.support f).finite) :
theorem
finsum_mul
{α : Type u_1}
{R : Type u_2}
[semiring R]
(f : α → R)
(r : R)
(h : (function.support f).finite) :
theorem
finset.mul_support_of_fiberwise_prod_subset_image
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[comm_monoid M]
[decidable_eq β]
(s : finset α)
(f : α → M)
(g : α → β) :
function.mul_support (λ (b : β), (finset.filter (λ (a : α), g a = b) s).prod f) ⊆ ↑(finset.image g s)
theorem
finset.support_of_fiberwise_sum_subset_image
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[add_comm_monoid M]
[decidable_eq β]
(s : finset α)
(f : α → M)
(g : α → β) :
function.support (λ (b : β), (finset.filter (λ (a : α), g a = b) s).sum f) ⊆ ↑(finset.image g s)
theorem
finsum_mem_finset_product'
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[add_comm_monoid M]
[decidable_eq α]
[decidable_eq β]
(s : finset (α × β))
(f : α × β → M) :
∑ᶠ (ab : α × β) (h : ab ∈ s), f ab = ∑ᶠ (a : α) (b : β) (h : b ∈ finset.image prod.snd (finset.filter (λ (ab : α × β), ab.fst = a) s)), f (a, b)
theorem
finprod_mem_finset_product'
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[comm_monoid M]
[decidable_eq α]
[decidable_eq β]
(s : finset (α × β))
(f : α × β → M) :
∏ᶠ (ab : α × β) (h : ab ∈ s), f ab = ∏ᶠ (a : α) (b : β) (h : b ∈ finset.image prod.snd (finset.filter (λ (ab : α × β), ab.fst = a) s)), f (a, b)
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.
theorem
finsum_mem_finset_product
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[add_comm_monoid M]
(s : finset (α × β))
(f : α × β → M) :
theorem
finprod_mem_finset_product
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[comm_monoid M]
(s : finset (α × β))
(f : α × β → M) :
See also finprod_mem_finset_product'.
theorem
finprod_curry
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[comm_monoid M]
(f : α × β → M)
(hf : (function.mul_support f).finite) :
theorem
finsum_curry
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[add_comm_monoid M]
(f : α × β → M)
(hf : (function.support f).finite) :
theorem
finsum_curry₃
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[add_comm_monoid M]
{γ : Type u_3}
(f : α × β × γ → M)
(h : (function.support f).finite) :
theorem
finprod_curry₃
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[comm_monoid M]
{γ : Type u_3}
(f : α × β × γ → M)
(h : (function.mul_support f).finite) :
theorem
finprod_dmem
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{s : set α}
[decidable_pred (λ (_x : α), _x ∈ s)]
(f : Π (a : α), a ∈ s → M) :
theorem
finsum_dmem
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{s : set α}
[decidable_pred (λ (_x : α), _x ∈ s)]
(f : Π (a : α), a ∈ s → M) :
theorem
finprod_emb_domain'
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[comm_monoid M]
{f : α → β}
(hf : function.injective f)
[decidable_pred (λ (_x : β), _x ∈ set.range f)]
(g : α → M) :
theorem
finsum_emb_domain'
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[add_comm_monoid M]
{f : α → β}
(hf : function.injective f)
[decidable_pred (λ (_x : β), _x ∈ set.range f)]
(g : α → M) :
theorem
finprod_emb_domain
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[comm_monoid M]
(f : α ↪ β)
[decidable_pred (λ (_x : β), _x ∈ set.range ⇑f)]
(g : α → M) :
theorem
finsum_emb_domain
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[add_comm_monoid M]
(f : α ↪ β)
[decidable_pred (λ (_x : β), _x ∈ set.range ⇑f)]
(g : α → M) :