Trivial MeasurableSpaces

Stream: maths

[Aaron Anderson]

While working on the Polynomial Freiman-Ruzsa project, I was mildly annoyed that I had to explicitly create an instance of [MeasurableSub₂] for a finite measure space where everything's measurable.

[Aaron Anderson]

It wasn't hard to prove - the assumptions are all there to use measurable_of_countable _, but given that in, say, combinatorics, people often care about finite regimes where measurability is trivial, would it be useful to create a typeclass for such measure spaces?

[Aaron Anderson]

This would have solved my particular use-case, because [MeasurableSpace X] [Fintype X] [MeasurableSingletonClass X] could be shown to imply [TrivialMeasurableSpace (X × X)] or whatever we want to call it, and that would imply [MeasurableSub₂ X].

[Yaël Dillies]

Surely the name should rather be DiscreteMeasurableSpace?

[Yaël Dillies]

I think that makes sense. We have DiscreteTopology.

[Aaron Anderson]

I'm trying it out over at #8859.

[Aaron Anderson]

I'd appreciate some help resolving some heartbeat issues, if anyone wants to take a look.

[Yaël Dillies]

FYI, #8859 is ready for review. This is one of the early prerequisites for PFR.