Discrete convolution of cofinite-zero families

In a nonarchimedean ring, additive convolution preserves families that tend to zero along the cofinite filter, without requiring a unit or associative multiplication. When the ring is also complete, every coefficient sum in the convolution is summable. If multiplication is associative and the ring is T0, convolution of such families is associative.

Main results

• Filter.ZeroAtFilter.addConvolutionExists: cofinite-zero families have summable additive convolution coefficients in a complete nonarchimedean ring.
• Filter.ZeroAtFilter.addRingConvolution: additive ring convolution preserves convergence to zero along the cofinite filter.
• Filter.ZeroAtFilter.summable_sigma_addFiber_mul_mul: the triple products of cofinite-zero families are summable over each fibre of a + b + c = n.
• Filter.ZeroAtFilter.addRingConvolution_assoc: additive ring convolution of cofinite-zero families is associative in a complete T0 nonarchimedean ring.

theorem Filter.ZeroAtFilter.addConvolutionExists {ι : Type u_1} {A : Type u_2} [AddMonoid ι] [NonUnitalNonAssocRing A] [UniformSpace A] [IsUniformAddGroup A] [NonarchimedeanAddGroup A] [ContinuousMul A] [CompleteSpace A] {f g : ι → A} (hf : cofinite.ZeroAtFilter f) (hg : cofinite.ZeroAtFilter g) : DiscreteConvolution.AddConvolutionExists (LinearMap.mul ℕ A) f g

In a complete nonarchimedean ring, not necessarily unital or associative, every additive convolution coefficient of two families that tend to zero cofinitely is summable.

theorem Filter.ZeroAtFilter.addRingConvolution {ι : Type u_1} {A : Type u_2} [AddMonoid ι] [NonUnitalNonAssocRing A] [TopologicalSpace A] [NonarchimedeanAddGroup A] [ContinuousMul A] {f g : ι → A} (hf : cofinite.ZeroAtFilter f) (hg : cofinite.ZeroAtFilter g) : cofinite.ZeroAtFilter (DiscreteConvolution.addRingConvolution f g)

Additive ring convolution preserves convergence to zero along the cofinite filter in a nonarchimedean ring, not necessarily unital or associative.

theorem Filter.ZeroAtFilter.summable_sigma_addFiber_mul_mul {ι : Type u_1} {A : Type u_2} [AddMonoid ι] [NonUnitalNonAssocRing A] [UniformSpace A] [IsUniformAddGroup A] [NonarchimedeanAddGroup A] [ContinuousMul A] [CompleteSpace A] {f g h : ι → A} (hf : cofinite.ZeroAtFilter f) (hg : cofinite.ZeroAtFilter g) (hh : cofinite.ZeroAtFilter h) (n : ι) : Summable fun (σ : (p : ↑(DiscreteConvolution.addFiber n)) × ↑(DiscreteConvolution.addFiber (↑p).1)) => f (↑σ.snd).1 * g (↑σ.snd).2 * h (↑σ.fst).2

In a complete nonarchimedean ring, not necessarily unital or associative, the family f a * g b * h c over the triples with a + b + c = n, indexed as pairs ((a, b), c) with a + b = m and m + c = n, is summable when f, g and h tend to zero cofinitely.

theorem Filter.ZeroAtFilter.addRingConvolution_assoc {ι : Type u_1} {A : Type u_2} [AddMonoid ι] [NonUnitalRing A] [UniformSpace A] [IsUniformAddGroup A] [NonarchimedeanAddGroup A] [ContinuousMul A] [CompleteSpace A] [T0Space A] {f g h : ι → A} (hf : cofinite.ZeroAtFilter f) (hg : cofinite.ZeroAtFilter g) (hh : cofinite.ZeroAtFilter h) : DiscreteConvolution.addRingConvolution (DiscreteConvolution.addRingConvolution f g) h = DiscreteConvolution.addRingConvolution f (DiscreteConvolution.addRingConvolution g h)

In a complete T0 nonarchimedean ring, not necessarily unital, additive ring convolution of families that tend to zero cofinitely is associative. The index monoid ι need not be commutative; to rebracket longer products, ZeroAtFilter.addRingConvolution supplies the hypotheses for the partial products.