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 α}
(μ : 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
- μ.trim hm = μ.toMeasure ⋯
Instances For
@[simp]
theorem
MeasureTheory.trim_eq_self
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
:
μ.trim ⋯ = μ
theorem
MeasureTheory.toOuterMeasure_trim_eq_trim_toOuterMeasure
{α : Type u_1}
{m m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(hm : m ≤ m0)
:
(μ.trim hm).toOuterMeasure = μ.trim
@[simp]
theorem
MeasureTheory.zero_trim
{α : Type u_1}
{m m0 : MeasurableSpace α}
(hm : m ≤ m0)
:
MeasureTheory.Measure.trim 0 hm = 0
theorem
MeasureTheory.trim_measurableSet_eq
{α : Type u_1}
{m m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(hm : m ≤ m0)
(hs : MeasurableSet s)
:
(μ.trim hm) s = μ s
theorem
MeasureTheory.le_trim
{α : Type u_1}
{m m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(hm : m ≤ m0)
:
μ s ≤ (μ.trim hm) s
theorem
MeasureTheory.trim_add
{α : Type u_1}
{m m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
(hm : m ≤ m0)
:
theorem
MeasureTheory.measure_eq_zero_of_trim_eq_zero
{α : Type u_1}
{m m0 : MeasurableSpace α}
{μ : MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
{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 : MeasurableSpace α}
(hm : m ≤ m0)
{μ : MeasureTheory.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 α}
{μ : MeasureTheory.Measure α}
{E : Type u_2}
{hm : m ≤ m0}
{f₁ f₂ : α → E}
(h12 : f₁ =ᵐ[μ.trim hm] f₂)
:
theorem
MeasureTheory.ae_le_of_ae_le_trim
{α : Type u_1}
{m m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_2}
[LE E]
{hm : m ≤ m0}
{f₁ f₂ : α → E}
(h12 : f₁ ≤ᵐ[μ.trim hm] f₂)
:
theorem
MeasureTheory.trim_trim
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.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)
(μ : MeasureTheory.Measure α)
(hs : MeasurableSet s)
:
(μ.trim hm).restrict s = (μ.restrict s).trim hm
instance
MeasureTheory.isFiniteMeasure_trim
{α : Type u_1}
{m m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
:
MeasureTheory.IsFiniteMeasure (μ.trim hm)
theorem
MeasureTheory.sigmaFiniteTrim_mono
{α : Type u_1}
{m m₂ m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
(hm₂ : m₂ ≤ m)
[MeasureTheory.SigmaFinite (μ.trim ⋯)]
:
MeasureTheory.SigmaFinite (μ.trim hm)
theorem
MeasureTheory.sigmaFinite_trim_bot_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
:
MeasureTheory.SigmaFinite (μ.trim ⋯) ↔ MeasureTheory.IsFiniteMeasure μ
theorem
MeasureTheory.Measure.AbsolutelyContinuous.trim
{α : Type u_1}
{m m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
(hμν : μ.AbsolutelyContinuous ν)
(hm : m ≤ m0)
:
(μ.trim hm).AbsolutelyContinuous (ν.trim hm)