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

## Main definitions #

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
• μ.trim hm = μ.toMeasure
Instances For
@[simp]
theorem MeasureTheory.trim_eq_self {α : Type u_1} [] {μ : } :
μ.trim = μ
theorem MeasureTheory.toOuterMeasure_trim_eq_trim_toOuterMeasure {α : Type u_1} {m : } {m0 : } (μ : ) (hm : m m0) :
(μ.trim hm).toOuterMeasure = μ.trim
@[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 : ) :
(μ.trim hm) s = μ s
theorem MeasureTheory.le_trim {α : Type u_1} {m : } {m0 : } {μ : } {s : Set α} (hm : m m0) :
μ s (μ.trim hm) s
theorem MeasureTheory.trim_add {α : Type u_1} {m : } {m0 : } {μ : } {ν : } (hm : m m0) :
(μ + ν).trim hm = μ.trim hm + ν.trim hm
theorem MeasureTheory.measure_eq_zero_of_trim_eq_zero {α : Type u_1} {m : } {m0 : } {μ : } {s : Set α} (hm : m m0) (h : (μ.trim hm) s = 0) :
μ s = 0
theorem MeasureTheory.measure_trim_toMeasurable_eq_zero {α : Type u_1} {m : } {m0 : } {μ : } {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 : } {m0 : } (hm : m m0) {μ : } {P : αProp} (h : ∀ᵐ (x : α) ∂μ.trim hm, 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 : f₁ =ᵐ[μ.trim hm] f₂) :
f₁ =ᵐ[μ] f₂
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 : f₁ ≤ᵐ[μ.trim hm] f₂) :
f₁ ≤ᵐ[μ] f₂
theorem MeasureTheory.trim_trim {α : Type u_1} {m0 : } {μ : } {m₁ : } {m₂ : } {hm₁₂ : m₁ m₂} {hm₂ : m₂ m0} :
(μ.trim hm₂).trim hm₁₂ = μ.trim
theorem MeasureTheory.restrict_trim {α : Type u_1} {m : } {m0 : } {s : Set α} (hm : m m0) (μ : ) (hs : ) :
(μ.trim hm).restrict s = (μ.restrict s).trim hm
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 (μ.trim )] :
theorem MeasureTheory.sigmaFinite_trim_bot_iff {α : Type u_1} {m0 : } {μ : } :
theorem MeasureTheory.Measure.AbsolutelyContinuous.trim {α : Type u_1} {m : } {m0 : } {μ : } {ν : } (hμν : μ.AbsolutelyContinuous ν) (hm : m m0) :
(μ.trim hm).AbsolutelyContinuous (ν.trim hm)