Mean value inequalities

In this file we prove several inequalities, including AM-GM inequality, Young's inequality, Hölder inequality, and Minkowski inequality.

Main theorems

AM-GM inequality:

The inequality says that the geometric mean of a tuple of non-negative numbers is less than or equal to their arithmetic mean. We prove the weighted version of this inequality: if $w$ and $z$ are two non-negative vectors and $\sum_{i\in s} w_i=1$, then $$ \prod_{i\in s} z_i^{w_i} ≤ \sum_{i\in s} w_iz_i. $$ The classical version is a special case of this inequality for $w_i=\frac{1}{n}$.

We prove a few versions of this inequality. Each of the following lemmas comes in two versions: a version for real-valued non-negative functions is in the real namespace, and a version for nnreal-valued functions is in the nnreal namespace.

• geom_mean_le_arith_mean_weighted : weighted version for functions on finsets;
• geom_mean_le_arith_mean2_weighted : weighted version for two numbers;
• geom_mean_le_arith_mean3_weighted : weighted version for three numbers.

Generalized mean inequality

The inequality says that for two non-negative vectors $w$ and $z$ with $\sum_{i\in s} w_i=1$ and $p ≤ q$ we have $$ \sqrt[p]{\sum_{i\in s} w_i z_i^p} ≤ \sqrt[q]{\sum_{i\in s} w_i z_i^q}. $$

Currently we only prove this inequality for $p=1$. As in the rest of mathlib, we provide different theorems for natural exponents (pow_arith_mean_le_arith_mean_pow), integer exponents (fpow_arith_mean_le_arith_mean_fpow), and real exponents (rpow_arith_mean_le_arith_mean_rpow and arith_mean_le_rpow_mean). In the first two cases we prove $$ \left(\sum_{i\in s} w_i z_i\right)^n ≤ \sum_{i\in s} w_i z_i^n $$ in order to avoid using real exponents. For real exponents we prove both this and standard versions.

Young's inequality

Young's inequality says that for non-negative numbers a, b, p, q such that $\frac{1}{p}+\frac{1}{q}=1$ we have $$ ab ≤ \frac{a^p}{p} + \frac{b^q}{q}. $$

This inequality is a special case of the AM-GM inequality. It can be used to prove Hölder's inequality (see below) but we use a different proof.

Hölder's inequality

The inequality says that for two conjugate exponents p and q (i.e., for two positive numbers such that $\frac{1}{p}+\frac{1}{q}=1$) and any two non-negative vectors their inner product is less than or equal to the product of the $L_p$ norm of the first vector and the $L_q$ norm of the second vector: $$ \sum_{i\in s} a_ib_i ≤ \sqrt[p]{\sum_{i\in s} a_i^p}\sqrt[q]{\sum_{i\in s} b_i^q}. $$

We give versions of this result in real, nnreal and ennreal.

There are at least two short proofs of this inequality. In one proof we prenormalize both vectors, then apply Young's inequality to each $a_ib_i$. We use a different proof deducing this inequality from the generalized mean inequality for well-chosen vectors and weights.

Minkowski's inequality

The inequality says that for p ≥ 1 the function $$ \|a\|_p=\sqrt[p]{\sum_{i\in s} a_i^p} $$ satisfies the triangle inequality $\|a+b\|_p\le \|a\|_p+\|b\|_p$.

We give versions of this result in real, nnreal and ennreal.

We deduce this inequality from Hölder's inequality. Namely, Hölder inequality implies that $\|a\|_p$ is the maximum of the inner product $\sum_{i\in s}a_ib_i$ over b such that $\|b\|_q\le 1$. Now Minkowski's inequality follows from the fact that the maximum value of the sum of two functions is less than or equal to the sum of the maximum values of the summands.

TODO

• each inequality A ≤ B should come with a theorem A = B ↔ _; one of the ways to prove them is to define strict_convex_on functions.
• generalized mean inequality with any p ≤ q, including negative numbers;
• prove that the power mean tends to the geometric mean as the exponent tends to zero.
• prove integral versions of these inequalities.