Fenchel–Young inequality

Fenchel's inequality (also called the Fenchel–Young inequality).

For $f : \mathbb{R}^n \to \mathbb{R}$ let $f^{*}(y) = \sup_x(\langle x,y\rangle - f(x))$ be its Fenchel conjugate, with values in $(-\infty,+\infty]$. Then for all $x, y \in \mathbb{R}^n$,

The inequality holds for every function $f$ — no convexity, continuity or measurability is needed — since it is nothing but the definition of the supremum applied at the point $x$. Equality holds exactly when $y$ is a subgradient of $f$ at $x$, which is how the inequality is used to characterize the solutions of dual pairs of problems.

Specialized to $f(x) = |x|^{p}/p$ on $\mathbb{R}$, whose conjugate is $|y|^{q}/q$ with $1/p + 1/q = 1$, it becomes Young's inequality $xy \le x^{p}/p + y^{q}/q$, and hence — after integration — Hölder's inequality.

Formalization Note The inequality is stated in EReal, adding the real value $f(x)$ (coerced) to the EReal-valued conjugate, so the case $f^{*}(y) = +\infty$ needs no separate treatment. Source: B&V §3.3.1, p. 94.