# mathlibdocumentation

measure_theory.regular

# Regular measures #

A measure is regular if it satisfies the following properties:

• it is finite on compact sets;
• it is outer regular for measurable sets with respect to open sets: the measure of any measurable set A is the infimum of μ U over all open sets U containing A;
• 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 for measurable sets with respect to open sets: the measure of any measurable set A is the infimum of μ U over all open sets U containing A;
• 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.

Regularity implies weak regularity. Both these conditions are registered as typeclasses for a measure μ, and this implication is recorded as an instance.

These conditions imply inner regularity for all measurable sets of finite measure (with respect to compact sets or closed sets respectively), but in general not for all sets. 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 and results #

• regular μ: a typeclass registering that a measure μ on a topological space is regular.

• measurable_set.measure_eq_infi_is_open' asserts that, when μ is regular, the measure of a measurable set is the infimum of the measure of open sets containing it. The unprimed version is reserved for weakly regular measures, as it should apply most of the time. Such open sets with suitable measures can be constructed with measurable_set.exists_is_open_lt_of_lt'.

• is_open.measure_eq_supr_is_compact asserts that the measure of an open set is the supremum of the measure of compact sets it contains. Such a compact set with suitable measure can be constructed with is_open.exists_lt_is_compact.

• measurable_set.measure_eq_supr_is_compact_of_lt_top asserts that the measure of a measurable set of finite measure is the supremum of the measure of compact sets it contains. Such a compact set with suitable measure can be constructed with measurable_set.exists_lt_is_compact_of_lt_top or measurable_set.exists_lt_is_compact_of_lt_top_of_pos.

• regular.of_sigma_compact_space_of_locally_finite_measure is an instance registering that a locally finite measure on a locally compact metric space is regular (in fact, an emetric space is enough).

• weakly_regular μ: a typeclass registering that a measure μ on a topological space is weakly regular.

• measurable_set.measure_eq_infi_is_open, measurable_set.exists_is_open_lt_of_lt, is_open.measure_eq_supr_is_closed, is_open.exists_lt_is_closed, measurable_set.measure_eq_supr_is_closed_of_lt_top, measurable_set.exists_lt_is_closed_of_lt_top and measurable_set.exists_lt_is_closed_of_lt_top_of_pos state the corresponding properties for weakly regular measures.

• weakly_regular.of_pseudo_emetric_space_of_finite_measure is an instance registering that a finite measure on a metric space is weakly regular (in fact, a pseudo emetric space is enough).

## Implementation notes #

The main nontrivial statement is weakly_regular.exists_closed_subset_self_subset_open, expressing that in a finite measure space, if every open set can be approximated from inside by closed sets, then 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 general 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