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

## Main definitions #

- `MeasureTheory.Measure.trim`: restriction of a measure to a sub-sigma algebra.

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

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

source
@[simp]
theorem MeasureTheory.trim_eq_self {α : Type u_1} [MeasurableSpace α] {μ : Measure α} :
μ.trim ⋯ = μ
source
theorem MeasureTheory.toOuterMeasure_trim_eq_trim_toOuterMeasure {α : Type u_1} {m m0 : MeasurableSpace α} (μ : Measure α) (hm : m ≤ m0) :
(μ.trim hm).toOuterMeasure = μ.trim
source
@[simp]
theorem MeasureTheory.zero_trim {α : Type u_1} {m m0 : MeasurableSpace α} (hm : m ≤ m0) :
Measure.trim 0 hm = 0
source
theorem MeasureTheory.trim_measurableSet_eq {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hm : m ≤ m0) (hs : MeasurableSet s) :
(μ.trim hm) s = μ s
source
theorem MeasureTheory.le_trim {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hm : m ≤ m0) :
μ s ≤ (μ.trim hm) s
source
theorem MeasureTheory.trim_eq_map {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) :
μ.trim hm = Measure.map id μ
source
theorem MeasureTheory.map_trim_comap {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {f : α → β} (hf : Measurable f) :
Measure.map f (μ.trim ⋯) = Measure.map f μ
source
theorem MeasureTheory.trim_comap_apply {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {f : α → β} (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) :
(μ.trim ⋯) (f ⁻¹' s) = (Measure.map f μ) s
source
theorem MeasureTheory.ae_map_iff_ae_trim {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {f : α → β} (hf : Measurable f) {p : β → Prop} (hp : MeasurableSet {x : β | p x}) :
(∀ᵐ (y : β) ∂Measure.map f μ, p y) ↔ ∀ᵐ (x : α) ∂μ.trim ⋯, p (f x)
source
theorem MeasureTheory.trim_add {α : Type u_1} {m m0 : MeasurableSpace α} {μ ν : Measure α} (hm : m ≤ m0) :
(μ + ν).trim hm = μ.trim hm + ν.trim hm
source
theorem MeasureTheory.measure_eq_zero_of_trim_eq_zero {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hm : m ≤ m0) (h : (μ.trim hm) s = 0) :
μ s = 0
source
theorem MeasureTheory.measure_trim_toMeasurable_eq_zero {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {hm : m ≤ m0} (hs : (μ.trim hm) s = 0) :
μ (toMeasurable (μ.trim hm) s) = 0
source
theorem MeasureTheory.ae_of_ae_trim {α : Type u_1} {m m0 : MeasurableSpace α} (hm : m ≤ m0) {μ : Measure α} {P : α → Prop} (h : ∀ᵐ (x : α) ∂μ.trim hm, P x) :
∀ᵐ (x : α) ∂μ, P x
source
theorem MeasureTheory.ae_eq_of_ae_eq_trim {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {E : Type u_3} {hm : m ≤ m0} {f₁ f₂ : α → E} (h12 : f₁ =ᶠ[ae (μ.trim hm)] f₂) :
f₁ =ᶠ[ae μ] f₂
source
theorem MeasureTheory.ae_le_of_ae_le_trim {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {E : Type u_3} [LE E] {hm : m ≤ m0} {f₁ f₂ : α → E} (h12 : f₁ ≤ᶠ[ae (μ.trim hm)] f₂) :
f₁ ≤ᶠ[ae μ] f₂
source
theorem MeasureTheory.trim_trim {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {m₁ m₂ : MeasurableSpace α} {hm₁₂ : m₁ ≤ m₂} {hm₂ : m₂ ≤ m0} :
(μ.trim hm₂).trim hm₁₂ = μ.trim ⋯
source
theorem MeasureTheory.restrict_trim {α : Type u_1} {m m0 : MeasurableSpace α} {s : Set α} (hm : m ≤ m0) (μ : Measure α) (hs : MeasurableSet s) :
(μ.trim hm).restrict s = (μ.restrict s).trim hm
source
instance MeasureTheory.isFiniteMeasure_trim {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) [IsFiniteMeasure μ] :
IsFiniteMeasure (μ.trim hm)
source
theorem MeasureTheory.sigmaFiniteTrim_mono {α : Type u_1} {m m₂ m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) (hm₂ : m₂ ≤ m) [SigmaFinite (μ.trim ⋯)] :
SigmaFinite (μ.trim hm)
source
theorem MeasureTheory.sigmaFinite_trim_bot_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} :
SigmaFinite (μ.trim ⋯) ↔ IsFiniteMeasure μ
source
theorem MeasureTheory.Measure.AbsolutelyContinuous.trim {α : Type u_1} {m m0 : MeasurableSpace α} {μ ν : Measure α} (hμν : μ.AbsolutelyContinuous ν) (hm : m ≤ m0) :
(μ.trim hm).AbsolutelyContinuous (ν.trim hm)