Documentation

Mathlib.MeasureTheory.Measure.Regular

Regular measures #

A measure is OuterRegular if the measure of any measurable set A is the infimum of μ U over all open sets U containing A.

A measure is WeaklyRegular if it satisfies the following properties:

A measure is Regular if it satisfies the following properties:

A measure is InnerRegular if it is inner regular for measurable sets with respect to compact sets: the measure of any measurable set s is the supremum of μ K over all compact sets contained in s.

A measure is InnerRegularCompactLTTop if it is inner regular for measurable sets of finite measure with respect to compact sets: the measure of any measurable set s is the supremum of μ K over all compact sets contained in s.

There is a reason for this zoo of regularity classes:

While traditional textbooks on measure theory on locally compact spaces emphasize regular measures, more recent textbooks emphasize that inner regular Haar measures are better behaved than regular Haar measures, so we will develop both notions.

The five conditions above are registered as typeclasses for a measure μ, and implications between them are recorded as instances. For example, in a Hausdorff topological space, regularity implies weak regularity. Also, regularity or inner regularity both imply InnerRegularCompactLTTop. In a regular locally compact finite measure space, then regularity, inner regularity and InnerRegularCompactLTTop are all equivalent.

In order to avoid code duplication, we also define a measure μ to be InnerRegularWRT 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.

There are two main nontrivial results in the development below:

All other results are deduced from these ones.

Here is an example showing how regularity and inner regularity may differ even on locally compact spaces. 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. Let us consider the regular version of Haar measure. Then the set ℝ × {0} has infinite measure (by outer regularity), but any compact set it contains has zero measure (as it is finite). In fact, this set only contains subset with measure zero or infinity. The inner regular version of Haar measure, on the other hand, gives zero mass to the set ℝ × {0}.

Another interesting example is the sum of the Dirac masses at rational points in the real line. It is a σ-finite measure on a locally compact metric space, but it is not outer regular: for outer regularity, one needs additional locally finite assumptions. On the other hand, it is inner regular.

Several authors require both regularity and inner regularity for their measures. We have opted for the more fine grained definitions above as they apply more generally.

Main definitions #

Main results #

Outer regular measures #

Weakly regular measures #

Regular measures #

Inner regular measures #

Inner regular measures for finite measure sets with respect to compact sets #

Implementation notes #

The main nontrivial statement is MeasureTheory.Measure.InnerRegular.weaklyRegular_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).

For non-Hausdorff spaces, one may argue whether the right condition for inner regularity is with respect to compact sets, or to compact closed sets. For instance, [Fremlin, Measure Theory (volume 4, 411J)][fremlin_vol4] considers measures which are inner regular with respect to compact closed sets (and calls them tight). However, since most of the literature uses mere compact sets, we have chosen to follow this convention. It doesn't make a difference in Hausdorff spaces, of course. In locally compact topological groups, the two conditions coincide, since if a compact set k is contained in a measurable set u, then the closure of k is a compact closed set still contained in u, see IsCompact.closure_subset_of_measurableSet_of_group.

References #

[Halmos, Measure Theory, §52][halmos1950measure]. 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][billingsley1999]

[Bogachev, Measure Theory, volume 2, Theorem 7.11.1][bogachev2007]

