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
Instances For
    @[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) :
    (MeasureTheory.Measure.trim μ hm) s = μ s
    theorem MeasureTheory.le_trim {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m m0) :
    μ s (MeasureTheory.Measure.trim μ hm) s
    theorem MeasureTheory.measure_eq_zero_of_trim_eq_zero {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m m0) (h : (MeasureTheory.Measure.trim μ hm) s = 0) :
    μ s = 0
    theorem MeasureTheory.ae_of_ae_trim {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} (hm : m m0) {μ : MeasureTheory.Measure α} {P : αProp} (h : ∀ᵐ (x : α) ∂MeasureTheory.Measure.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₁ =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.trim μ hm)] 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₁ ≤ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.trim μ hm)] f₂) :
    theorem MeasureTheory.trim_trim {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace α} {hm₁₂ : m₁ m₂} {hm₂ : m₂ m0} :