Mean value inequalities

In this file we prove several inequalities for finite sums, including AM-GM inequality, Young's inequality, Hölder inequality, and Minkowski inequality. Versions for integrals of some of these inequalities are available in MeasureTheory.MeanInequalities.

Main theorems

AM-GM inequality:

The inequality says that the geometric mean of a tuple of non-negative numbers is less than or equal to their arithmetic mean. We prove the weighted version of this inequality: if $w$ and $z$ are two non-negative vectors and $\sum_{i\in s} w_i=1$, then $$ \prod_{i\in s} z_i^{w_i} ≤ \sum_{i\in s} w_iz_i. $$ The classical version is a special case of this inequality for $w_i=\frac{1}{n}$.

We prove a few versions of this inequality. Each of the following lemmas comes in two versions: a version for real-valued non-negative functions is in the Real namespace, and a version for NNReal-valued functions is in the NNReal namespace.

• geom_mean_le_arith_mean_weighted : weighted version for functions on Finsets;
• geom_mean_le_arith_mean2_weighted : weighted version for two numbers;
• geom_mean_le_arith_mean3_weighted : weighted version for three numbers;
• geom_mean_le_arith_mean4_weighted : weighted version for four numbers.

Young's inequality

Young's inequality says that for non-negative numbers a, b, p, q such that $\frac{1}{p}+\frac{1}{q}=1$ we have $$ ab ≤ \frac{a^p}{p} + \frac{b^q}{q}. $$

This inequality is a special case of the AM-GM inequality. It is then used to prove Hölder's inequality (see below).

Hölder's inequality

The inequality says that for two conjugate exponents p and q (i.e., for two positive numbers such that $\frac{1}{p}+\frac{1}{q}=1$) and any two non-negative vectors their inner product is less than or equal to the product of the $L_p$ norm of the first vector and the $L_q$ norm of the second vector: $$ \sum_{i\in s} a_ib_i ≤ \sqrt[p]{\sum_{i\in s} a_i^p}\sqrt[q]{\sum_{i\in s} b_i^q}. $$

We give versions of this result in ℝ, ℝ≥0 and ℝ≥0∞.

There are at least two short proofs of this inequality. In our proof we prenormalize both vectors, then apply Young's inequality to each $a_ib_i$. Another possible proof would be to deduce this inequality from the generalized mean inequality for well-chosen vectors and weights.

Minkowski's inequality

The inequality says that for p ≥ 1 the function $$ |a|p=\sqrt[p]{\sum{i\in s} a_i^p} $$ satisfies the triangle inequality $|a+b|_p\le |a|_p+|b|_p$.

We give versions of this result in Real, ℝ≥0 and ℝ≥0∞.

We deduce this inequality from Hölder's inequality. Namely, Hölder inequality implies that $|a|p$ is the maximum of the inner product $\sum{i\in s}a_ib_i$ over b such that $|b|_q\le 1$. Now Minkowski's inequality follows from the fact that the maximum value of the sum of two functions is less than or equal to the sum of the maximum values of the summands.

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.

AM-GM inequality

theorem Real.geom_mean_le_arith_mean_weighted {ι : Type u} (s : Finset ι) (w : ι → ℝ) (z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : (Finset.sum s fun (i : ι) => w i) = 1) (hz : ∀ i ∈ s, 0 ≤ z i) : (Finset.prod s fun (i : ι) => z i ^ w i) ≤ Finset.sum s fun (i : ι) => w i * z i

AM-GM inequality: the geometric mean is less than or equal to the arithmetic mean, weighted version for real-valued nonnegative functions.

theorem Real.geom_mean_le_arith_mean {ι : Type u_1} (s : Finset ι) (w : ι → ℝ) (z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : 0 < Finset.sum s fun (i : ι) => w i) (hz : ∀ i ∈ s, 0 ≤ z i) : (Finset.prod s fun (i : ι) => z i ^ w i) ^ (Finset.sum s fun (i : ι) => w i)⁻¹ ≤ (Finset.sum s fun (i : ι) => w i * z i) / Finset.sum s fun (i : ι) => w i

AM-GM inequality: the geometric mean is less than or equal to the arithmetic mean. -

