Type of SFinite measures

Stream: Is there code for X?

[Josha Dekker]

How would I denote the type of SFinite measures on a monoid M? I'm interested in establishing that these form a MulZeroOneClass (or a related structure), but I cannot write MulZeroOneClass (Measure M), as that would not use the restriction that the measures should be SFinite. Is there some way to restrict this to some prop? The following shows my idea, but I know that this is not the way to go, as SFiniteMeas is a set of measures here.

import Mathlib.MeasureTheory.Constructions.Prod.Basic
import Mathlib.MeasureTheory.Measure.MeasureSpace

namespace MeasureTheory

namespace Measure

def SFiniteMeas {M : Type*} [Monoid M] [MeasurableSpace M] : Set (Measure M) :=
  {μ | SFinite μ}

instance {M : Type*} [Monoid M] [MeasurableSpace M] [MeasurableMul₂ M] : MulZeroOneClass (SFiniteMeas M) where
  sorry

[Yury G. Kudryashov]

If we're going to use more measure subtypes, then we may want to do the FunLike refactor for (outer) measures.

[Josha Dekker]

So you mean that it is better to wait until that is added? I'm fine with waiting a bit with adding this.

[Yury G. Kudryashov]

As a temporary solution, you may use def SFiniteMeasure (α : Type*) [MeasurableSpace M] : Type _ := {μ // SFinite μ}

[Rémy Degenne]

You can define a type of SFinite measures like that, and show some properties of it. But I am not sure that defining such a type is really useful. For example, we only defined a type for finite measures because we wanted to put a topology on the space of finite measures, and for everything else we just work on a measure together with the IsFiniteMeasure property.

What makes you want a new type, instead of simply proving things about measures with the SFinite property?

[Josha Dekker]

I just thought it would be nice to encode the basic properties of convolution of measures (has a 0, has a 1, acts as a multiplication) in something like a MulZeroOneClass, I didn't have a particular goal in mind yet. The reason for this is that in order to get the results that I currently have in #9372, you'd need to assume that the measures are SFinite; which is why I thought it would be nice to encode it in a type in the first place.

[Josha Dekker]

I think it is better that I don't think too much about these things at this point anyway and just focus on building some more results for convolutions.