Products over filters and cartesian products of multisets #
[UPSTREAM] candidates, absent from mathlib: the Multiset analogues of Finset.prod_filter
and Finset.sum_mul_sum.
theorem
Multiset.prod_map_filter
{ι : Type u_1}
{M : Type u_2}
[CommMonoid M]
(p : ι → Prop)
[DecidablePred p]
(f : ι → M)
(s : Multiset ι)
:
(map f (filter p s)).prod = (map (fun (a : ι) => if p a then f a else 1) s).prod
The product over a filter is the product of the indicator (Finset.prod_filter
analogue).
theorem
Multiset.sum_map_filter
{ι : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
(p : ι → Prop)
[DecidablePred p]
(f : ι → M)
(s : Multiset ι)
:
(map f (filter p s)).sum = (map (fun (a : ι) => if p a then f a else 0) s).sum
The sum over a filter is the sum of the indicator (Finset.sum_filter
analogue).
theorem
Multiset.sum_map_product_mul
{α : Type u_1}
{β : Type u_2}
{M : Type u_3}
[NonUnitalNonAssocSemiring M]
(s : Multiset α)
(t : Multiset β)
(f : α → M)
(g : β → M)
:
(map (fun (p : α × β) => f p.1 * g p.2) (s ×ˢ t)).sum = (map f s).sum * (map g t).sum
Sum of a pointwise product over a cartesian product factors as a product of sums.