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

• 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 closed sets F contained in U.

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 closed sets: the measure of any open set U is the supremum of μ K over all compact sets K contained in U.

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:

• A finite measure on a metric space is always weakly regular. Therefore, in probability theory, weakly regular measures play a prominent role.
• In locally compact topological spaces, there are two competing notions of Radon measures: the ones that are regular, and the ones that are inner regular. For any of these two notions, there is a Riesz representation theorem, and an existence and uniqueness statement for the Haar measure in locally compact topological groups. The two notions coincide in sigma-compact spaces, but they differ in general, so it is worth having the two of them.
• Both notions of Haar measure satisfy the weaker notion InnerRegularCompactLTTop, so it is worth trying to express theorems using this weaker notion whenever possible, to make sure that it applies to both Haar measures simultaneously.

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:

• InnerRegularWRT.measurableSet_of_isOpen shows that, for an outer regular measure, 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).
• InnerRegularWRT.weaklyRegular_of_finite shows that a finite measure which is inner regular for open sets with respect to closed sets (for instance a finite measure on a metric space) is weakly regular.

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 #

• MeasureTheory.Measure.OuterRegular μ: a typeclass registering that a measure μ on a topological space is outer regular.
• MeasureTheory.Measure.Regular μ: a typeclass registering that a measure μ on a topological space is regular.
• MeasureTheory.Measure.WeaklyRegular μ: a typeclass registering that a measure μ on a topological space is weakly regular.
• MeasureTheory.Measure.InnerRegularWRT μ p q: a non-typeclass predicate saying that a measure μ is inner regular for sets satisfying q with respect to sets satisfying p.
• MeasureTheory.Measure.InnerRegular μ: a typeclass registering that a measure μ on a topological space is inner regular for measurable sets with respect to compact sets.
• MeasureTheory.Measure.InnerRegularCompactLTTop μ: a typeclass registering that a measure μ on a topological space is inner regular for measurable sets of finite measure with respect to compact sets.

## Main results #

### Outer regular measures #

• Set.measure_eq_iInf_isOpen asserts that, when μ is outer regular, the measure of a set is the infimum of the measure of open sets containing it.
• Set.exists_isOpen_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.

### Weakly regular measures #

• IsOpen.measure_eq_iSup_isClosed asserts that the measure of an open set is the supremum of the measure of closed sets it contains.
• IsOpen.exists_lt_isClosed: for an open set U and r < μ U, there exists a closed F ⊆ U of measure greater than r;
• MeasurableSet.measure_eq_iSup_isClosed_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.
• MeasurableSet.exists_lt_isClosed_of_ne_top and MeasurableSet.exists_isClosed_lt_add: a measurable set of finite measure can be approximated by a closed subset (stated as r < μ F and μ s < μ F + ε, respectively).
• MeasureTheory.Measure.WeaklyRegular.of_pseudoMetrizableSpace_of_isFiniteMeasure is an instance registering that a finite measure on a metric space is weakly regular (in fact, a pseudo metrizable space is enough);
• MeasureTheory.Measure.WeaklyRegular.of_pseudoMetrizableSpace_secondCountable_of_locallyFinite is an instance registering that a locally finite measure on a second countable metric space (or even a pseudo metrizable space) is weakly regular.

### Regular measures #

• IsOpen.measure_eq_iSup_isCompact asserts that the measure of an open set is the supremum of the measure of compact sets it contains.
• IsOpen.exists_lt_isCompact: for an open set U and r < μ U, there exists a compact K ⊆ U of measure greater than r;
• MeasureTheory.Measure.Regular.of_sigmaCompactSpace_of_isLocallyFiniteMeasure is an instance registering that a locally finite measure on a σ-compact metric space is regular (in fact, an emetric space is enough).

### Inner regular measures #

• MeasurableSet.measure_eq_iSup_isCompact asserts that the measure of a measurable set is the supremum of the measure of compact sets it contains.
• MeasurableSet.exists_lt_isCompact: for a measurable set s and r < μ s, there exists a compact K ⊆ s of measure greater than r;

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

• MeasurableSet.measure_eq_iSup_isCompact_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.
• MeasurableSet.exists_lt_isCompact_of_ne_top and MeasurableSet.exists_isCompact_lt_add: a measurable set of finite measure can be approximated by a compact subset (stated as r < μ K and μ s < μ K + ε, respectively).

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

Bogachev, Measure Theory, volume 2, Theorem 7.11.1