theorem Real.geom_mean_weighted_of_constant {ι : Type u} (s : Finset ι) (w : ι → ℝ) (z : ι → ℝ) (x : ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : (Finset.sum s fun (i : ι) => w i) = 1) (hz : ∀ i ∈ s, 0 ≤ z i) (hx : ∀ i ∈ s, w i ≠ 0 → z i = x) : (Finset.prod s fun (i : ι) => z i ^ w i) = x

theorem Real.arith_mean_weighted_of_constant {ι : Type u} (s : Finset ι) (w : ι → ℝ) (z : ι → ℝ) (x : ℝ) (hw' : (Finset.sum s fun (i : ι) => w i) = 1) (hx : ∀ i ∈ s, w i ≠ 0 → z i = x) : (Finset.sum s fun (i : ι) => w i * z i) = x

theorem Real.geom_mean_eq_arith_mean_weighted_of_constant {ι : Type u} (s : Finset ι) (w : ι → ℝ) (z : ι → ℝ) (x : ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : (Finset.sum s fun (i : ι) => w i) = 1) (hz : ∀ i ∈ s, 0 ≤ z i) (hx : ∀ i ∈ s, w i ≠ 0 → z i = x) : (Finset.prod s fun (i : ι) => z i ^ w i) = Finset.sum s fun (i : ι) => w i * z i

theorem NNReal.geom_mean_le_arith_mean_weighted {ι : Type u} (s : Finset ι) (w : ι → NNReal) (z : ι → NNReal) (hw' : (Finset.sum s fun (i : ι) => w i) = 1) : (Finset.prod s fun (i : ι) => z i ^ ↑(w i)) ≤ Finset.sum s fun (i : ι) => w i * z i

The geometric mean is less than or equal to the arithmetic mean, weighted version for NNReal-valued functions.

theorem NNReal.geom_mean_le_arith_mean2_weighted (w₁ : NNReal) (w₂ : NNReal) (p₁ : NNReal) (p₂ : NNReal) : w₁ + w₂ = 1 → p₁ ^ ↑w₁ * p₂ ^ ↑w₂ ≤ w₁ * p₁ + w₂ * p₂

The geometric mean is less than or equal to the arithmetic mean, weighted version for two NNReal numbers.

theorem NNReal.geom_mean_le_arith_mean3_weighted (w₁ : NNReal) (w₂ : NNReal) (w₃ : NNReal) (p₁ : NNReal) (p₂ : NNReal) (p₃ : NNReal) : w₁ + w₂ + w₃ = 1 → p₁ ^ ↑w₁ * p₂ ^ ↑w₂ * p₃ ^ ↑w₃ ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃

theorem NNReal.geom_mean_le_arith_mean4_weighted (w₁ : NNReal) (w₂ : NNReal) (w₃ : NNReal) (w₄ : NNReal) (p₁ : NNReal) (p₂ : NNReal) (p₃ : NNReal) (p₄ : NNReal) : w₁ + w₂ + w₃ + w₄ = 1 → p₁ ^ ↑w₁ * p₂ ^ ↑w₂ * p₃ ^ ↑w₃ * p₄ ^ ↑w₄ ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃ + w₄ * p₄

theorem Real.geom_mean_le_arith_mean2_weighted {w₁ : ℝ} {w₂ : ℝ} {p₁ : ℝ} {p₂ : ℝ} (hw₁ : 0 ≤ w₁) (hw₂ : 0 ≤ w₂) (hp₁ : 0 ≤ p₁) (hp₂ : 0 ≤ p₂) (hw : w₁ + w₂ = 1) : p₁ ^ w₁ * p₂ ^ w₂ ≤ w₁ * p₁ + w₂ * p₂

theorem Real.geom_mean_le_arith_mean3_weighted {w₁ : ℝ} {w₂ : ℝ} {w₃ : ℝ} {p₁ : ℝ} {p₂ : ℝ} {p₃ : ℝ} (hw₁ : 0 ≤ w₁) (hw₂ : 0 ≤ w₂) (hw₃ : 0 ≤ w₃) (hp₁ : 0 ≤ p₁) (hp₂ : 0 ≤ p₂) (hp₃ : 0 ≤ p₃) (hw : w₁ + w₂ + w₃ = 1) : p₁ ^ w₁ * p₂ ^ w₂ * p₃ ^ w₃ ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃

theorem Real.geom_mean_le_arith_mean4_weighted {w₁ : ℝ} {w₂ : ℝ} {w₃ : ℝ} {w₄ : ℝ} {p₁ : ℝ} {p₂ : ℝ} {p₃ : ℝ} {p₄ : ℝ} (hw₁ : 0 ≤ w₁) (hw₂ : 0 ≤ w₂) (hw₃ : 0 ≤ w₃) (hw₄ : 0 ≤ w₄) (hp₁ : 0 ≤ p₁) (hp₂ : 0 ≤ p₂) (hp₃ : 0 ≤ p₃) (hp₄ : 0 ≤ p₄) (hw : w₁ + w₂ + w₃ + w₄ = 1) : p₁ ^ w₁ * p₂ ^ w₂ * p₃ ^ w₃ * p₄ ^ w₄ ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃ + w₄ * p₄

Young's inequality

theorem Real.young_inequality_of_nonneg {a : ℝ} {b : ℝ} {p : ℝ} {q : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hpq : Real.IsConjugateExponent p q) : a * b ≤ a ^ p / p + b ^ q / q

Young's inequality, a version for nonnegative real numbers.

theorem Real.young_inequality (a : ℝ) (b : ℝ) {p : ℝ} {q : ℝ} (hpq : Real.IsConjugateExponent p q) : a * b ≤ |a| ^ p / p + |b| ^ q / q

Young's inequality, a version for arbitrary real numbers.

theorem NNReal.young_inequality (a : NNReal) (b : NNReal) {p : NNReal} {q : NNReal} (hp : 1 < p) (hpq : 1 / p + 1 / q = 1) : a * b ≤ a ^ ↑p / p + b ^ ↑q / q

Young's inequality, ℝ≥0 version. We use {p q : ℝ≥0} in order to avoid constructing witnesses of 0 ≤ p and 0 ≤ q for the denominators.

theorem NNReal.young_inequality_real (a : NNReal) (b : NNReal) {p : ℝ} {q : ℝ} (hpq : Real.IsConjugateExponent p q) : a * b ≤ a ^ p / Real.toNNReal p + b ^ q / Real.toNNReal q

Young's inequality, ℝ≥0 version with real conjugate exponents.

theorem ENNReal.young_inequality (a : ENNReal) (b : ENNReal) {p : ℝ} {q : ℝ} (hpq : Real.IsConjugateExponent p q) : a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q

Young's inequality, ℝ≥0∞ version with real conjugate exponents.

Hölder's and Minkowski's inequalities

theorem NNReal.inner_le_Lp_mul_Lq {ι : Type u} (s : Finset ι) (f : ι → NNReal) (g : ι → NNReal) {p : ℝ} {q : ℝ} (hpq : Real.IsConjugateExponent p q) : (Finset.sum s fun (i : ι) => f i * g i) ≤ (Finset.sum s fun (i : ι) => f i ^ p) ^ (1 / p) * (Finset.sum s fun (i : ι) => g i ^ q) ^ (1 / q)

Hölder inequality: the scalar product of two functions is bounded by the product of their L^p and L^q norms when p and q are conjugate exponents. Version for sums over finite sets, with ℝ≥0-valued functions.

theorem NNReal.inner_le_Lp_mul_Lq_tsum {ι : Type u} {f : ι → NNReal} {g : ι → NNReal} {p : ℝ} {q : ℝ} (hpq : Real.IsConjugateExponent p q) (hf : Summable fun (i : ι) => f i ^ p) (hg : Summable fun (i : ι) => g i ^ q) : (Summable fun (i : ι) => f i * g i) ∧ ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)

Hölder inequality: the scalar product of two functions is bounded by the product of their L^p and L^q norms when p and q are conjugate exponents. A version for NNReal-valued functions. For an alternative version, convenient if the infinite sums are already expressed as p-th powers, see inner_le_Lp_mul_Lq_hasSum.

theorem NNReal.summable_mul_of_Lp_Lq {ι : Type u} {f : ι → NNReal} {g : ι → NNReal} {p : ℝ} {q : ℝ} (hpq : Real.IsConjugateExponent p q) (hf : Summable fun (i : ι) => f i ^ p) (hg : Summable fun (i : ι) => g i ^ q) : Summable fun (i : ι) => f i * g i

theorem NNReal.inner_le_Lp_mul_Lq_tsum' {ι : Type u} {f : ι → NNReal} {g : ι → NNReal} {p : ℝ} {q : ℝ} (hpq : Real.IsConjugateExponent p q) (hf : Summable fun (i : ι) => f i ^ p) (hg : Summable fun (i : ι) => g i ^ q) : ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)

theorem NNReal.inner_le_Lp_mul_Lq_hasSum {ι : Type u} {f : ι → NNReal} {g : ι → NNReal} {A : NNReal} {B : NNReal} {p : ℝ} {q : ℝ} (hpq : Real.IsConjugateExponent p q) (hf : HasSum (fun (i : ι) => f i ^ p) (A ^ p)) (hg : HasSum (fun (i : ι) => g i ^ q) (B ^ q)) : ∃ C ≤ A * B, HasSum (fun (i : ι) => f i * g i) C

Hölder inequality: the scalar product of two functions is bounded by the product of their L^p and L^q norms when p and q are conjugate exponents. A version for NNReal-valued functions. For an alternative version, convenient if the infinite sums are not already expressed as p-th powers, see inner_le_Lp_mul_Lq_tsum.

theorem NNReal.rpow_sum_le_const_mul_sum_rpow {ι : Type u} (s : Finset ι) (f : ι → NNReal) {p : ℝ} (hp : 1 ≤ p) : (Finset.sum s fun (i : ι) => f i) ^ p ≤ ↑s.card ^ (p - 1) * Finset.sum s fun (i : ι) => f i ^ p

For 1 ≤ p, the p-th power of the sum of f i is bounded above by a constant times the sum of the p-th powers of f i. Version for sums over finite sets, with ℝ≥0-valued functions.

theorem NNReal.isGreatest_Lp {ι : Type u} (s : Finset ι) (f : ι → NNReal) {p : ℝ} {q : ℝ} (hpq : Real.IsConjugateExponent p q) : IsGreatest ((fun (g : ι → NNReal) => Finset.sum s fun (i : ι) => f i * g i) '' {g : ι → NNReal | (Finset.sum s fun (i : ι) => g i ^ q) ≤ 1}) ((Finset.sum s fun (i : ι) => f i ^ p) ^ (1 / p))

The L_p seminorm of a vector f is the greatest value of the inner product ∑ i in s, f i * g i over functions g of L_q seminorm less than or equal to one.

theorem NNReal.Lp_add_le {ι : Type u} (s : Finset ι) (f : ι → NNReal) (g : ι → NNReal) {p : ℝ} (hp : 1 ≤ p) : (Finset.sum s fun (i : ι) => (f i + g i) ^ p) ^ (1 / p) ≤ (Finset.sum s fun (i : ι) => f i ^ p) ^ (1 / p) + (Finset.sum s fun (i : ι) => g i ^ p) ^ (1 / p)

Minkowski inequality: the L_p seminorm of the sum of two vectors is less than or equal to the sum of the L_p-seminorms of the summands. A version for NNReal-valued functions.

theorem NNReal.Lp_add_le_tsum {ι : Type u} {f : ι → NNReal} {g : ι → NNReal} {p : ℝ} (hp : 1 ≤ p) (hf : Summable fun (i : ι) => f i ^ p) (hg : Summable fun (i : ι) => g i ^ p) : (Summable fun (i : ι) => (f i + g i) ^ p) ∧ (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)

Minkowski inequality: the L_p seminorm of the infinite sum of two vectors is less than or equal to the infinite sum of the L_p-seminorms of the summands, if these infinite sums both exist. A version for NNReal-valued functions. For an alternative version, convenient if the infinite sums are already expressed as p-th powers, see Lp_add_le_hasSum_of_nonneg.

theorem NNReal.summable_Lp_add {ι : Type u} {f : ι → NNReal} {g : ι → NNReal} {p : ℝ} (hp : 1 ≤ p) (hf : Summable fun (i : ι) => f i ^ p) (hg : Summable fun (i : ι) => g i ^ p) : Summable fun (i : ι) => (f i + g i) ^ p

theorem NNReal.Lp_add_le_tsum' {ι : Type u} {f : ι → NNReal} {g : ι → NNReal} {p : ℝ} (hp : 1 ≤ p) (hf : Summable fun (i : ι) => f i ^ p) (hg : Summable fun (i : ι) => g i ^ p) : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)

theorem NNReal.Lp_add_le_hasSum {ι : Type u} {f : ι → NNReal} {g : ι → NNReal} {A : NNReal} {B : NNReal} {p : ℝ} (hp : 1 ≤ p) (hf : HasSum (fun (i : ι) => f i ^ p) (A ^ p)) (hg : HasSum (fun (i : ι) => g i ^ p) (B ^ p)) : ∃ C ≤ A + B, HasSum (fun (i : ι) => (f i + g i) ^ p) (C ^ p)

Minkowski inequality: the L_p seminorm of the infinite sum of two vectors is less than or equal to the infinite sum of the L_p-seminorms of the summands, if these infinite sums both exist. A version for NNReal-valued functions. For an alternative version, convenient if the infinite sums are not already expressed as p-th powers, see Lp_add_le_tsum_of_nonneg.

theorem Real.inner_le_Lp_mul_Lq {ι : Type u} (s : Finset ι) (f : ι → ℝ) (g : ι → ℝ) {p : ℝ} {q : ℝ} (hpq : Real.IsConjugateExponent p q) : (Finset.sum s fun (i : ι) => f i * g i) ≤ (Finset.sum s fun (i : ι) => |f i| ^ p) ^ (1 / p) * (Finset.sum s fun (i : ι) => |g i| ^ q) ^ (1 / q)

Hölder inequality: the scalar product of two functions is bounded by the product of their L^p and L^q norms when p and q are conjugate exponents. Version for sums over finite sets, with real-valued functions.

theorem Real.rpow_sum_le_const_mul_sum_rpow {ι : Type u} (s : Finset ι) (f : ι → ℝ) {p : ℝ} (hp : 1 ≤ p) : (Finset.sum s fun (i : ι) => |f i|) ^ p ≤ ↑s.card ^ (p - 1) * Finset.sum s fun (i : ι) => |f i| ^ p

For 1 ≤ p, the p-th power of the sum of f i is bounded above by a constant times the sum of the p-th powers of f i. Version for sums over finite sets, with ℝ-valued functions.

theorem Real.Lp_add_le {ι : Type u} (s : Finset ι) (f : ι → ℝ) (g : ι → ℝ) {p : ℝ} (hp : 1 ≤ p) : (Finset.sum s fun (i : ι) => |f i + g i| ^ p) ^ (1 / p) ≤ (Finset.sum s fun (i : ι) => |f i| ^ p) ^ (1 / p) + (Finset.sum s fun (i : ι) => |g i| ^ p) ^ (1 / p)

Minkowski inequality: the L_p seminorm of the sum of two vectors is less than or equal to the sum of the L_p-seminorms of the summands. A version for Real-valued functions.

theorem Real.inner_le_Lp_mul_Lq_of_nonneg {ι : Type u} (s : Finset ι) {f : ι → ℝ} {g : ι → ℝ} {p : ℝ} {q : ℝ} (hpq : Real.IsConjugateExponent p q) (hf : ∀ i ∈ s, 0 ≤ f i) (hg : ∀ i ∈ s, 0 ≤ g i) : (Finset.sum s fun (i : ι) => f i * g i) ≤ (Finset.sum s fun (i : ι) => f i ^ p) ^ (1 / p) * (Finset.sum s fun (i : ι) => g i ^ q) ^ (1 / q)

Hölder inequality: the scalar product of two functions is bounded by the product of their L^p and L^q norms when p and q are conjugate exponents. Version for sums over finite sets, with real-valued nonnegative functions.

theorem Real.inner_le_Lp_mul_Lq_tsum_of_nonneg {ι : Type u} {f : ι → ℝ} {g : ι → ℝ} {p : ℝ} {q : ℝ} (hpq : Real.IsConjugateExponent p q) (hf : ∀ (i : ι), 0 ≤ f i) (hg : ∀ (i : ι), 0 ≤ g i) (hf_sum : Summable fun (i : ι) => f i ^ p) (hg_sum : Summable fun (i : ι) => g i ^ q) : (Summable fun (i : ι) => f i * g i) ∧ ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)

