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} {ε : Type u_2} {m m0 : MeasurableSpace α} {q : ℝ} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] (hm : m ≤ m0) {f : α → ε} (hf : StronglyMeasurable f) : eLpNorm' f q (μ.trim hm) = eLpNorm' f q μ

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) : essSup f (μ.trim hm) = essSup f μ

theorem MeasureTheory.eLpNormEssSup_trim {α : Type u_1} {ε : Type u_2} {m m0 : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] (hm : m ≤ m0) {f : α → ε} (hf : StronglyMeasurable f) : eLpNormEssSup f (μ.trim hm) = eLpNormEssSup f μ

theorem MeasureTheory.eLpNorm_trim {α : Type u_1} {ε : Type u_2} {m m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] (hm : m ≤ m0) {f : α → ε} (hf : StronglyMeasurable f) : eLpNorm f p (μ.trim hm) = eLpNorm f p μ

theorem MeasureTheory.eLpNorm_trim_ae {α : Type u_1} {ε : Type u_2} {m m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] (hm : m ≤ m0) {f : α → ε} (hf : AEStronglyMeasurable f (μ.trim hm)) : eLpNorm f p (μ.trim hm) = eLpNorm f p μ

theorem MeasureTheory.memLp_of_memLp_trim {α : Type u_1} {ε : Type u_2} {m m0 : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] (hm : m ≤ m0) {f : α → ε} (hf : MemLp f p (μ.trim hm)) : MemLp f p μ