def MeasureTheory.Measure.InnerRegularWRT {α : Type u_1} :
{x : } → (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 : } {μ : } {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 : } {μ : } {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} [] [] {μ : } {pa : Set αProp} {qa : Set αProp} (H : μ.InnerRegularWRT pa qa) {f : αβ} (hf : ) {pb : Set βProp} {qb : Set βProp} (hAB : ∀ (U : Set β), qb Uqa (f ⁻¹' U)) (hAB' : ∀ (K : Set α), pa Kpb (f '' K)) (hB₂ : ∀ (U : Set β), qb U) :
.InnerRegularWRT pb qb
theorem MeasureTheory.Measure.InnerRegularWRT.map' {α : Type u_2} {β : Type u_3} [] [] {μ : } {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 : } {μ : } {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 : } {μ : } {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 : } {μ : } {p : Set αProp} :
μ.InnerRegularWRT p p
theorem MeasureTheory.Measure.InnerRegularWRT.of_imp {α : Type u_1} {m : } {μ : } {p : Set αProp} {q : Set αProp} (h : ∀ (s : Set α), q sp s) :
μ.InnerRegularWRT p q
theorem MeasureTheory.Measure.InnerRegularWRT.mono {α : Type u_1} {m : } {μ : } {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'
class MeasureTheory.Measure.OuterRegular {α : Type u_1} [] [] (μ : ) :

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.

• outerRegular : ∀ ⦃A : Set α⦄, r > μ A, UA, μ U < r
Instances
theorem MeasureTheory.Measure.OuterRegular.outerRegular {α : Type u_1} [] [] {μ : } [self : μ.OuterRegular] ⦃A : Set α :
r > μ A, UA, μ 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 α⦄, μ K <
• outerRegular : ∀ ⦃A : Set α⦄, r > μ A, UA, μ U < r
• innerRegular : μ.InnerRegularWRT IsCompact IsOpen
Instances
theorem MeasureTheory.Measure.Regular.innerRegular {α : Type u_1} [] [] {μ : } [self : μ.Regular] :
μ.InnerRegularWRT IsCompact IsOpen
class MeasureTheory.Measure.WeaklyRegular {α : Type u_1} [] [] (μ : ) extends :

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 α⦄, r > μ A, UA, μ U < r
• innerRegular : μ.InnerRegularWRT IsClosed IsOpen
Instances
theorem MeasureTheory.Measure.WeaklyRegular.innerRegular {α : Type u_1} [] [] {μ : } [self : μ.WeaklyRegular] :
μ.InnerRegularWRT IsClosed IsOpen
class MeasureTheory.Measure.InnerRegular {α : Type u_1} [] [] (μ : ) :

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

• innerRegular : μ.InnerRegularWRT IsCompact fun (s : Set α) =>
Instances
theorem MeasureTheory.Measure.InnerRegular.innerRegular {α : Type u_1} [] [] {μ : } [self : μ.InnerRegular] :
μ.InnerRegularWRT IsCompact fun (s : Set α) =>

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

• innerRegular : μ.InnerRegularWRT IsCompact fun (s : Set α) => μ s
Instances
theorem MeasureTheory.Measure.InnerRegularCompactLTTop.innerRegular {α : Type u_1} [] [] {μ : } [self : μ.InnerRegularCompactLTTop] :
μ.InnerRegularWRT IsCompact fun (s : Set α) => μ s
@[instance 100]
instance MeasureTheory.Measure.Regular.weaklyRegular {α : Type u_1} [] {μ : } [] [] [μ.Regular] :
μ.WeaklyRegular

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

Equations
• =
instance MeasureTheory.Measure.OuterRegular.zero {α : Type u_1} [] [] :
Equations
• =
theorem Set.exists_isOpen_lt_of_lt {α : Type u_1} [] {μ : } [] [μ.OuterRegular] (A : Set α) (r : ENNReal) (hr : μ A < r) :
UA, μ 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} [] [] (A : Set α) (μ : ) [μ.OuterRegular] :
μ A = ⨅ (U : Set α), ⨅ (_ : A 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} [] {μ : } [] [μ.OuterRegular] (A : Set α) (hA : μ A ) {ε : ENNReal} (hε : ε 0) :
UA, μ U < μ A + ε
theorem Set.exists_isOpen_le_add {α : Type u_1} [] [] (A : Set α) (μ : ) [μ.OuterRegular] {ε : ENNReal} (hε : ε 0) :
UA, μ U μ A + ε
theorem MeasurableSet.exists_isOpen_diff_lt {α : Type u_1} [] {μ : } [] [μ.OuterRegular] {A : Set α} (hA : ) (hA' : μ A ) {ε : ENNReal} (hε : ε 0) :
UA, μ U < μ (U \ A) < ε
theorem MeasureTheory.Measure.OuterRegular.map {α : Type u_1} {β : Type u_2} [] [] [] [] [] (f : α ≃ₜ β) (μ : ) [μ.OuterRegular] :
(MeasureTheory.Measure.map (⇑f) μ).OuterRegular
theorem MeasureTheory.Measure.OuterRegular.smul {α : Type u_1} [] [] (μ : ) [μ.OuterRegular] {x : ENNReal} (hx : x ) :
(x μ).OuterRegular
instance MeasureTheory.Measure.OuterRegular.smul_nnreal {α : Type u_1} [] [] (μ : ) [μ.OuterRegular] (c : NNReal) :
(c μ).OuterRegular
Equations
• =
theorem MeasureTheory.Measure.OuterRegular.of_restrict {α : Type u_1} [] [] {μ : } {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} [] {μ : } [] [] [μ.OuterRegular] {k : Set α} (hk : ) :
μ (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} [] [] {μ : } (s : μ.FiniteSpanningSetsIn {U : Set α | (μ.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} [] {p : Set αProp} {μ : } {s : Set α} (h : ∀ (n : ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet) (hs : Set.univ ⋃ (n : ), s n) (hmono : ) :
μ.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} [] {μ : } {p : Set αProp} (h : μ.InnerRegularWRT p fun (s : Set α) => μ s ) (A : Set α) :
(μ.restrict A).InnerRegularWRT p fun (s : Set α) => (μ.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} [] {μ : } {p : Set αProp} (h : μ.InnerRegularWRT p fun (s : Set α) => μ s ) {A : Set α} (hA : μ A ) :
(μ.restrict A).InnerRegularWRT p fun (s : Set α) =>

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} [] {μ : } :
μ.InnerRegularWRT (fun (s : Set α) => μ s ) fun (s : Set α) =>

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} [] {μ : } {p : Set αProp} [] [μ.OuterRegular] (H : μ.InnerRegularWRT p IsOpen) (hd : ∀ ⦃s U : Set α⦄, p sp (s \ U)) :
μ.InnerRegularWRT p fun (s : Set α) => μ 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} [] [] [] (μ : ) (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.

theorem MeasureTheory.Measure.InnerRegularWRT.of_pseudoMetrizableSpace {X : Type u_3} [] [] (μ : ) :
μ.InnerRegularWRT IsClosed IsOpen

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

theorem MeasureTheory.Measure.InnerRegularWRT.isCompact_isClosed {X : Type u_3} [] [] (μ : ) :
μ.InnerRegularWRT IsCompact IsClosed

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

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

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

instance MeasureTheory.Measure.InnerRegular.zero {α : Type u_1} [] [] :
Equations
• =
instance MeasureTheory.Measure.InnerRegular.smul {α : Type u_1} [] {μ : } [] [h : μ.InnerRegular] (c : ENNReal) :
(c μ).InnerRegular
Equations
• =
instance MeasureTheory.Measure.InnerRegular.smul_nnreal {α : Type u_1} [] {μ : } [] [μ.InnerRegular] (c : NNReal) :
(c μ).InnerRegular
Equations
• =
@[instance 100]
instance MeasureTheory.Measure.InnerRegular.instInnerRegularCompactLTTop {α : Type u_1} [] {μ : } [] [μ.InnerRegular] :
μ.InnerRegularCompactLTTop
Equations
• =
theorem MeasureTheory.Measure.InnerRegular.innerRegularWRT_isClosed_isOpen {α : Type u_1} [] {μ : } [] [] [h : μ.InnerRegular] :
μ.InnerRegularWRT IsClosed IsOpen
theorem MeasureTheory.Measure.InnerRegular.exists_compact_not_null {α : Type u_1} [] {μ : } [] [μ.InnerRegular] :
(∃ (K : Set α), μ K 0) μ 0
theorem MeasurableSet.exists_lt_isCompact {α : Type u_1} [] {μ : } [] [μ.InnerRegular] ⦃A : Set α (hA : ) {r : ENNReal} (hr : r < μ A) :
KA, 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} [] {μ : } [] [] [] [] [] [h : μ.InnerRegular] {f : αβ} (hf : ) :
.InnerRegular
theorem MeasureTheory.Measure.InnerRegular.map {α : Type u_1} {β : Type u_2} [] {μ : } [] [] [] [] [] [μ.InnerRegular] (f : α ≃ₜ β) :
(MeasureTheory.Measure.map (⇑f) μ).InnerRegular
theorem MeasureTheory.Measure.InnerRegular.map_iff {α : Type u_1} {β : Type u_2} [] {μ : } [] [] [] [] [] (f : α ≃ₜ β) :
(MeasureTheory.Measure.map (⇑f) μ).InnerRegular μ.InnerRegular
theorem MeasurableSet.exists_isCompact_lt_add {α : Type u_1} [] {μ : } [] [μ.InnerRegularCompactLTTop] ⦃A : Set α (hA : ) (h'A : μ A ) {ε : ENNReal} (hε : ε 0) :
KA, μ 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} [] {μ : } [] [μ.InnerRegularCompactLTTop] [] [] ⦃A : Set α (hA : ) (h'A : μ A ) {ε : ENNReal} (hε : ε 0) :
KA, μ 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} [] {μ : } [] [] [μ.InnerRegularCompactLTTop] ⦃A : Set α (hA : ) (h'A : μ A ) {ε : ENNReal} (hε : ε 0) :
KA, μ (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} [] {μ : } [] [] [] [μ.InnerRegularCompactLTTop] ⦃A : Set α (hA : ) (h'A : μ A ) {ε : ENNReal} (hε : ε 0) :
KA, μ (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} [] {μ : } [] [μ.InnerRegularCompactLTTop] ⦃A : Set α (hA : ) (h'A : μ A ) {r : ENNReal} (hr : r < μ A) :
KA, 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} [] {μ : } [] [μ.InnerRegularCompactLTTop] ⦃A : Set α (hA : ) (h'A : μ A ) :
μ A = ⨆ (K : Set α), ⨆ (_ : K A), ⨆ (_ : ), μ 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} [] {μ : } [] [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]
instance MeasureTheory.Measure.InnerRegularCompactLTTop.instInnerRegularOfIsFiniteMeasure {α : Type u_1} [] {μ : } [] [h : μ.InnerRegularCompactLTTop] :
μ.InnerRegular
Equations
• =
@[instance 50]
instance MeasureTheory.Measure.InnerRegularCompactLTTop.instWeaklyRegularOfBorelSpaceOfR1SpaceOfIsFiniteMeasure {α : Type u_1} [] {μ : } [] [] [] [μ.InnerRegularCompactLTTop] :
μ.WeaklyRegular
Equations
• =
@[instance 50]
instance MeasureTheory.Measure.InnerRegularCompactLTTop.instRegularOfBorelSpaceOfR1SpaceOfIsFiniteMeasure {α : Type u_1} [] {μ : } [] [] [] [h : μ.InnerRegularCompactLTTop] :
μ.Regular
Equations
• =
theorem IsCompact.exists_isOpen_lt_of_lt {α : Type u_1} [] {μ : } [] [μ.InnerRegularCompactLTTop] [] [] {K : Set α} (hK : ) (r : ENNReal) (hr : μ K < r) :
∃ (U : Set α), K U μ U < r
theorem IsCompact.measure_eq_iInf_isOpen {α : Type u_1} [] {μ : } [] [μ.InnerRegularCompactLTTop] [] [] {K : Set α} (hK : ) :
μ K = ⨅ (U : Set α), ⨅ (_ : K 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} [] {μ : } [] [μ.InnerRegularCompactLTTop] [] [] {K : Set α} (hK : ) :
μ K = ⨅ (U : Set α), ⨅ (_ : K 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} [] {μ : } [] [μ.InnerRegularCompactLTTop] [] [] {K : Set α} (hK : ) {ε : ENNReal} (hε : ε 0) :
∃ (U : Set α), K U μ U < μ K + ε
theorem MeasurableSet.exists_isOpen_symmDiff_lt {α : Type u_1} [] {μ : } [] [μ.InnerRegularCompactLTTop] [] [] {s : Set α} (hs : ) (hμs : μ s ) {ε : ENNReal} (hε : ε 0) :
∃ (U : Set α), μ 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} [] {μ : } [] [μ.InnerRegularCompactLTTop] [] [] {s : Set α} (hs : ) (hμs : μ s ) {ε : ENNReal} (hε : ε 0) :
∃ (U : Set α), μ 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} [] {μ : } [] [h : μ.InnerRegularCompactLTTop] (c : ENNReal) :
(c μ).InnerRegularCompactLTTop
Equations
• =
instance MeasureTheory.Measure.InnerRegularCompactLTTop.smul_nnreal {α : Type u_1} [] {μ : } [] [μ.InnerRegularCompactLTTop] (c : NNReal) :
(c μ).InnerRegularCompactLTTop
Equations
• =
@[instance 80]
instance MeasureTheory.Measure.InnerRegularCompactLTTop.instInnerRegularOfSigmaFinite {α : Type u_1} [] {μ : } [] [μ.InnerRegularCompactLTTop] :
μ.InnerRegular
Equations
• =
theorem MeasureTheory.Measure.InnerRegularCompactLTTop.map_of_continuous {α : Type u_1} {β : Type u_2} [] {μ : } [] [] [] [] [] [h : μ.InnerRegularCompactLTTop] {f : αβ} (hf : ) :
.InnerRegularCompactLTTop
Equations
• =
theorem IsOpen.exists_lt_isClosed {α : Type u_1} [] {μ : } [] [μ.WeaklyRegular] ⦃U : Set α (hU : ) {r : ENNReal} (hr : r < μ U) :
FU, 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} [] [] ⦃U : Set α (hU : ) (μ : ) [μ.WeaklyRegular] :
μ U = ⨆ (F : Set α), ⨆ (_ : F U), ⨆ (_ : ), μ 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} [] {μ : } [] [μ.WeaklyRegular] :
μ.InnerRegularWRT IsClosed fun (s : Set α) => μ s
theorem MeasurableSet.exists_isClosed_lt_add {α : Type u_1} [] {μ : } [] [μ.WeaklyRegular] {s : Set α} (hs : ) (hμs : μ s ) {ε : ENNReal} (hε : ε 0) :
Ks, μ 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} [] {μ : } [] [μ.WeaklyRegular] ⦃A : Set α (hA : ) (h'A : μ A ) {ε : ENNReal} (hε : ε 0) :
FA, μ (A \ F) < ε
theorem MeasurableSet.exists_lt_isClosed_of_ne_top {α : Type u_1} [] {μ : } [] [μ.WeaklyRegular] ⦃A : Set α (hA : ) (h'A : μ A ) {r : ENNReal} (hr : r < μ A) :
KA, 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} [] {μ : } [] [μ.WeaklyRegular] ⦃A : Set α (hA : ) (h'A : μ A ) :
μ A = ⨆ (K : Set α), ⨆ (_ : K A), ⨆ (_ : ), μ 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} [] {μ : } [] [] [μ.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} [] {μ : } [] [μ.WeaklyRegular] {x : ENNReal} (hx : x ) :
(x μ).WeaklyRegular
instance MeasureTheory.Measure.WeaklyRegular.smul_nnreal {α : Type u_1} [] {μ : } [] [μ.WeaklyRegular] (c : NNReal) :
(c μ).WeaklyRegular
Equations
• =
instance MeasureTheory.Measure.Regular.zero {α : Type u_1} [] [] :
Equations
• =
theorem IsOpen.exists_lt_isCompact {α : Type u_1} [] {μ : } [] [μ.Regular] ⦃U : Set α (hU : ) {r : ENNReal} (hr : r < μ U) :
KU, 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} [] [] ⦃U : Set α (hU : ) (μ : ) [μ.Regular] :
μ U = ⨆ (K : Set α), ⨆ (_ : K U), ⨆ (_ : ), μ 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} [] {μ : } [] [μ.Regular] :
(∃ (K : Set α), μ K 0) μ 0
@[instance 100]
instance MeasureTheory.Measure.Regular.instInnerRegularCompactLTTop {α : Type u_1} [] {μ : } [] [μ.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} [] {μ : } [] [] [] [] [] [μ.Regular] (f : α ≃ₜ β) :
(MeasureTheory.Measure.map (⇑f) μ).Regular
theorem MeasureTheory.Measure.Regular.map_iff {α : Type u_1} {β : Type u_2} [] {μ : } [] [] [] [] [] (f : α ≃ₜ β) :
(MeasureTheory.Measure.map (⇑f) μ).Regular μ.Regular
theorem MeasureTheory.Measure.Regular.smul {α : Type u_1} [] {μ : } [] [μ.Regular] {x : ENNReal} (hx : x ) :
(x μ).Regular
instance MeasureTheory.Measure.Regular.smul_nnreal {α : Type u_1} [] {μ : } [] [μ.Regular] (c : NNReal) :
(c μ).Regular
Equations
• =
theorem MeasureTheory.Measure.Regular.restrict_of_measure_ne_top {α : Type u_1} [] {μ : } [] [] [] [μ.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
• =