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 : MeasurableSpace α}
{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 = MeasureTheory.OuterMeasure.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 : MeasurableSpace α}
{m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(hm : m ≤ m0)
:
↑(μ.trim hm) = MeasureTheory.OuterMeasure.trim ↑μ
@[simp]
theorem
MeasureTheory.zero_trim
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
(hm : m ≤ m0)
:
0.trim hm = 0
theorem
MeasureTheory.trim_measurableSet_eq
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(hm : m ≤ m0)
(hs : MeasurableSet s)
:
↑↑(μ.trim hm) s = ↑↑μ s
theorem
MeasureTheory.le_trim
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(hm : m ≤ m0)
:
↑↑μ s ≤ ↑↑(μ.trim hm) s
theorem
MeasureTheory.measure_eq_zero_of_trim_eq_zero
{α : Type u_1}
{m : MeasurableSpace α}
{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 : MeasurableSpace α}
{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 : MeasurableSpace α}
{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 : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_2}
{hm : m ≤ m0}
{f₁ : α → E}
{f₂ : α → E}
(h12 : f₁ =ᶠ[MeasureTheory.Measure.ae (μ.trim hm)] f₂)
:
f₁ =ᶠ[MeasureTheory.Measure.ae μ] f₂
theorem
MeasureTheory.ae_le_of_ae_le_trim
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_2}
[LE E]
{hm : m ≤ m0}
{f₁ : α → E}
{f₂ : α → E}
(h12 : f₁ ≤ᶠ[MeasureTheory.Measure.ae (μ.trim hm)] f₂)
:
f₁ ≤ᶠ[MeasureTheory.Measure.ae μ] f₂
theorem
MeasureTheory.trim_trim
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{m₁ : MeasurableSpace α}
{m₂ : MeasurableSpace α}
{hm₁₂ : m₁ ≤ m₂}
{hm₂ : m₂ ≤ m0}
:
(μ.trim hm₂).trim hm₁₂ = μ.trim ⋯
theorem
MeasureTheory.restrict_trim
{α : Type u_1}
{m : MeasurableSpace α}
{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 : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
:
MeasureTheory.IsFiniteMeasure (μ.trim hm)
Equations
- ⋯ = ⋯
theorem
MeasureTheory.sigmaFiniteTrim_mono
{α : Type u_1}
{m : MeasurableSpace α}
{m₂ : MeasurableSpace α}
{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 : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(hμν : MeasureTheory.Measure.AbsolutelyContinuous μ ν)
(hm : m ≤ m0)
:
MeasureTheory.Measure.AbsolutelyContinuous (μ.trim hm) (ν.trim hm)