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 _ _) :
_)