Documentation

Mathlib.MeasureTheory.Function.LpSeminorm.Trim

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 : MeasurableSpace α} {m0 : MeasurableSpace α} {q : } {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] (hm : m m0) {f : αE} (hf : MeasureTheory.StronglyMeasurable f) :
@[deprecated MeasureTheory.eLpNorm'_trim]
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) :

Alias of MeasureTheory.eLpNorm'_trim.

theorem MeasureTheory.limsup_trim {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m m0) {f : αENNReal} (hf : Measurable f) :
theorem MeasureTheory.essSup_trim {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m m0) {f : αENNReal} (hf : Measurable f) :
essSup f (μ.trim hm) = essSup f μ
@[deprecated MeasureTheory.eLpNormEssSup_trim]

Alias of MeasureTheory.eLpNormEssSup_trim.

theorem MeasureTheory.eLpNorm_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) :
@[deprecated MeasureTheory.eLpNorm_trim]
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) :

Alias of MeasureTheory.eLpNorm_trim.

theorem MeasureTheory.eLpNorm_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)) :
@[deprecated MeasureTheory.eLpNorm_trim_ae]
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)) :

Alias of MeasureTheory.eLpNorm_trim_ae.

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)) :