Measured sets

Consider a measure μ on a measurable space. One can define an extended distance on the space of measurable sets, by edist s t := μ (s ∆ t). In this file, we introduce this definition on the type synonym MeasuredSets μ, and we prove that μ is a continuous function on this space.

We also give a density criterion for this distance, in exists_measure_symmDiff_lt_of_generateFrom_isSetRing: given a ring of sets C covering the space modulo 0 and generating the measurable space structure, then any measurable set can be approximated by elements of C. Note that the covering condition is necessary: for a counterexample otherwise, take {0, 1} with the counting measure and C = {∅, {0}}. Then the set {1} can not be approximated by an element of C.

def MeasureTheory.MeasuredSets {α : Type u_1} [mα : MeasurableSpace α] (μ : Measure α) : Type u_1

The subtype of all measurable sets. We denote it as MeasuredSets μ, with an explicit but unused parameter μ, to be able to define a distance on it given by edist s t = μ (s ∆ t)

Equations

• MeasureTheory.MeasuredSets μ = { s : Set α // MeasurableSet s }

instance MeasureTheory.instSetLikeMeasuredSets {α : Type u_1} [mα : MeasurableSpace α] {μ : Measure α} : SetLike (MeasuredSets μ) α

Equations

• MeasureTheory.instSetLikeMeasuredSets = { coe := fun (s : MeasureTheory.MeasuredSets μ) => ↑s, coe_injective' := ⋯ }

instance MeasureTheory.instPseudoEMetricSpaceMeasuredSets {α : Type u_1} [mα : MeasurableSpace α] {μ : Measure α} : PseudoEMetricSpace (MeasuredSets μ)

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.MeasuredSets.edist_def {α : Type u_1} [mα : MeasurableSpace α] {μ : Measure α} (s t : MeasuredSets μ) : edist s t = μ (symmDiff ↑s ↑t)

theorem MeasureTheory.MeasuredSets.sub_le_edist {α : Type u_1} [mα : MeasurableSpace α] {μ : Measure α} (s t : MeasuredSets μ) : μ ↑s - μ ↑t ≤ edist s t

Measure on MeasuredSets is a 1-lipschitz function.

We cannot state this in terms of LipschitzWith, because ℝ≥0∞ is not a PseudoEMetricSpace.

theorem MeasureTheory.MeasuredSets.continuous_measure {α : Type u_1} [mα : MeasurableSpace α] {μ : Measure α} : Continuous fun (s : MeasuredSets μ) => μ ↑s

instance MeasureTheory.instPseudoMetricSpaceMeasuredSetsOfIsFiniteMeasure {α : Type u_1} [mα : MeasurableSpace α] {μ : Measure α} [IsFiniteMeasure μ] : PseudoMetricSpace (MeasuredSets μ)

Equations

• MeasureTheory.instPseudoMetricSpaceMeasuredSetsOfIsFiniteMeasure = PseudoEMetricSpace.toPseudoMetricSpaceOfDist (fun (s t : MeasureTheory.MeasuredSets μ) => μ.real (symmDiff ↑s ↑t)) ⋯ ⋯

theorem MeasureTheory.MeasuredSets.dist_def {α : Type u_1} [mα : MeasurableSpace α] {μ : Measure α} [IsFiniteMeasure μ] (s t : MeasuredSets μ) : dist s t = μ.real (symmDiff ↑s ↑t)

theorem MeasureTheory.MeasuredSets.real_sub_real_le_dist {α : Type u_1} [mα : MeasurableSpace α] {μ : Measure α} [IsFiniteMeasure μ] (s t : MeasuredSets μ) : μ.real ↑s - μ.real ↑t ≤ dist s t

theorem MeasureTheory.MeasuredSets.lipschitzWith_measureReal {α : Type u_1} [mα : MeasurableSpace α] {μ : Measure α} [IsFiniteMeasure μ] : LipschitzWith 1 fun (s : MeasuredSets μ) => μ.real ↑s

theorem MeasureTheory.exists_measure_symmDiff_lt_of_generateFrom_isSetRing {α : Type u_1} [mα : MeasurableSpace α] {μ : Measure α} [IsFiniteMeasure μ] {C : Set (Set α)} (hC : IsSetRing C) (h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0) (h : mα = MeasurableSpace.generateFrom C) {s : Set α} (hs : MeasurableSet s) {ε : ENNReal} (hε : 0 < ε) : ∃ t ∈ C, μ (symmDiff t s) < ε

Given a ring of sets C covering the space modulo 0 and generating the measurable space structure, any measurable set can be approximated by elements of C.

theorem MeasureTheory.exists_measure_symmDiff_lt_of_generateFrom_isSetSemiring {α : Type u_1} [mα : MeasurableSpace α] {μ : Measure α} [IsFiniteMeasure μ] {C : Set (Set α)} (hC : IsSetSemiring C) (h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0) (h : mα = MeasurableSpace.generateFrom C) {s : Set α} (hs : MeasurableSet s) {ε : ENNReal} (hε : 0 < ε) : ∃ t ∈ supClosure C, μ (symmDiff t s) < ε

Given a semiring of sets C covering the space modulo 0 and generating the measurable space structure, any measurable set can be approximated by finite unions of elements of C.

theorem MeasureTheory.dense_of_generateFrom_isSetRing {α : Type u_1} [mα : MeasurableSpace α] {μ : Measure α} [IsFiniteMeasure μ] {C : Set (Set α)} (hC : IsSetRing C) (h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0) (h : mα = MeasurableSpace.generateFrom C) : Dense (SetLike.coe ⁻¹' C)

A ring of sets covering the space modulo 0 and generating the measurable space structure is dense among measurable sets.

theorem MeasureTheory.dense_of_generateFrom_isSetSemiring {α : Type u_1} [mα : MeasurableSpace α] {μ : Measure α} [IsFiniteMeasure μ] {C : Set (Set α)} (hC : IsSetSemiring C) (h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0) (h : mα = MeasurableSpace.generateFrom C) : Dense (SetLike.coe ⁻¹' supClosure C)

Given a semiring of sets C covering the space modulo 0 and generating the measurable space structure, finite unions of elements of C are dense among measurable sets.