Hölder's inequality for sums

Statement

Let $p, q > 1$ be real numbers with $\frac{1}{p} + \frac{1}{q} = 1$, and let $a_1, \dots, a_n, b_1, \dots, b_n$ be real numbers. Then $$\sum_{i=1}^{n} |a_i b_i| \le \Big( \sum_{i=1}^{n} |a_i|^p \Big)^{1/p} \Big( \sum_{i=1}^{n} |b_i|^q \Big)^{1/q}.$$

Remarks

Scale so that both factors on the right are $1$. Then apply Young's inequality to each product $|a_i| |b_i|$ and add. For $p = q = 2$ it is the Cauchy–Schwarz inequality. Mathlib states a form as Real.inner_le_Lp_mul_Lq.

Explanations

L1 human

Hölder's inequality bounds a sum of products by the sizes of the two sequences. Each size is measured with its own exponent, $p$ for one and $q$ for the other.