theorem MeasureTheory.eLpNorm_mul_le_mul_eLpNorm {𝕜 : Type u_1} {α : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedRing 𝕜] {p q r : ENNReal} {f g : α → 𝕜} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) [p.HolderTriple q r] : eLpNorm (f * g) r μ ≤ eLpNorm f p μ * eLpNorm g q μ

Hölder's inequality.