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)
:
theorem
MeasureTheory.limsup_trim
{α : Type u_1}
{m m0 : MeasurableSpace α}
{μ : Measure α}
(hm : m ≤ m0)
{f : α → ENNReal}
(hf : Measurable f)
:
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)
:
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)
:
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))
:
theorem
MeasureTheory.memLp_of_memLp_trim
{α : Type u_1}
{E : Type u_2}
{m m0 : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
(hm : m ≤ m0)
{f : α → E}
(hf : MemLp f p (μ.trim hm))
:
MemLp f p μ
@[deprecated MeasureTheory.memLp_of_memLp_trim (since := "2025-02-21")]
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 : MemLp f p (μ.trim hm))
:
MemLp f p μ
Alias of MeasureTheory.memLp_of_memLp_trim.