Lemma A1: Lebesgue decomposition with respect to a set of measures

def MeasureTheory.aeSet {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (S : Set (Measure 𝓧)) : Filter 𝓧

The almost everywhere filter with respect to a set of measures, defined as the supremum of the almost everywhere filters of the measures in the set.

Equations

• MeasureTheory.aeSet S = ⨆ m ∈ S, MeasureTheory.ae m

theorem MeasureTheory.mem_aeSet_iff {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (Measure 𝓧)} {t : Set 𝓧} : t ∈ aeSet S ↔ ∀ m ∈ S, m tᶜ = 0

structure MeasureTheory.nullSet {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (s : Set 𝓧) (S : Set (Measure 𝓧)) : Prop

A set is null for a set of measures if it is measurable and has measure zero for all measures in the set.

• measurableSet : MeasurableSet s
• null (μ : Measure 𝓧) : μ ∈ S → μ s = 0

@[simp]

theorem MeasureTheory.nullSet_empty {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (Measure 𝓧)} : nullSet ∅ S

theorem MeasureTheory.nullSet.union {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (Measure 𝓧)} {s t : Set 𝓧} (hs : nullSet s S) (ht : nullSet t S) : nullSet (s ∪ t) S

theorem MeasureTheory.compl_mem_aeSet_of_nullSet {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {s : Set 𝓧} {S : Set (Measure 𝓧)} (hs : nullSet s S) : sᶜ ∈ aeSet S

Copied and adapted from the exhaustion file. Should probably be generalized.

theorem MeasureTheory.exists_auxMaxNullSet_measure_ge {α : Type u_2} {mα : MeasurableSpace α} (ν : Measure α) [IsFiniteMeasure ν] (S : Set (Measure α)) (n : ℕ) : ∃ (t : Set α), MeasurableSet t ∧ nullSet t S ∧ (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : nullSet s S), ν s) - 1 / ↑n ≤ ν t

def MeasureTheory.Measure.auxMaxNullSet {α : Type u_2} {mα : MeasurableSpace α} (ν : Measure α) [IsFiniteMeasure ν] (S : Set (Measure α)) (n : ℕ) : Set α

A null set for S with close to maximal measure with respect to ν.

Equations

• ν.auxMaxNullSet S n = ⋯.choose

theorem MeasureTheory.measurableSet_auxMaxNullSet {α : Type u_2} {mα : MeasurableSpace α} {ν : Measure α} {S : Set (Measure α)} [IsFiniteMeasure ν] (n : ℕ) : MeasurableSet (ν.auxMaxNullSet S n)

theorem MeasureTheory.nullSet_auxMaxNullSet {α : Type u_2} {mα : MeasurableSpace α} (ν : Measure α) [IsFiniteMeasure ν] (S : Set (Measure α)) (n : ℕ) : nullSet (ν.auxMaxNullSet S n) S

theorem MeasureTheory.measure_auxMaxNullSet_le {α : Type u_2} {mα : MeasurableSpace α} (ν : Measure α) [IsFiniteMeasure ν] (S : Set (Measure α)) (n : ℕ) : ν (ν.auxMaxNullSet S n) ≤ ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : nullSet s S), ν s

theorem MeasureTheory.measure_auxMaxNullSet_ge {α : Type u_2} {mα : MeasurableSpace α} (ν : Measure α) [IsFiniteMeasure ν] (S : Set (Measure α)) (n : ℕ) : (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : nullSet s S), ν s) - 1 / ↑n ≤ ν (ν.auxMaxNullSet S n)

theorem MeasureTheory.tendsto_measure_auxMaxNullSet {α : Type u_2} {mα : MeasurableSpace α} (ν : Measure α) [IsFiniteMeasure ν] (S : Set (Measure α)) : Filter.Tendsto (fun (n : ℕ) => ν (ν.auxMaxNullSet S n)) Filter.atTop (nhds (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : nullSet s S), ν s))

def MeasureTheory.Measure.maxNullSet {α : Type u_2} {mα : MeasurableSpace α} (ν : Measure α) [IsFiniteMeasure ν] (S : Set (Measure α)) : Set α

A null set for S with maximal measure with respect to ν.

Equations

• ν.maxNullSet S = ⋃ (n : ℕ), ν.auxMaxNullSet S n

theorem MeasureTheory.measurableSet_maxNullSet {α : Type u_2} {mα : MeasurableSpace α} {ν : Measure α} {S : Set (Measure α)} [IsFiniteMeasure ν] : MeasurableSet (ν.maxNullSet S)

theorem MeasureTheory.nullSet_maxNullSet {α : Type u_2} {mα : MeasurableSpace α} (ν : Measure α) [IsFiniteMeasure ν] (S : Set (Measure α)) : nullSet (ν.maxNullSet S) S

