Regular measures #

A measure is OuterRegular if the measure of any measurable set A is the infimum of μ U over all open sets U containing A.

A measure is Regular if it satisfies the following properties:

it is finite on compact sets;
it is outer regular;
it is inner regular for open sets with respect to compacts sets: the measure of any open set U is the supremum of μ K over all compact sets K contained in U.

A measure is WeaklyRegular if it satisfies the following properties:

it is outer regular;
it is inner regular for open sets with respect to closed sets: the measure of any open set U is the supremum of μ F over all closed sets F contained in U.

In a Hausdorff topological space, regularity implies weak regularity. These three conditions are registered as typeclasses for a measure μ, and this implication is recorded as an instance.

In order to avoid code duplication, we also define a measure μ to be InnerRegular for sets satisfying a predicate q with respect to sets satisfying a predicate p if for any set U ∈ {U | q U} and a number r < μ U there exists F ⊆ U such that p F and r < μ F.

We prove that inner regularity for open sets with respect to compact sets or closed sets implies inner regularity for all measurable sets of finite measure (with respect to compact sets or closed sets respectively), and register some corollaries for (weakly) regular measures.

Note that a similar statement for measurable sets of infinite mass can fail. For a counterexample, consider the group ℝ × ℝ where the first factor has the discrete topology and the second one the usual topology. It is a locally compact Hausdorff topological group, with Haar measure equal to Lebesgue measure on each vertical fiber. The set ℝ × {0} has infinite measure (by outer regularity), but any compact set it contains has zero measure (as it is finite).

Several authors require as a definition of regularity that all measurable sets are inner regular. We have opted for the slightly weaker definition above as it holds for all Haar measures, it is enough for essentially all applications, and it is equivalent to the other definition when the measure is finite.

The interest of the notion of weak regularity is that it is enough for many applications, and it is automatically satisfied by any finite measure on a metric space.

Main definitions #

MeasureTheory.Measure.OuterRegular μ: a typeclass registering that a measure μ on a topological space is outer regular.
MeasureTheory.Measure.Regular μ: a typeclass registering that a measure μ on a topological space is regular.
MeasureTheory.Measure.WeaklyRegular μ: a typeclass registering that a measure μ on a topological space is weakly regular.
MeasureTheory.Measure.InnerRegular μ p q: a non-typeclass predicate saying that a measure μ is inner regular for sets satisfying q with respect to sets satisfying p.

Main results #

Outer regular measures #

Set.measure_eq_iInf_isOpen asserts that, when μ is outer regular, the measure of a set is the infimum of the measure of open sets containing it.
Set.exists_isOpen_lt_of_lt asserts that, when μ is outer regular, for every set s and r > μ s there exists an open superset U ⊇ s of measure less than r.
push forward of an outer regular measure is outer regular, and scalar multiplication of a regular measure by a finite number is outer regular.

Weakly regular measures #

IsOpen.measure_eq_iSup_isClosed asserts that the measure of an open set is the supremum of the measure of closed sets it contains.
IsOpen.exists_lt_isClosed: for an open set U and r < μ U, there exists a closed F ⊆ U of measure greater than r;
MeasurableSet.measure_eq_iSup_isClosed_of_ne_top asserts that the measure of a measurable set of finite measure is the supremum of the measure of closed sets it contains.
MeasurableSet.exists_lt_isClosed_of_ne_top and MeasurableSet.exists_isClosed_lt_add: a measurable set of finite measure can be approximated by a closed subset (stated as r < μ F and μ s < μ F + ε, respectively).
MeasureTheory.Measure.WeaklyRegular.of_pseudoEMetricSpace_of_isFiniteMeasure is an instance registering that a finite measure on a metric space is weakly regular (in fact, a pseudo emetric space is enough);
MeasureTheory.Measure.WeaklyRegular.of_pseudoEMetric_secondCountable_of_locallyFinite is an instance registering that a locally finite measure on a second countable metric space (or even a pseudo emetric space) is weakly regular.

Regular measures #

IsOpen.measure_eq_iSup_isCompact asserts that the measure of an open set is the supremum of the measure of compact sets it contains.
IsOpen.exists_lt_isCompact: for an open set U and r < μ U, there exists a compact K ⊆ U of measure greater than r;
MeasurableSet.measure_eq_iSup_isCompact_of_ne_top asserts that the measure of a measurable set of finite measure is the supremum of the measure of compact sets it contains.
MeasurableSet.exists_lt_isCompact_of_ne_top and MeasurableSet.exists_isCompact_lt_add: a measurable set of finite measure can be approximated by a compact subset (stated as r < μ K and μ s < μ K + ε, respectively).
MeasureTheory.Measure.Regular.of_sigmaCompactSpace_of_isLocallyFiniteMeasure is an instance registering that a locally finite measure on a σ-compact metric space is regular (in fact, an emetric space is enough).

Implementation notes #

The main nontrivial statement is MeasureTheory.Measure.InnerRegular.weaklyRegular_of_finite, expressing that in a finite measure space, if every open set can be approximated from inside by closed sets, then the measure is in fact weakly regular. To prove that we show that any measurable set can be approximated from inside by closed sets and from outside by open sets. This statement is proved by measurable induction, starting from open sets and checking that it is stable by taking complements (this is the point of this condition, being symmetrical between inside and outside) and countable disjoint unions.

Once this statement is proved, one deduces results for σ-finite measures from this statement, by restricting them to finite measure sets (and proving that this restriction is weakly regular, using again the same statement).

References #

[Halmos, Measure Theory, §52][halmos1950measure]. Note that Halmos uses an unusual definition of Borel sets (for him, they are elements of the σ-algebra generated by compact sets!), so his proofs or statements do not apply directly.

[Billingsley, Convergence of Probability Measures][billingsley1999]