### 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.

### License

BSD License

### Topics

- Mathematics/Analysis

### Session Youngs_Inequality

- Youngs

## Cite

×

Youngs_Inequality-AFP

    @article{Youngs_Inequality-AFP,
      author  = {Lawrence C. Paulson},
      title   = {Young's Inequality for Increasing Functions},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Youngs_Inequality.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Feb 4, 2022 : Isabelle2021-1