# Separable measure #

The goal of this file is to give a sufficient condition on the measure space `(X, μ)`

and the
`NormedAddCommGroup E`

for the space `MeasureTheory.Lp E p μ`

to have `SecondCountableTopology`

when
`1 ≤ p < ∞`

. To do so we define the notion of a `MeasureTheory.MeasureDense`

family and a
separable measure (`MeasureTheory.IsSeparable`

).
We prove that if `X`

is `MeasurableSpace.CountablyGenerated`

and `μ`

is s-finite, then `μ`

is separable. We then prove that if `μ`

is separable and `E`

is second-countable,
then `Lp E p μ`

is second-countable.

A family `𝒜`

of subsets of `X`

is said to be **measure-dense** if it contains only measurable sets
and can approximate any measurable set with finite measure, in the sense that
for any measurable set `s`

such that `μ s ≠ ∞`

, `μ (s ∆ t)`

can be made
arbitrarily small when `t ∈ 𝒜`

. We show below that such a family can be chosen to contain only
sets with finite measure.
The term "measure-dense" is justified by the fact that the approximating condition translates
to the usual notion of density in the metric space made by constant indicators of measurable sets
equipped with the `Lᵖ`

norm.

A measure `μ`

is **separable** if it admits a countable and measure-dense family of sets.
The term "separable" is justified by the fact that the definition translates to the usual notion
of separability in the metric space made by constant indicators equipped with the `Lᵖ`

norm.

## Main definitions #

`MeasureTheory.Measure.MeasureDense μ 𝒜`

:`𝒜`

is a measure-dense family if it only contains measurable sets and if the following condition is satisfied: if`s`

is measurable with finite measure, then for any`ε > 0`

there exists`t ∈ 𝒜`

such that`μ (s ∆ t) < ε`

.`MeasureTheory.IsSeparable`

: A measure is separable if there exists a countable and measure-dense family.

## Main statements #

`MeasureTheory.instSecondCountableLp`

: If`μ`

is separable,`E`

is second-countable and`1 ≤ p < ∞`

then`Lp E p μ`

is second-countable. This is in particular true if`X`

is countably generated and`μ`

is s-finite.

## Implementation notes #

Through the whole file we consider a measurable space `X`

equipped with a measure `μ`

, and also
a normed commutative group `E`

. We also consider an extended non-negative real `p`

such that
`1 ≤ p < ∞`

. This is registered as instances via `one_le_p : Fact (1 ≤ p)`

and
`p_ne_top : Fact (p ≠ ∞)`

, so the properties are accessible via `one_le_p.elim`

and `p_ne_top.elim`

.

Through the whole file, when we write that an extended non-negative real is finite, it is always
written `≠ ∞`

rather than `< ∞`

. See `Ne.lt_top`

and `ne_of_lt`

to switch from one to the other.

## References #

- [D. L. Cohn,
*Measure Theory*][cohn2013measure]

## Tags #

separable measure, measure-dense, Lp space, second-countable

### Definition of a measure-dense family, basic properties and sufficient conditions #

A family `𝒜`

of sets of a measure space is said to be measure-dense if it contains only
measurable sets and can approximate any measurable set with finite measure, in the sense that
for any measurable set `s`

with finite measure the symmetric difference `s ∆ t`

can be made
arbitrarily small when `t ∈ 𝒜`

. We show below that such a family can be chosen to contain only
sets with finite measures.

The term "measure-dense" is justified by the fact that the approximating condition translates
to the usual notion of density in the metric space made by constant indicators of measurable sets
equipped with the `Lᵖ`

norm.

- measurable : ∀ s ∈ 𝒜, MeasurableSet s
Each set has to be measurable.

- approx : ∀ (s : Set X), MeasurableSet s → μ s ≠ ⊤ → ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ (symmDiff s t) < ENNReal.ofReal ε
Any measurable set can be approximated by sets in the family.

## Instances For

Each set has to be measurable.

Any measurable set can be approximated by sets in the family.

The set of measurable sets is measure-dense.

If a family of sets `𝒜`

is measure-dense in `X`

, then any measurable set with finite measure
can be approximated by sets in `𝒜`

with finite measure.

If `𝒜`

is a measure-dense family of sets and `c : E`

, then the set of constant indicators
with constant `c`

whose underlying set is in `𝒜`

is dense in the set of constant indicators
which are in `Lp E p μ`

when `1 ≤ p < ∞`

.

If a family of sets `𝒜`

is measure-dense in `X`

, then it is also the case for the sets in `𝒜`

with finite measure.

If a measurable space equipped with a finite measure is generated by an algebra of sets, then this algebra of sets is measure-dense.

If a measure space `X`

is generated by an algebra of sets which contains a monotone countable
family of sets with finite measure spanning `X`

(thus the measure is `σ`

-finite), then this algebra
of sets is measure-dense.

### Definition of a separable measure space, sufficient condition #

A measure `μ`

is separable if there exists a countable and measure-dense family of sets.

The term "separable" is justified by the fact that the definition translates to the usual notion
of separability in the metric space made by constant indicators equipped with the `Lᵖ`

norm.

## Instances

By definition, a separable measure admits a countable and measure-dense family of sets.

If a measurable space is countably generated and equipped with a `σ`

-finite measure, then the
measure is separable. This is not an instance because it is used below to prove the more
general case where `μ`

is s-finite.

If a measurable space is countably generated and equipped with an s-finite measure, then the measure is separable.

## Equations

- ⋯ = ⋯

### A sufficient condition for $L^p$ spaces to be second-countable #

If the measure `μ`

is separable (in particular if `X`

is countably generated and `μ`

is
`s`

-finite), if `E`

is a second-countable `NormedAddCommGroup`

, and if `1 ≤ p < +∞`

,
then the associated `Lᵖ`

space is second-countable.

## Equations

- ⋯ = ⋯