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.eLpNorm'_trim
{α : Type u_1}
{E : Type u_2}
{m m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(hm : m ≤ m0)
{f : α → E}
(hf : MeasureTheory.StronglyMeasurable f)
:
MeasureTheory.eLpNorm' f q (μ.trim hm) = MeasureTheory.eLpNorm' f q μ
@[deprecated MeasureTheory.eLpNorm'_trim]
theorem
MeasureTheory.snorm'_trim
{α : Type u_1}
{E : Type u_2}
{m m0 : MeasurableSpace α}
{q : ℝ}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(hm : m ≤ m0)
{f : α → E}
(hf : MeasureTheory.StronglyMeasurable f)
:
MeasureTheory.eLpNorm' f q (μ.trim hm) = MeasureTheory.eLpNorm' f q μ
Alias of MeasureTheory.eLpNorm'_trim.
theorem
MeasureTheory.limsup_trim
{α : Type u_1}
{m 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 m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(hm : m ≤ m0)
{f : α → ENNReal}
(hf : Measurable f)
:
theorem
MeasureTheory.eLpNormEssSup_trim
{α : Type u_1}
{E : Type u_2}
{m m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(hm : m ≤ m0)
{f : α → E}
(hf : MeasureTheory.StronglyMeasurable f)
:
MeasureTheory.eLpNormEssSup f (μ.trim hm) = MeasureTheory.eLpNormEssSup f μ
@[deprecated MeasureTheory.eLpNormEssSup_trim]
theorem
MeasureTheory.snormEssSup_trim
{α : Type u_1}
{E : Type u_2}
{m m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(hm : m ≤ m0)
{f : α → E}
(hf : MeasureTheory.StronglyMeasurable f)
:
MeasureTheory.eLpNormEssSup f (μ.trim hm) = MeasureTheory.eLpNormEssSup f μ
Alias of MeasureTheory.eLpNormEssSup_trim.
theorem
MeasureTheory.eLpNorm_trim
{α : Type u_1}
{E : Type u_2}
{m m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(hm : m ≤ m0)
{f : α → E}
(hf : MeasureTheory.StronglyMeasurable f)
:
MeasureTheory.eLpNorm f p (μ.trim hm) = MeasureTheory.eLpNorm f p μ
@[deprecated MeasureTheory.eLpNorm_trim]
theorem
MeasureTheory.snorm_trim
{α : Type u_1}
{E : Type u_2}
{m m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(hm : m ≤ m0)
{f : α → E}
(hf : MeasureTheory.StronglyMeasurable f)
:
MeasureTheory.eLpNorm f p (μ.trim hm) = MeasureTheory.eLpNorm f p μ
Alias of MeasureTheory.eLpNorm_trim.
theorem
MeasureTheory.eLpNorm_trim_ae
{α : Type u_1}
{E : Type u_2}
{m m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(hm : m ≤ m0)
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f (μ.trim hm))
:
MeasureTheory.eLpNorm f p (μ.trim hm) = MeasureTheory.eLpNorm f p μ
@[deprecated MeasureTheory.eLpNorm_trim_ae]
theorem
MeasureTheory.snorm_trim_ae
{α : Type u_1}
{E : Type u_2}
{m m0 : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
(hm : m ≤ m0)
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f (μ.trim hm))
:
MeasureTheory.eLpNorm f p (μ.trim hm) = MeasureTheory.eLpNorm f p μ
Alias of MeasureTheory.eLpNorm_trim_ae.
theorem
MeasureTheory.memℒp_of_memℒp_trim
{α : Type u_1}
{E : Type u_2}
{m 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 μ