# 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 definitions #

• measure_theory.measure.outer_regular μ: a typeclass registering that a measure μ on a topological space is outer regular.
• measure_theory.measure.regular μ: a typeclass registering that a measure μ on a topological space is regular.
• measure_theory.measure.weakly_regular μ: a typeclass registering that a measure μ on a topological space is weakly regular.
• measure_theory.measure.inner_regular μ 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_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.

### Weakly regular measures #

• is_open.measure_eq_supr_is_closed asserts that the measure of an open set is the supremum of the measure of closed sets it contains.
• is_open.exists_lt_is_closed: for an open set U and r < μ U, there exists a closed F ⊆ U of measure greater than r;
• measurable_set.measure_eq_supr_is_closed_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.
• measurable_set.exists_lt_is_closed_of_ne_top and measurable_set.exists_is_closed_lt_add: a measurable set of finite measure can be approximated by a closed subset (stated as r < μ F and μ s < μ F + ε, respectively).
• measure_theory.measure.weakly_regular.of_pseudo_emetric_space_of_is_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);
• measure_theory.measure.weakly_regular.of_pseudo_emetric_sigma_compact_space_of_locally_finite is an instance registering that a locally finite measure on a σ-compact metric space (or even a pseudo emetric space) is weakly regular.

### Regular measures #

• 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.
• is_open.exists_lt_is_compact: for an open set U and r < μ U, there exists a compact K ⊆ U of measure greater than r;
• measurable_set.measure_eq_supr_is_compact_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.
• measurable_set.exists_lt_is_compact_of_ne_top and measurable_set.exists_is_compact_lt_add: a measurable set of finite measure can be approximated by a compact subset (stated as r < μ K and μ s < μ K + ε, respectively).
• measure_theory.measure.regular.of_sigma_compact_space_of_is_locally_finite_measure 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 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).

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

Billingsley, Convergence of Probability Measures

def measure_theory.measure.inner_regular {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) (p q : set α → Prop) :
Prop

We say that a measure μ is inner regular with respect to predicates p q : set α → Prop, if for every U such that q U and r < μ U, there exists a subset K ⊆ U satisfying p K of measure greater than r.

This definition is used to prove some facts about regular and weakly regular measures without repeating the proofs.

