Zulip Chat Archive

Stream: maths

Topic: ongoing measure_theory refactor


Yury G. Kudryashov (Jan 16 2022 at 18:18):

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 (Jan 16 2022 at 18:19):

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

Sebastien Gouezel (Jan 17 2022 at 20:39):

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 (Jan 18 2022 at 06:13):

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 (Jan 18 2022 at 06:13):

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

Yury G. Kudryashov (Jan 18 2022 at 06:14):

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 (Jan 18 2022 at 11:34):

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!


Last updated: Dec 20 2023 at 11:08 UTC