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
Instances For
@[simp]
theorem
MeasureTheory.trim_eq_self
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
:
MeasureTheory.Measure.trim μ ⋯ = μ
theorem
MeasureTheory.toOuterMeasure_trim_eq_trim_toOuterMeasure
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(hm : m ≤ m0)
:
@[simp]
theorem
MeasureTheory.zero_trim
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
(hm : m ≤ m0)
:
MeasureTheory.Measure.trim 0 hm = 0
theorem
MeasureTheory.trim_measurableSet_eq
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(hm : m ≤ m0)
(hs : MeasurableSet s)
:
↑↑(MeasureTheory.Measure.trim μ hm) s = ↑↑μ s
theorem
MeasureTheory.le_trim
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(hm : m ≤ m0)
:
↑↑μ s ≤ ↑↑(MeasureTheory.Measure.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 : ↑↑(MeasureTheory.Measure.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 : ↑↑(MeasureTheory.Measure.trim μ hm) s = 0)
:
↑↑μ (MeasureTheory.toMeasurable (MeasureTheory.Measure.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 : α) ∂MeasureTheory.Measure.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 (MeasureTheory.Measure.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 (MeasureTheory.Measure.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}
:
MeasureTheory.Measure.trim (MeasureTheory.Measure.trim μ hm₂) hm₁₂ = MeasureTheory.Measure.trim μ ⋯
theorem
MeasureTheory.restrict_trim
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{s : Set α}
(hm : m ≤ m0)
(μ : MeasureTheory.Measure α)
(hs : MeasurableSet s)
:
instance
MeasureTheory.isFiniteMeasure_trim
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
:
Equations
- ⋯ = ⋯
theorem
MeasureTheory.sigmaFiniteTrim_mono
{α : Type u_1}
{m : MeasurableSpace α}
{m₂ : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
(hm₂ : m₂ ≤ m)
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ ⋯)]
:
theorem
MeasureTheory.sigmaFinite_trim_bot_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
: