Convolution of multisets

The convolution of two multisets in an additive structure collects the sums x + y of an element of each, with multiplicity, as MeasureTheory.Measure.conv does for measures. It distributes over +, and in a commutative monoid it is commutative and associative with unit {0}, so it folds over a multiset of multisets.

Main definitions

• Multiset.conv: the convolution of two multisets.

Main results

• Multiset.conv_comm, Multiset.conv_assoc, Multiset.singleton_zero_conv: the commutative monoid laws.
• Multiset.map_conv: a map taking sums to sums of images takes convolutions to convolutions.
• Multiset.bind_map_product, Multiset.bind_conv: so does a bind taking each combination to a convolution.

def Multiset.conv {M : Type u_1} [Add M] (s t : Multiset M) : Multiset M

The convolution of two multisets: the sums of an element of each, with multiplicity.

Equations

• s.conv t = Multiset.map (fun (x : M × M) => x.1 + x.2) (s ×ˢ t)

theorem Multiset.conv_eq_bind {M : Type u_1} [Add M] (s t : Multiset M) : s.conv t = s.bind fun (x : M) => map (fun (x_1 : M) => x + x_1) t

@[simp]

theorem Multiset.zero_conv {M : Type u_1} [Add M] (t : Multiset M) : conv 0 t = 0

@[simp]

theorem Multiset.conv_zero {M : Type u_1} [Add M] (s : Multiset M) : s.conv 0 = 0

theorem Multiset.add_conv {M : Type u_1} [Add M] (s t u : Multiset M) : (s + t).conv u = s.conv u + t.conv u

theorem Multiset.conv_add {M : Type u_1} [Add M] (s t u : Multiset M) : s.conv (t + u) = s.conv t + s.conv u

@[simp]

theorem Multiset.singleton_conv {M : Type u_1} [Add M] (t : Multiset M) (x : M) : {x}.conv t = map (fun (x_1 : M) => x + x_1) t

theorem Multiset.map_conv {M : Type u_1} {N : Type u_2} [Add M] (s t : Multiset M) [Add N] {f f' g : M → N} (h : ∀ (x y : M), g (x + y) = f x + f' y) : map g (s.conv t) = (map f s).conv (map f' t)

A map taking each sum to a sum of images takes convolutions to convolutions.

theorem Multiset.bind_conv_bind {M : Type u_1} [Add M] {A : Type u_3} {B : Type u_4} (f : A → Multiset M) (g : B → Multiset M) (S : Multiset A) (T : Multiset B) : (S.bind f).conv (T.bind g) = S.bind fun (a : A) => T.bind fun (b : B) => (f a).conv (g b)

Convolving two binds convolves their values pairwise.

theorem Multiset.bind_map_product {M : Type u_1} [Add M] {A : Type u_3} {c : A → A → A} {h : A → Multiset M} (hh : ∀ (x y : A), h (c x y) = (h x).conv (h y)) (S T : Multiset A) : (map (fun (x : A × A) => c x.1 x.2) (S ×ˢ T)).bind h = (S.bind h).conv (T.bind h)

A bind taking each combination c x y to the convolution of the values at x and y takes the combinations of two multisets to the convolution of their binds.

theorem Multiset.bind_conv {M : Type u_1} [Add M] {A : Type u_3} [Add A] {h : A → Multiset M} (hh : ∀ (x y : A), h (x + y) = (h x).conv (h y)) (S T : Multiset A) : (S.conv T).bind h = (S.bind h).conv (T.bind h)

A bind taking each sum to a convolution takes convolutions to convolutions.

theorem Multiset.singleton_zero_conv {M : Type u_1} [AddZeroClass M] (s : Multiset M) : {0}.conv s = s

theorem Multiset.conv_comm {M : Type u_1} [AddCommMagma M] (s t : Multiset M) : s.conv t = t.conv s

theorem Multiset.conv_singleton_zero {M : Type u_1} [AddZeroClass M] (s : Multiset M) : s.conv {0} = s

theorem Multiset.conv_assoc {M : Type u_1} [AddSemigroup M] (s t u : Multiset M) : (s.conv t).conv u = s.conv (t.conv u)

theorem Multiset.conv_left_comm {M : Type u_1} [AddCommSemigroup M] (s t u : Multiset M) : s.conv (t.conv u) = t.conv (s.conv u)

instance Multiset.instLeftCommutativeConv {M : Type u_1} [AddCommSemigroup M] : LeftCommutative conv