# Regular measures #

A measure is `outer_regular`

if the measure of any measurable set `A`

is the infimum of `μ U`

over
all open sets `U`

containing `A`

.

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 sets: the measure of any open set
`U`

is the supremum of`μ K`

over all compact sets`K`

contained in`U`

.

A measure is `weakly_regular`

if it satisfies the following properties:

- it is outer regular;
- it is inner regular for open sets with respect to closed sets: the measure of any open set
`U`

is the supremum of`μ F`

over all compact sets`F`

contained in`U`

.

In a Hausdorff topological space, regularity implies weak regularity. These three conditions are
registered as typeclasses for a measure `μ`

, and this implication is recorded as an instance.

In order to avoid code duplication, we also define a measure `μ`

to be `inner_regular`

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`

.

We prove that 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), and register some corollaries for (weakly) regular measures.

Note that a similar statement for measurable sets of infinite mass can fail. For a counterexample,
consider the group `ℝ × ℝ`

where the first factor has the discrete topology and the second one the
usual topology. It is a locally compact Hausdorff topological group, with Haar measure equal to
Lebesgue measure on each vertical fiber. The set `ℝ × {0}`

has infinite measure (by outer
regularity), but any compact set it contains has zero measure (as it is finite).

Several authors require as a definition of regularity that all measurable sets are inner regular. We have opted for the slightly weaker definition above as it holds for all Haar measures, it is enough for essentially all applications, and it is equivalent to the other definition when the measure is finite.

The interest of the notion of weak regularity is that it is enough for many applications, and it is automatically satisfied by any finite measure on a metric space.

## Main definitions #

`measure_theory.measure.outer_regular μ`

: a typeclass registering that a measure`μ`

on a topological space is outer regular.`measure_theory.measure.regular μ`

: a typeclass registering that a measure`μ`

on a topological space is regular.`measure_theory.measure.weakly_regular μ`

: a typeclass registering that a measure`μ`

on a topological space is weakly regular.`measure_theory.measure.inner_regular μ p q`

: a non-typeclass predicate saying that a measure`μ`

is inner regular for sets satisfying`q`

with respect to sets satisfying`p`

.

## Main results #

### Outer regular measures #

`set.measure_eq_infi_is_open`

asserts that, when`μ`

is outer regular, the measure of a set is the infimum of the measure of open sets containing it.`set.exists_is_open_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.
`measure_theory.measure.outer_regular.of_sigma_compact_space_of_is_locally_finite_measure`

: a locally finite measure on a`σ`

-compact metric (or even pseudo emetric) space is outer regular.

### Weakly regular measures #

`is_open.measure_eq_supr_is_closed`

asserts that the measure of an open set is the supremum of the measure of closed sets it contains.`is_open.exists_lt_is_closed`

: for an open set`U`

and`r < μ U`

, there exists a closed`F ⊆ U`

of measure greater than`r`

;`measurable_set.measure_eq_supr_is_closed_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.`measurable_set.exists_lt_is_closed_of_ne_top`

and`measurable_set.exists_is_closed_lt_add`

: a measurable set of finite measure can be approximated by a closed subset (stated as`r < μ F`

and`μ s < μ F + ε`

, respectively).`measure_theory.measure.weakly_regular.of_pseudo_emetric_space_of_is_finite_measure`

is an instance registering that a finite measure on a metric space is weakly regular (in fact, a pseudo emetric space is enough);`measure_theory.measure.weakly_regular.of_pseudo_emetric_sigma_compact_space_of_locally_finite`

is an instance registering that a locally finite measure on a`σ`

-compact metric space (or even a pseudo emetric space) is weakly regular.

### Regular measures #

`is_open.measure_eq_supr_is_compact`

asserts that the measure of an open set is the supremum of the measure of compact sets it contains.`is_open.exists_lt_is_compact`

: for an open set`U`

and`r < μ U`

, there exists a compact`K ⊆ U`

of measure greater than`r`

;`measurable_set.measure_eq_supr_is_compact_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.`measurable_set.exists_lt_is_compact_of_ne_top`

and`measurable_set.exists_is_compact_lt_add`

: a measurable set of finite measure can be approximated by a compact subset (stated as`r < μ K`

and`μ s < μ K + ε`

, respectively).`measure_theory.measure.regular.of_sigma_compact_space_of_is_locally_finite_measure`

is an instance registering that a locally finite measure on a`σ`

-compact metric space is regular (in fact, an emetric space is enough).

## Implementation notes #

The main nontrivial statement is `measure_theory.measure.inner_regular.weakly_regular_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).

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

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.

- outer_regular : ∀ ⦃A : set α⦄, measurable_set A → ∀ (r : ℝ≥0∞), r > ⇑μ A → (∃ (U : set α) (H : U ⊇ A), is_open U ∧ ⇑μ U < r)

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_infi_is_open`

.

- to_outer_regular : μ.outer_regular
- lt_top_of_is_compact : ∀ ⦃K : set α⦄, is_compact K → ⇑μ K < ⊤
- inner_regular : μ.inner_regular is_compact is_open

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

- measure_theory.measure.regular.of_sigma_compact_space_of_is_locally_finite_measure
- measure_theory.measure.regular.zero
- measure_theory.measure.regular.inv
- measure_theory.measure.regular.neg
- measure_theory.content.regular
- measure_theory.measure.regular_haar_measure
- measure_theory.measure.regular_add_haar_measure

- to_outer_regular : μ.outer_regular
- inner_regular : μ.inner_regular is_closed is_open

A measure `μ`

is weakly regular if

- it is outer regular:
`μ(A) = inf { μ(U) | A ⊆ U open }`

for`A`

measurable; - it is inner regular for open sets, using closed sets:
`μ(U) = sup {μ(F) | F ⊆ U compact}`

for`U`

open.

A regular measure is weakly regular.

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.

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), then every measurable set of finite measure can by 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.

In a metric space (or even a pseudo emetric 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 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 `measurable_set.exists_is_compact_lt_add`

and
`measurable_set.exists_lt_is_compact_of_ne_top`

.

If `μ`

is a regular measure, then any measurable set of finite measure can be approximated by a
compact subset. See also `measurable_set.exists_lt_is_compact_of_ne_top`

.

If `μ`

is a regular measure, then any measurable set of finite measure can be approximated by a
compact subset. See also `measurable_set.exists_is_compact_lt_add`

and
`measurable_set.exists_lt_is_compact_of_ne_top`

.

If `μ`

is a regular measure, then any measurable set of finite measure can be approximated by a
compact subset. See also `measurable_set.exists_is_compact_lt_add`

.

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

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

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 metric space (or even a pseudo emetric space) is weakly regular.

Any locally finite measure on a `σ`

-compact metric space (or even a pseudo emetric space) is
weakly regular.

Any locally finite measure on a `σ`

-compact (e)metric space is regular.