mathlibdocumentation

measure_theory.measure.regular

Regular measures #

A measure is outer_regular 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 weakly_regular 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 compact 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 inner_regular 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 results #

Outer regular measures #

• set.measure_eq_infi_is_open asserts that, when μ is outer regular, the measure of a set is the infimum of the measure of open sets containing it.
• set.exists_is_open_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.
• measure_theory.measure.outer_regular.of_sigma_compact_space_of_is_locally_finite_measure: a locally finite measure on a σ-compact metric (or even pseudo emetric) space is outer regular.

Implementation notes #

The main nontrivial statement is measure_theory.measure.inner_regular.weakly_regular_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).

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.

Billingsley, Convergence of Probability Measures