smul — Mathlib

English

If MemLp f q μ and MemLp φ p μ, then MemLp (φ * f) r μ holds under HolderTriple.

Русский

Если MemLp f q μ и MemLp φ p μ, то MemLp (φ * f) r μ выполняется при HolderTriple.

LaTeX

$$MemLp f q μ → MemLp φ p μ → MemLp (φ * f) r μ$$

Lean4

theorem smul {p q r : ℝ≥0∞} {f : α → E} {φ : α → 𝕜} (hf : MemLp f q μ) (hφ : MemLp φ p μ) [hpqr : HolderTriple p q r] :
    MemLp (φ • f) r μ :=
  ⟨hφ.1.smul hf.1,
    eLpNorm_smul_le_mul_eLpNorm hf.1 hφ.1 |>.trans_lt <| ENNReal.mul_lt_top hφ.eLpNorm_lt_top hf.eLpNorm_lt_top⟩

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