Single-point families and associativity of discrete convolution

Mathlib's DiscreteConvolution.single_convolution says that Pi.single 1 e is a unit for convolution when e acts as one. More generally, the convolution of two families supported at one point each is supported at the product of the points, with the bilinear map applied to the values.

Mathlib has no associativity for DiscreteConvolution.ringConvolution. Both bracketings of f ⋆ᵣ g ⋆ᵣ h are sums of f a * g b * h c over the triples with a * b * c = x, grouped in two ways; when that triple family is summable and each inner convolution sum converges, the two groupings agree.

Main results

• DiscreteConvolution.single_convolution_single and its additive version DiscreteConvolution.single_addConvolution_single: Pi.single m a ⋆[L] Pi.single n b = Pi.single (m * n) (L a b).
• DiscreteConvolution.single_ringConvolution_single and its additive version DiscreteConvolution.single_addRingConvolution_single: Pi.single m a ⋆ᵣ Pi.single n b = Pi.single (m * n) (a * b).
• DiscreteConvolution.ringConvolution_assoc and its additive version DiscreteConvolution.addRingConvolution_assoc: ring convolution is associative when the triple family and the inner convolutions are summable.

@[simp]

theorem DiscreteConvolution.single_convolution_single {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [Monoid M] [DecidableEq M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [AddCommMonoid F] [Module S E] [Module S E'] [Module S F] [TopologicalSpace F] (L : E →ₗ[S] E' →ₗ[S] F) (m n : M) (a : E) (b : E') : convolution L (Pi.single m a) (Pi.single n b) = Pi.single (m * n) ((L a) b)

The convolution of two single-point families is a single-point family, at the product of the points and with the bilinear map applied to the values.

@[simp]

theorem DiscreteConvolution.single_addConvolution_single {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [AddMonoid M] [DecidableEq M] [CommSemiring S] [AddCommMonoid E] [AddCommMonoid E'] [AddCommMonoid F] [Module S E] [Module S E'] [Module S F] [TopologicalSpace F] (L : E →ₗ[S] E' →ₗ[S] F) (m n : M) (a : E) (b : E') : addConvolution L (Pi.single m a) (Pi.single n b) = Pi.single (m + n) ((L a) b)

@[simp]

theorem DiscreteConvolution.single_ringConvolution_single {M : Type u_1} {R : Type u_6} [Monoid M] [DecidableEq M] [NonUnitalNonAssocSemiring R] [TopologicalSpace R] (m n : M) (a b : R) : ringConvolution (Pi.single m a) (Pi.single n b) = Pi.single (m * n) (a * b)

The ring convolution of two single-point families is a single-point family, at the product of the points and with the product of the values.

@[simp]

theorem DiscreteConvolution.single_addRingConvolution_single {M : Type u_1} {R : Type u_6} [AddMonoid M] [DecidableEq M] [NonUnitalNonAssocSemiring R] [TopologicalSpace R] (m n : M) (a b : R) : addRingConvolution (Pi.single m a) (Pi.single n b) = Pi.single (m + n) (a * b)

theorem DiscreteConvolution.ringConvolution_assoc {M : Type u_1} {R : Type u_2} [Monoid M] [NonUnitalSemiring R] [TopologicalSpace R] [IsTopologicalSemiring R] [T3Space R] {f g h : M → R} (hfg : ConvolutionExists (LinearMap.mul ℕ R) f g) (hgh : ConvolutionExists (LinearMap.mul ℕ R) g h) (hfgh : ∀ (x : M), Summable fun (σ : (p : ↑(mulFiber x)) × ↑(mulFiber (↑p).1)) => f (↑σ.snd).1 * g (↑σ.snd).2 * h (↑σ.fst).2) : ringConvolution (ringConvolution f g) h = ringConvolution f (ringConvolution g h)

Ring convolution is associative when the family f a * g b * h c over the triples with a * b * c = x is summable for every x, and so are the convolution sums of f with g and of g with h. The triples are indexed as pairs ((a, b), c) with a * b = m and m * c = x.

theorem DiscreteConvolution.addRingConvolution_assoc {M : Type u_1} {R : Type u_2} [AddMonoid M] [NonUnitalSemiring R] [TopologicalSpace R] [IsTopologicalSemiring R] [T3Space R] {f g h : M → R} (hfg : AddConvolutionExists (LinearMap.mul ℕ R) f g) (hgh : AddConvolutionExists (LinearMap.mul ℕ R) g h) (hfgh : ∀ (x : M), Summable fun (σ : (p : ↑(addFiber x)) × ↑(addFiber (↑p).1)) => f (↑σ.snd).1 * g (↑σ.snd).2 * h (↑σ.fst).2) : addRingConvolution (addRingConvolution f g) h = addRingConvolution f (addRingConvolution g h)

Additive ring convolution is associative when the family f a * g b * h c over the triples with a + b + c = x is summable for every x, and so are the convolution sums of f with g and of g with h. The triples are indexed as pairs ((a, b), c) with a + b = m and m + c = x.