Method of exhaustion

If μ, ν are two measures with ν s-finite, then there exists a set s such that μ is sigma-finite on s, and for all sets t ⊆ sᶜ, either ν t = 0 or μ t = ∞.

Main definitions

• MeasureTheory.Measure.sigmaFiniteSetWRT: if such a set exists, μ.sigmaFiniteSetWRT ν is a measurable set such that μ.restrict (μ.sigmaFiniteSetWRT ν) is sigma-finite and for all sets t ⊆ (μ.sigmaFiniteSetWRT ν)ᶜ, either ν t = 0 or μ t = ∞. If no such set exists (which is only possible if ν is not s-finite), we define μ.sigmaFiniteSetWRT ν = ∅.
• MeasureTheory.Measure.sigmaFiniteSet: for an s-finite measure μ, a measurable set such that μ.restrict μ.sigmaFiniteSet is sigma-finite, and for all sets s ⊆ μ.sigmaFiniteSetᶜ, either μ s = 0 or μ s = ∞. Defined as μ.sigmaFiniteSetWRT μ.

Main statements

• measure_eq_top_of_subset_compl_sigmaFiniteSetWRT: for s-finite ν, for all sets s in (sigmaFiniteSetWRT μ ν)ᶜ, if ν s ≠ 0 then μ s = ∞.

• An instance showing that μ.restrict (sigmaFiniteSetWRT μ ν) is sigma-finite.

• restrict_compl_sigmaFiniteSetWRT: if μ ≪ ν and ν is s-finite, then μ.restrict (μ.sigmaFiniteSetWRT ν)ᶜ = ∞ • ν.restrict (μ.sigmaFiniteSetWRT ν)ᶜ. As a consequence, that restriction is s-finite.

• An instance showing that μ.restrict μ.sigmaFiniteSet is sigma-finite.

• restrict_compl_sigmaFiniteSet_eq_zero_or_top: the measure μ.restrict μ.sigmaFiniteSetᶜ takes only two values: 0 and ∞ .

• measure_compl_sigmaFiniteSet_eq_zero_iff_sigmaFinite: a measure μ is sigma-finite iff μ μ.sigmaFiniteSetᶜ = 0.

References

• [P. R. Halmos, Measure theory, 17.3 and 30.11][halmos1950measure]

def MeasureTheory.Measure.sigmaFiniteSetWRT {α : Type u_1} {mα : MeasurableSpace α} (μ ν : Measure α) : Set α

A measurable set such that μ.restrict (μ.sigmaFiniteSetWRT ν) is sigma-finite and for all measurable sets t ⊆ sᶜ, either ν t = 0 or μ t = ∞.

Equations

• μ.sigmaFiniteSetWRT ν = if h : ∃ (s : Set α), MeasurableSet s ∧ MeasureTheory.SigmaFinite (μ.restrict s) ∧ ∀ t ⊆ sᶜ, ν t ≠ 0 → μ t = ⊤ then h.choose else ∅

theorem MeasureTheory.measurableSet_sigmaFiniteSetWRT {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} : MeasurableSet (μ.sigmaFiniteSetWRT ν)

instance MeasureTheory.instSigmaFiniteRestrictSigmaFiniteSetWRT {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} : SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT ν))

We prove that the condition in the definition of sigmaFiniteSetWRT is true for finite measures. Since every s-finite measure is absolutely continuous with respect to a finite measure, the condition will then also be true for s-finite measures.

theorem MeasureTheory.exists_isSigmaFiniteSet_measure_ge {α : Type u_1} {mα : MeasurableSpace α} (μ ν : Measure α) [IsFiniteMeasure ν] (n : ℕ) : ∃ (t : Set α), MeasurableSet t ∧ SigmaFinite (μ.restrict t) ∧ (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / ↑n ≤ ν t

Let C be the supremum of ν s over all measurable sets s such that μ.restrict s is sigma-finite. C is finite since ν is a finite measure. Then there exists a measurable set t with μ.restrict t sigma-finite such that ν t ≥ C - 1/n.

def MeasureTheory.Measure.sigmaFiniteSetGE {α : Type u_1} {mα : MeasurableSpace α} (μ ν : Measure α) [IsFiniteMeasure ν] (n : ℕ) : Set α

A measurable set such that μ.restrict (μ.sigmaFiniteSetGE ν n) is sigma-finite and for C the supremum of ν s over all measurable sets s with μ.restrict s sigma-finite, ν (μ.sigmaFiniteSetGE ν n) ≥ C - 1/n.

Equations

• μ.sigmaFiniteSetGE ν n = ⋯.choose

theorem MeasureTheory.measurableSet_sigmaFiniteSetGE {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} [IsFiniteMeasure ν] (n : ℕ) : MeasurableSet (μ.sigmaFiniteSetGE ν n)

theorem MeasureTheory.sigmaFinite_restrict_sigmaFiniteSetGE {α : Type u_1} {mα : MeasurableSpace α} (μ ν : Measure α) [IsFiniteMeasure ν] (n : ℕ) : SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))

theorem MeasureTheory.measure_sigmaFiniteSetGE_le {α : Type u_1} {mα : MeasurableSpace α} (μ ν : Measure α) [IsFiniteMeasure ν] (n : ℕ) : ν (μ.sigmaFiniteSetGE ν n) ≤ ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s

