Mean inequalities

This file collects classical inequalities complementing Mathlib.Analysis.MeanInequalities.

For nonnegative weights w i summing to 1, the weighted geometric mean G(a) = ∏ i, a i ^ w i of a nonnegative family is superadditive:

G(a) + G(b) ≤ G(a + b).

Since G is also positively homogeneous, this says that the weighted geometric mean is concave on the nonnegative orthant. Applied to the eigenvalues of a positive semidefinite matrix M with equal weights, it gives 1 + det M ^ (1 / n) ≤ det (1 + M) ^ (1 / n), the core of Minkowski's determinant inequality (Matrix.PosSemidef.det_rpow_add_det_rpow_le).

The proof divides by a i + b i and applies the inequality of arithmetic and geometric means Real.geom_mean_le_arith_mean_weighted to the two normalized families, whose weighted means add up to at most 1.

Minkowski's inequality also holds for unconditional sums of ℝ≥0∞-valued families over an arbitrary index type, with no summability hypotheses: infinite sums and infinite terms are allowed. Mathlib states it for finite sums (ENNReal.Lp_add_le) and for summable ℝ≥0-valued families (NNReal.Lp_add_le_tsum); the ℝ≥0∞ form follows from the finite one by taking the supremum over finite partial sums. It is the counting-measure case of ENNReal.lintegral_Lp_add_le, stated without measure theory. It gives the triangle inequality for gauges defined as ℓᵖ sums in ℝ≥0∞, such as the Hilbert–Schmidt energy of an operator. Hölder's inequality holds for such sums in the same way, extending ENNReal.inner_le_Lp_mul_Lq and NNReal.inner_le_Lp_mul_Lq_tsum. The ℓᵖ norm of such a family is antitone in the exponent, which gives the inclusions between Schatten classes of operators.

Mathlib states the two-point weighted AM-GM inequality in ℝ≥0∞ with ℝ≥0 weights (ENNReal.geom_mean_le_arith_mean2_weighted); it is restated here for the real weights 1 - θ and θ, as they appear in interpolation inequalities such as Prékopa–Leindler.

The two-point weighted AM-GM inequality is also restated after normalizing by positive scalars a and b: A ^ (1 - θ) * B ^ θ ≤ ((1 - θ) * (A / a) + θ * (B / b)) * (a ^ (1 - θ) * b ^ θ), strictly when 0 < θ < 1 and A / a ≠ B / b. This is the form used to compare volumes of hyperplane sections in the Kneser–Süss equality argument for Brunn–Minkowski.

The triangle inequality for the Euclidean norm on ℝ², applied to finitely many coordinate pairs (a i, b i), reads √((∑ a i) ^ 2 + (∑ b i) ^ 2) ≤ ∑ √(a i ^ 2 + b i ^ 2). It bounds a norm defined as the Euclidean combination of two component norms, each subadditive, such as the norm of a higher-order Sobolev space.

Main statements

• Real.prod_rpow_add_prod_rpow_le_prod_add_rpow: the weighted geometric mean is superadditive.
• Real.geom_mean_le_arith_mean2_weighted_div_mul, Real.geom_mean_lt_arith_mean2_weighted_div_mul: two-point weighted AM-GM after normalizing by positive scalars, with the strict form.
• Real.sqrt_sum_sq_add_sum_sq_le_sum_sqrt: the triangle inequality in the plane for finite sums of coordinate pairs.
• ENNReal.geom_mean_le_arith_mean2_weighted_ofReal: two-point weighted AM-GM in ℝ≥0∞ with the real weights 1 - θ and θ.
• ENNReal.Lp_add_le_tsum: Minkowski's inequality for unconditional sums in ℝ≥0∞.
• ENNReal.inner_le_Lp_mul_Lq_tsum: Hölder's inequality for unconditional sums in ℝ≥0∞.
• ENNReal.Lq_le_Lp_tsum: the ℓᵖ norm of an ℝ≥0∞-valued family is antitone in p.
• Real.Lq_le_Lp_of_nonneg: the same for finite sums of nonnegative reals.
• Real.Lp_le_mul_Lp_of_nonneg: termwise domination 0 ≤ f i ≤ c * g i bounds the finite ℓᵖ expression of f by c times that of g.
• Real.Lp_const_of_nonneg: the finite ℓᵖ expression of a constant t ≥ 0 over s is #s ^ (1 / p) * t.

References

• G. H. Hardy, J. E. Littlewood and G. Pólya, Inequalities, 2nd ed., Cambridge University Press 1952, Chapter II.

theorem Real.prod_rpow_add_prod_rpow_le_prod_add_rpow {ι : Type u_1} (s : Finset ι) {w a b : ι → ℝ} (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : ∑ i ∈ s, w i = 1) (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 ≤ b i) : ∏ i ∈ s, a i ^ w i + ∏ i ∈ s, b i ^ w i ≤ ∏ i ∈ s, (a i + b i) ^ w i

Superadditivity of the weighted geometric mean. For nonnegative weights w i summing to 1 and nonnegative families a and b, ∏ i ∈ s, a i ^ w i + ∏ i ∈ s, b i ^ w i ≤ ∏ i ∈ s, (a i + b i) ^ w i.

theorem Real.rpow_one_sub_mul_rpow_eq_div_mul {A B a b θ : ℝ} (ha : 0 < a) (hb : 0 < b) : A ^ (1 - θ) * B ^ θ = (A / a) ^ (1 - θ) * (B / b) ^ θ * (a ^ (1 - θ) * b ^ θ)

Splitting a weighted geometric mean through positive normalizers a and b: A ^ (1 - θ) * B ^ θ = (A / a) ^ (1 - θ) * (B / b) ^ θ * (a ^ (1 - θ) * b ^ θ).

