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