ongoing measure_theory refactor

Stream: maths

[Yury G. Kudryashov]

Hi, I'm working on a refactor of measure_theory/measure (I have a half-ready branch and I'm cherry-picking changes to PRs). My goals are:

• split the huge file measure_space.lean into smaller pieces;
• drop measurable_set assumptions here and there.

[Yury G. Kudryashov]

If someone else is going to refactor measure_space, then please talk to me first.

[Sebastien Gouezel]

I have just PRed a bunch of small changes, cherry picked from a bigger branch on the change of variable formula in integrals. One of these PRs touches measure_theory/measure and may interfere with your refactor, sorry (it's #11529).

[Yury G. Kudryashov]

One more trick to consider about measure_to_measurable_inter: if you only want μ (s ∩ t) = μ (s' ∩ t) for countably many measurable ts, then we have docs#measure_theory.exists_measurable_superset_forall_eq.

[Yury G. Kudryashov]

And it doesn't need any measure to be (sigma) finite.

[Yury G. Kudryashov]

In nonempty_inter_of_measure_lt_add you need only one of s, t to be measurable, see better measure_union in #11536

[Sebastien Gouezel]

Yury G. Kudryashov said:

In nonempty_inter_of_measure_lt_add you need only one of s, t to be measurable, see better measure_union in #11536

Done. As for docs#measure_theory.exists_measurable_superset_forall_eq, in my use case I need uncountably many sets (balls of arbitrary radius) and my measure is already sigma-finite, but I agree your trick is worthwile in other situations!