Hölder inequality: the scalar product of two functions is bounded by the product of their L^p and L^q norms when p and q are conjugate exponents. A version for ℝ-valued functions. For an alternative version, convenient if the infinite sums are already expressed as p-th powers, see inner_le_Lp_mul_Lq_hasSum_of_nonneg.

theorem Real.summable_mul_of_Lp_Lq_of_nonneg {ι : Type u} {f : ι → ℝ} {g : ι → ℝ} {p : ℝ} {q : ℝ} (hpq : Real.IsConjugateExponent p q) (hf : ∀ (i : ι), 0 ≤ f i) (hg : ∀ (i : ι), 0 ≤ g i) (hf_sum : Summable fun (i : ι) => f i ^ p) (hg_sum : Summable fun (i : ι) => g i ^ q) : Summable fun (i : ι) => f i * g i

theorem Real.inner_le_Lp_mul_Lq_tsum_of_nonneg' {ι : Type u} {f : ι → ℝ} {g : ι → ℝ} {p : ℝ} {q : ℝ} (hpq : Real.IsConjugateExponent p q) (hf : ∀ (i : ι), 0 ≤ f i) (hg : ∀ (i : ι), 0 ≤ g i) (hf_sum : Summable fun (i : ι) => f i ^ p) (hg_sum : Summable fun (i : ι) => g i ^ q) : ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)

