Is `MeasurableSMul` useful?

Stream: mathlib4

[David Loeffler]

For actions of a group (or monoid) G on a measurable space X, there are 3 typeclasses about the measurability of the action:

• MeasurableConstSMul : x ↦ g • x is measurable for each g
• MeasurableSMul : x ↦ g • x is measurable for each g, and g ↦ g • x measurable for each x
• MeasurableSMul₂ : (g, x) ↦ g • x is measurable (this is strictly stronger than MeasurableSMul)

The first doesn't require a measurable-space structure on G, only on X, while the other two require measurable-space structures on both.

While experimenting with how to define the SL2R-invariant measure on the upper half-plane, I realised that for something like 90% of the theorems in Mathlib that had MeasurableSMul as hypothesis, the measurability in g isn't needed and the theorems worked fine with MeasurableConstSMul (avoiding the necessity of fixing a measurable-space structure on G). This modification is in PRs #33659 and #33710; thanks @Rémy Degenne for the quick review on those.

This makes me wonder: is MeasurableSMul actually needed at all? Perhaps it might be simpler to get rid of the existing MeasurableSMul and re-name what's currently called MeasurableSMul₂ to MeasurableSMul. This would be consistent with the existing ContinuousSMul (which asserts joint continuity G × X → X, not continuity in either argument separately). Any thoughts?

[Rémy Degenne]

If I remember correctly, there is one result somewhere in Mathlib that uses MeasurableSMul becauses it wants the second condition in that typeclass (but not the first), but we don't have a MeasurableSMulConst. Now I need to remember which result that was.
That does not answer your questions at all, but that's related.

[David Loeffler]

I guess that would be docs#Measurable.smul_const (and its cousin docs#AEMeasurable.smul_const)

[Rémy Degenne]

Right, there is that one. I was thinking about another, but it's possibly just because it's using this.

[Eric Wieser]

MeasurableConstSMul was probably introduced much later, FWIW

[David Loeffler]

I think I may have found out the answer to my question, after having a go at replacing MeasurableSMul instances with MeasurableSMul₂.

If G, X are topological spaces satisfying ContinuousSMul G X, and we give both of them the Borel measurable-space structure, then MeasurableSMul is automatic; but MeasurableSMul₂ isn't -- it needs an additional assumption, that one of G, X be second-countable, in order to ensure that the product measurable-space structure on G × X is Borel.

So I guess that's a good reason for keeping the existing MeasurableSMul. Sorry for the noise!

[Kevin Buzzard]

We even have a typeclass for "either G or X is second countable", which I found to my surprise a few months ago :-)