### Abstract

This article provides a formalisation of the Weighted Arithmetic–Geometric Mean Inequality: given non-negative reals $a_1, \ldots, a_n$ and non-negative weights $w_1, \ldots, w_n$ such that $w_1 + \ldots + w_n = 1$, we have \[\prod\limits_{i=1}^n a_i^{w_i} \leq \sum\limits_{i=1}^n w_i a_i\ .\] If the weights are additionally all non-zero, equality holds if and only if $a_1 = \ldots = a_n$.

As a corollary with $w_1 = \ldots = w_n = 1/n$, the regular arithmetic–geometric mean inequality follows, namely that \[\sqrt[n]{a_1\,\cdots\, a_n} \leq \tfrac{1}{n}(a_1 + \ldots + a_n)\ .\]

I follow Pólya's elegant proof, which uses the inequality $1 + x \leq e^x$ as a starting point. Pólya claims that this proof came to him in a dream, and that it was “the best mathematics he had ever dreamt.”

### License

BSD License

### Topics

- Mathematics/Analysis

### Session Weighted_Arithmetic_Geometric_Mean

- Weighted_Arithmetic_Geometric_Mean

### Used by

- Expander Graphs

## Cite

×

Weighted_Arithmetic_Geometric_Mean-AFP

    @article{Weighted_Arithmetic_Geometric_Mean-AFP,
      author  = {Manuel Eberl},
      title   = {Pólya’s Proof of the Weighted Arithmetic–Geometric Mean Inequality},
      journal = {Archive of Formal Proofs},
      month   = {July},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Weighted_Arithmetic_Geometric_Mean.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Jul 11, 2022 : Isabelle2021-1