Young's Inequality for Increasing Functions

Lawrence C. Paulson 🌐

January 31, 2022

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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


Session Youngs_Inequality