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 : Finset ι) (w : ι → ℝ) (z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : ∑ i ∈ s, w i = 1) (hz : ∀ i ∈ s, 0 ≤ z i) (n : ℕ) : (∑ i ∈ s, w i * z i) ^ n ≤ ∑ i ∈ s, w i * z i ^ n

theorem Real.pow_arith_mean_le_arith_mean_pow_of_even {ι : Type u} (s : Finset ι) (w : ι → ℝ) (z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : ∑ i ∈ s, w i = 1) {n : ℕ} (hn : Even n) : (∑ i ∈ s, w i * z i) ^ n ≤ ∑ i ∈ s, w i * z i ^ n

theorem Real.pow_sum_div_card_le_sum_pow {ι : Type u} (s : Finset ι) {f : ι → ℝ} (n : ℕ) (hf : ∀ a ∈ s, 0 ≤ f a) : (∑ x ∈ s, f x) ^ (n + 1) / ↑s.card ^ n ≤ ∑ x ∈ s, 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 : Finset ι) (w : ι → ℝ) (z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : ∑ i ∈ s, w i = 1) (hz : ∀ i ∈ s, 0 < z i) (m : ℤ) : (∑ i ∈ s, w i * z i) ^ m ≤ ∑ i ∈ s, w i * z i ^ m

theorem Real.rpow_arith_mean_le_arith_mean_rpow {ι : Type u} (s : Finset ι) (w : ι → ℝ) (z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : ∑ i ∈ s, w i = 1) (hz : ∀ i ∈ s, 0 ≤ z i) {p : ℝ} (hp : 1 ≤ p) : (∑ i ∈ s, w i * z i) ^ p ≤ ∑ i ∈ s, w i * z i ^ p

theorem Real.arith_mean_le_rpow_mean {ι : Type u} (s : Finset ι) (w : ι → ℝ) (z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : ∑ i ∈ s, w i = 1) (hz : ∀ i ∈ s, 0 ≤ z i) {p : ℝ} (hp : 1 ≤ p) : ∑ i ∈ s, w i * z i ≤ (∑ i ∈ s, w i * z i ^ p) ^ (1 / p)

theorem NNReal.pow_arith_mean_le_arith_mean_pow {ι : Type u} (s : Finset ι) (w : ι → NNReal) (z : ι → NNReal) (hw' : ∑ i ∈ s, w i = 1) (n : ℕ) : (∑ i ∈ s, w i * z i) ^ n ≤ ∑ i ∈ s, 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 : Finset ι) (f : ι → NNReal) (n : ℕ) : ↑(∑ x ∈ s, f x) ^ (n + 1) / ↑s.card ^ n ≤ ↑(∑ x ∈ s, f x ^ (n + 1))

theorem NNReal.rpow_arith_mean_le_arith_mean_rpow {ι : Type u} (s : Finset ι) (w : ι → NNReal) (z : ι → NNReal) (hw' : ∑ i ∈ s, w i = 1) {p : ℝ} (hp : 1 ≤ p) : (∑ i ∈ s, w i * z i) ^ p ≤ ∑ i ∈ s, 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 : Finset ι) (w : ι → NNReal) (z : ι → NNReal) (hw' : ∑ i ∈ s, w i = 1) {p : ℝ} (hp : 1 ≤ p) : ∑ i ∈ s, w i * z i ≤ (∑ i ∈ s, 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 : Finset ι) (w : ι → ENNReal) (z : ι → ENNReal) (hw' : ∑ i ∈ s, w i = 1) {p : ℝ} (hp : 1 ≤ p) : (∑ i ∈ s, w i * z i) ^ p ≤ ∑ i ∈ s, 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