theorem Real.geom_mean_le_arith_mean2_weighted_div_mul {A B a b θ : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (ha : 0 < a) (hb : 0 < b) (hθ₀ : 0 ≤ θ) (hθ₁ : θ ≤ 1) : A ^ (1 - θ) * B ^ θ ≤ ((1 - θ) * (A / a) + θ * (B / b)) * (a ^ (1 - θ) * b ^ θ)

Normalized weighted AM-GM. For positive normalizers a and b, the weighted geometric mean of A and B is at most the weighted arithmetic mean of A / a and B / b times the weighted geometric mean of a and b.

theorem Real.geom_mean_lt_arith_mean2_weighted_div_mul {A B a b θ : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (ha : 0 < a) (hb : 0 < b) (hθ₀ : 0 < θ) (hθ₁ : θ < 1) (hne : A / a ≠ B / b) : A ^ (1 - θ) * B ^ θ < ((1 - θ) * (A / a) + θ * (B / b)) * (a ^ (1 - θ) * b ^ θ)

The strict form of Real.geom_mean_le_arith_mean2_weighted_div_mul for 0 < θ < 1 and A / a ≠ B / b.

theorem Real.sqrt_sum_sq_add_sum_sq_le_sum_sqrt {ι : Type u_1} (s : Finset ι) (a b : ι → ℝ) : √((∑ i ∈ s, a i) ^ 2 + (∑ i ∈ s, b i) ^ 2) ≤ ∑ i ∈ s, √(a i ^ 2 + b i ^ 2)

Triangle inequality in the plane. For finite families a and b, √((∑ i ∈ s, a i) ^ 2 + (∑ i ∈ s, b i) ^ 2) ≤ ∑ i ∈ s, √(a i ^ 2 + b i ^ 2).

theorem ENNReal.geom_mean_le_arith_mean2_weighted_ofReal {θ : ℝ} (hθ₀ : 0 ≤ θ) (hθ₁ : θ ≤ 1) (a b : ENNReal) : a ^ (1 - θ) * b ^ θ ≤ ENNReal.ofReal (1 - θ) * a + ENNReal.ofReal θ * b

The weighted AM-GM inequality in ℝ≥0∞ for the real weights 1 - θ and θ: a ^ (1 - θ) * b ^ θ ≤ ofReal (1 - θ) * a + ofReal θ * b for 0 ≤ θ ≤ 1.

theorem ENNReal.Lp_add_le_tsum {ι : Type u_1} (f g : ι → ENNReal) {p : ℝ} (hp : 1 ≤ p) : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)

Minkowski's inequality for unconditional sums in ℝ≥0∞: for 1 ≤ p, (∑' i, (f i + g i) ^ p) ^ (1 / p) ≤ (∑' i, f i ^ p) ^ (1 / p) + (∑' i, g i ^ p) ^ (1 / p). No summability hypotheses are needed; both sides may be infinite.

theorem ENNReal.inner_le_Lp_mul_Lq_tsum {ι : Type u_1} (f g : ι → ENNReal) {p q : ℝ} (hpq : p.HolderConjugate q) : ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)

Hölder's inequality for unconditional sums in ℝ≥0∞: for conjugate exponents p and q, ∑' i, f i * g i ≤ (∑' i, f i ^ p) ^ (1 / p) * (∑' i, g i ^ q) ^ (1 / q). No summability hypotheses are needed; both sides may be infinite.

theorem ENNReal.Lq_le_Lp_tsum {ι : Type u_1} (f : ι → ENNReal) {p q : ℝ} (hp : 0 < p) (hpq : p ≤ q) : (∑' (i : ι), f i ^ q) ^ (1 / q) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p)

The ℓᵖ norms of an ℝ≥0∞-valued family decrease as the exponent grows: for 0 < p ≤ q, (∑' i, f i ^ q) ^ (1 / q) ≤ (∑' i, f i ^ p) ^ (1 / p). No summability hypotheses are needed; both sides may be infinite. This is the unconditional-sum form of ENNReal.rpow_add_rpow_le.

theorem Real.Lq_le_Lp_of_nonneg {ι : Type u_1} (s : Finset ι) {f : ι → ℝ} (hf : ∀ i ∈ s, 0 ≤ f i) {p q : ℝ} (hp : 0 < p) (hpq : p ≤ q) : (∑ i ∈ s, f i ^ q) ^ (1 / q) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p)

The ℓᵖ norms of a finite nonnegative real family decrease as the exponent grows: for 0 < p ≤ q, (∑ i ∈ s, f i ^ q) ^ (1 / q) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p).

theorem Real.Lp_le_mul_Lp_of_nonneg {ι : Type u_1} (s : Finset ι) {f g : ι → ℝ} {p c : ℝ} (hp : 0 < p) (hc : 0 ≤ c) (hf : ∀ i ∈ s, 0 ≤ f i) (hfg : ∀ i ∈ s, f i ≤ c * g i) : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≤ c * (∑ i ∈ s, g i ^ p) ^ (1 / p)

The ℓᵖ expression of a finite nonnegative family dominated termwise by c times another is at most c times the other's: if 0 ≤ f i ≤ c * g i, then (∑ i ∈ s, f i ^ p) ^ (1 / p) ≤ c * (∑ i ∈ s, g i ^ p) ^ (1 / p).

theorem Real.Lp_const_of_nonneg {ι : Type u_1} (s : Finset ι) {t p : ℝ} (ht : 0 ≤ t) (hp : p ≠ 0) : (∑ _i ∈ s, t ^ p) ^ (1 / p) = ↑s.card ^ (1 / p) * t

The finite ℓᵖ expression of a constant t ≥ 0 over s is #s ^ (1 / p) * t.