mathlib3 documentation

analysis.mean_inequalities_pow

Mean value inequalities #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 ∈ s → 0 ≤ w i) (hw' : s.sum (λ (i : ι), w i) = 1) (hz : ∀ (i : ι), i ∈ s → 0 ≤ 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 ∈ s → 0 ≤ 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.pow_sum_div_card_le_sum_pow {ι : Type u} (s : finset ι) {f : ι → ℝ} (n : ℕ) (hf : ∀ (a : ι), a ∈ s → 0 ≤ f a) :

s.sum (λ (x : ι), f x) ^ (n + 1) / ↑(s.card) ^ n ≤ s.sum (λ (x : ι), 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 : ι), i ∈ s → 0 ≤ w i) (hw' : s.sum (λ (i : ι), w i) = 1) (hz : ∀ (i : ι), i ∈ s → 0 < 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 ∈ s → 0 ≤ w i) (hw' : s.sum (λ (i : ι), w i) = 1) (hz : ∀ (i : ι), i ∈ s → 0 ≤ 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 ∈ s → 0 ≤ w i) (hw' : s.sum (λ (i : ι), w i) = 1) (hz : ∀ (i : ι), i ∈ s → 0 ≤ 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.pow_sum_div_card_le_sum_pow {ι : Type u} (s : finset ι) (f : ι → nnreal) (n : ℕ) :

s.sum (λ (x : ι), f x) ^ (n + 1) / ↑(s.card) ^ n ≤ s.sum (λ (x : ι), f x ^ (n + 1))

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.rpow_add_le_mul_rpow_add_rpow (z₁ 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 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 : 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.rpow_add_le_mul_rpow_add_rpow (z₁ 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 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 : 0 ≤ p) (hp1 : p ≤ 1) :

(a + b) ^ p ≤ a ^ p + b ^ p