eLpNorm'_smul_le_mul_eLpNorm' — Mathlib

English

If MemLp f q μ holds and p ≤ q, then MemLp f p μ holds; this persists under suitable finiteness conditions of μ.

Русский

Если MemLp f q μ верно и p ≤ q, то MemLp f p μ сохраняется; условие финитности μ учитывается.

LaTeX

$$$MemLp f q μ \\Rightarrow p ≤ q \\Rightarrow MemLp f p μ$$$

Lean4

theorem eLpNorm'_smul_le_mul_eLpNorm' {p q r : ℝ} {f : α → E} (hf : AEStronglyMeasurable f μ) {φ : α → 𝕜}
    (hφ : AEStronglyMeasurable φ μ) (hp0_lt : 0 < p) (hpq : p < q) (hpqr : 1 / p = 1 / q + 1 / r) :
    eLpNorm' (φ • f) p μ ≤ eLpNorm' φ q μ * eLpNorm' f r μ := by
  simpa using
    eLpNorm'_le_eLpNorm'_mul_eLpNorm' hφ hf (· • ·) 1 (.of_forall fun _ => by simpa using nnnorm_smul_le _ _) hp0_lt hpq
      hpqr

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