theorem Real.inner_le_Lp_mul_Lq_hasSum_of_nonneg {ι : Type u} {f : ι → ℝ} {g : ι → ℝ} {p : ℝ} {q : ℝ} (hpq : Real.IsConjugateExponent p q) {A : ℝ} {B : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hf : ∀ (i : ι), 0 ≤ f i) (hg : ∀ (i : ι), 0 ≤ g i) (hf_sum : HasSum (fun (i : ι) => f i ^ p) (A ^ p)) (hg_sum : HasSum (fun (i : ι) => g i ^ q) (B ^ q)) : ∃ (C : ℝ), 0 ≤ C ∧ C ≤ A * B ∧ HasSum (fun (i : ι) => f i * g i) C

Hölder inequality: the scalar product of two functions is bounded by the product of their L^p and L^q norms when p and q are conjugate exponents. A version for NNReal-valued functions. For an alternative version, convenient if the infinite sums are not already expressed as p-th powers, see inner_le_Lp_mul_Lq_tsum_of_nonneg.

theorem Real.rpow_sum_le_const_mul_sum_rpow_of_nonneg {ι : Type u} (s : Finset ι) {f : ι → ℝ} {p : ℝ} (hp : 1 ≤ p) (hf : ∀ i ∈ s, 0 ≤ f i) : (Finset.sum s fun (i : ι) => f i) ^ p ≤ ↑s.card ^ (p - 1) * Finset.sum s fun (i : ι) => f i ^ p

