Amenability and refactoring bits of MeasureTheory?

Stream: mathlib4

[Josh Deprez]

I'm interested in adding some classical results on group amenability to mathlib4. There are several equivalent formulations, but I would like to include the equivalence of means (functionals on ℓ^∞) and finitely-additive measures (see e.g. Wagon S, The Banach-Tarski Paradox). I think some results are easier when framed in terms of finitely-additive measures.

I'm able to derive a finitely-additive measure from a mean fairly easily out of the box. But for the other direction, I would like to reuse the Lebesgue integral from MeasureTheory. MeasureTheory is (clearly) concerned with sigma algebras and countably additive measures, and I suppose I could assume DiscreteMeasurableSpace. I also found MeasureTheory.FinMeasAdditive, but I'm not sure it's set up in a useful way for my intended goal.

Would a reasonable approach be to:

• add some external "SimpleFun" structure that doesn't concern MeasurableSpace specifically, and have MeasureTheory.SimpleFunc extend it.
• define some "PreMeasure" typeclass that could be extended both by Measure and other typeclasses with different starting assumptions (perhaps PreMeasure merely requires measureOf)
• extract the definitions and lemmas regarding lintegral that don't make use of countable additivity, and have them rely on "PreMeasure" from above?

Am I on the right track? Or would it be better to just copy and modify SimpleFunc, lintegral, and the relevant lemmas?

[Aaron Liu]

We have docs#MeasureTheory.OuterMeasure

[Aaron Liu]

weakens countable additivity to countable subadditivity

[Aaron Liu]

I don't know of anything weaker than that in measure theory in mathlib

[Josh Deprez]

Thanks, I'll have a look

[Thomas Zhu]

We have docs#MeasureTheory.AddContent

[Josh Deprez]

AddContent looks promising

[Yaël Dillies]

There was a series of PRs on amenable groups to mathlib3 that never got merged. I can't seem to find it, though :thinking:

[Josh Deprez]

The ones linked from here? #new members > ✔ How to treat (ℤ,+) as a group? @ 💬

[Yaël Dillies]

Yep, that's right! Not sure why the search on github isn't finding them

[Junyan Xu]

Reported to Github: https://github.com/orgs/community/discussions/170753