def MeasureTheory.Measure.InnerRegularWRT {α : Type u_1} :
{x : MeasurableSpace α} → MeasureTheory.Measure α(Set αProp)(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
Instances For
    theorem MeasureTheory.Measure.InnerRegularWRT.measure_eq_iSup {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : Set αProp} {q : Set αProp} {U : Set α} (H : MeasureTheory.Measure.InnerRegularWRT μ p q) (hU : q U) :
    μ U = ⨆ (K : Set α), ⨆ (_ : K U), ⨆ (_ : p K), μ K
    theorem MeasureTheory.Measure.InnerRegularWRT.exists_subset_lt_add {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : Set αProp} {q : Set αProp} {U : Set α} {ε : ENNReal} (H : MeasureTheory.Measure.InnerRegularWRT μ p q) (h0 : p ) (hU : q U) (hμU : μ U ) (hε : ε 0) :
    ∃ K ⊆ U, p K μ U < μ K + ε
    theorem MeasureTheory.Measure.InnerRegularWRT.map {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {pa : Set αProp} {qa : Set αProp} (H : MeasureTheory.Measure.InnerRegularWRT μ pa qa) {f : αβ} (hf : AEMeasurable f μ) {pb : Set βProp} {qb : Set βProp} (hAB : ∀ (U : Set β), qb Uqa (f ⁻¹' U)) (hAB' : ∀ (K : Set α), pa Kpb (f '' K)) (hB₂ : ∀ (U : Set β), qb UMeasurableSet U) :
    theorem MeasureTheory.Measure.InnerRegularWRT.map' {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {pa : Set αProp} {qa : Set αProp} (H : MeasureTheory.Measure.InnerRegularWRT μ pa qa) (f : α ≃ᵐ β) {pb : Set βProp} {qb : Set βProp} (hAB : ∀ (U : Set β), qb Uqa (f ⁻¹' U)) (hAB' : ∀ (K : Set α), pa Kpb (f '' K)) :
    theorem MeasureTheory.Measure.InnerRegularWRT.of_imp {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : Set αProp} {q : Set αProp} (h : ∀ (s : Set α), q sp s) :
    theorem MeasureTheory.Measure.InnerRegularWRT.mono {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : Set αProp} {q : Set αProp} {p' : Set αProp} {q' : Set αProp} (H : MeasureTheory.Measure.InnerRegularWRT μ p q) (h : ∀ (s : Set α), q' sq s) (h' : ∀ (s : Set α), p sp' s) :

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

    Instances

      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

        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 closed} for U open.
        Instances

          A measure μ is inner regular if, for any measurable set s, then μ(s) = sup {μ(K) | K ⊆ s compact}.

          Instances

            A measure μ is inner regular for finite measure sets with respect to compact sets: for any measurable set s with finite measure, then μ(s) = sup {μ(K) | K ⊆ s compact}. The main interest of this class is that it is satisfied for both natural Haar measures (the regular one and the inner regular one).

            Instances

              A regular measure is weakly regular in an R₁ space.

              Equations
              • =
              theorem Set.exists_isOpen_lt_of_lt {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.Measure.OuterRegular μ] (A : Set α) (r : ENNReal) (hr : μ A < r) :
              ∃ U ⊇ A, IsOpen 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_iInf_isOpen {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] (A : Set α) (μ : MeasureTheory.Measure α) [MeasureTheory.Measure.OuterRegular μ] :
              μ A = ⨅ (U : Set α), ⨅ (_ : A U), ⨅ (_ : IsOpen 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_isOpen_lt_add {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.Measure.OuterRegular μ] (A : Set α) (hA : μ A ) {ε : ENNReal} (hε : ε 0) :
              ∃ U ⊇ A, IsOpen U μ U < μ A + ε
              theorem Set.exists_isOpen_le_add {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] (A : Set α) (μ : MeasureTheory.Measure α) [MeasureTheory.Measure.OuterRegular μ] {ε : ENNReal} (hε : ε 0) :
              ∃ U ⊇ A, IsOpen U μ U μ A + ε
              theorem MeasurableSet.exists_isOpen_diff_lt {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.Measure.OuterRegular μ] {A : Set α} (hA : MeasurableSet A) (hA' : μ A ) {ε : ENNReal} (hε : ε 0) :
              ∃ U ⊇ A, IsOpen U μ U < μ (U \ A) < ε

              If the restrictions of a measure to countably many open sets covering the space are outer regular, then the measure itself is outer regular.

              See also IsCompact.measure_closure for a version that assumes the σ-algebra to be the Borel σ-algebra but makes no assumptions on μ.

              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.

              If a measure is inner regular (using closed or compact sets) for open sets, then every measurable set of finite measure can be 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.

              theorem MeasureTheory.Measure.InnerRegularWRT.of_restrict {α : Type u_1} [MeasurableSpace α] {p : Set αProp} {μ : MeasureTheory.Measure α} {s : Set α} (h : ∀ (n : ), MeasureTheory.Measure.InnerRegularWRT (MeasureTheory.Measure.restrict μ (s n)) p MeasurableSet) (hs : Set.univ ⋃ (n : ), s n) (hmono : Monotone s) :

              If the restrictions of a measure to a monotone sequence of sets covering the space are inner regular for some property p and all measurable sets, then the measure itself is inner regular.

              In a metrizable space (or even a pseudo metrizable 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.

              If μ is inner regular for measurable finite measure sets with respect to some class of sets, then its restriction to any set is also inner regular for measurable finite measure sets, with respect to the same class of sets.

              If μ is inner regular for measurable finite measure sets with respect to some class of sets, then its restriction to any finite measure set is also inner regular for measurable sets with respect to the same class of sets.

              Given a σ-finite measure, any measurable set can be approximated from inside by a measurable set of finite measure.

              theorem MeasurableSet.measure_eq_iSup_isCompact {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] ⦃U : Set α (hU : MeasurableSet U) (μ : MeasureTheory.Measure α) [MeasureTheory.Measure.InnerRegular μ] :
              μ U = ⨆ (K : Set α), ⨆ (_ : K U), ⨆ (_ : IsCompact K), μ K

              The measure of a measurable set is the supremum of the measures of compact sets it contains.

              theorem MeasurableSet.exists_lt_isCompact {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.Measure.InnerRegular μ] ⦃A : Set α (hA : MeasurableSet A) {r : ENNReal} (hr : r < μ A) :
              ∃ K ⊆ A, IsCompact K r < μ K

              If μ is inner regular, then any measurable set can be approximated by a compact subset. See also MeasurableSet.exists_isCompact_lt_add_of_ne_top.

              theorem MeasurableSet.exists_isCompact_lt_add {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.Measure.InnerRegularCompactLTTop μ] ⦃A : Set α (hA : MeasurableSet A) (h'A : μ A ) {ε : ENNReal} (hε : ε 0) :
              ∃ K ⊆ A, IsCompact K μ A < μ K + ε

              If μ is inner regular for finite measure sets with respect to compact sets, then any measurable set of finite measure can be approximated by a compact subset. See also MeasurableSet.exists_lt_isCompact_of_ne_top.

              theorem MeasurableSet.exists_isCompact_diff_lt {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] {μ : MeasureTheory.Measure α} [OpensMeasurableSpace α] [T2Space α] [MeasureTheory.Measure.InnerRegularCompactLTTop μ] ⦃A : Set α (hA : MeasurableSet A) (h'A : μ A ) {ε : ENNReal} (hε : ε 0) :
              ∃ K ⊆ A, IsCompact K μ (A \ K) < ε

              If μ is inner regular for finite measure sets with respect to compact sets, then any measurable set of finite measure can be approximated by a compact subset. See also MeasurableSet.exists_isCompact_lt_add and MeasurableSet.exists_lt_isCompact_of_ne_top.

              theorem MeasurableSet.exists_lt_isCompact_of_ne_top {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.Measure.InnerRegularCompactLTTop μ] ⦃A : Set α (hA : MeasurableSet A) (h'A : μ A ) {r : ENNReal} (hr : r < μ A) :
              ∃ K ⊆ A, IsCompact K r < μ K

              If μ is inner regular for finite measure sets with respect to compact sets, then any measurable set of finite measure can be approximated by a compact subset. See also MeasurableSet.exists_isCompact_lt_add.

              theorem MeasurableSet.measure_eq_iSup_isCompact_of_ne_top {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.Measure.InnerRegularCompactLTTop μ] ⦃A : Set α (hA : MeasurableSet A) (h'A : μ A ) :
              μ A = ⨆ (K : Set α), ⨆ (_ : K A), ⨆ (_ : IsCompact K), μ K

              If μ is inner regular for finite measure sets with respect to compact sets, any measurable set of finite mass can be approximated from inside by compact sets.

              If μ is inner regular for finite measure sets with respect to compact sets, then its restriction to any set also is.

              Equations
              • =
              theorem IsCompact.exists_isOpen_lt_of_lt {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.Measure.InnerRegularCompactLTTop μ] [MeasureTheory.IsLocallyFiniteMeasure μ] [R1Space α] [BorelSpace α] {K : Set α} (hK : IsCompact K) (r : ENNReal) (hr : μ K < r) :
              ∃ (U : Set α), K U IsOpen U μ U < r
              theorem IsCompact.measure_eq_iInf_isOpen {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.Measure.InnerRegularCompactLTTop μ] [MeasureTheory.IsLocallyFiniteMeasure μ] [R1Space α] [BorelSpace α] {K : Set α} (hK : IsCompact K) :
              μ K = ⨅ (U : Set α), ⨅ (_ : K U), ⨅ (_ : IsOpen U), μ U

              If μ is inner regular for finite measure sets with respect to compact sets and is locally finite in an R₁ space, then any compact set can be approximated from outside by open sets.

              @[deprecated IsCompact.measure_eq_iInf_isOpen]
              theorem IsCompact.measure_eq_infi_isOpen {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.Measure.InnerRegularCompactLTTop μ] [MeasureTheory.IsLocallyFiniteMeasure μ] [R1Space α] [BorelSpace α] {K : Set α} (hK : IsCompact K) :
              μ K = ⨅ (U : Set α), ⨅ (_ : K U), ⨅ (_ : IsOpen U), μ U

              Alias of IsCompact.measure_eq_iInf_isOpen.


              If μ is inner regular for finite measure sets with respect to compact sets and is locally finite in an R₁ space, then any compact set can be approximated from outside by open sets.

              theorem IsCompact.exists_isOpen_lt_add {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.Measure.InnerRegularCompactLTTop μ] [MeasureTheory.IsLocallyFiniteMeasure μ] [R1Space α] [BorelSpace α] {K : Set α} (hK : IsCompact K) {ε : ENNReal} (hε : ε 0) :
              ∃ (U : Set α), K U IsOpen U μ U < μ K + ε
              theorem IsOpen.exists_lt_isClosed {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.Measure.WeaklyRegular μ] ⦃U : Set α (hU : IsOpen U) {r : ENNReal} (hr : r < μ U) :
              ∃ F ⊆ U, IsClosed F r < μ F

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

              theorem IsOpen.measure_eq_iSup_isClosed {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] ⦃U : Set α (hU : IsOpen U) (μ : MeasureTheory.Measure α) [MeasureTheory.Measure.WeaklyRegular μ] :
              μ U = ⨆ (F : Set α), ⨆ (_ : F U), ⨆ (_ : IsClosed F), μ F

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

              theorem MeasurableSet.exists_isClosed_lt_add {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.Measure.WeaklyRegular μ] {s : Set α} (hs : MeasurableSet s) (hμs : μ s ) {ε : ENNReal} (hε : ε 0) :
              ∃ K ⊆ s, IsClosed 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 MeasurableSet.exists_isClosed_diff_lt {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] {μ : MeasureTheory.Measure α} [OpensMeasurableSpace α] [MeasureTheory.Measure.WeaklyRegular μ] ⦃A : Set α (hA : MeasurableSet A) (h'A : μ A ) {ε : ENNReal} (hε : ε 0) :
              ∃ F ⊆ A, IsClosed F μ (A \ F) < ε
              theorem MeasurableSet.exists_lt_isClosed_of_ne_top {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.Measure.WeaklyRegular μ] ⦃A : Set α (hA : MeasurableSet A) (h'A : μ A ) {r : ENNReal} (hr : r < μ A) :
              ∃ K ⊆ A, IsClosed K r < μ K

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

              theorem MeasurableSet.measure_eq_iSup_isClosed_of_ne_top {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.Measure.WeaklyRegular μ] ⦃A : Set α (hA : MeasurableSet A) (h'A : μ A ) :
              μ A = ⨆ (K : Set α), ⨆ (_ : K A), ⨆ (_ : IsClosed 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.

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

              Equations
              • =

              Any locally finite measure on a second countable metrizable space (or even a pseudo metrizable space) is weakly regular.

              Equations
              • =
              theorem IsOpen.exists_lt_isCompact {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.Measure.Regular μ] ⦃U : Set α (hU : IsOpen U) {r : ENNReal} (hr : r < μ U) :
              ∃ K ⊆ U, IsCompact K r < μ K

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

              theorem IsOpen.measure_eq_iSup_isCompact {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] ⦃U : Set α (hU : IsOpen U) (μ : MeasureTheory.Measure α) [MeasureTheory.Measure.Regular μ] :
              μ U = ⨆ (K : Set α), ⨆ (_ : K U), ⨆ (_ : IsCompact 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 MeasurableSet.exists_isCompact_lt_add and MeasurableSet.exists_lt_isCompact_of_ne_top.

              Equations
              • =

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

              Any sigma finite measure on a σ-compact pseudometrizable space is inner regular.

              Equations
              • =