Distributions on a topological monoid

We show that if G is a topological monoid, then D(G, R) inherits a convolution product from G, and that if G is locally compact, this makes D(G, R) into a ring (and C(G, R) into a module over it). Moreover, if G is abelian and compact, then D(G, R) is a commutative ring.

Convolution of a measure and a function

When G has a continuous multiplication law, we can define the convolution of a measure with a function.

def AbstractMeasure.convolveFunRight {G : Type u_1} {R : Type u_2} [TopologicalSpace G] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Monoid G] [ContinuousMul G] : AbstractMeasure G R R →ₗ[R] C(G, R) →ₗ[R] C(G, R)

For μ a measure and f a function, return the convolution of f with μ acting on the right, i.e. the function fun x ↦ ∫ y, f (x * y) dμ (bundled as a continuous map).

Equations

• AbstractMeasure.convolveFunRight = LinearMap.lcomp R C(G, R) ↑(ContinuousMap.compCLM R R { toFun := fun (p : G × G) => p.1 * p.2, continuous_toFun := ⋯ }) ∘ₗ AbstractMeasure.contractSnd

theorem AbstractMeasure.convolveFunRight_apply {G : Type u_1} {R : Type u_2} [TopologicalSpace G] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Monoid G] [ContinuousMul G] (μ : AbstractMeasure G R R) (f : C(G, R)) (x : G) : ((convolveFunRight μ) f) x = μ { toFun := fun (y : G) => f (x * y), continuous_toFun := ⋯ }

@[simp]

theorem AbstractMeasure.convolveFunRight_dirac_apply {G : Type u_1} {R : Type u_2} [TopologicalSpace G] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Monoid G] [ContinuousMul G] (x : G) (f : C(G, R)) (y : G) : ((convolveFunRight (dirac R x)) f) y = f (y * x)

@[simp]

theorem AbstractMeasure.convolveFunRight_apply_one {G : Type u_1} {R : Type u_2} [TopologicalSpace G] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Monoid G] [ContinuousMul G] (μ : AbstractMeasure G R R) (f : C(G, R)) : ((convolveFunRight μ) f) 1 = μ f

@[instance_reducible]

instance AbstractMeasure.instOne {G : Type u_1} {R : Type u_2} [TopologicalSpace G] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Monoid G] : One (AbstractMeasure G R R)

We define 1 : D(G, R) to be the Dirac measure at 1 : G (since we are writing convolution as multiplication).

Equations

• AbstractMeasure.instOne = { one := AbstractMeasure.dirac R 1 }

theorem AbstractMeasure.one_def {G : Type u_1} {R : Type u_2} [TopologicalSpace G] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Monoid G] : 1 = dirac R 1

@[simp]

theorem AbstractMeasure.one_apply {G : Type u_1} {R : Type u_2} [TopologicalSpace G] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Monoid G] (f : C(G, R)) : 1 f = f 1

@[simp]

theorem AbstractMeasure.convolveFunRight_one {G : Type u_1} {R : Type u_2} [TopologicalSpace G] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Monoid G] [ContinuousMul G] (f : C(G, R)) : (convolveFunRight 1) f = f

Convolution of two measures

@[instance_reducible]

instance AbstractMeasure.instMul {G : Type u_1} {R : Type u_2} [TopologicalSpace G] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Monoid G] [ContinuousMul G] [LocallyCompactSpace G] : Mul (AbstractMeasure G R R)

Equations

• One or more equations did not get rendered due to their size.

theorem AbstractMeasure.mul_def {G : Type u_1} {R : Type u_2} [TopologicalSpace G] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Monoid G] [ContinuousMul G] [LocallyCompactSpace G] (μ ν : AbstractMeasure G R R) : μ * ν = (map { toFun := fun (p : G × G) => p.1 * p.2, continuous_toFun := ⋯ }) ((prodMk' μ) ν)

@[instance_reducible]

instance AbstractMeasure.instNonUnitalNonAssocRing {G : Type u_1} {R : Type u_2} [TopologicalSpace G] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Monoid G] [ContinuousMul G] [LocallyCompactSpace G] : NonUnitalNonAssocRing (AbstractMeasure G R R)

Equations

• One or more equations did not get rendered due to their size.

theorem AbstractMeasure.mul_apply {G : Type u_1} {R : Type u_2} [TopologicalSpace G] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Monoid G] [ContinuousMul G] [LocallyCompactSpace G] (μ ν : AbstractMeasure G R R) (f : C(G, R)) : (μ * ν) f = μ ((convolveFunRight ν) f)

theorem AbstractMeasure.dirac_mul_dirac {G : Type u_1} {R : Type u_2} [TopologicalSpace G] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Monoid G] [ContinuousMul G] [LocallyCompactSpace G] (x y : G) : dirac R x * dirac R y = dirac R (x * y)

