# Documentation

Mathlib.MeasureTheory.Measure.Trim

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

## Main definitions #

• MeasureTheory.Measure.trim: restriction of a measure to a sub-sigma algebra.
noncomputable def MeasureTheory.Measure.trim {α : Type u_1} {m : } {m0 : } (μ : ) (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.trim_eq_self {α : Type u_1} [] {μ : } :
MeasureTheory.Measure.trim μ (_ : inst✝ inst✝) = μ
theorem MeasureTheory.toOuterMeasure_trim_eq_trim_toOuterMeasure {α : Type u_1} {m : } {m0 : } (μ : ) (hm : m m0) :
@[simp]
theorem MeasureTheory.zero_trim {α : Type u_1} {m : } {m0 : } (hm : m m0) :
theorem MeasureTheory.trim_measurableSet_eq {α : Type u_1} {m : } {m0 : } {μ : } {s : Set α} (hm : m m0) (hs : ) :
() s = μ s
theorem MeasureTheory.le_trim {α : Type u_1} {m : } {m0 : } {μ : } {s : Set α} (hm : m m0) :
μ s () s
theorem MeasureTheory.measure_eq_zero_of_trim_eq_zero {α : Type u_1} {m : } {m0 : } {μ : } {s : Set α} (hm : m m0) (h : () s = 0) :
μ s = 0
theorem MeasureTheory.measure_trim_toMeasurable_eq_zero {α : Type u_1} {m : } {m0 : } {μ : } {s : Set α} {hm : m m0} (hs : () s = 0) :
μ = 0
theorem MeasureTheory.ae_of_ae_trim {α : Type u_1} {m : } {m0 : } (hm : m m0) {μ : } {P : αProp} (h : ∀ᵐ (x : α) ∂, P x) :
∀ᵐ (x : α) ∂μ, P x
theorem MeasureTheory.ae_eq_of_ae_eq_trim {α : Type u_1} {m : } {m0 : } {μ : } {E : Type u_2} {hm : m m0} {f₁ : αE} {f₂ : αE} (h12 : ) :
theorem MeasureTheory.ae_le_of_ae_le_trim {α : Type u_1} {m : } {m0 : } {μ : } {E : Type u_2} [LE E] {hm : m m0} {f₁ : αE} {f₂ : αE} (h12 : ) :
theorem MeasureTheory.trim_trim {α : Type u_1} {m0 : } {μ : } {m₁ : } {m₂ : } {hm₁₂ : m₁ m₂} {hm₂ : m₂ m0} :
= MeasureTheory.Measure.trim μ (_ : m₁ m0)
theorem MeasureTheory.restrict_trim {α : Type u_1} {m : } {m0 : } {s : Set α} (hm : m m0) (μ : ) (hs : ) :
instance MeasureTheory.isFiniteMeasure_trim {α : Type u_1} {m : } {m0 : } {μ : } (hm : m m0) :
Equations
theorem MeasureTheory.sigmaFiniteTrim_mono {α : Type u_1} {m : } {m₂ : } {m0 : } {μ : } (hm : m m0) (hm₂ : m₂ m) [MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ (_ : m₂ m0))] :
theorem MeasureTheory.sigmaFinite_trim_bot_iff {α : Type u_1} {m0 : } {μ : } :