For 1 ≤ p, the p-th power of the sum of f i is bounded above by a constant times the sum of the p-th powers of f i. Version for sums over finite sets, with nonnegative ℝ-valued functions.

theorem Real.Lp_add_le_of_nonneg {ι : Type u} (s : Finset ι) {f : ι → ℝ} {g : ι → ℝ} {p : ℝ} (hp : 1 ≤ p) (hf : ∀ i ∈ s, 0 ≤ f i) (hg : ∀ i ∈ s, 0 ≤ g i) : (Finset.sum s fun (i : ι) => (f i + g i) ^ p) ^ (1 / p) ≤ (Finset.sum s fun (i : ι) => f i ^ p) ^ (1 / p) + (Finset.sum s fun (i : ι) => g i ^ p) ^ (1 / p)

Minkowski inequality: the L_p seminorm of the sum of two vectors is less than or equal to the sum of the L_p-seminorms of the summands. A version for ℝ-valued nonnegative functions.

theorem Real.Lp_add_le_tsum_of_nonneg {ι : Type u} {f : ι → ℝ} {g : ι → ℝ} {p : ℝ} (hp : 1 ≤ p) (hf : ∀ (i : ι), 0 ≤ f i) (hg : ∀ (i : ι), 0 ≤ g i) (hf_sum : Summable fun (i : ι) => f i ^ p) (hg_sum : Summable fun (i : ι) => g i ^ p) : (Summable fun (i : ι) => (f i + g i) ^ p) ∧ (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)

