# mathlibdocumentation

analysis.mean_inequalities_pow

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

## 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 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.
theorem real.pow_arith_mean_le_arith_mean_pow {ι : Type u} (s : finset ι) (w z : ι → ) (hw : ∀ (i : ι), i s0 w i) (hw' : s.sum (λ (i : ι), w i) = 1) (hz : ∀ (i : ι), i s0 z i) (n : ) :
s.sum (λ (i : ι), w i * z i) ^ n s.sum (λ (i : ι), w i * z i ^ n)
theorem real.pow_arith_mean_le_arith_mean_pow_of_even {ι : Type u} (s : finset ι) (w z : ι → ) (hw : ∀ (i : ι), i s0 w i) (hw' : s.sum (λ (i : ι), w i) = 1) {n : } (hn : even n) :
s.sum (λ (i : ι), w i * z i) ^ n s.sum (λ (i : ι), w i * z i ^ n)
theorem real.zpow_arith_mean_le_arith_mean_zpow {ι : Type u} (s : finset ι) (w z : ι → ) (hw : ∀ (i : ι), i s0 w i) (hw' : s.sum (λ (i : ι), w i) = 1) (hz : ∀ (i : ι), i s0 < z i) (m : ) :
s.sum (λ (i : ι), w i * z i) ^ m s.sum (λ (i : ι), w i * z i ^ m)
theorem real.rpow_arith_mean_le_arith_mean_rpow {ι : Type u} (s : finset ι) (w z : ι → ) (hw : ∀ (i : ι), i s0 w i) (hw' : s.sum (λ (i : ι), w i) = 1) (hz : ∀ (i : ι), i s0 z i) {p : } (hp : 1 p) :
s.sum (λ (i : ι), w i * z i) ^ p s.sum (λ (i : ι), w i * z i ^ p)
theorem real.arith_mean_le_rpow_mean {ι : Type u} (s : finset ι) (w z : ι → ) (hw : ∀ (i : ι), i s0 w i) (hw' : s.sum (λ (i : ι), w i) = 1) (hz : ∀ (i : ι), i s0 z i) {p : } (hp : 1 p) :
s.sum (λ (i : ι), w i * z i) s.sum (λ (i : ι), w i * z i ^ p) ^ (1 / p)
theorem nnreal.pow_arith_mean_le_arith_mean_pow {ι : Type u} (s : finset ι) (w z : ι → nnreal) (hw' : s.sum (λ (i : ι), w i) = 1) (n : ) :
s.sum (λ (i : ι), w i * z i) ^ n s.sum (λ (i : ι), w i * z i ^ n)

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

theorem nnreal.rpow_arith_mean_le_arith_mean_rpow {ι : Type u} (s : finset ι) (w z : ι → nnreal) (hw' : s.sum (λ (i : ι), w i) = 1) {p : } (hp : 1 p) :
s.sum (λ (i : ι), w i * z i) ^ p s.sum (λ (i : ι), 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₁ w₂ z₁ 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.arith_mean_le_rpow_mean {ι : Type u} (s : finset ι) (w z : ι → nnreal) (hw' : s.sum (λ (i : ι), w i) = 1) {p : } (hp : 1 p) :
s.sum (λ (i : ι), w i * z i) s.sum (λ (i : ι), 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 b : nnreal) (hp1 : 1 p) :
a ^ p + b ^ p (a + b) ^ p
theorem nnreal.rpow_add_rpow_le_add {p : } (a b : nnreal) (hp1 : 1 p) :
(a ^ p + b ^ p) ^ (1 / p) a + b
theorem nnreal.rpow_add_rpow_le {p q : } (a 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 b : nnreal) (hp_pos : 0 < p) (hp1 : p 1) :
(a + b) ^ p a ^ p + b ^ p
theorem ennreal.rpow_arith_mean_le_arith_mean_rpow {ι : Type u} (s : finset ι) (w z : ι → ennreal) (hw' : s.sum (λ (i : ι), w i) = 1) {p : } (hp : 1 p) :
s.sum (λ (i : ι), w i * z i) ^ p s.sum (λ (i : ι), 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₁ w₂ z₁ 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.add_rpow_le_rpow_add {p : } (a b : ennreal) (hp1 : 1 p) :
a ^ p + b ^ p (a + b) ^ p
theorem ennreal.rpow_add_rpow_le_add {p : } (a b : ennreal) (hp1 : 1 p) :
(a ^ p + b ^ p) ^ (1 / p) a + b
theorem ennreal.rpow_add_rpow_le {p q : } (a 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 b : ennreal) (hp_pos : 0 < p) (hp1 : p 1) :
(a + b) ^ p a ^ p + b ^ p