theorem MeasureTheory.measure_maxNullSet {α : Type u_2} {mα : MeasurableSpace α} (ν : Measure α) [IsFiniteMeasure ν] (S : Set (Measure α)) : ν (ν.maxNullSet S) = ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : nullSet s S), ν s

theorem MeasureTheory.A1_of_isFiniteMeasure {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (Q : Measure 𝓧) [IsFiniteMeasure Q] (S : Set (Measure 𝓧)) : ∃ (ρ : Measure 𝓧 × Measure 𝓧), (∀ (t : Set 𝓧), nullSet t S → ρ.1 t = 0) ∧ ρ.2 (Q.maxNullSet S)ᶜ = 0 ∧ Q = ρ.1 + ρ.2

theorem MeasureTheory.A1 {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (Q : Measure 𝓧) [SFinite Q] (S : Set (Measure 𝓧)) : ∃ (ρ : Measure 𝓧 × Measure 𝓧), (∀ (t : Set 𝓧), nullSet t S → ρ.1 t = 0) ∧ (∃ (s : Set 𝓧), nullSet s S ∧ ρ.2 sᶜ = 0) ∧ Q = ρ.1 + ρ.2

noncomputable def MeasureTheory.Measure.acSetPart {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (Q : Measure 𝓧) [SFinite Q] (S : Set (Measure 𝓧)) : Measure 𝓧

Absolutely continuous part of a measure with respect to a set of measures.

Equations

• Q.acSetPart S = ⋯.choose.1

noncomputable def MeasureTheory.Measure.singularSetPart {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (Q : Measure 𝓧) [SFinite Q] (S : Set (Measure 𝓧)) : Measure 𝓧

Singular part of a measure with respect to a set of measures.

Equations

• Q.singularSetPart S = ⋯.choose.2

def MeasureTheory.acSet {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (Q : Measure 𝓧) [SFinite Q] (S : Set (Measure 𝓧)) : Set 𝓧

A null set for S such that Q.acSetPart S (acSet Q S) = 0 and Q.singularSetPart S (Q.acSet Q S)ᶜ = 0 and

Equations

• MeasureTheory.acSet Q S = ⋯.choose

theorem MeasureTheory.acSetPart_nullSet {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (Q : Measure 𝓧) [SFinite Q] (S : Set (Measure 𝓧)) {t : Set 𝓧} (ht : nullSet t S) : (Q.acSetPart S) t = 0

theorem MeasureTheory.nullSet_acSet {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (Q : Measure 𝓧) [SFinite Q] (S : Set (Measure 𝓧)) : nullSet (acSet Q S) S

theorem MeasureTheory.measurableSet_acSet {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (Q : Measure 𝓧) [SFinite Q] (S : Set (Measure 𝓧)) : MeasurableSet (acSet Q S)

@[simp]

theorem MeasureTheory.acSetPart_acSet {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (Q : Measure 𝓧) [SFinite Q] (S : Set (Measure 𝓧)) : (Q.acSetPart S) (acSet Q S) = 0

@[simp]

theorem MeasureTheory.singularSetPart_acSet_compl {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (Q : Measure 𝓧) [SFinite Q] (S : Set (Measure 𝓧)) : (Q.singularSetPart S) (acSet Q S)ᶜ = 0

theorem MeasureTheory.singular_singularSetPart {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (Q : Measure 𝓧) [SFinite Q] (S : Set (Measure 𝓧)) : (Q.acSetPart S).MutuallySingular (Q.singularSetPart S)

theorem MeasureTheory.acSetPart_add_singularSetPart {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (Q : Measure 𝓧) [SFinite Q] (S : Set (Measure 𝓧)) : Q.acSetPart S + Q.singularSetPart S = Q

theorem MeasureTheory.measure_acSet_diff {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {Q : Measure 𝓧} [SFinite Q] {S : Set (Measure 𝓧)} {s : Set 𝓧} (hs : nullSet s S) : Q (s \ acSet Q S) = 0

theorem MeasureTheory.ae_imp_mem_acSet {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} (Q : Measure 𝓧) [SFinite Q] {S : Set (Measure 𝓧)} {s : Set 𝓧} (hs : nullSet s S) : ∀ᵐ (x : 𝓧) ∂Q, x ∈ s → x ∈ acSet Q S

theorem MeasureTheory.measure_acSet {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (Measure 𝓧)} {Q μ : Measure 𝓧} [SFinite Q] (hS : μ ∈ S) : μ (acSet Q S) = 0

theorem MeasureTheory.ae_mem_compl_acSet {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (Measure 𝓧)} (Q : Measure 𝓧) [SFinite Q] {μ : Measure 𝓧} (hS : μ ∈ S) : ∀ᵐ (x : 𝓧) ∂μ, x ∈ (acSet Q S)ᶜ