mathlib3 documentation

measure_theory.measure.regular

Regular measures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

A measure is weakly_regular if it satisfies the following properties:

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 #

Main results #

Outer regular measures #

Weakly regular measures #

Regular measures #

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 : μ.inner_regular p 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 α} {ε : ennreal} (H : μ.inner_regular p 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} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {pa qa : set α Prop} (H : μ.inner_regular pa qa) (f : α β) (hf : ae_measurable f μ) {pb qb : set β Prop} (hAB : (U : set β), qb U qa (f ⁻¹' U)) (hAB' : (K : set α), pa K pb (f '' K)) (hB₁ : (K : set β), pb K measurable_set K) (hB₂ : (U : set β), qb U measurable_set U) :
theorem measure_theory.measure.inner_regular.smul {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {p q : set α Prop} (H : μ.inner_regular p q) (c : ennreal) :
(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 : μ.inner_regular p q) (H' : μ.inner_regular q q') :
@[class]

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 of this typeclass
@[class]

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 of this typeclass
@[class]

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 of this typeclass
@[protected, instance]

A regular measure is weakly regular.

theorem set.exists_is_open_lt_of_lt {α : Type u_1} [measurable_space α] [topological_space α] {μ : measure_theory.measure α} [μ.outer_regular] (A : set α) (r : ennreal) (hr : μ A < r) :
(U : set α) (H : U A), is_open U μ 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} [measurable_space α] [topological_space α] (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} [measurable_space α] [topological_space α] {μ : measure_theory.measure α} [μ.outer_regular] (A : set α) (hA : μ A ) {ε : ennreal} (hε : ε 0) :
(U : set α) (H : U A), is_open U μ U < μ A + ε
theorem set.exists_is_open_le_add {α : Type u_1} [measurable_space α] [topological_space α] (A : set α) (μ : measure_theory.measure α) [μ.outer_regular] {ε : ennreal} (hε : ε 0) :
(U : set α) (H : U A), is_open U μ U μ A + ε
theorem measurable_set.exists_is_open_diff_lt {α : Type u_1} [measurable_space α] [topological_space α] {μ : measure_theory.measure α} [μ.outer_regular] {A : set α} (hA : measurable_set A) (hA' : μ A ) {ε : ennreal} (hε : ε 0) :
(U : set α) (H : U A), is_open U μ U < μ (U \ A) < ε
@[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} [measurable_space α] [topological_space α] {μ : measure_theory.measure α} {p : set α Prop} [μ.outer_regular] (H : μ.inner_regular p is_open) (h0 : p ) (hd : ⦃s U : set α⦄, p s is_open U p (s \ U)) :
μ.inner_regular p (λ (s : set α), measurable_set s μ 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]
theorem is_open.exists_lt_is_compact {α : Type u_1} [measurable_space α] [topological_space α] {μ : measure_theory.measure α} [μ.regular] ⦃U : set α⦄ (hU : is_open U) {r : ennreal} (hr : r < μ U) :
(K : set α) (H : K U), is_compact K 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} [measurable_space α] [topological_space α] ⦃U : set α⦄ (hU : is_open U) (μ : measure_theory.measure α) [μ.regular] :
μ U = (K : set α) (h : K U) (h2 : is_compact K), μ K

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

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} [measurable_space α] [topological_space α] {μ : measure_theory.measure α} [μ.regular] ⦃A : set α⦄ (hA : measurable_set A) (h'A : μ A ) {ε : ennreal} (hε : ε 0) :
(K : set α) (H : K A), is_compact K μ 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} [measurable_space α] [topological_space α] {μ : measure_theory.measure α} [opens_measurable_space α] [t2_space α] [μ.regular] ⦃A : set α⦄ (hA : measurable_set A) (h'A : μ A ) {ε : ennreal} (hε : ε 0) :
(K : set α) (H : K A), is_compact K μ (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} [measurable_space α] [topological_space α] {μ : measure_theory.measure α} [μ.regular] ⦃A : set α⦄ (hA : measurable_set A) (h'A : μ A ) {r : ennreal} (hr : r < μ A) :
(K : set α) (H : K A), is_compact K 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} [measurable_space α] [topological_space α] {μ : measure_theory.measure α} [μ.regular] ⦃A : set α⦄ (hA : measurable_set A) (h'A : μ A ) :
μ A = (K : set α) (H : K A) (h : is_compact K), μ K

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

@[protected]
@[protected, instance]

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

theorem is_open.exists_lt_is_closed {α : Type u_1} [measurable_space α] [topological_space α] {μ : measure_theory.measure α} [μ.weakly_regular] ⦃U : set α⦄ (hU : is_open U) {r : ennreal} (hr : r < μ U) :
(F : set α) (H : F U), is_closed F 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} [measurable_space α] [topological_space α] ⦃U : set α⦄ (hU : is_open U) (μ : measure_theory.measure α) [μ.weakly_regular] :
μ U = (F : set α) (H : F U) (h : is_closed F), μ 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} [measurable_space α] [topological_space α] {μ : measure_theory.measure α} [μ.weakly_regular] {s : set α} (hs : measurable_set s) (hμs : μ s ) {ε : ennreal} (hε : ε 0) :
(K : set α) (H : K s), is_closed K μ 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} [measurable_space α] [topological_space α] {μ : measure_theory.measure α} [opens_measurable_space α] [μ.weakly_regular] ⦃A : set α⦄ (hA : measurable_set A) (h'A : μ A ) {ε : ennreal} (hε : ε 0) :
(F : set α) (H : F A), is_closed F μ (A \ F) < ε
theorem measurable_set.exists_lt_is_closed_of_ne_top {α : Type u_1} [measurable_space α] [topological_space α] {μ : measure_theory.measure α} [μ.weakly_regular] ⦃A : set α⦄ (hA : measurable_set A) (h'A : μ A ) {r : ennreal} (hr : r < μ A) :
(K : set α) (H : K A), is_closed K 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} [measurable_space α] [topological_space α] {μ : measure_theory.measure α} [μ.weakly_regular] ⦃A : set α⦄ (hA : measurable_set A) (h'A : μ A ) :
μ A = (K : set α) (H : K A) (h : is_closed K), μ 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 second countable 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.