theorem MeasureTheory.measure_sigmaFiniteSetGE_ge {α : Type u_1} {mα : MeasurableSpace α} (μ ν : Measure α) [IsFiniteMeasure ν] (n : ℕ) : (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / ↑n ≤ ν (μ.sigmaFiniteSetGE ν n)

theorem MeasureTheory.tendsto_measure_sigmaFiniteSetGE {α : Type u_1} {mα : MeasurableSpace α} (μ ν : Measure α) [IsFiniteMeasure ν] : Filter.Tendsto (fun (n : ℕ) => ν (μ.sigmaFiniteSetGE ν n)) Filter.atTop (nhds (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s))

def MeasureTheory.Measure.sigmaFiniteSetWRT' {α : Type u_1} {mα : MeasurableSpace α} (μ ν : Measure α) [IsFiniteMeasure ν] : Set α

A measurable set such that μ.restrict (μ.sigmaFiniteSetWRT' ν) is sigma-finite and ν (μ.sigmaFiniteSetWRT' ν) has maximal measure among such sets.

Equations

• μ.sigmaFiniteSetWRT' ν = ⋃ (n : ℕ), μ.sigmaFiniteSetGE ν n

theorem MeasureTheory.measurableSet_sigmaFiniteSetWRT' {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} [IsFiniteMeasure ν] : MeasurableSet (μ.sigmaFiniteSetWRT' ν)

theorem MeasureTheory.sigmaFinite_restrict_sigmaFiniteSetWRT' {α : Type u_1} {mα : MeasurableSpace α} (μ ν : Measure α) [IsFiniteMeasure ν] : SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν))

theorem MeasureTheory.measure_sigmaFiniteSetWRT' {α : Type u_1} {mα : MeasurableSpace α} (μ ν : Measure α) [IsFiniteMeasure ν] : ν (μ.sigmaFiniteSetWRT' ν) = ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s

μ.sigmaFiniteSetWRT' ν has maximal ν-measure among all measurable sets s with sigma-finite μ.restrict s.

theorem MeasureTheory.measure_eq_top_of_subset_compl_sigmaFiniteSetWRT'_of_measurableSet {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} {s : Set α} [IsFiniteMeasure ν] (hs : MeasurableSet s) (hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ) (hνs : ν s ≠ 0) : μ s = ⊤

Auxiliary lemma for measure_eq_top_of_subset_compl_sigmaFiniteSetWRT'.

theorem MeasureTheory.measure_eq_top_of_subset_compl_sigmaFiniteSetWRT' {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} {s : Set α} [IsFiniteMeasure ν] (hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ) (hνs : ν s ≠ 0) : μ s = ⊤

For all sets s in (μ.sigmaFiniteSetWRT ν)ᶜ, if ν s ≠ 0 then μ s = ∞.

theorem MeasureTheory.measure_eq_top_of_subset_compl_sigmaFiniteSetWRT {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} {s : Set α} [SFinite ν] (hs_subset : s ⊆ (μ.sigmaFiniteSetWRT ν)ᶜ) (hνs : ν s ≠ 0) : μ s = ⊤

For all sets s in (μ.sigmaFiniteSetWRT ν)ᶜ, if ν s ≠ 0 then μ s = ∞.

theorem MeasureTheory.restrict_compl_sigmaFiniteSetWRT {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} [SFinite ν] (hμν : μ.AbsolutelyContinuous ν) : μ.restrict (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤ • ν.restrict (μ.sigmaFiniteSetWRT ν)ᶜ

@[simp]

theorem MeasureTheory.measure_compl_sigmaFiniteSetWRT {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} (hμν : μ.AbsolutelyContinuous ν) [SigmaFinite μ] [SFinite ν] : ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0

def MeasureTheory.Measure.sigmaFiniteSet {α : Type u_1} {mα : MeasurableSpace α} (μ : Measure α) : Set α

A measurable set such that μ.restrict μ.sigmaFiniteSet is sigma-finite, and for all measurable sets s ⊆ μ.sigmaFiniteSetᶜ, either μ s = 0 or μ s = ∞.

Equations

• μ.sigmaFiniteSet = μ.sigmaFiniteSetWRT μ

theorem MeasureTheory.measurableSet_sigmaFiniteSet {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} : MeasurableSet μ.sigmaFiniteSet

theorem MeasureTheory.measure_eq_zero_or_top_of_subset_compl_sigmaFiniteSet {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {t : Set α} [SFinite μ] (ht_subset : t ⊆ μ.sigmaFiniteSetᶜ) : μ t = 0 ∨ μ t = ⊤

theorem MeasureTheory.restrict_compl_sigmaFiniteSet_eq_zero_or_top {α : Type u_1} {mα : MeasurableSpace α} (μ : Measure α) [SFinite μ] (s : Set α) : (μ.restrict μ.sigmaFiniteSetᶜ) s = 0 ∨ (μ.restrict μ.sigmaFiniteSetᶜ) s = ⊤

The measure μ.restrict μ.sigmaFiniteSetᶜ takes only two values: 0 and ∞ .

instance MeasureTheory.instSigmaFiniteRestrictSigmaFiniteSet {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} : SigmaFinite (μ.restrict μ.sigmaFiniteSet)

The restriction of an s-finite measure μ to μ.sigmaFiniteSet is sigma-finite.

theorem MeasureTheory.sigmaFinite_of_measure_compl_sigmaFiniteSet_eq_zero {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} (h : μ μ.sigmaFiniteSetᶜ = 0) : SigmaFinite μ

@[simp]

theorem MeasureTheory.measure_compl_sigmaFiniteSet {α : Type u_1} {mα : MeasurableSpace α} (μ : Measure α) [SigmaFinite μ] : μ μ.sigmaFiniteSetᶜ = 0

theorem MeasureTheory.measure_compl_sigmaFiniteSet_eq_zero_iff_sigmaFinite {α : Type u_1} {mα : MeasurableSpace α} (μ : Measure α) : μ μ.sigmaFiniteSetᶜ = 0 ↔ SigmaFinite μ

An s-finite measure μ is sigma-finite iff μ μ.sigmaFiniteSetᶜ = 0.