Documentation

Mathlib.MeasureTheory.Measure.Trim

Restriction of a measure to a sub-σ-algebra #

Main definitions #

noncomputable def MeasureTheory.Measure.trim {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (hm : m m0) :

Restriction of a measure to a sub-σ-algebra. It is common to see a measure μ on a measurable space structure m0 as being also a measure on any m ≤ m0. Since measures in mathlib have to be trimmed to the measurable space, μ itself cannot be a measure on m, hence the definition of μ.trim hm.

This notion is related to OuterMeasure.trim, see the lemma toOuterMeasure_trim_eq_trim_toOuterMeasure.

Equations
  • μ.trim hm = μ.toMeasure
Instances For
    @[simp]
    theorem MeasureTheory.trim_eq_self {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} :
    μ.trim = μ
    theorem MeasureTheory.toOuterMeasure_trim_eq_trim_toOuterMeasure {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (hm : m m0) :
    (μ.trim hm).toOuterMeasure = μ.trim
    @[simp]
    theorem MeasureTheory.zero_trim {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} (hm : m m0) :
    theorem MeasureTheory.trim_measurableSet_eq {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m m0) (hs : MeasurableSet s) :
    (μ.trim hm) s = μ s
    theorem MeasureTheory.le_trim {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m m0) :
    μ s (μ.trim hm) s
    theorem MeasureTheory.trim_add {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (hm : m m0) :
    (μ + ν).trim hm = μ.trim hm + ν.trim hm
    theorem MeasureTheory.measure_eq_zero_of_trim_eq_zero {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m m0) (h : (μ.trim hm) s = 0) :
    μ s = 0
    theorem MeasureTheory.measure_trim_toMeasurable_eq_zero {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m m0} (hs : (μ.trim hm) s = 0) :
    μ (MeasureTheory.toMeasurable (μ.trim hm) s) = 0
    theorem MeasureTheory.ae_of_ae_trim {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} (hm : m m0) {μ : MeasureTheory.Measure α} {P : αProp} (h : ∀ᵐ (x : α) ∂μ.trim hm, P x) :
    ∀ᵐ (x : α) ∂μ, P x
    theorem MeasureTheory.ae_eq_of_ae_eq_trim {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} {hm : m m0} {f₁ : αE} {f₂ : αE} (h12 : f₁ =ᵐ[μ.trim hm] f₂) :
    f₁ =ᵐ[μ] f₂
    theorem MeasureTheory.ae_le_of_ae_le_trim {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [LE E] {hm : m m0} {f₁ : αE} {f₂ : αE} (h12 : f₁ ≤ᵐ[μ.trim hm] f₂) :
    f₁ ≤ᵐ[μ] f₂
    theorem MeasureTheory.trim_trim {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} {hm₁₂ : m₁ m₂} {hm₂ : m₂ m0} :
    (μ.trim hm₂).trim hm₁₂ = μ.trim
    theorem MeasureTheory.restrict_trim {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {s : Set α} (hm : m m0) (μ : MeasureTheory.Measure α) (hs : MeasurableSet s) :
    (μ.trim hm).restrict s = (μ.restrict s).trim hm
    theorem MeasureTheory.sigmaFiniteTrim_mono {α : Type u_1} {m : MeasurableSpace α} {m₂ : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m m0) (hm₂ : m₂ m) [MeasureTheory.SigmaFinite (μ.trim )] :
    theorem MeasureTheory.Measure.AbsolutelyContinuous.trim {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} (hμν : μ.AbsolutelyContinuous ν) (hm : m m0) :
    (μ.trim hm).AbsolutelyContinuous (ν.trim hm)