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 #

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