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