MeasureTheory.memℒp_of_memℒp_trim

theorem MeasureTheory.memℒp_of_memℒp_trim : ∀ {α : Type u_1} {E : Type u_2} {m m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E] (hm : m ≤ m0) {f : α → E}, MeasureTheory.Memℒp f p (μ.trim hm) → MeasureTheory.Memℒp f p μ

The theorem `MeasureTheory.memℒp_of_memℒp_trim` states that for any types `α` and `E`, measurable spaces `m` and `m0` on `α`, an extended nonnegative real number `p`, and a measure `μ` on `α`, if there is an instance of `E` being a normed add commutative group, and if `m` is a subset of `m0`, then for any function `f` from `α` to `E`, if `f` meets the `L^p` space conditions (being almost everywhere strongly measurable and having its `p`-th power integral finite) with respect to the trimmed measure `μ.trim` (the restriction of `μ` to the smaller sigma-algebra `m`), then `f` also meets the `L^p` space conditions with respect to the original measure `μ`.

More concisely: If `α` is a type, `E` is a normed add commutative group, `m` and `m0` are measurable spaces on `α`, `p` is an extended nonnegative real number, `μ` is a measure on `α`, and `f` is a function from `α` to `E` that is almost everywhere strongly measurable and has finite `p`-th power integral with respect to the trimmed measure `μ.trim` on the subset `m` of `m0`, then `f` also satisfies the `L^p` space conditions with respect to the original measure `μ`.