OuterMeasure constructors

Stream: maths

[Yury G. Kudryashov]

We have three very similar constructors for an out measure:

• docs#MeasureTheory.OuterMeasure.boudedBy returns the maximal outer measure such that μ s ≤ f s for all s;
• docs#MeasureTheory.OuterMeasure.ofFunction does the same but assumes f ∅ = 0 to have a better defeq;
• docs#MeasureTheory.inducedOuterMeasure returns the maximal outer measure such that μ s ≤ f s for all s satisfying a predicate P.

I suggest that we

• rename inducedOuterMeasure to OuterMeasure.boundedByOn, possibly taking a set of sets instead of a predicate;
• drop docs#MeasureTheory.extend unless it is needed for something else.
• define boundedBy as boundedByOn Set.univ
• drop ofFunction, assume f ∅ = 0 in lemmas that need it.

What do you think?

[Rémy Degenne]

Can you give more details on how you want to change inducedOuterMeasure once you remove extend? Perhaps give code for the definitions that would remain.

@Peter Pfaffelhuber and I used extend in the definitions of a project, notably in this file: https://github.com/RemyDegenne/kolmogorov_extension4/blob/master/KolmogorovExtension4/Content.lean
That repository contains a proof of Kolmogorov's extension theorem and is supposed to be merged to Mathlib one day, but that process is currently slow. I think I used extend mostly because that was used in inducedOuterMeasure, so I am definitely not saying that extend is an essential part of those definitions, and most probably your new way of writing it could be used also there.