Documentation

Mathlib.MeasureTheory.Decomposition.Lebesgue

Lebesgue decomposition #

This file proves the Lebesgue decomposition theorem. The Lebesgue decomposition theorem states that, given two σ-finite measures μ and ν, there exists a σ-finite measure ξ and a measurable function f such that μ = ξ + fν and ξ is mutually singular with respect to ν.

The Lebesgue decomposition provides the Radon-Nikodym theorem readily.

Main definitions #

Main results #

Tags #

Lebesgue decomposition theorem

A pair of measures μ and ν is said to HaveLebesgueDecomposition if there exists a measure ξ and a measurable function f, such that ξ is mutually singular with respect to ν and μ = ξ + ν.withDensity f.

Instances
    theorem MeasureTheory.Measure.singularPart_def {α : Type u_2} {m : MeasurableSpace α} (μ ν : Measure α) :
    μ.singularPart ν = if h : μ.HaveLebesgueDecomposition ν then (Classical.choose ).1 else 0
    @[irreducible]
    noncomputable def MeasureTheory.Measure.singularPart {α : Type u_2} {m : MeasurableSpace α} (μ ν : Measure α) :

    If a pair of measures HaveLebesgueDecomposition, then singularPart chooses the measure from HaveLebesgueDecomposition, otherwise it returns the zero measure. For sigma-finite measures, μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν).

    Equations
    @[irreducible]
    noncomputable def MeasureTheory.Measure.rnDeriv {α : Type u_2} {m : MeasurableSpace α} (μ ν : Measure α) :
    αENNReal

    If a pair of measures HaveLebesgueDecomposition, then rnDeriv chooses the measurable function from HaveLebesgueDecomposition, otherwise it returns the zero function. For sigma-finite measures, μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν).

    Equations
    theorem MeasureTheory.Measure.rnDeriv_def {α : Type u_2} {m : MeasurableSpace α} (μ ν : Measure α) :
    μ.rnDeriv ν = if h : μ.HaveLebesgueDecomposition ν then (Classical.choose ).2 else 0

    For the versions of this lemma where ν.withDensity (μ.rnDeriv ν) or μ.singularPart ν are isolated, see MeasureTheory.Measure.measure_sub_singularPart and MeasureTheory.Measure.measure_sub_rnDeriv.

    For the versions of this lemma where μ.singularPart ν or ν.withDensity (μ.rnDeriv ν) are isolated, see MeasureTheory.Measure.measure_sub_singularPart and MeasureTheory.Measure.measure_sub_rnDeriv.

    instance MeasureTheory.Measure.HaveLebesgueDecomposition.sum_left {α : Type u_1} {m : MeasurableSpace α} {ν : Measure α} {ι : Type u_2} [Countable ι] (μ : ιMeasure α) [∀ (i : ι), (μ i).HaveLebesgueDecomposition ν] :
    theorem MeasureTheory.Measure.singularPart_le {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) :
    μ.singularPart ν μ
    theorem AEMeasurable.singularPart {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_2} {x✝ : MeasurableSpace β} {f : αβ} (hf : AEMeasurable f μ) (ν : MeasureTheory.Measure α) :
    theorem AEMeasurable.withDensity_rnDeriv {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_2} {x✝ : MeasurableSpace β} {f : αβ} (hf : AEMeasurable f μ) (ν : MeasureTheory.Measure α) :
    @[simp]
    @[simp]
    theorem MeasureTheory.Measure.rnDeriv_zero {α : Type u_1} {m : MeasurableSpace α} (ν : Measure α) :
    rnDeriv 0 ν =ᶠ[ae ν] 0
    @[simp]
    theorem MeasureTheory.Measure.singularPart_withDensity {α : Type u_1} {m : MeasurableSpace α} (ν : Measure α) (f : αENNReal) :
    @[simp]
    theorem MeasureTheory.Measure.singularPart_self {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) :
    μ.singularPart μ = 0
    theorem MeasureTheory.Measure.rnDeriv_self {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) [SigmaFinite μ] :
    μ.rnDeriv μ =ᶠ[ae μ] fun (x : α) => 1
    theorem MeasureTheory.Measure.lintegral_rnDeriv_lt_top_of_measure_ne_top {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (ν : Measure α) {s : Set α} (hs : μ s ) :
    ∫⁻ (x : α) in s, μ.rnDeriv ν x ν <
    theorem MeasureTheory.Measure.integrable_toReal_rnDeriv {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} [IsFiniteMeasure μ] :
    Integrable (fun (x : α) => (μ.rnDeriv ν x).toReal) ν
    theorem MeasureTheory.Measure.rnDeriv_lt_top {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) [SigmaFinite μ] :
    ∀ᵐ (x : α) ν, μ.rnDeriv ν x <

    The Radon-Nikodym derivative of a sigma-finite measure μ with respect to another measure ν is ν-almost everywhere finite.

    theorem MeasureTheory.Measure.rnDeriv_ne_top {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) [SigmaFinite μ] :
    ∀ᵐ (x : α) ν, μ.rnDeriv ν x
    theorem MeasureTheory.Measure.eq_singularPart {α : Type u_1} {m : MeasurableSpace α} {μ ν s : Measure α} {f : αENNReal} (hf : Measurable f) (hs : s.MutuallySingular ν) (hadd : μ = s + ν.withDensity f) :
    s = μ.singularPart ν

    Given measures μ and ν, if s is a measure mutually singular to ν and f is a measurable function such that μ = s + fν, then s = μ.singularPart μ.

    This theorem provides the uniqueness of the singularPart in the Lebesgue decomposition theorem, while MeasureTheory.Measure.eq_rnDeriv provides the uniqueness of the rnDeriv.

    theorem MeasureTheory.Measure.singularPart_smul {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) (r : NNReal) :
    (r μ).singularPart ν = r μ.singularPart ν
    theorem MeasureTheory.Measure.singularPart_smul_right {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) (r : NNReal) (hr : r 0) :
    μ.singularPart (r ν) = μ.singularPart ν
    theorem MeasureTheory.Measure.singularPart_add {α : Type u_1} {m : MeasurableSpace α} (μ₁ μ₂ ν : Measure α) [μ₁.HaveLebesgueDecomposition ν] [μ₂.HaveLebesgueDecomposition ν] :
    (μ₁ + μ₂).singularPart ν = μ₁.singularPart ν + μ₂.singularPart ν
    theorem MeasureTheory.Measure.eq_withDensity_rnDeriv {α : Type u_1} {m : MeasurableSpace α} {μ ν s : Measure α} {f : αENNReal} (hf : Measurable f) (hs : s.MutuallySingular ν) (hadd : μ = s + ν.withDensity f) :

    Given measures μ and ν, if s is a measure mutually singular to ν and f is a measurable function such that μ = s + fν, then f = μ.rnDeriv ν.

    This theorem provides the uniqueness of the rnDeriv in the Lebesgue decomposition theorem, while MeasureTheory.Measure.eq_singularPart provides the uniqueness of the singularPart. Here, the uniqueness is given in terms of the measures, while the uniqueness in terms of the functions is given in eq_rnDeriv.

    theorem MeasureTheory.Measure.eq_withDensity_rnDeriv₀ {α : Type u_1} {m : MeasurableSpace α} {μ ν s : Measure α} {f : αENNReal} (hf : AEMeasurable f ν) (hs : s.MutuallySingular ν) (hadd : μ = s + ν.withDensity f) :
    theorem MeasureTheory.Measure.eq_rnDeriv₀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} [SigmaFinite ν] {s : Measure α} {f : αENNReal} (hf : AEMeasurable f ν) (hs : s.MutuallySingular ν) (hadd : μ = s + ν.withDensity f) :
    f =ᶠ[ae ν] μ.rnDeriv ν
    theorem MeasureTheory.Measure.eq_rnDeriv {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} [SigmaFinite ν] {s : Measure α} {f : αENNReal} (hf : Measurable f) (hs : s.MutuallySingular ν) (hadd : μ = s + ν.withDensity f) :
    f =ᶠ[ae ν] μ.rnDeriv ν

    Given measures μ and ν, if s is a measure mutually singular to ν and f is a measurable function such that μ = s + fν, then f = μ.rnDeriv ν.

    This theorem provides the uniqueness of the rnDeriv in the Lebesgue decomposition theorem, while MeasureTheory.Measure.eq_singularPart provides the uniqueness of the singularPart. Here, the uniqueness is given in terms of the functions, while the uniqueness in terms of the functions is given in eq_withDensity_rnDeriv.

    theorem MeasureTheory.Measure.rnDeriv_withDensity₀ {α : Type u_1} {m : MeasurableSpace α} (ν : Measure α) [SigmaFinite ν] {f : αENNReal} (hf : AEMeasurable f ν) :

    The Radon-Nikodym derivative of f ν with respect to ν is f.

    theorem MeasureTheory.Measure.rnDeriv_withDensity {α : Type u_1} {m : MeasurableSpace α} (ν : Measure α) [SigmaFinite ν] {f : αENNReal} (hf : Measurable f) :

    The Radon-Nikodym derivative of f ν with respect to ν is f.

    theorem MeasureTheory.Measure.rnDeriv_restrict {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) [μ.HaveLebesgueDecomposition ν] [SigmaFinite ν] {s : Set α} (hs : MeasurableSet s) :
    (μ.restrict s).rnDeriv ν =ᶠ[ae ν] s.indicator (μ.rnDeriv ν)
    theorem MeasureTheory.Measure.rnDeriv_restrict_self {α : Type u_1} {m : MeasurableSpace α} (ν : Measure α) [SigmaFinite ν] {s : Set α} (hs : MeasurableSet s) :

    The Radon-Nikodym derivative of the restriction of a measure to a measurable set is the indicator function of this set.

    theorem MeasureTheory.Measure.rnDeriv_smul_left {α : Type u_1} {m : MeasurableSpace α} (ν μ : Measure α) [IsFiniteMeasure ν] [ν.HaveLebesgueDecomposition μ] (r : NNReal) :
    (r ν).rnDeriv μ =ᶠ[ae μ] r ν.rnDeriv μ

    Radon-Nikodym derivative of the scalar multiple of a measure. See also rnDeriv_smul_left', which requires sigma-finite ν and μ.

    theorem MeasureTheory.Measure.rnDeriv_smul_left_of_ne_top {α : Type u_1} {m : MeasurableSpace α} (ν μ : Measure α) [IsFiniteMeasure ν] [ν.HaveLebesgueDecomposition μ] {r : ENNReal} (hr : r ) :
    (r ν).rnDeriv μ =ᶠ[ae μ] r ν.rnDeriv μ

    Radon-Nikodym derivative of the scalar multiple of a measure. See also rnDeriv_smul_left_of_ne_top', which requires sigma-finite ν and μ.

    theorem MeasureTheory.Measure.rnDeriv_smul_right {α : Type u_1} {m : MeasurableSpace α} (ν μ : Measure α) [IsFiniteMeasure ν] [ν.HaveLebesgueDecomposition μ] {r : NNReal} (hr : r 0) :
    ν.rnDeriv (r μ) =ᶠ[ae μ] r⁻¹ ν.rnDeriv μ

    Radon-Nikodym derivative with respect to the scalar multiple of a measure. See also rnDeriv_smul_right', which requires sigma-finite ν and μ.

    theorem MeasureTheory.Measure.rnDeriv_smul_right_of_ne_top {α : Type u_1} {m : MeasurableSpace α} (ν μ : Measure α) [IsFiniteMeasure ν] [ν.HaveLebesgueDecomposition μ] {r : ENNReal} (hr : r 0) (hr_ne_top : r ) :
    ν.rnDeriv (r μ) =ᶠ[ae μ] r⁻¹ ν.rnDeriv μ

    Radon-Nikodym derivative with respect to the scalar multiple of a measure. See also rnDeriv_smul_right_of_ne_top', which requires sigma-finite ν and μ.

    theorem MeasureTheory.Measure.rnDeriv_add {α : Type u_1} {m : MeasurableSpace α} (ν₁ ν₂ μ : Measure α) [IsFiniteMeasure ν₁] [IsFiniteMeasure ν₂] [ν₁.HaveLebesgueDecomposition μ] [ν₂.HaveLebesgueDecomposition μ] [(ν₁ + ν₂).HaveLebesgueDecomposition μ] :
    (ν₁ + ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ + ν₂.rnDeriv μ

    Radon-Nikodym derivative of a sum of two measures. See also rnDeriv_add', which requires sigma-finite ν₁, ν₂ and μ.

    theorem MeasureTheory.Measure.exists_positive_of_not_mutuallySingular {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h : ¬μ.MutuallySingular ν) :
    ∃ (ε : NNReal), 0 < ε ∃ (E : Set α), MeasurableSet E 0 < ν E ∀ (A : Set α), MeasurableSet Aε * ν (A E) μ (A E)

    If two finite measures μ and ν are not mutually singular, there exists some ε > 0 and a measurable set E, such that ν(E) > 0 and E is positive with respect to μ - εν.

    This lemma is useful for the Lebesgue decomposition theorem.

    Given two measures μ and ν, measurableLE μ ν is the set of measurable functions f, such that, for all measurable sets A, ∫⁻ x in A, f x ∂μ ≤ ν A.

    This is useful for the Lebesgue decomposition theorem.

    Equations
    theorem MeasureTheory.Measure.LebesgueDecomposition.sup_mem_measurableLE {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} {f g : αENNReal} (hf : f measurableLE μ ν) (hg : g measurableLE μ ν) :
    (fun (a : α) => f a g a) measurableLE μ ν
    theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_succ_eq_sup {α : Sort u_2} (f : αENNReal) (m : ) (a : α) :
    ⨆ (k : ), ⨆ (_ : k m + 1), f k a = f m.succ a ⨆ (k : ), ⨆ (_ : k m), f k a
    theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} (f : αENNReal) (hf : ∀ (n : ), f n measurableLE μ ν) (n : ) :
    (fun (x : α) => ⨆ (k : ), ⨆ (_ : k n), f k x) measurableLE μ ν
    theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE' {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} (f : αENNReal) (hf : ∀ (n : ), f n measurableLE μ ν) (n : ) :
    ⨆ (k : ), ⨆ (_ : k n), f k measurableLE μ ν
    theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone {α : Type u_2} (f : αENNReal) :
    Monotone fun (n : ) (x : α) => ⨆ (k : ), ⨆ (_ : k n), f k x
    theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone' {α : Type u_2} (f : αENNReal) (x : α) :
    Monotone fun (n : ) => ⨆ (k : ), ⨆ (_ : k n), f k x
    theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_le_le {α : Type u_2} (f : αENNReal) (n k : ) (hk : k n) :
    f k fun (x : α) => ⨆ (k : ), ⨆ (_ : k n), f k x

    Any pair of finite measures μ and ν, HaveLebesgueDecomposition. That is to say, there exist a measure ξ and a measurable function f, such that ξ is mutually singular with respect to ν and μ = ξ + ν.withDensity f.

    This is not an instance since this is also shown for the more general σ-finite measures with MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite.

    If any finite measure has a Lebesgue decomposition with respect to ν, then the same is true for any s-finite measure.

    @[instance 100]

    The Lebesgue decomposition theorem: Any s-finite measure μ has Lebesgue decomposition with respect to any σ-finite measure ν. That is to say, there exist a measure ξ and a measurable function f, such that ξ is mutually singular with respect to ν and μ = ξ + ν.withDensity f

    theorem MeasureTheory.Measure.rnDeriv_smul_left' {α : Type u_1} {m : MeasurableSpace α} (ν μ : Measure α) [SigmaFinite ν] [SigmaFinite μ] (r : NNReal) :
    (r ν).rnDeriv μ =ᶠ[ae μ] r ν.rnDeriv μ

    Radon-Nikodym derivative of the scalar multiple of a measure. See also rnDeriv_smul_left, which has no hypothesis on μ but requires finite ν.

    theorem MeasureTheory.Measure.rnDeriv_smul_left_of_ne_top' {α : Type u_1} {m : MeasurableSpace α} (ν μ : Measure α) [SigmaFinite ν] [SigmaFinite μ] {r : ENNReal} (hr : r ) :
    (r ν).rnDeriv μ =ᶠ[ae μ] r ν.rnDeriv μ

    Radon-Nikodym derivative of the scalar multiple of a measure. See also rnDeriv_smul_left_of_ne_top, which has no hypothesis on μ but requires finite ν.

    theorem MeasureTheory.Measure.rnDeriv_smul_right' {α : Type u_1} {m : MeasurableSpace α} (ν μ : Measure α) [SigmaFinite ν] [SigmaFinite μ] {r : NNReal} (hr : r 0) :
    ν.rnDeriv (r μ) =ᶠ[ae μ] r⁻¹ ν.rnDeriv μ

    Radon-Nikodym derivative with respect to the scalar multiple of a measure. See also rnDeriv_smul_right, which has no hypothesis on μ but requires finite ν.

    theorem MeasureTheory.Measure.rnDeriv_smul_right_of_ne_top' {α : Type u_1} {m : MeasurableSpace α} (ν μ : Measure α) [SigmaFinite ν] [SigmaFinite μ] {r : ENNReal} (hr : r 0) (hr_ne_top : r ) :
    ν.rnDeriv (r μ) =ᶠ[ae μ] r⁻¹ ν.rnDeriv μ

    Radon-Nikodym derivative with respect to the scalar multiple of a measure. See also rnDeriv_smul_right_of_ne_top, which has no hypothesis on μ but requires finite ν.

    theorem MeasureTheory.Measure.rnDeriv_add' {α : Type u_1} {m : MeasurableSpace α} (ν₁ ν₂ μ : Measure α) [SigmaFinite ν₁] [SigmaFinite ν₂] [SigmaFinite μ] :
    (ν₁ + ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ + ν₂.rnDeriv μ

    Radon-Nikodym derivative of a sum of two measures. See also rnDeriv_add, which has no hypothesis on μ but requires finite ν₁ and ν₂.

    theorem MeasureTheory.Measure.rnDeriv_add_of_mutuallySingular {α : Type u_1} {m : MeasurableSpace α} (ν₁ ν₂ μ : Measure α) [SigmaFinite ν₁] [SigmaFinite ν₂] [SigmaFinite μ] (h : ν₂.MutuallySingular μ) :
    (ν₁ + ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