Pólya’s Proof of the Weighted Arithmetic–Geometric Mean Inequality

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

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

I follow Pólya's elegant proof, which uses the inequality $1+x\le 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.”