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 : MeasurableSpace α} (μ : 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 α] {μ : Measure α} :

μ.trim ⋯ = μ

theorem MeasureTheory.toOuterMeasure_trim_eq_trim_toOuterMeasure {α : Type u_1} {m m0 : MeasurableSpace α} (μ : Measure α) (hm : m ≤ m0) :

(μ.trim hm).toOuterMeasure = μ.trim

@[simp]

theorem MeasureTheory.zero_trim {α : Type u_1} {m m0 : MeasurableSpace α} (hm : m ≤ m0) :

Measure.trim 0 hm = 0

theorem MeasureTheory.trim_measurableSet_eq {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hm : m ≤ m0) (hs : MeasurableSet s) :

(μ.trim hm) s = μ s

theorem MeasureTheory.le_trim {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hm : m ≤ m0) :

μ s ≤ (μ.trim hm) s

theorem MeasureTheory.trim_eq_map {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) :

μ.trim hm = Measure.map id μ

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 μ

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

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)

theorem MeasureTheory.trim_add {α : Type u_1} {m m0 : MeasurableSpace α} {μ ν : Measure α} (hm : m ≤ m0) :

(μ + ν).trim hm = μ.trim hm + ν.trim hm

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

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

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

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₁ =ᵐ[μ.trim hm] f₂) :

f₁ =ᵐ[μ] f₂

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₁ ≤ᵐ[μ.trim hm] f₂) :

f₁ ≤ᵐ[μ] f₂

theorem MeasureTheory.trim_trim {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {m₁ m₂ : MeasurableSpace α} {hm₁₂ : m₁ ≤ m₂} {hm₂ : m₂ ≤ m0} :

(μ.trim hm₂).trim hm₁₂ = μ.trim ⋯

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

theorem MeasureTheory.measure_spanningSets_trim_lt_top {α : Type u_1} {m m0 : MeasurableSpace α} (hm : m ≤ m0) (μ : Measure α) [SigmaFinite (μ.trim hm)] (n : ℕ) :

μ (spanningSets (μ.trim hm) n) < ⊤

instance MeasureTheory.instIsFiniteMeasureRestrictSpanningSetsTrim {α : Type u_1} {m m0 : MeasurableSpace α} (hm : m ≤ m0) (μ : Measure α) [SigmaFinite (μ.trim hm)] (n : ℕ) :

IsFiniteMeasure (μ.restrict (spanningSets (μ.trim hm) n))

instance MeasureTheory.isFiniteMeasure_trim {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) [IsFiniteMeasure μ] :

IsFiniteMeasure (μ.trim hm)

theorem MeasureTheory.sigmaFiniteTrim_mono {α : Type u_1} {m m₂ m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) (hm₂ : m₂ ≤ m) [SigmaFinite (μ.trim ⋯)] :

SigmaFinite (μ.trim hm)

theorem MeasureTheory.SigmaFinite.of_trim {α : Type u_1} {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] :

theorem MeasureTheory.sigmaFinite_trim_bot_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} :

SigmaFinite (μ.trim ⋯) ↔ IsFiniteMeasure μ

theorem MeasureTheory.Measure.AbsolutelyContinuous.trim {α : Type u_1} {m m0 : MeasurableSpace α} {μ ν : Measure α} (hμν : μ.AbsolutelyContinuous ν) (hm : m ≤ m0) :

(μ.trim hm).AbsolutelyContinuous (ν.trim hm)

theorem ae_eq_trim_of_measurable {α : Type u_3} {β : Type u_4} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSpace β] [MeasurableEq β] (hm : m ≤ m0) {f g : α → β} (hf : Measurable f) (hg : Measurable g) (hfg : f =ᵐ[μ] g) :

f =ᵐ[μ.trim hm] g