# 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)][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]

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.

## Instances For

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 α⦄, MeasurableSet A → ∀ r > μ A, ∃ U ⊇ A, IsOpen U ∧ μ U < r

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

- outerRegular : ∀ ⦃A : Set α⦄, MeasurableSet A → ∀ r > μ A, ∃ U ⊇ A, IsOpen U ∧ μ U < r
- innerRegular : μ.InnerRegularWRT IsCompact IsOpen

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

- outerRegular : ∀ ⦃A : Set α⦄, MeasurableSet A → ∀ r > μ A, ∃ U ⊇ A, IsOpen U ∧ μ U < r
- innerRegular : μ.InnerRegularWRT IsClosed IsOpen

## Instances

A measure `μ`

is inner regular if, for any measurable set `s`

, then
`μ(s) = sup {μ(K) | K ⊆ s compact}`

.

- innerRegular : μ.InnerRegularWRT IsCompact fun (s : Set α) => MeasurableSet s

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

- innerRegular : μ.InnerRegularWRT IsCompact fun (s : Set α) => MeasurableSet s ∧ μ s ≠ ⊤

## Instances

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

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

Given `r`

larger than the measure of a set `A`

, there exists an open superset of `A`

with
measure less than `r`

.

For an outer regular measure, the measure of a set is the infimum of the measures of open sets containing it.

## Equations

- ⋯ = ⋯

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.

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.

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

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

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`

.

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`

.

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`

.

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`

.

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

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

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.

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

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

If `μ`

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

If `μ`

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

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 + ε`

.

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

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

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

If `μ`

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

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

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

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

Any locally finite measure on a `σ`

-compact pseudometrizable space is regular.

## Equations

- ⋯ = ⋯

Any sigma finite measure on a `σ`

-compact pseudometrizable space is inner regular.

## Equations

- ⋯ = ⋯