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

structure MeasureTheory.Measure.MeasureDense {X : Type u_1} [m : MeasurableSpace X] (μ : MeasureTheory.Measure X) (𝒜 : Set (Set X)) : Prop

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 : Set X) : 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.

theorem MeasureTheory.Measure.MeasureDense.nonempty {X : Type u_1} [m : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝒜 : Set (Set X)} (h𝒜 : μ.MeasureDense 𝒜) : 𝒜.Nonempty

theorem MeasureTheory.Measure.MeasureDense.nonempty' {X : Type u_1} [m : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝒜 : Set (Set X)} (h𝒜 : μ.MeasureDense 𝒜) : {s : Set X | s ∈ 𝒜 ∧ μ s ≠ ⊤}.Nonempty

theorem MeasureTheory.measureDense_measurableSet {X : Type u_1} [m : MeasurableSpace X] {μ : MeasureTheory.Measure X} : μ.MeasureDense {s : Set X | MeasurableSet s}

The set of measurable sets is measure-dense.

theorem MeasureTheory.Measure.MeasureDense.fin_meas_approx {X : Type u_1} [m : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝒜 : Set (Set X)} (h𝒜 : μ.MeasureDense 𝒜) {s : Set X} (ms : MeasurableSet s) (hμs : μ s ≠ ⊤) (ε : ℝ) (ε_pos : 0 < ε) : ∃ t ∈ 𝒜, μ t ≠ ⊤ ∧ μ (symmDiff s t) < ENNReal.ofReal ε

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.

theorem MeasureTheory.Measure.MeasureDense.indicatorConstLp_subset_closure {X : Type u_1} {E : Type u_2} [m : MeasurableSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} (p : ENNReal) [one_le_p : Fact (1 ≤ p)] [p_ne_top : Fact (p ≠ ⊤)] {𝒜 : Set (Set X)} (h𝒜 : μ.MeasureDense 𝒜) (c : E) : {x : ↥(MeasureTheory.Lp E p μ) | ∃ (s : Set X) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤), MeasureTheory.indicatorConstLp p hs hμs c = x} ⊆ closure {x : ↥(MeasureTheory.Lp E p μ) | ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : μ s ≠ ⊤), MeasureTheory.indicatorConstLp p ⋯ hμs c = x}

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

theorem MeasureTheory.Measure.MeasureDense.fin_meas {X : Type u_1} [m : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝒜 : Set (Set X)} (h𝒜 : μ.MeasureDense 𝒜) : μ.MeasureDense {s : Set X | s ∈ 𝒜 ∧ μ s ≠ ⊤}

If a family of sets 𝒜 is measure-dense in X, then it is also the case for the sets in 𝒜 with finite measure.

theorem MeasureTheory.Measure.MeasureDense.of_generateFrom_isSetAlgebra_finite {X : Type u_1} [m : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝒜 : Set (Set X)} [MeasureTheory.IsFiniteMeasure μ] (h𝒜 : MeasureTheory.IsSetAlgebra 𝒜) (hgen : m = MeasurableSpace.generateFrom 𝒜) : μ.MeasureDense 𝒜

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

theorem MeasureTheory.Measure.MeasureDense.of_generateFrom_isSetAlgebra_sigmaFinite {X : Type u_1} [m : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝒜 : Set (Set X)} (h𝒜 : MeasureTheory.IsSetAlgebra 𝒜) (S : μ.FiniteSpanningSetsIn 𝒜) (hgen : m = MeasurableSpace.generateFrom 𝒜) : μ.MeasureDense 𝒜

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

class MeasureTheory.IsSeparable {X : Type u_1} [m : MeasurableSpace X] (μ : MeasureTheory.Measure X) : Prop

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.

• exists_countable_measureDense : ∃ (𝒜 : Set (Set X)), 𝒜.Countable ∧ μ.MeasureDense 𝒜

theorem MeasureTheory.exists_countable_measureDense {X : Type u_1} [m : MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsSeparable μ] : ∃ (𝒜 : Set (Set X)), 𝒜.Countable ∧ μ.MeasureDense 𝒜

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

theorem MeasureTheory.isSeparable_of_sigmaFinite {X : Type u_1} [m : MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasurableSpace.CountablyGenerated X] [MeasureTheory.SigmaFinite μ] : MeasureTheory.IsSeparable μ

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.

instance MeasureTheory.instIsSeparableOfCountablyGeneratedOfSFinite {X : Type u_1} [m : MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasurableSpace.CountablyGenerated X] [MeasureTheory.SFinite μ] : MeasureTheory.IsSeparable μ

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

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

instance MeasureTheory.Lp.SecondCountableTopology {X : Type u_1} {E : Type u_2} [m : MeasurableSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} {p : ENNReal} [one_le_p : Fact (1 ≤ p)] [p_ne_top : Fact (p ≠ ⊤)] [MeasureTheory.IsSeparable μ] [TopologicalSpace.SeparableSpace E] : SecondCountableTopology ↥(MeasureTheory.Lp E p μ)

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.