Documentation

Mathlib.MeasureTheory.Decomposition.Exhaustion

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 #

Main statements #

References #

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

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
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))

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

Equations
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' {α : 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 = ∞.

@[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
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 =

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

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

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