### Abstract

Young's inequality states that $$ ab \leq \int_0^a f(x)dx +
\int_0^b f^{-1}(y) dy $$ where $a\geq 0$, $b\geq 0$ and $f$ is
strictly increasing and continuous. Its proof is formalised following
the
development by Cunningham and Grossman. Their idea is to
make the intuitive, geometric folklore proof rigorous by reasoning
about step functions. The lack of the Riemann integral makes the
development longer than one would like, but their argument is
reproduced faithfully.

BSD License