Convolution of Dirac measures corresponds to addition in the group.

theorem AbstractMeasure.convolveFunRight_mul {G : Type u_1} {R : Type u_2} [TopologicalSpace G] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Monoid G] [ContinuousMul G] [LocallyCompactSpace G] (μ ν : AbstractMeasure G R R) (f : C(G, R)) : (convolveFunRight (μ * ν)) f = (convolveFunRight μ) ((convolveFunRight ν) f)

@[instance_reducible]

instance AbstractMeasure.instRing {G : Type u_1} {R : Type u_2} [TopologicalSpace G] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Monoid G] [ContinuousMul G] [LocallyCompactSpace G] : Ring (AbstractMeasure G R R)

Equations

• One or more equations did not get rendered due to their size.

def AbstractMeasure.diracHom {G : Type u_1} {R : Type u_2} [TopologicalSpace G] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Monoid G] [ContinuousMul G] [LocallyCompactSpace G] : G →* AbstractMeasure G R R

The Dirac map G → D(G, R), packaged as a multiplicative homomorphism.

Equations

• AbstractMeasure.diracHom = { toFun := AbstractMeasure.dirac R, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem AbstractMeasure.diracHom_apply {G : Type u_1} {R : Type u_2} [TopologicalSpace G] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Monoid G] [ContinuousMul G] [LocallyCompactSpace G] (x : G) : diracHom x = dirac R x

@[instance_reducible]

noncomputable instance AbstractMeasure.instAlgebra {G : Type u_1} {R : Type u_2} [TopologicalSpace G] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Monoid G] [ContinuousMul G] [LocallyCompactSpace G] : Algebra R (AbstractMeasure G R R)

Measures form a R-algebra.

Equations

• AbstractMeasure.instAlgebra = Algebra.ofModule ⋯ ⋯

noncomputable def AbstractMeasure.monoidAlgebraHom {G : Type u_1} {R : Type u_2} [TopologicalSpace G] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Monoid G] [ContinuousMul G] [LocallyCompactSpace G] : MonoidAlgebra R G →ₐ[R] AbstractMeasure G R R

The canonical homomorphism from the monoid algebra R[G] to D(G, R).

Equations

• AbstractMeasure.monoidAlgebraHom = (MonoidAlgebra.lift R (AbstractMeasure G R R) G) AbstractMeasure.diracHom

@[simp]

theorem AbstractMeasure.monoidAlgebraHom_single {G : Type u_1} {R : Type u_2} [TopologicalSpace G] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Monoid G] [ContinuousMul G] [LocallyCompactSpace G] (g : G) : monoidAlgebraHom (MonoidAlgebra.single g 1) = dirac R g

@[instance_reducible]

instance AbstractMeasure.instSMulContinuousMap {G : Type u_1} {R : Type u_2} [TopologicalSpace G] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Monoid G] [ContinuousMul G] : SMul (AbstractMeasure G R R) C(G, R)

Equations

• AbstractMeasure.instSMulContinuousMap = { smul := fun (μ : AbstractMeasure G R R) => ⇑(AbstractMeasure.convolveFunRight μ) }

@[simp]

theorem AbstractMeasure.smul_def {G : Type u_1} {R : Type u_2} [TopologicalSpace G] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Monoid G] [ContinuousMul G] (μ : AbstractMeasure G R R) (a : C(G, R)) : μ • a = (convolveFunRight μ) a

@[instance_reducible]

instance AbstractMeasure.instModuleContinuousMap {G : Type u_1} {R : Type u_2} [TopologicalSpace G] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Monoid G] [ContinuousMul G] [LocallyCompactSpace G] : Module (AbstractMeasure G R R) C(G, R)

Equations

• AbstractMeasure.instModuleContinuousMap = { toSMul := AbstractMeasure.instSMulContinuousMap, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

Commutativity for compact abelian G

We show that if G is compact, Hausdorff, and commutative, then D(G, R) is a commutative ring.

The compactness and separation assumptions arise since the product of two measures is defined by an iterated integral over G × G; a Fubini-type theorem is needed to swap the order of the two integration variables. The Fubini theorem we use (AbstractMeasure.prodMk_eq_prodMk') requires the space to be compact and separated.

@[instance_reducible]

noncomputable instance AbstractMeasure.instCommRing {G : Type u_1} {R : Type u_2} [TopologicalSpace G] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CommMonoid G] [ContinuousMul G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] [T0Space R] : CommRing (AbstractMeasure G R R)

Equations

• AbstractMeasure.instCommRing = { toRing := AbstractMeasure.instRing, mul_comm := ⋯ }