Documentation

TauCeti.RingTheory.Huber.Restricted.TwoSidedSeries.Convolution

Convolution of two-sided restricted series #

The coefficient family underlying a two-sided restricted series is closed under additive convolution. For restricted families f g : ℤ → A, the coefficient at n is

∑' (i,j), i + j = n, f i * g j.

The products f i * g j tend to zero cofinitely on ℤ × ℤ; completeness of A upgrades this to summability on every addition fiber. The resulting coefficients again tend to zero: modulo an open additive subgroup, only finitely many pairs contribute, hence only their finitely many degrees can contribute.

This supplies the analytic part of multiplication on Wedhorn's A⟨X, X⁻¹⟩ (Example 6.39). This module constructs the bilinear convolution; the unit and the ring structure are built in TauCeti.RingTheory.Huber.Restricted.TwoSidedSeries.Ring.

Main results #

References #

source
theorem TauCeti.Huber.addConvolutionExists_of_mem_twoSidedRestrictedSubmodule {A : Type u_1} [Ring A] [UniformSpace A] [IsUniformAddGroup A] [NonarchimedeanRing A] [CompleteSpace A] {f g : ℤ → A} (hf : f ∈ twoSidedRestrictedSubmodule A A) (hg : g ∈ twoSidedRestrictedSubmodule A A) :
DiscreteConvolution.AddConvolutionExists (LinearMap.mul ℕ A) f g

In a complete nonarchimedean ring, the convolution coefficients of two two-sided restricted families are summable.

source
theorem TauCeti.Huber.addRingConvolution_mem_twoSidedRestrictedSubmodule {A : Type u_1} [Ring A] [TopologicalSpace A] [NonarchimedeanRing A] {f g : ℤ → A} (hf : f ∈ twoSidedRestrictedSubmodule A A) (hg : g ∈ twoSidedRestrictedSubmodule A A) :
DiscreteConvolution.addRingConvolution f g ∈ twoSidedRestrictedSubmodule A A

Additive ring convolution preserves two-sided restrictedness.

source
noncomputable def TauCeti.Huber.twoSidedRestrictedMul {A : Type u_1} [CommRing A] [UniformSpace A] [hA : IsUniformAddGroup A] [NonarchimedeanRing A] [hComplete : CompleteSpace A] [T2Space A] :
↥(twoSidedRestrictedSubmodule A A) →ₗ[A] ↥(twoSidedRestrictedSubmodule A A) →ₗ[A] ↥(twoSidedRestrictedSubmodule A A)

Multiplication convolution on two-sided restricted coefficients, as a bilinear map.

Its value is Mathlib's additive discrete convolution, restricted to the coefficient submodule by addRingConvolution_mem_twoSidedRestrictedSubmodule.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Huber.coe_twoSidedRestrictedMul {A : Type u_1} [CommRing A] [UniformSpace A] [hA : IsUniformAddGroup A] [NonarchimedeanRing A] [hComplete : CompleteSpace A] [T2Space A] (f g : ↥(twoSidedRestrictedSubmodule A A)) :
    ↑((twoSidedRestrictedMul f) g) = DiscreteConvolution.addRingConvolution ↑f ↑g

    The coefficient family of twoSidedRestrictedMul f g is the additive ring convolution of the coefficient families of f and g.

    source
    theorem TauCeti.Huber.coe_twoSidedRestrictedMul_apply {A : Type u_1} [CommRing A] [UniformSpace A] [hA : IsUniformAddGroup A] [NonarchimedeanRing A] [hComplete : CompleteSpace A] [T2Space A] (f g : ↥(twoSidedRestrictedSubmodule A A)) (n : ℤ) :
    ↑((twoSidedRestrictedMul f) g) n = ∑' (p : ↑(DiscreteConvolution.addFiber n)), ↑f (↑p).1 * ↑g (↑p).2

    The n-th coefficient of twoSidedRestrictedMul f g is the sum over pairs of degrees adding to n.

    source
    theorem TauCeti.Huber.twoSidedRestrictedMul_comm {A : Type u_1} [CommRing A] [UniformSpace A] [hA : IsUniformAddGroup A] [NonarchimedeanRing A] [hComplete : CompleteSpace A] [T2Space A] (f g : ↥(twoSidedRestrictedSubmodule A A)) :
    (twoSidedRestrictedMul f) g = (twoSidedRestrictedMul g) f

    Multiplication convolution of two-sided restricted coefficient families is commutative.