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
  • μ.InnerRegularWRT p q = ∀ ⦃U : Set α⦄, q Ur < μ U, KU, p K r < μ K
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 : μ.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 : μ.InnerRegularWRT p q) (h0 : p ) (hU : q U) (hμU : μ U ) (hε : ε 0) :
    KU, 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 : μ.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) :
    (MeasureTheory.Measure.map f μ).InnerRegularWRT pb qb
    theorem MeasureTheory.Measure.InnerRegularWRT.map' {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {pa : Set αProp} {qa : Set αProp} (H : μ.InnerRegularWRT pa qa) (f : α ≃ᵐ β) {pb : Set βProp} {qb : Set βProp} (hAB : ∀ (U : Set β), qb Uqa (f ⁻¹' U)) (hAB' : ∀ (K : Set α), pa Kpb (f '' K)) :
    (MeasureTheory.Measure.map (⇑f) μ).InnerRegularWRT pb qb
    theorem MeasureTheory.Measure.InnerRegularWRT.smul {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : Set αProp} {q : Set αProp} (H : μ.InnerRegularWRT p q) (c : ENNReal) :
    (c μ).InnerRegularWRT p q
    theorem MeasureTheory.Measure.InnerRegularWRT.trans {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : Set αProp} {q : Set αProp} {q' : Set αProp} (H : μ.InnerRegularWRT p q) (H' : μ.InnerRegularWRT q q') :
    μ.InnerRegularWRT p q'
    theorem MeasureTheory.Measure.InnerRegularWRT.rfl {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : Set αProp} :
    μ.InnerRegularWRT p p
    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) :
    μ.InnerRegularWRT p q
    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 : μ.InnerRegularWRT p q) (h : ∀ (s : Set α), q' sq s) (h' : ∀ (s : Set α), p sp' s) :
    μ.InnerRegularWRT p' q'

    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
      theorem MeasureTheory.Measure.OuterRegular.outerRegular {α : Type u_1} :
      ∀ {inst : MeasurableSpace α} {inst_1 : TopologicalSpace α} {μ : MeasureTheory.Measure α} [self : μ.OuterRegular] ⦃A : Set α⦄, MeasurableSet Ar > μ A, UA, IsOpen U μ U < r

      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.
      • lt_top_of_isCompact : ∀ ⦃K : Set α⦄, IsCompact Kμ K <
      • outerRegular : ∀ ⦃A : Set α⦄, MeasurableSet Ar > μ A, UA, IsOpen U μ U < r
      • innerRegular : μ.InnerRegularWRT IsCompact IsOpen
      Instances
        theorem MeasureTheory.Measure.Regular.innerRegular {α : Type u_1} :
        ∀ {inst : MeasurableSpace α} {inst_1 : TopologicalSpace α} {μ : MeasureTheory.Measure α} [self : μ.Regular], μ.InnerRegularWRT IsCompact IsOpen

        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.
        • outerRegular : ∀ ⦃A : Set α⦄, MeasurableSet Ar > μ A, UA, IsOpen U μ U < r
        • innerRegular : μ.InnerRegularWRT IsClosed IsOpen
        Instances
          theorem MeasureTheory.Measure.WeaklyRegular.innerRegular {α : Type u_1} :
          ∀ {inst : MeasurableSpace α} {inst_1 : TopologicalSpace α} {μ : MeasureTheory.Measure α} [self : μ.WeaklyRegular], μ.InnerRegularWRT IsClosed IsOpen

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

          • innerRegular : μ.InnerRegularWRT IsCompact MeasurableSet
          Instances
            theorem MeasureTheory.Measure.InnerRegular.innerRegular {α : Type u_1} :
            ∀ {inst : MeasurableSpace α} {inst_1 : TopologicalSpace α} {μ : MeasureTheory.Measure α} [self : μ.InnerRegular], μ.InnerRegularWRT IsCompact MeasurableSet

            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
              theorem MeasureTheory.Measure.InnerRegularCompactLTTop.innerRegular {α : Type u_1} :
              ∀ {inst : MeasurableSpace α} {inst_1 : TopologicalSpace α} {μ : MeasureTheory.Measure α} [self : μ.InnerRegularCompactLTTop], μ.InnerRegularWRT IsCompact fun (s : Set α) => MeasurableSet s μ s
              @[instance 100]
              instance MeasureTheory.Measure.Regular.weaklyRegular {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [R1Space α] [μ.Regular] :
              μ.WeaklyRegular

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

              Equations
              • =
              theorem Set.exists_isOpen_lt_of_lt {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.OuterRegular] (A : Set α) (r : ENNReal) (hr : μ A < r) :
              UA, 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 α) [μ.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 α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.OuterRegular] (A : Set α) (hA : μ A ) {ε : ENNReal} (hε : ε 0) :
              UA, IsOpen U μ U < μ A + ε
              theorem Set.exists_isOpen_le_add {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] (A : Set α) (μ : MeasureTheory.Measure α) [μ.OuterRegular] {ε : ENNReal} (hε : ε 0) :
              UA, IsOpen U μ U μ A + ε
              theorem MeasurableSet.exists_isOpen_diff_lt {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.OuterRegular] {A : Set α} (hA : MeasurableSet A) (hA' : μ A ) {ε : ENNReal} (hε : ε 0) :
              UA, IsOpen U μ U < μ (U \ A) < ε
              theorem MeasureTheory.Measure.OuterRegular.map {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [TopologicalSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] [TopologicalSpace β] [BorelSpace β] (f : α ≃ₜ β) (μ : MeasureTheory.Measure α) [μ.OuterRegular] :
              (MeasureTheory.Measure.map (⇑f) μ).OuterRegular
              theorem MeasureTheory.Measure.OuterRegular.smul {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] (μ : MeasureTheory.Measure α) [μ.OuterRegular] {x : ENNReal} (hx : x ) :
              (x μ).OuterRegular
              instance MeasureTheory.Measure.OuterRegular.smul_nnreal {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] (μ : MeasureTheory.Measure α) [μ.OuterRegular] (c : NNReal) :
              (c μ).OuterRegular
              Equations
              • =
              theorem MeasureTheory.Measure.OuterRegular.of_restrict {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [OpensMeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (h : ∀ (n : ), (μ.restrict (s n)).OuterRegular) (h' : ∀ (n : ), IsOpen (s n)) (h'' : Set.univ ⋃ (n : ), s n) :
              μ.OuterRegular

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

              theorem MeasureTheory.Measure.OuterRegular.measure_closure_eq_of_isCompact {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [R1Space α] [μ.OuterRegular] {k : Set α} (hk : IsCompact k) :
              μ (closure k) = μ k

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

              theorem MeasureTheory.Measure.FiniteSpanningSetsIn.outerRegular {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [OpensMeasurableSpace α] {μ : MeasureTheory.Measure α} (s : μ.FiniteSpanningSetsIn {U : Set α | IsOpen U (μ.restrict U).OuterRegular}) :
              μ.OuterRegular

              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 MeasureTheory.Measure.InnerRegularWRT.of_restrict {α : Type u_1} [MeasurableSpace α] {p : Set αProp} {μ : MeasureTheory.Measure α} {s : Set α} (h : ∀ (n : ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet) (hs : Set.univ ⋃ (n : ), s n) (hmono : Monotone s) :
              μ.InnerRegularWRT p MeasurableSet

              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.

              theorem MeasureTheory.Measure.InnerRegularWRT.restrict {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : Set αProp} (h : μ.InnerRegularWRT p fun (s : Set α) => MeasurableSet s μ s ) (A : Set α) :
              (μ.restrict A).InnerRegularWRT p fun (s : Set α) => MeasurableSet s (μ.restrict A) s

              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.

              theorem MeasureTheory.Measure.InnerRegularWRT.restrict_of_measure_ne_top {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : Set αProp} (h : μ.InnerRegularWRT p fun (s : Set α) => MeasurableSet s μ s ) {A : Set α} (hA : μ A ) :
              (μ.restrict A).InnerRegularWRT p fun (s : Set α) => MeasurableSet s

              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.

              theorem MeasureTheory.Measure.InnerRegularWRT.of_sigmaFinite {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] :
              μ.InnerRegularWRT (fun (s : Set α) => MeasurableSet s μ s ) fun (s : Set α) => MeasurableSet s

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

              theorem MeasureTheory.Measure.InnerRegularWRT.measurableSet_of_isOpen {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : Set αProp} [TopologicalSpace α] [μ.OuterRegular] (H : μ.InnerRegularWRT p IsOpen) (hd : ∀ ⦃s U : Set α⦄, p sIsOpen Up (s \ U)) :
              μ.InnerRegularWRT p fun (s : Set α) => MeasurableSet s μ s

              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.

              theorem MeasureTheory.Measure.InnerRegularWRT.weaklyRegular_of_finite {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [BorelSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (H : μ.InnerRegularWRT IsClosed IsOpen) :
              μ.WeaklyRegular

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

              theorem MeasurableSet.measure_eq_iSup_isCompact {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] ⦃U : Set α (hU : MeasurableSet U) (μ : 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.

              instance MeasureTheory.Measure.InnerRegular.smul {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [h : μ.InnerRegular] (c : ENNReal) :
              (c μ).InnerRegular
              Equations
              • =
              instance MeasureTheory.Measure.InnerRegular.smul_nnreal {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.InnerRegular] (c : NNReal) :
              (c μ).InnerRegular
              Equations
              • =
              @[instance 100]
              instance MeasureTheory.Measure.InnerRegular.instInnerRegularCompactLTTop {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.InnerRegular] :
              μ.InnerRegularCompactLTTop
              Equations
              • =
              theorem MeasureTheory.Measure.InnerRegular.innerRegularWRT_isClosed_isOpen {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [R1Space α] [OpensMeasurableSpace α] [h : μ.InnerRegular] :
              μ.InnerRegularWRT IsClosed IsOpen
              theorem MeasureTheory.Measure.InnerRegular.exists_compact_not_null {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.InnerRegular] :
              (∃ (K : Set α), IsCompact K μ K 0) μ 0
              theorem MeasurableSet.exists_lt_isCompact {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.InnerRegular] ⦃A : Set α (hA : MeasurableSet A) {r : ENNReal} (hr : r < μ A) :
              KA, 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 MeasureTheory.Measure.InnerRegular.map_of_continuous {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [MeasurableSpace β] [TopologicalSpace β] [BorelSpace β] [h : μ.InnerRegular] {f : αβ} (hf : Continuous f) :
              (MeasureTheory.Measure.map f μ).InnerRegular
              theorem MeasureTheory.Measure.InnerRegular.map {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [MeasurableSpace β] [TopologicalSpace β] [BorelSpace β] [μ.InnerRegular] (f : α ≃ₜ β) :
              (MeasureTheory.Measure.map (⇑f) μ).InnerRegular
              theorem MeasureTheory.Measure.InnerRegular.map_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [MeasurableSpace β] [TopologicalSpace β] [BorelSpace β] (f : α ≃ₜ β) :
              (MeasureTheory.Measure.map (⇑f) μ).InnerRegular μ.InnerRegular
              theorem MeasurableSet.exists_isCompact_lt_add {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.InnerRegularCompactLTTop] ⦃A : Set α (hA : MeasurableSet A) (h'A : μ A ) {ε : ENNReal} (hε : ε 0) :
              KA, 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_isClosed_lt_add {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.InnerRegularCompactLTTop] [R1Space α] [BorelSpace α] ⦃A : Set α (hA : MeasurableSet A) (h'A : μ A ) {ε : ENNReal} (hε : ε 0) :
              KA, IsCompact K IsClosed 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 closed subset. Compared to MeasurableSet.exists_isCompact_lt_add, this version additionally assumes that α is an R₁ space with Borel σ-algebra.

              theorem MeasurableSet.exists_isCompact_diff_lt {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [OpensMeasurableSpace α] [T2Space α] [μ.InnerRegularCompactLTTop] ⦃A : Set α (hA : MeasurableSet A) (h'A : μ A ) {ε : ENNReal} (hε : ε 0) :
              KA, 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_isCompact_isClosed_diff_lt {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [R1Space α] [μ.InnerRegularCompactLTTop] ⦃A : Set α (hA : MeasurableSet A) (h'A : μ A ) {ε : ENNReal} (hε : ε 0) :
              KA, IsCompact K IsClosed 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 closed subset. Compared to MeasurableSet.exists_isCompact_diff_lt, this lemma additionally assumes that α is an R₁ space with Borel σ-algebra.

              theorem MeasurableSet.exists_lt_isCompact_of_ne_top {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.InnerRegularCompactLTTop] ⦃A : Set α (hA : MeasurableSet A) (h'A : μ A ) {r : ENNReal} (hr : r < μ A) :
              KA, 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 α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.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.

              instance MeasureTheory.Measure.InnerRegularCompactLTTop.restrict {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [h : μ.InnerRegularCompactLTTop] (A : Set α) :
              (μ.restrict A).InnerRegularCompactLTTop

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

              Equations
              • =
              @[instance 50]
              Equations
              • =
              @[instance 50]
              Equations
              • =
              @[instance 50]
              Equations
              • =
              theorem IsCompact.exists_isOpen_lt_of_lt {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.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 α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.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 α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.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 α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure μ] [R1Space α] [BorelSpace α] {K : Set α} (hK : IsCompact K) {ε : ENNReal} (hε : ε 0) :
              ∃ (U : Set α), K U IsOpen U μ U < μ K + ε
              theorem MeasurableSet.exists_isOpen_symmDiff_lt {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure μ] [R1Space α] [BorelSpace α] {s : Set α} (hs : MeasurableSet s) (hμs : μ s ) {ε : ENNReal} (hε : ε 0) :
              ∃ (U : Set α), IsOpen U μ U < μ (symmDiff U s) < ε

              Let μ be a locally finite measure on an R₁ topological space with Borel σ-algebra. If μ is inner regular for finite measure sets with respect to compact sets, then any measurable set of finite measure can be approximated in measure by an open set. See also Set.exists_isOpen_lt_of_lt and MeasurableSet.exists_isOpen_diff_lt for the case of an outer regular measure.

              theorem MeasureTheory.NullMeasurableSet.exists_isOpen_symmDiff_lt {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure μ] [R1Space α] [BorelSpace α] {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) (hμs : μ s ) {ε : ENNReal} (hε : ε 0) :
              ∃ (U : Set α), IsOpen U μ U < μ (symmDiff U s) < ε

              Let μ be a locally finite measure on an R₁ topological space with Borel σ-algebra. If μ is inner regular for finite measure sets with respect to compact sets, then any null measurable set of finite measure can be approximated in measure by an open set. See also Set.exists_isOpen_lt_of_lt and MeasurableSet.exists_isOpen_diff_lt for the case of an outer regular measure.

              instance MeasureTheory.Measure.InnerRegularCompactLTTop.smul {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [h : μ.InnerRegularCompactLTTop] (c : ENNReal) :
              (c μ).InnerRegularCompactLTTop
              Equations
              • =
              instance MeasureTheory.Measure.InnerRegularCompactLTTop.smul_nnreal {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.InnerRegularCompactLTTop] (c : NNReal) :
              (c μ).InnerRegularCompactLTTop
              Equations
              • =
              @[instance 80]
              Equations
              • =
              theorem MeasureTheory.Measure.InnerRegularCompactLTTop.map_of_continuous {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [MeasurableSpace β] [TopologicalSpace β] [BorelSpace β] [h : μ.InnerRegularCompactLTTop] {f : αβ} (hf : Continuous f) :
              (MeasureTheory.Measure.map f μ).InnerRegularCompactLTTop
              theorem IsOpen.exists_lt_isClosed {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.WeaklyRegular] ⦃U : Set α (hU : IsOpen U) {r : ENNReal} (hr : r < μ U) :
              FU, 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 α) [μ.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 MeasureTheory.Measure.WeaklyRegular.innerRegular_measurable {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.WeaklyRegular] :
              μ.InnerRegularWRT IsClosed fun (s : Set α) => MeasurableSet s μ s
              theorem MeasurableSet.exists_isClosed_lt_add {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.WeaklyRegular] {s : Set α} (hs : MeasurableSet s) (hμs : μ s ) {ε : ENNReal} (hε : ε 0) :
              Ks, 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 α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [OpensMeasurableSpace α] [μ.WeaklyRegular] ⦃A : Set α (hA : MeasurableSet A) (h'A : μ A ) {ε : ENNReal} (hε : ε 0) :
              FA, IsClosed F μ (A \ F) < ε
              theorem MeasurableSet.exists_lt_isClosed_of_ne_top {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.WeaklyRegular] ⦃A : Set α (hA : MeasurableSet A) (h'A : μ A ) {r : ENNReal} (hr : r < μ A) :
              KA, 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 α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.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.

              theorem MeasureTheory.Measure.WeaklyRegular.restrict_of_measure_ne_top {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [μ.WeaklyRegular] {A : Set α} (h'A : μ A ) :
              (μ.restrict A).WeaklyRegular

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

              @[instance 100]

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

              Equations
              • =
              @[instance 100]

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

              Equations
              • =
              theorem MeasureTheory.Measure.WeaklyRegular.smul {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.WeaklyRegular] {x : ENNReal} (hx : x ) :
              (x μ).WeaklyRegular
              instance MeasureTheory.Measure.WeaklyRegular.smul_nnreal {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.WeaklyRegular] (c : NNReal) :
              (c μ).WeaklyRegular
              Equations
              • =
              theorem IsOpen.exists_lt_isCompact {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.Regular] ⦃U : Set α (hU : IsOpen U) {r : ENNReal} (hr : r < μ U) :
              KU, 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 α) [μ.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.

              theorem MeasureTheory.Measure.Regular.exists_compact_not_null {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.Regular] :
              (∃ (K : Set α), IsCompact K μ K 0) μ 0
              @[instance 100]
              instance MeasureTheory.Measure.Regular.instInnerRegularCompactLTTop {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.Regular] :
              μ.InnerRegularCompactLTTop

              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
              • =
              theorem MeasureTheory.Measure.Regular.map {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [MeasurableSpace β] [TopologicalSpace β] [BorelSpace β] [μ.Regular] (f : α ≃ₜ β) :
              (MeasureTheory.Measure.map (⇑f) μ).Regular
              theorem MeasureTheory.Measure.Regular.map_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [BorelSpace α] [MeasurableSpace β] [TopologicalSpace β] [BorelSpace β] (f : α ≃ₜ β) :
              (MeasureTheory.Measure.map (⇑f) μ).Regular μ.Regular
              theorem MeasureTheory.Measure.Regular.smul {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.Regular] {x : ENNReal} (hx : x ) :
              (x μ).Regular
              instance MeasureTheory.Measure.Regular.smul_nnreal {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [μ.Regular] (c : NNReal) :
              (c μ).Regular
              Equations
              • =
              theorem MeasureTheory.Measure.Regular.restrict_of_measure_ne_top {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace α] [R1Space α] [BorelSpace α] [μ.Regular] {A : Set α} (h'A : μ A ) :
              (μ.restrict A).Regular

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

              @[instance 100]

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

              Equations
              • =
              @[instance 100]

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

              Equations
              • =