# Mean value inequalities #

In this file we prove several mean inequalities for finite sums. Versions for integrals of some of these inequalities are available in MeasureTheory.MeanInequalities.

## Main theorems: 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 (zpow_arith_mean_le_arith_mean_zpow), 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.

## TODO #

• each inequality A ≤ B should come with a theorem A = B ↔ _; one of the ways to prove them is to define StrictConvexOn 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.
theorem Real.pow_arith_mean_le_arith_mean_pow {ι : Type u} (s : ) (w : ι) (z : ι) (hw : is, 0 w i) (hw' : is, w i = 1) (hz : is, 0 z i) (n : ) :
(is, w i * z i) ^ n is, w i * z i ^ n
theorem Real.pow_arith_mean_le_arith_mean_pow_of_even {ι : Type u} (s : ) (w : ι) (z : ι) (hw : is, 0 w i) (hw' : is, w i = 1) {n : } (hn : Even n) :
(is, w i * z i) ^ n is, w i * z i ^ n
theorem Real.pow_sum_div_card_le_sum_pow {ι : Type u} (s : ) {f : ι} (n : ) (hf : as, 0 f a) :
(xs, f x) ^ (n + 1) / s.card ^ n xs, f x ^ (n + 1)

Specific case of Jensen's inequality for sums of powers

theorem Real.zpow_arith_mean_le_arith_mean_zpow {ι : Type u} (s : ) (w : ι) (z : ι) (hw : is, 0 w i) (hw' : is, w i = 1) (hz : is, 0 < z i) (m : ) :
(is, w i * z i) ^ m is, w i * z i ^ m
theorem Real.rpow_arith_mean_le_arith_mean_rpow {ι : Type u} (s : ) (w : ι) (z : ι) (hw : is, 0 w i) (hw' : is, w i = 1) (hz : is, 0 z i) {p : } (hp : 1 p) :
(is, w i * z i) ^ p is, w i * z i ^ p
theorem Real.arith_mean_le_rpow_mean {ι : Type u} (s : ) (w : ι) (z : ι) (hw : is, 0 w i) (hw' : is, w i = 1) (hz : is, 0 z i) {p : } (hp : 1 p) :
is, w i * z i (is, w i * z i ^ p) ^ (1 / p)
theorem NNReal.pow_arith_mean_le_arith_mean_pow {ι : Type u} (s : ) (w : ιNNReal) (z : ιNNReal) (hw' : is, w i = 1) (n : ) :
(is, w i * z i) ^ n is, w i * z i ^ n

Weighted generalized mean inequality, version sums over finite sets, with ℝ≥0-valued functions and natural exponent.

theorem NNReal.pow_sum_div_card_le_sum_pow {ι : Type u} (s : ) (f : ιNNReal) (n : ) :
(xs, f x) ^ (n + 1) / s.card ^ n (xs, f x ^ (n + 1))
theorem NNReal.rpow_arith_mean_le_arith_mean_rpow {ι : Type u} (s : ) (w : ιNNReal) (z : ιNNReal) (hw' : is, w i = 1) {p : } (hp : 1 p) :
(is, w i * z i) ^ p is, w i * z i ^ p

Weighted generalized mean inequality, version for sums over finite sets, with ℝ≥0-valued functions and real exponents.

theorem NNReal.rpow_arith_mean_le_arith_mean2_rpow (w₁ : NNReal) (w₂ : NNReal) (z₁ : NNReal) (z₂ : NNReal) (hw' : w₁ + w₂ = 1) {p : } (hp : 1 p) :
(w₁ * z₁ + w₂ * z₂) ^ p w₁ * z₁ ^ p + w₂ * z₂ ^ p

Weighted generalized mean inequality, version for two elements of ℝ≥0 and real exponents.

theorem NNReal.rpow_add_le_mul_rpow_add_rpow (z₁ : NNReal) (z₂ : NNReal) {p : } (hp : 1 p) :
(z₁ + z₂) ^ p 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)

Unweighted mean inequality, version for two elements of ℝ≥0 and real exponents.

theorem NNReal.arith_mean_le_rpow_mean {ι : Type u} (s : ) (w : ιNNReal) (z : ιNNReal) (hw' : is, w i = 1) {p : } (hp : 1 p) :
is, w i * z i (is, w i * z i ^ p) ^ (1 / p)

Weighted generalized mean inequality, version for sums over finite sets, with ℝ≥0-valued functions and real exponents.

theorem NNReal.add_rpow_le_rpow_add {p : } (a : NNReal) (b : NNReal) (hp1 : 1 p) :
a ^ p + b ^ p (a + b) ^ p
theorem NNReal.rpow_add_rpow_le_add {p : } (a : NNReal) (b : NNReal) (hp1 : 1 p) :
(a ^ p + b ^ p) ^ (1 / p) a + b
theorem NNReal.rpow_add_rpow_le {p : } {q : } (a : NNReal) (b : NNReal) (hp_pos : 0 < p) (hpq : p q) :
(a ^ q + b ^ q) ^ (1 / q) (a ^ p + b ^ p) ^ (1 / p)
theorem NNReal.rpow_add_le_add_rpow {p : } (a : NNReal) (b : NNReal) (hp : 0 p) (hp1 : p 1) :
(a + b) ^ p a ^ p + b ^ p
theorem ENNReal.rpow_arith_mean_le_arith_mean_rpow {ι : Type u} (s : ) (w : ιENNReal) (z : ιENNReal) (hw' : is, w i = 1) {p : } (hp : 1 p) :
(is, w i * z i) ^ p is, w i * z i ^ p

Weighted generalized mean inequality, version for sums over finite sets, with ℝ≥0∞-valued functions and real exponents.

theorem ENNReal.rpow_arith_mean_le_arith_mean2_rpow (w₁ : ENNReal) (w₂ : ENNReal) (z₁ : ENNReal) (z₂ : ENNReal) (hw' : w₁ + w₂ = 1) {p : } (hp : 1 p) :
(w₁ * z₁ + w₂ * z₂) ^ p w₁ * z₁ ^ p + w₂ * z₂ ^ p

Weighted generalized mean inequality, version for two elements of ℝ≥0∞ and real exponents.

theorem ENNReal.rpow_add_le_mul_rpow_add_rpow (z₁ : ENNReal) (z₂ : ENNReal) {p : } (hp : 1 p) :
(z₁ + z₂) ^ p 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)

Unweighted mean inequality, version for two elements of ℝ≥0∞ and real exponents.

theorem ENNReal.add_rpow_le_rpow_add {p : } (a : ENNReal) (b : ENNReal) (hp1 : 1 p) :
a ^ p + b ^ p (a + b) ^ p
theorem ENNReal.rpow_add_rpow_le_add {p : } (a : ENNReal) (b : ENNReal) (hp1 : 1 p) :
(a ^ p + b ^ p) ^ (1 / p) a + b
theorem ENNReal.rpow_add_rpow_le {p : } {q : } (a : ENNReal) (b : ENNReal) (hp_pos : 0 < p) (hpq : p q) :
(a ^ q + b ^ q) ^ (1 / q) (a ^ p + b ^ p) ^ (1 / p)
theorem ENNReal.rpow_add_le_add_rpow {p : } (a : ENNReal) (b : ENNReal) (hp : 0 p) (hp1 : p 1) :
(a + b) ^ p a ^ p + b ^ p