memLp_of_memLp_trim — Mathlib

English

If f is MemLp with respect to the trimmed measure, then f is MemLp with respect to μ.

Русский

Если f принадлежит MemLp по обрезанному комплекту, то f принадлежит MemLp по исходной мере μ.

LaTeX

$$MemLp f p (μ.trim hm) → MemLp f p μ$$

Lean4

theorem memLp_of_memLp_trim (hm : m ≤ m0) {f : α → ε} (hf : MemLp f p (μ.trim hm)) : MemLp f p μ :=
  ⟨aestronglyMeasurable_of_aestronglyMeasurable_trim hm hf.1, (le_of_eq (eLpNorm_trim_ae hm hf.1).symm).trans_lt hf.2⟩

Похожие утверждения