Equations
theorem measure_theory.measure.inner_regular.measure_eq_supr {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {p q : set α → Prop} {U : set α} (H : q) (hU : q U) :
μ U = ⨆ (K : set α) (H : K U) (hK : p K), μ K
theorem measure_theory.measure.inner_regular.exists_subset_lt_add {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {p q : set α → Prop} {U : set α} {ε : ℝ≥0∞} (H : q) (h0 : p ) (hU : q U) (hμU : μ U ) (hε : ε 0) :
∃ (K : set α) (H : K U), p K μ U < μ K + ε
theorem measure_theory.measure.inner_regular.map {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} {pa qa : set α → Prop} (H : μ.inner_regular pa qa) (f : α β) (hf : measurable f) {pb qb : set β → Prop} (hAB : ∀ (U : set β), qb Uqa (f ⁻¹' U)) (hAB' : ∀ (K : set α), pa Kpb (f '' K)) (hB₁ : ∀ (K : set β), pb K) (hB₂ : ∀ (U : set β), qb U) :
pb qb
theorem measure_theory.measure.inner_regular.smul {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {p q : set α → Prop} (H : q) (c : ℝ≥0∞) :
(c μ).inner_regular p q
theorem measure_theory.measure.inner_regular.trans {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {p q q' : set α → Prop} (H : q) (H' : q') :
q'
@[class]
structure measure_theory.measure.outer_regular {α : Type u_1} (μ : measure_theory.measure α) :
Prop

A measure μ is outer regular if μ(A) = inf {μ(U) | A ⊆ U open} for a measurable set A.

This definition implies the same equality for any (not necessarily measurable) set, see set.measure_eq_infi_is_open.

Instances
@[class]
structure measure_theory.measure.regular {α : Type u_1} (μ : measure_theory.measure α) :
Prop
• to_is_finite_measure_on_compacts :
• to_outer_regular :
• inner_regular :

A measure μ is regular if

• it is finite on all compact sets;
• it is outer regular: μ(A) = inf {μ(U) | A ⊆ U open} for A measurable;
• it is inner regular for open sets, using compact sets: μ(U) = sup {μ(K) | K ⊆ U compact} for U open.
Instances
@[class]
structure measure_theory.measure.weakly_regular {α : Type u_1} (μ : measure_theory.measure α) :
Prop
• to_outer_regular :
• inner_regular :

A measure μ is weakly regular if

• it is outer regular: μ(A) = inf {μ(U) | A ⊆ U open} for A measurable;
• it is inner regular for open sets, using closed sets: μ(U) = sup {μ(F) | F ⊆ U compact} for U open.
Instances
@[protected, instance]

A regular measure is weakly regular.

@[protected, instance]
theorem set.exists_is_open_lt_of_lt {α : Type u_1} {μ : measure_theory.measure α} [μ.outer_regular] (A : set α) (r : ℝ≥0∞) (hr : μ A < r) :
∃ (U : set α) (H : U A), μ U < r

Given r larger than the measure of a set A, there exists an open superset of A with measure less than r.

theorem set.measure_eq_infi_is_open {α : Type u_1} (A : set α) (μ : measure_theory.measure α) [μ.outer_regular] :
μ A = ⨅ (U : set α) (h : A U) (h2 : is_open U), μ U

For an outer regular measure, the measure of a set is the infimum of the measures of open sets containing it.

theorem set.exists_is_open_lt_add {α : Type u_1} {μ : measure_theory.measure α} [μ.outer_regular] (A : set α) (hA : μ A ) {ε : ℝ≥0∞} (hε : ε 0) :
∃ (U : set α) (H : U A), μ U < μ A + ε
theorem set.exists_is_open_le_add {α : Type u_1} (A : set α) (μ : measure_theory.measure α) [μ.outer_regular] {ε : ℝ≥0∞} (hε : ε 0) :
∃ (U : set α) (H : U A), μ U μ A + ε
theorem measurable_set.exists_is_open_diff_lt {α : Type u_1} {μ : measure_theory.measure α} [μ.outer_regular] {A : set α} (hA : measurable_set A) (hA' : μ A ) {ε : ℝ≥0∞} (hε : ε 0) :
∃ (U : set α) (H : U A), μ U < μ (U \ A) < ε
@[protected]
theorem measure_theory.measure.outer_regular.map {α : Type u_1} {β : Type u_2} [borel_space β] (f : α ≃ₜ β) (μ : measure_theory.measure α) [μ.outer_regular] :
@[protected]
theorem measure_theory.measure.outer_regular.smul {α : Type u_1} (μ : measure_theory.measure α) [μ.outer_regular] {x : ℝ≥0∞} (hx : x ) :
@[protected]

If a measure μ admits finite spanning open sets such that the restriction of μ to each set is outer regular, then the original measure is outer regular as well.

theorem measure_theory.measure.inner_regular.measurable_set_of_open {α : Type u_1} {μ : measure_theory.measure α} {p : set α → Prop} [μ.outer_regular] (H : is_open) (h0 : p ) (hd : ∀ ⦃s U : set α⦄, p sp (s \ U)) :
(λ (s : set α), μ s )

If a measure is inner regular (using closed or compact sets), then every measurable set of finite measure can by approximated by a (closed or compact) subset.

In a finite measure space, assume that any open set can be approximated from inside by closed sets. Then the 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.

In a σ-compact space, any closed set can be approximated by a compact subset.

@[protected, instance]
def measure_theory.measure.regular.zero {α : Type u_1}  :
theorem is_open.exists_lt_is_compact {α : Type u_1} {μ : measure_theory.measure α} [μ.regular] ⦃U : set α⦄ (hU : is_open U) {r : ℝ≥0∞} (hr : r < μ U) :
∃ (K : set α) (H : K U), r < μ K

If μ is a regular measure, then any open set can be approximated by a compact subset.

theorem is_open.measure_eq_supr_is_compact {α : Type u_1} ⦃U : set α⦄ (hU : is_open U) (μ : measure_theory.measure α) [μ.regular] :
μ U = ⨆ (K : set α) (h : K U) (h2 : , μ K

The measure of an open set is the supremum of the measures of compact sets it contains.

theorem measure_theory.measure.regular.exists_compact_not_null {α : Type u_1} {μ : measure_theory.measure α} [μ.regular] :
(∃ (K : set α), μ K 0) μ 0
theorem measure_theory.measure.regular.inner_regular_measurable {α : Type u_1} {μ : measure_theory.measure α} [μ.regular] :
(λ (s : set α), μ s )

If μ is a regular measure, then any measurable set of finite measure can be approximated by a compact subset. See also measurable_set.exists_is_compact_lt_add and measurable_set.exists_lt_is_compact_of_ne_top.

theorem measurable_set.exists_is_compact_lt_add {α : Type u_1} {μ : measure_theory.measure α} [μ.regular] ⦃A : set α⦄ (hA : measurable_set A) (h'A : μ A ) {ε : ℝ≥0∞} (hε : ε 0) :
∃ (K : set α) (H : K A), μ A < μ K + ε

If μ is a regular measure, then any measurable set of finite measure can be approximated by a compact subset. See also measurable_set.exists_lt_is_compact_of_ne_top.

theorem measurable_set.exists_is_compact_diff_lt {α : Type u_1} {μ : measure_theory.measure α} [t2_space α] [μ.regular] ⦃A : set α⦄ (hA : measurable_set A) (h'A : μ A ) {ε : ℝ≥0∞} (hε : ε 0) :
∃ (K : set α) (H : K A), μ (A \ K) < ε

If μ is a regular measure, then any measurable set of finite measure can be approximated by a compact subset. See also measurable_set.exists_is_compact_lt_add and measurable_set.exists_lt_is_compact_of_ne_top.

theorem measurable_set.exists_lt_is_compact_of_ne_top {α : Type u_1} {μ : measure_theory.measure α} [μ.regular] ⦃A : set α⦄ (hA : measurable_set A) (h'A : μ A ) {r : ℝ≥0∞} (hr : r < μ A) :
∃ (K : set α) (H : K A), r < μ K

If μ is a regular measure, then any measurable set of finite measure can be approximated by a compact subset. See also measurable_set.exists_is_compact_lt_add.

theorem measurable_set.measure_eq_supr_is_compact_of_ne_top {α : Type u_1} {μ : measure_theory.measure α} [μ.regular] ⦃A : set α⦄ (hA : measurable_set A) (h'A : μ A ) :
μ A = ⨆ (K : set α) (H : K A) (h : , μ K

Given a regular measure, any measurable set of finite mass can be approximated from inside by compact sets.

@[protected]
theorem measure_theory.measure.regular.map {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [t2_space β] [borel_space β] [μ.regular] (f : α ≃ₜ β) :
μ).regular
@[protected]
theorem measure_theory.measure.regular.smul {α : Type u_1} {μ : measure_theory.measure α} [μ.regular] {x : ℝ≥0∞} (hx : x ) :
(x μ).regular
@[protected, instance]

A regular measure in a σ-compact space is σ-finite.

theorem is_open.exists_lt_is_closed {α : Type u_1} {μ : measure_theory.measure α} [μ.weakly_regular] ⦃U : set α⦄ (hU : is_open U) {r : ℝ≥0∞} (hr : r < μ U) :
∃ (F : set α) (H : F U), r < μ F

If μ is a weakly regular measure, then any open set can be approximated by a closed subset.

theorem is_open.measure_eq_supr_is_closed {α : Type u_1} ⦃U : set α⦄ (hU : is_open U) (μ : measure_theory.measure α) [μ.weakly_regular] :
μ U = ⨆ (F : set α) (H : F U) (h : , μ F

If μ is a weakly regular measure, then any open set can be approximated by a closed subset.

theorem measurable_set.exists_is_closed_lt_add {α : Type u_1} {μ : measure_theory.measure α} [μ.weakly_regular] {s : set α} (hs : measurable_set s) (hμs : μ s ) {ε : ℝ≥0∞} (hε : ε 0) :
∃ (K : set α) (H : K s), μ s < μ K + ε

If s is a measurable set, a weakly regular measure μ is finite on s, and ε is a positive number, then there exist a closed set K ⊆ s such that μ s < μ K + ε.

theorem measurable_set.exists_is_closed_diff_lt {α : Type u_1} {μ : measure_theory.measure α} [μ.weakly_regular] ⦃A : set α⦄ (hA : measurable_set A) (h'A : μ A ) {ε : ℝ≥0∞} (hε : ε 0) :
∃ (F : set α) (H : F A), μ (A \ F) < ε
theorem measurable_set.exists_lt_is_closed_of_ne_top {α : Type u_1} {μ : measure_theory.measure α} [μ.weakly_regular] ⦃A : set α⦄ (hA : measurable_set A) (h'A : μ A ) {r : ℝ≥0∞} (hr : r < μ A) :
∃ (K : set α) (H : K A), r < μ K

Given a weakly regular measure, any measurable set of finite mass can be approximated from inside by closed sets.

theorem measurable_set.measure_eq_supr_is_closed_of_ne_top {α : Type u_1} {μ : measure_theory.measure α} [μ.weakly_regular] ⦃A : set α⦄ (hA : measurable_set A) (h'A : μ A ) :
μ A = ⨆ (K : set α) (H : K A) (h : , μ K

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.

@[protected, instance]

Any finite measure on a metric space (or even a pseudo emetric space) is weakly regular.

@[protected, instance]

Any locally finite measure on a σ-compact metric space (or even a pseudo emetric space) is weakly regular.

@[protected, instance]

Any locally finite measure on a σ-compact (e)metric space is regular.