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 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.

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 closed sets: the measure of any open set U is the supremum of μ K over all compact sets K contained in U.

A measure is InnerRegular if it is inner regular for measurable sets with respect to compact sets: the measure of any measurable set s is the supremum of μ K over all compact sets contained in s.

A measure is InnerRegularCompactLTTop if it is inner regular for measurable sets of finite measure with respect to compact sets: the measure of any measurable set s is the supremum of μ K over all compact sets contained in s.

There is a reason for this zoo of regularity classes:

A finite measure on a metric space is always weakly regular. Therefore, in probability theory, weakly regular measures play a prominent role.
In locally compact topological spaces, there are two competing notions of Radon measures: the ones that are regular, and the ones that are inner regular. For any of these two notions, there is a Riesz representation theorem, and an existence and uniqueness statement for the Haar measure in locally compact topological groups. The two notions coincide in sigma-compact spaces, but they differ in general, so it is worth having the two of them.
Both notions of Haar measure satisfy the weaker notion InnerRegularCompactLTTop, so it is worth trying to express theorems using this weaker notion whenever possible, to make sure that it applies to both Haar measures simultaneously.

While traditional textbooks on measure theory on locally compact spaces emphasize regular measures, more recent textbooks emphasize that inner regular Haar measures are better behaved than regular Haar measures, so we will develop both notions.

The five conditions above are registered as typeclasses for a measure μ, and implications between them are recorded as instances. For example, in a Hausdorff topological space, regularity implies weak regularity. Also, regularity or inner regularity both imply InnerRegularCompactLTTop. In a regular locally compact finite measure space, then regularity, inner regularity and InnerRegularCompactLTTop are all equivalent.

In order to avoid code duplication, we also define a measure μ to be InnerRegularWRT 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.

There are two main nontrivial results in the development below:

InnerRegularWRT.measurableSet_of_isOpen shows that, for an outer regular measure, 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).
InnerRegularWRT.weaklyRegular_of_finite shows that a finite measure which is inner regular for open sets with respect to closed sets (for instance a finite measure on a metric space) is weakly regular.

All other results are deduced from these ones.

Here is an example showing how regularity and inner regularity may differ even on locally compact spaces. 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. Let us consider the regular version of Haar measure. Then the set ℝ × {0} has infinite measure (by outer regularity), but any compact set it contains has zero measure (as it is finite). In fact, this set only contains subset with measure zero or infinity. The inner regular version of Haar measure, on the other hand, gives zero mass to the set ℝ × {0}.

Another interesting example is the sum of the Dirac masses at rational points in the real line. It is a σ-finite measure on a locally compact metric space, but it is not outer regular: for outer regularity, one needs additional locally finite assumptions. On the other hand, it is inner regular.

Several authors require both regularity and inner regularity for their measures. We have opted for the more fine grained definitions above as they apply more generally.

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.InnerRegularWRT μ p q: a non-typeclass predicate saying that a measure μ is inner regular for sets satisfying q with respect to sets satisfying p.
MeasureTheory.Measure.InnerRegular μ: a typeclass registering that a measure μ on a topological space is inner regular for measurable sets with respect to compact sets.
MeasureTheory.Measure.InnerRegularCompactLTTop μ: a typeclass registering that a measure μ on a topological space is inner regular for measurable sets of finite measure with respect to compact sets.

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_pseudoMetrizableSpace_of_isFiniteMeasure is an instance registering that a finite measure on a metric space is weakly regular (in fact, a pseudo metrizable space is enough);
MeasureTheory.Measure.WeaklyRegular.of_pseudoMetrizableSpace_secondCountable_of_locallyFinite is an instance registering that a locally finite measure on a second countable metric space (or even a pseudo metrizable 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;
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).

Inner regular measures #

MeasurableSet.measure_eq_iSup_isCompact asserts that the measure of a measurable set is the supremum of the measure of compact sets it contains.
MeasurableSet.exists_lt_isCompact: for a measurable set s and r < μ s, there exists a compact K ⊆ s of measure greater than r;

Inner regular measures for finite measure sets with respect to compact sets #

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).

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).

For non-Hausdorff spaces, one may argue whether the right condition for inner regularity is with respect to compact sets, or to compact closed sets. For instance, Fremlin, Measure Theory (volume 4, 411J) considers measures which are inner regular with respect to compact closed sets (and calls them tight). However, since most of the literature uses mere compact sets, we have chosen to follow this convention. It doesn't make a difference in Hausdorff spaces, of course. In locally compact topological groups, the two conditions coincide, since if a compact set k is contained in a measurable set u, then the closure of k is a compact closed set still contained in u, see IsCompact.closure_subset_of_measurableSet_of_group.

References #

Halmos, Measure Theory, §52. 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.