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.

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.

Billingsley, Convergence of Probability Measures

@[class]
structure measure_theory.measure.regular {α : Type u_1} (μ : measure_theory.measure α) :
Prop
• lt_top_of_is_compact : ∀ ⦃K : set α⦄, μ K <
• outer_regular : ∀ ⦃A : set α⦄, (⨅ (U : set α) (h : is_open U) (h2 : A U), μ U) μ A
• inner_regular : ∀ ⦃U : set α⦄, (μ U ⨆ (K : set α) (h : (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} 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
• outer_regular : ∀ ⦃A : set α⦄, (⨅ (U : set α) (h : is_open U) (h2 : A U), μ U) μ A
• inner_regular : ∀ ⦃U : set α⦄, (μ U ⨆ (F : set α) (h : (h2 : F U), μ F)

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
@[instance]

A regular measure is weakly regular.

theorem measurable_set.measure_eq_infi_is_open' {α : Type u_1} ⦃A : set α⦄ (hA : measurable_set A) (μ : measure_theory.measure α) [μ.regular] :
μ A = ⨅ (U : set α) (h : is_open U) (h2 : A U), μ U

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.

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

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.

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 : (h2 : K U), μ K

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

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 α), K U r < μ K
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.map {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [t2_space β] [borel_space β] [μ.regular] (f : α ≃ₜ β) :
μ).regular
theorem measure_theory.measure.regular.smul {α : Type u_1} {μ : measure_theory.measure α} [μ.regular] {x : ℝ≥0∞} (hx : x < ) :
(x μ).regular
@[instance]

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

theorem measurable_set.measure_eq_infi_is_open {α : Type u_1} ⦃A : set α⦄ (hA : measurable_set A) (μ : measure_theory.measure α) [μ.weakly_regular] :
μ A = ⨅ (U : set α) (h : is_open U) (h2 : A U), μ U
theorem measurable_set.exists_is_open_lt_of_lt {α : Type u_1} {μ : measure_theory.measure α} [μ.weakly_regular] ⦃A : set α⦄ (hA : measurable_set A) (r : ℝ≥0∞) (hr : μ A < r) :
∃ (U : set α), A U μ U < r
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 : (h2 : F U), μ F
theorem is_open.exists_lt_is_closed_of_gt {α : Type u_1} {μ : measure_theory.measure α} [μ.weakly_regular] ⦃U : set α⦄ (hU : is_open U) (r : ℝ≥0∞) (hr : r < μ U) :
∃ (F : set α), F U r < μ F
theorem measure_theory.measure.weakly_regular.exists_subset_is_open_measure_lt_top {α : Type u_1} {μ : measure_theory.measure α} [μ.weakly_regular] {A : set α} (h'A : μ A < ) :
∃ (U : set α), A U μ U <

Given a weakly regular measure, any finite measure set is contained in a finite measure open set.

theorem measure_theory.measure.weakly_regular.exists_closed_subset_self_subset_open_of_pos {α : Type u_1} [borel_space α] (μ : measure_theory.measure α) (h0 : ∀ (U : set α), (μ U ⨆ (F : set α) (hF : (FU : F U), μ F)) ⦃s : set α⦄ (hs : measurable_set s) (ε : ℝ≥0∞) (H : ε > 0) :
(∃ (U : set α), s U μ U μ s + ε) ∃ (F : set α), F s μ s μ F + ε

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.

theorem measure_theory.measure.weakly_regular.weakly_regular_of_inner_regular_of_finite_measure {α : Type u_1} [borel_space α] (μ : measure_theory.measure α) (h0 : ∀ (U : set α), (μ U ⨆ (F : set α) (hF : (FU : F U), μ F)) :

In a finite measure space, if every open set can be approximated from inside by closed sets, then the measure is weakly regular

theorem measure_theory.measure.weakly_regular.restrict_of_is_open {α : Type u_1} {μ : measure_theory.measure α} [borel_space α] [μ.weakly_regular] (U : set α) (hU : is_open U) (h'U : μ U < ) :

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.

theorem measurable_set.measure_eq_supr_is_closed_of_finite_measure {α : Type u_1} [borel_space α] (μ : measure_theory.measure α) [μ.weakly_regular] ⦃A : set α⦄ (hA : measurable_set A) :
μ A = ⨆ (F : set α) (h : (h2 : F A), μ F

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

theorem measurable_set.measure_eq_supr_is_closed_of_lt_top {α : Type u_1} {μ : measure_theory.measure α} [borel_space α] [μ.weakly_regular] ⦃A : set α⦄ (hA : measurable_set A) (h'A : μ A < ) :
μ A = ⨆ (F : set α) (h : (h2 : F A), μ F

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

theorem measurable_set.exists_lt_is_closed_of_lt_top {α : Type u_1} {μ : measure_theory.measure α} [borel_space α] [μ.weakly_regular] ⦃A : set α⦄ (hA : measurable_set A) (h'A : μ A < ) {r : ℝ≥0∞} (hr : r < μ A) :
∃ (F : set α), F A r < μ F
theorem measurable_set.exists_lt_is_closed_of_lt_top_of_pos {α : Type u_1} {μ : measure_theory.measure α} [borel_space α] [μ.weakly_regular] ⦃A : set α⦄ (hA : measurable_set A) (h'A : μ A < ) {ε : ℝ≥0∞} (εpos : 0 < ε) :
∃ (F : set α), F A μ A < μ F + ε

The restriction of a weakly regular measure to a measurable set of finite measure is weakly regular.

theorem measure_theory.measure.weakly_regular.inner_regular_of_pseudo_emetric_space {X : Type u_1} [borel_space X] (μ : measure_theory.measure X) (U : set X) (U_open : is_open U) :
μ U ⨆ (F : set X) (hF : (FU : F U), μ F

In a metric space (or even a pseudo emetric space), an open set can be approximated from inside by closed sets.

@[instance]

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

@[instance]

Any locally finite measure on a sigma compact locally compact metric space is regular.

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

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

theorem measurable_set.exists_lt_is_compact_of_lt_top {α : Type u_1} {μ : measure_theory.measure α} [borel_space α] [t2_space α] [μ.regular] ⦃A : set α⦄ (hA : measurable_set A) (h'A : μ A < ) {r : ℝ≥0∞} (hr : r < μ A) :
∃ (K : set α), K A r < μ K
theorem measurable_set.exists_lt_is_compact_of_lt_top_of_pos {α : Type u_1} {μ : measure_theory.measure α} [borel_space α] [t2_space α] [μ.regular] ⦃A : set α⦄ (hA : measurable_set A) (h'A : μ A < ) {ε : ℝ≥0∞} (εpos : 0 < ε) :
∃ (K : set α), K A μ A < μ K + ε