Monoids with non additive or multiplicative notation

Stream: maths

[David Ledvinka]

Is there anyway to use monoid theorems and lemmas for a monoid that doesn't use additive or multiplicative notation or does everything need to be reproved?

My specific use case is that the SFinite measures on a monoid should form a monoid under measure convolution (defined here). Note that additive notation is taken by setwise sum of measures.

I would like to be able to define notation for the equivalent of Finset.prod and then use all the results for it.

[Aaron Liu]

You can make a local instance of monoid

[Yaël Dillies]

How have you decided to talk about the type of s-finite measures?

[David Ledvinka]

That's a good point. I hadn't thought of this detail. For my purposes it would suffice to define this on the type ProbabilityMeasure but this doesn't seem ideal.

I don't yet have a very good intuition for these type theory considerations. Perhaps to be even more specific if I want to state and prove facts like: the convolution of $n$ Gaussians is a Gaussian or the law of the sum of $n$ independent random variables is the convolution of their laws, how would I best go about this?

[Yaël Dillies]

Naïvely, I think you want to define an analogue of docs#Finset.prod for the convolution. The approach you envision of reusing Finset.prod would only work if you were working on a type of measures where all convolutions make sense. This goes against the basic design decision we've made in measure theory to work with docs#MeasureTheory.Measure as much as possible.

[David Ledvinka]

Well its convolution is always defined, its just not a monoid (and infact I just realized that Finset.prod assumes its a CommMonoid which I did not realize previously). How does one state theorems like this in a non commutative monoid even?

[Yaël Dillies]

docs#Finset.noncommProd, which is somewhat unwieldy as it requires you to pass around a proof that the elements you take a product over all commute

[Yaël Dillies]

David Ledvinka said:

I just realized that Finset.prod assumes its a CommMonoid

Indeed, that's the whole issue: docs#MeasureTheory.Measure.mconv_comm only holds for s-finite measures

[David Ledvinka]

Well associativity as well but I didn't even want to assume even commutative.

As an application (way down the line) if you want to study random walks on groups you use the fact the distribution of $X_n$ is given by the $n$ convolution power of the step distribution.

[David Ledvinka]

Ah I realized I am being imprecise and need to take something ordered instead of finset for that to make sense

[David Ledvinka]

So if I have X : Fin n → M where M is a non-commutative monoid is there a concise way to express $X_0 * X_1 ... X_{n-1}$ currently?

[Aaron Liu]

Do a docs#List.prod with docs#List.finRange

[Edward van de Meent]

via Lists

[David Ledvinka]

So I guess perhaps the best approach is to define List.conv? And you say for example the law of the product of a list of random variables is equal to List.conv of their laws?

[Yaël Dillies]

But are you going to take the convolution of non s-finite measures?

[David Ledvinka]

This is what I had in mind.

noncomputable def List.mconv := List.foldl (fun (μ₁ μ₂ : Measure M) ↦ μ₁ ∗ₘ μ₂) (dirac 1)

It won't be well-behaved for non s-Finite measures but its defined.

[Yaël Dillies]

I strongly advise you take s : Finset ι + μ : ι → Measure Ω in instead of l : List (Measure Ω) (you can recover l as s.toList.map μ, see docs#Finset.toList). This is much more ergonomic in practice

[David Ledvinka]

Sorry I am confused. Are you suggesting I essentially do just define an analogue of Finset.prod that works for convolution from scratch? Or just define this as an API on top of the List.mconv definition? The former doesn't work if I want to include non commutative monoids.

[David Ledvinka]

I just (for the first time) looked at the definition of Finset.prod and it appears to reduce down to folding on lists too anyway. So I guess you just mean there should be an API for Finsets?

[Yaël Dillies]

Oh I see, you really care about non-commutative monoids. In that case yes you should use lists

[Aaron Liu]

maybe you could write a type synonym

[Eric Wieser]

Is it common to take elementwise products and convolutive products at the same time? Is it common to take elementwise products and convolutive products at the same time?

[Eric Wieser]

We solve this elsewhere by having Finsupp for pointwise multiplication vs docs#AddMonoidAlgebra to enable multiplication-as-convolution, since it's very rare to have both in the same statement.

[David Ledvinka]

Eric Wieser said:

Is it common to take elementwise products and convolutive products at the same time? Is it common to take elementwise products and convolutive products at the same time?

Most likely no so this seems promising to me (it will take me sometime to understand whats going on here though).

[Antoine Chambert-Loir]

Eric Wieser said:

Is it common to take elementwise products and convolutive products at the same time? Is it common to take elementwise products and convolutive products at the same time?

What about the Fourier transform of a convolution product of two integrable functions , which is the product of their Fourier transforms?

[David Ledvinka]

Antoine Chambert-Loir said:

Eric Wieser said:

Is it common to take elementwise products and convolutive products at the same time? Is it common to take elementwise products and convolutive products at the same time?

What about the Fourier transform of a convolution product of two integrable functions , which is the product of their Fourier transforms?

For my purposes here this is not an issue since I want to take convolution of measures and their Fourier Transforms are functions. If you want to do the same thing for functions it may be problematic.

[David Ledvinka]

I think there may still however be cases where this comes up, say convolution with a mixture distribution. However I assume they are relatively rare.

[Antoine Chambert-Loir]

David Ledvinka said:

If you want to do the same thing for functions it may be problematic.

Some people might want to do this, yes…