theorem holder_inequality {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p q : ℝ} (hpq : p.HolderConjugate q) {f g : α → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal p) μ) (hg : MeasureTheory.MemLp g (ENNReal.ofReal q) μ) : ∫ (x : α), |f x * g x| ∂μ ≤ (∫ (x : α), |f x| ^ p ∂μ) ^ (1 / p) * (∫ (x : α), |g x| ^ q ∂μ) ^ (1 / q)

Hölder's inequality. For Hölder-conjugate exponents p, q ≥ 1 with 1/p + 1/q = 1, and f ∈ L^p(μ), g ∈ L^q(μ): ∫ |f · g| dμ ≤ (∫ |f|^p dμ)^{1/p} · (∫ |g|^q dμ)^{1/q}, i.e. ‖fg‖_1 ≤ ‖f‖_p · ‖g‖_q.