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 setsU
containingA
;  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 setsK
contained inU
.
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 setsU
containingA
;  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 setsF
contained inU
.
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 withmeasurable_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 withis_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 withmeasurable_set.exists_lt_is_compact_of_lt_top
ormeasurable_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
andmeasurable_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).
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.
 lt_top_of_is_compact : ∀ ⦃K : set α⦄, is_compact K → ⇑μ K < ⊤
 outer_regular : ∀ ⦃A : set α⦄, measurable_set A → (⨅ (U : set α) (h : is_open U) (h2 : A ⊆ U), ⇑μ U) ≤ ⇑μ A
 inner_regular : ∀ ⦃U : set α⦄, is_open U → (⇑μ U ≤ ⨆ (K : set α) (h : is_compact K) (h2 : K ⊆ U), ⇑μ K)
A measure μ
is regular if
 it is finite on all compact sets;
 it is outer regular:
μ(A) = inf {μ(U)  A ⊆ U open}
forA
measurable;  it is inner regular for open sets, using compact sets:
μ(U) = sup {μ(K)  K ⊆ U compact}
forU
open.
 outer_regular : ∀ ⦃A : set α⦄, measurable_set A → (⨅ (U : set α) (h : is_open U) (h2 : A ⊆ U), ⇑μ U) ≤ ⇑μ A
 inner_regular : ∀ ⦃U : set α⦄, is_open U → (⇑μ U ≤ ⨆ (F : set α) (h : is_closed F) (h2 : F ⊆ U), ⇑μ F)
A measure μ
is weakly regular if
 it is outer regular:
μ(A) = inf { μ(U)  A ⊆ U open }
forA
measurable;  it is inner regular for open sets, using closed sets:
μ(U) = sup {μ(F)  F ⊆ U compact}
forU
open.
A regular measure is weakly regular.
The measure of a measurable set is the infimum of the measures of open sets containing it. The unprimed version is reserved for weakly regular measures, as regular measures are automatically weakly regular most of the time.
Given r
larger than the measure of a measurable set A
, there exists an open superset of A
with measure < r
. The unprimed version is reserved for weakly regular measures, as regular
measures are automatically weakly regular most of the time.
The measure of an open set is the supremum of the measures of compact sets it contains.
A regular measure in a σcompact space is σfinite.
Given a weakly regular measure, any finite measure set is contained in a finite measure open set.
In a finite measure space, assume that any 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.
In a finite measure space, if every open set can be approximated from inside by closed sets, then the measure is weakly regular
The restriction of a weakly regular measure to an open set of finite measure is
weakly regular. Superseded by restrict_of_measurable_set
, proving the same statement for
measurable sets instead of open sets.
Given a weakly regular measure of finite mass, any measurable set can be approximated from inside by closed sets.
Given a weakly regular measure, any measurable set of finite mass can be approximated from inside by closed sets.
The restriction of a weakly regular measure to a measurable set of finite measure is weakly regular.
In a metric space (or even a pseudo emetric space), an open set can be approximated from inside by closed sets.
Any finite measure on a metric space (or even a pseudo emetric space) is weakly regular.
Any locally finite measure on a sigma compact locally compact metric space is regular.
Given a regular measure, any measurable set of finite mass can be approximated from inside by compact sets.