Minkowski inequality: the L_p seminorm of the infinite sum of two vectors is less than or equal to the infinite sum of the L_p-seminorms of the summands, if these infinite sums both exist. A version for ℝ-valued functions. For an alternative version, convenient if the infinite sums are already expressed as p-th powers, see Lp_add_le_hasSum_of_nonneg.

theorem Real.summable_Lp_add_of_nonneg {ι : Type u} {f : ι → ℝ} {g : ι → ℝ} {p : ℝ} (hp : 1 ≤ p) (hf : ∀ (i : ι), 0 ≤ f i) (hg : ∀ (i : ι), 0 ≤ g i) (hf_sum : Summable fun (i : ι) => f i ^ p) (hg_sum : Summable fun (i : ι) => g i ^ p) : Summable fun (i : ι) => (f i + g i) ^ p

theorem Real.Lp_add_le_tsum_of_nonneg' {ι : Type u} {f : ι → ℝ} {g : ι → ℝ} {p : ℝ} (hp : 1 ≤ p) (hf : ∀ (i : ι), 0 ≤ f i) (hg : ∀ (i : ι), 0 ≤ g i) (hf_sum : Summable fun (i : ι) => f i ^ p) (hg_sum : Summable fun (i : ι) => g i ^ p) : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)

theorem Real.Lp_add_le_hasSum_of_nonneg {ι : Type u} {f : ι → ℝ} {g : ι → ℝ} {p : ℝ} (hp : 1 ≤ p) (hf : ∀ (i : ι), 0 ≤ f i) (hg : ∀ (i : ι), 0 ≤ g i) {A : ℝ} {B : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hfA : HasSum (fun (i : ι) => f i ^ p) (A ^ p)) (hgB : HasSum (fun (i : ι) => g i ^ p) (B ^ p)) : ∃ (C : ℝ), 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun (i : ι) => (f i + g i) ^ p) (C ^ p)

