Lp seminorm with respect to trimmed measure #
In this file we prove basic properties of the Lp-seminorm of a function with respect to the restriction of a measure to a sub-σ-algebra.
theorem
MeasureTheory.snorm'_trim
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(hm : m ≤ m0)
{f : α → E}
(hf : MeasureTheory.StronglyMeasurable f)
:
MeasureTheory.snorm' f q (μ.trim hm) = MeasureTheory.snorm' f q μ
theorem
MeasureTheory.limsup_trim
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
{f : α → ENNReal}
(hf : Measurable f)
:
Filter.limsup f (MeasureTheory.ae (μ.trim hm)) = Filter.limsup f (MeasureTheory.ae μ)
theorem
MeasureTheory.essSup_trim
{α : Type u_1}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
{f : α → ENNReal}
(hf : Measurable f)
:
theorem
MeasureTheory.snormEssSup_trim
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(hm : m ≤ m0)
{f : α → E}
(hf : MeasureTheory.StronglyMeasurable f)
:
MeasureTheory.snormEssSup f (μ.trim hm) = MeasureTheory.snormEssSup f μ
theorem
MeasureTheory.snorm_trim
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(hm : m ≤ m0)
{f : α → E}
(hf : MeasureTheory.StronglyMeasurable f)
:
MeasureTheory.snorm f p (μ.trim hm) = MeasureTheory.snorm f p μ
theorem
MeasureTheory.snorm_trim_ae
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(hm : m ≤ m0)
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f (μ.trim hm))
:
MeasureTheory.snorm f p (μ.trim hm) = MeasureTheory.snorm f p μ
theorem
MeasureTheory.memℒp_of_memℒp_trim
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
{m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(hm : m ≤ m0)
{f : α → E}
(hf : MeasureTheory.Memℒp f p (μ.trim hm))
:
MeasureTheory.Memℒp f p μ