eLpNorm_smul_le_mul_eLpNorm — Mathlib

English

If f ∈ MemLp q and φ ∈ MemLp p, then φ • f ∈ MemLp r provided HolderTriple holds with appropriate exponents.

Русский

Если f ∈ MemLp q, φ ∈ MemLp p, то φ • f ∈ MemLp r при условии HolderTriple.

LaTeX

$$$MemLp (φ \\cdot f) r μ ≤ c \\cdot MemLp f p μ · MemLp φ p μ$ under HolderTriple$$

Lean4

/-- Hölder's inequality, as an inequality on the `ℒp` seminorm of a scalar product `φ • f`. -/
theorem eLpNorm_smul_le_mul_eLpNorm {p q r : ℝ≥0∞} {f : α → E} (hf : AEStronglyMeasurable f μ) {φ : α → 𝕜}
    (hφ : AEStronglyMeasurable φ μ) [hpqr : HolderTriple p q r] : eLpNorm (φ • f) r μ ≤ eLpNorm φ p μ * eLpNorm f q μ :=
  by
  simpa using
    (eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm hφ hf (· • ·) 1 (.of_forall fun _ => by simpa using nnnorm_smul_le _ _) :
      _)

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