Minkowski inequality: the L_p seminorm of the infinite sum of two vectors is less than or equal to the infinite sum of the L_p-seminorms of the summands, if these infinite sums both exist. A version for ℝ-valued functions. For an alternative version, convenient if the infinite sums are not already expressed as p-th powers, see Lp_add_le_tsum_of_nonneg.

theorem ENNReal.inner_le_Lp_mul_Lq {ι : Type u} (s : Finset ι) (f : ι → ENNReal) (g : ι → ENNReal) {p : ℝ} {q : ℝ} (hpq : Real.IsConjugateExponent p q) : (Finset.sum s fun (i : ι) => f i * g i) ≤ (Finset.sum s fun (i : ι) => f i ^ p) ^ (1 / p) * (Finset.sum s fun (i : ι) => g i ^ q) ^ (1 / q)

Hölder inequality: the scalar product of two functions is bounded by the product of their L^p and L^q norms when p and q are conjugate exponents. Version for sums over finite sets, with ℝ≥0∞-valued functions.

theorem ENNReal.rpow_sum_le_const_mul_sum_rpow {ι : Type u} (s : Finset ι) (f : ι → ENNReal) {p : ℝ} (hp : 1 ≤ p) : (Finset.sum s fun (i : ι) => f i) ^ p ≤ ↑s.card ^ (p - 1) * Finset.sum s fun (i : ι) => f i ^ p

For 1 ≤ p, the p-th power of the sum of f i is bounded above by a constant times the sum of the p-th powers of f i. Version for sums over finite sets, with ℝ≥0∞-valued functions.

theorem ENNReal.Lp_add_le {ι : Type u} (s : Finset ι) (f : ι → ENNReal) (g : ι → ENNReal) {p : ℝ} (hp : 1 ≤ p) : (Finset.sum s fun (i : ι) => (f i + g i) ^ p) ^ (1 / p) ≤ (Finset.sum s fun (i : ι) => f i ^ p) ^ (1 / p) + (Finset.sum s fun (i : ι) => g i ^ p) ^ (1 / p)

Minkowski inequality: the L_p seminorm of the sum of two vectors is less than or equal to the sum of the L_p-seminorms of the summands. A version for ℝ≥0∞ valued nonnegative functions.