mathlib documentation

analysis.mean_inequalities

Mean value inequalities #

In this file we prove several inequalities, including AM-GM inequality, Young's inequality, Hölder inequality, and Minkowski inequality.

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.

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 (fpow_arith_mean_le_arith_mean_fpow), 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.

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 can be used to prove Hölder's inequality (see below) but we use a different proof.

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 one proof we prenormalize both vectors, then apply Young's inequality to each $a_ib_i$. We use a different proof deducing this inequality from the generalized mean inequality for well-chosen vectors and weights.

Hölder's inequality for the Lebesgue integral of ℝ≥0∞ and ℝ≥0 functions: we prove ∫ (f * g) ∂μ ≤ (∫ f^p ∂μ) ^ (1/p) * (∫ g^q ∂μ) ^ (1/q) for p, q conjugate real exponents and α→(e)nnreal functions in two cases,

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.

Minkowski's inequality for the Lebesgue integral of measurable functions with ℝ≥0∞ values: we prove (∫ (f + g)^p ∂μ) ^ (1/p) ≤ (∫ f^p ∂μ) ^ (1/p) + (∫ g^p ∂μ) ^ (1/p) for 1 ≤ p.

TODO #

theorem real.geom_mean_le_arith_mean_weighted {ι : Type u} (s : finset ι) (w z : ι → ) (hw : ∀ (i : ι), i s0 w i) (hw' : ∑ (i : ι) in s, w i = 1) (hz : ∀ (i : ι), i s0 z i) :
∏ (i : ι) in s, z i ^ w i ∑ (i : ι) in s, (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.pow_arith_mean_le_arith_mean_pow {ι : Type u} (s : finset ι) (w z : ι → ) (hw : ∀ (i : ι), i s0 w i) (hw' : ∑ (i : ι) in s, w i = 1) (hz : ∀ (i : ι), i s0 z i) (n : ) :
(∑ (i : ι) in s, (w i) * z i) ^ n ∑ (i : ι) in 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 : ι), i s0 w i) (hw' : ∑ (i : ι) in s, w i = 1) {n : } (hn : even n) :
(∑ (i : ι) in s, (w i) * z i) ^ n ∑ (i : ι) in s, (w i) * z i ^ n
theorem real.fpow_arith_mean_le_arith_mean_fpow {ι : Type u} (s : finset ι) (w z : ι → ) (hw : ∀ (i : ι), i s0 w i) (hw' : ∑ (i : ι) in s, w i = 1) (hz : ∀ (i : ι), i s0 < z i) (m : ) :
(∑ (i : ι) in s, (w i) * z i) ^ m ∑ (i : ι) in s, (w i) * z i ^ m
theorem real.rpow_arith_mean_le_arith_mean_rpow {ι : Type u} (s : finset ι) (w z : ι → ) (hw : ∀ (i : ι), i s0 w i) (hw' : ∑ (i : ι) in s, w i = 1) (hz : ∀ (i : ι), i s0 z i) {p : } (hp : 1 p) :
(∑ (i : ι) in s, (w i) * z i) ^ p ∑ (i : ι) in s, (w i) * z i ^ p
theorem real.arith_mean_le_rpow_mean {ι : Type u} (s : finset ι) (w z : ι → ) (hw : ∀ (i : ι), i s0 w i) (hw' : ∑ (i : ι) in s, w i = 1) (hz : ∀ (i : ι), i s0 z i) {p : } (hp : 1 p) :
∑ (i : ι) in s, (w i) * z i (∑ (i : ι) in s, (w i) * z i ^ p) ^ (1 / p)
theorem nnreal.geom_mean_le_arith_mean_weighted {ι : Type u} (s : finset ι) (w z : ι → ℝ≥0) (hw' : ∑ (i : ι) in s, w i = 1) :
∏ (i : ι) in s, z i ^ (w i) ∑ (i : ι) in s, (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₁ w₂ p₁ p₂ : ℝ≥0) :
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₁ w₂ w₃ p₁ p₂ p₃ : ℝ≥0) :
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₁ w₂ w₃ w₄ p₁ p₂ p₃ p₄ : ℝ≥0) :
w₁ + w₂ + w₃ + w₄ = 1(((p₁ ^ w₁) * p₂ ^ w₂) * p₃ ^ w₃) * p₄ ^ w₄ w₁ * p₁ + w₂ * p₂ + w₃ * p₃ + w₄ * p₄
theorem nnreal.pow_arith_mean_le_arith_mean_pow {ι : Type u} (s : finset ι) (w z : ι → ℝ≥0) (hw' : ∑ (i : ι) in s, w i = 1) (n : ) :
(∑ (i : ι) in s, (w i) * z i) ^ n ∑ (i : ι) in s, (w i) * z i ^ n

Weighted generalized mean inequality, version sums over finite sets, with ℝ≥0-valued functions and natural exponent.

theorem nnreal.rpow_arith_mean_le_arith_mean_rpow {ι : Type u} (s : finset ι) (w z : ι → ℝ≥0) (hw' : ∑ (i : ι) in s, w i = 1) {p : } (hp : 1 p) :
(∑ (i : ι) in s, (w i) * z i) ^ p ∑ (i : ι) in 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₁ w₂ z₁ z₂ : ℝ≥0) (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.arith_mean_le_rpow_mean {ι : Type u} (s : finset ι) (w z : ι → ℝ≥0) (hw' : ∑ (i : ι) in s, w i = 1) {p : } (hp : 1 p) :
∑ (i : ι) in s, (w i) * z i (∑ (i : ι) in 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 ennreal.rpow_arith_mean_le_arith_mean_rpow {ι : Type u} (s : finset ι) (w z : ι → ℝ≥0∞) (hw' : ∑ (i : ι) in s, w i = 1) {p : } (hp : 1 p) :
(∑ (i : ι) in s, (w i) * z i) ^ p ∑ (i : ι) in 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₁ w₂ z₁ z₂ : ℝ≥0∞) (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 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₄
theorem real.young_inequality_of_nonneg {a b p q : } (ha : 0 a) (hb : 0 b) (hpq : p.is_conjugate_exponent 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 : p.is_conjugate_exponent q) :
a * b abs a ^ p / p + abs b ^ q / q

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

theorem nnreal.young_inequality (a b : ℝ≥0) {p q : ℝ≥0} (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 b : ℝ≥0) {p q : } (hpq : p.is_conjugate_exponent q) :

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

theorem nnreal.inner_le_Lp_mul_Lq {ι : Type u} (s : finset ι) (f g : ι → ℝ≥0) {p q : } (hpq : p.is_conjugate_exponent q) :
∑ (i : ι) in s, (f i) * g i ((∑ (i : ι) in s, f i ^ p) ^ (1 / p)) * (∑ (i : ι) in s, 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.is_greatest_Lp {ι : Type u} (s : finset ι) (f : ι → ℝ≥0) {p q : } (hpq : p.is_conjugate_exponent q) :
is_greatest ((λ (g : ι → ℝ≥0), ∑ (i : ι) in s, (f i) * g i) '' {g : ι → ℝ≥0 | ∑ (i : ι) in s, g i ^ q 1}) ((∑ (i : ι) in s, 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 g : ι → ℝ≥0) {p : } (hp : 1 p) :
(∑ (i : ι) in s, (f i + g i) ^ p) ^ (1 / p) (∑ (i : ι) in s, f i ^ p) ^ (1 / p) + (∑ (i : ι) in s, 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 real.inner_le_Lp_mul_Lq {ι : Type u} (s : finset ι) (f g : ι → ) {p q : } (hpq : p.is_conjugate_exponent q) :
∑ (i : ι) in s, (f i) * g i ((∑ (i : ι) in s, abs (f i) ^ p) ^ (1 / p)) * (∑ (i : ι) in s, abs (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.Lp_add_le {ι : Type u} (s : finset ι) (f g : ι → ) {p : } (hp : 1 p) :
(∑ (i : ι) in s, abs (f i + g i) ^ p) ^ (1 / p) (∑ (i : ι) in s, abs (f i) ^ p) ^ (1 / p) + (∑ (i : ι) in s, abs (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 : p.is_conjugate_exponent q) (hf : ∀ (i : ι), i s0 f i) (hg : ∀ (i : ι), i s0 g i) :
∑ (i : ι) in s, (f i) * g i ((∑ (i : ι) in s, f i ^ p) ^ (1 / p)) * (∑ (i : ι) in s, 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.Lp_add_le_of_nonneg {ι : Type u} (s : finset ι) {f g : ι → } {p : } (hp : 1 p) (hf : ∀ (i : ι), i s0 f i) (hg : ∀ (i : ι), i s0 g i) :
(∑ (i : ι) in s, (f i + g i) ^ p) ^ (1 / p) (∑ (i : ι) in s, f i ^ p) ^ (1 / p) + (∑ (i : ι) in s, 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 nonnegative functions.

theorem ennreal.young_inequality (a b : ℝ≥0∞) {p q : } (hpq : p.is_conjugate_exponent q) :

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

theorem ennreal.inner_le_Lp_mul_Lq {ι : Type u} (s : finset ι) (f g : ι → ℝ≥0∞) {p q : } (hpq : p.is_conjugate_exponent q) :
∑ (i : ι) in s, (f i) * g i ((∑ (i : ι) in s, f i ^ p) ^ (1 / p)) * (∑ (i : ι) in s, 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.Lp_add_le {ι : Type u} (s : finset ι) (f g : ι → ℝ≥0∞) {p : } (hp : 1 p) :
(∑ (i : ι) in s, (f i + g i) ^ p) ^ (1 / p) (∑ (i : ι) in s, f i ^ p) ^ (1 / p) + (∑ (i : ι) in s, 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.

theorem ennreal.add_rpow_le_rpow_add {p : } (a b : ℝ≥0∞) (hp1 : 1 p) :
a ^ p + b ^ p (a + b) ^ p
theorem ennreal.rpow_add_rpow_le_add {p : } (a b : ℝ≥0∞) (hp1 : 1 p) :
(a ^ p + b ^ p) ^ (1 / p) a + b
theorem ennreal.rpow_add_rpow_le {p q : } (a b : ℝ≥0∞) (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 : ℝ≥0∞) (hp_pos : 0 < p) (hp1 : p 1) :
(a + b) ^ p a ^ p + b ^ p

Hölder's inequality for the Lebesgue integral of ℝ≥0∞ and nnreal functions #

We prove ∫ (f * g) ∂μ ≤ (∫ f^p ∂μ) ^ (1/p) * (∫ g^q ∂μ) ^ (1/q) for p, q conjugate real exponents and α→(e)nnreal functions in several cases, the first two being useful only to prove the more general results:

theorem ennreal.lintegral_mul_le_one_of_lintegral_rpow_eq_one {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {p q : } (hpq : p.is_conjugate_exponent q) {f g : α → ℝ≥0∞} (hf : ae_measurable f μ) (hg : ae_measurable g μ) (hf_norm : ∫⁻ (a : α), f a ^ p μ = 1) (hg_norm : ∫⁻ (a : α), g a ^ q μ = 1) :
∫⁻ (a : α), (f * g) a μ 1
def ennreal.fun_mul_inv_snorm {α : Type u_1} [measurable_space α] (f : α → ℝ≥0∞) (p : ) (μ : measure_theory.measure α) :
α → ℝ≥0∞

Function multiplied by the inverse of its p-seminorm (∫⁻ f^p ∂μ) ^ 1/p

Equations
theorem ennreal.fun_eq_fun_mul_inv_snorm_mul_snorm {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {p : } (f : α → ℝ≥0∞) (hf_nonzero : ∫⁻ (a : α), f a ^ p μ 0) (hf_top : ∫⁻ (a : α), f a ^ p μ ) {a : α} :
f a = (ennreal.fun_mul_inv_snorm f p μ a) * (∫⁻ (c : α), f c ^ p μ) ^ (1 / p)
theorem ennreal.fun_mul_inv_snorm_rpow {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {p : } (hp0 : 0 < p) {f : α → ℝ≥0∞} {a : α} :
ennreal.fun_mul_inv_snorm f p μ a ^ p = (f a ^ p) * (∫⁻ (c : α), f c ^ p μ)⁻¹
theorem ennreal.lintegral_rpow_fun_mul_inv_snorm_eq_one {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {p : } (hp0_lt : 0 < p) {f : α → ℝ≥0∞} (hf : ae_measurable f μ) (hf_nonzero : ∫⁻ (a : α), f a ^ p μ 0) (hf_top : ∫⁻ (a : α), f a ^ p μ ) :
∫⁻ (c : α), ennreal.fun_mul_inv_snorm f p μ c ^ p μ = 1
theorem ennreal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {p q : } (hpq : p.is_conjugate_exponent q) {f g : α → ℝ≥0∞} (hf : ae_measurable f μ) (hg : ae_measurable g μ) (hf_nontop : ∫⁻ (a : α), f a ^ p μ ) (hg_nontop : ∫⁻ (a : α), g a ^ q μ ) (hf_nonzero : ∫⁻ (a : α), f a ^ p μ 0) (hg_nonzero : ∫⁻ (a : α), g a ^ q μ 0) :
∫⁻ (a : α), (f * g) a μ ((∫⁻ (a : α), f a ^ p μ) ^ (1 / p)) * (∫⁻ (a : α), g a ^ q μ) ^ (1 / q)

Hölder's inequality in case of finite non-zero integrals

theorem ennreal.ae_eq_zero_of_lintegral_rpow_eq_zero {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {p : } (hp0_lt : 0 < p) {f : α → ℝ≥0∞} (hf : ae_measurable f μ) (hf_zero : ∫⁻ (a : α), f a ^ p μ = 0) :
f =ᵐ[μ] 0
theorem ennreal.lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {p : } (hp0_lt : 0 < p) {f g : α → ℝ≥0∞} (hf : ae_measurable f μ) (hf_zero : ∫⁻ (a : α), f a ^ p μ = 0) :
∫⁻ (a : α), (f * g) a μ = 0
theorem ennreal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {p q : } (hp0_lt : 0 < p) (hq0 : 0 q) {f g : α → ℝ≥0∞} (hf_top : ∫⁻ (a : α), f a ^ p μ = ) (hg_nonzero : ∫⁻ (a : α), g a ^ q μ 0) :
∫⁻ (a : α), (f * g) a μ ((∫⁻ (a : α), f a ^ p μ) ^ (1 / p)) * (∫⁻ (a : α), g a ^ q μ) ^ (1 / q)
theorem ennreal.lintegral_mul_le_Lp_mul_Lq {α : Type u_1} [measurable_space α] (μ : measure_theory.measure α) {p q : } (hpq : p.is_conjugate_exponent q) {f g : α → ℝ≥0∞} (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
∫⁻ (a : α), (f * g) a μ ((∫⁻ (a : α), f a ^ p μ) ^ (1 / p)) * (∫⁻ (a : α), g a ^ q μ) ^ (1 / q)

Hölder's inequality for functions α → ℝ≥0∞. The integral of the product of two functions is bounded by the product of their ℒp and ℒq seminorms when p and q are conjugate exponents.

theorem ennreal.lintegral_rpow_add_lt_top_of_lintegral_rpow_lt_top {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {p : } {f g : α → ℝ≥0∞} (hf : ae_measurable f μ) (hf_top : ∫⁻ (a : α), f a ^ p μ < ) (hg : ae_measurable g μ) (hg_top : ∫⁻ (a : α), g a ^ p μ < ) (hp1 : 1 p) :
∫⁻ (a : α), (f + g) a ^ p μ <
theorem ennreal.lintegral_Lp_mul_le_Lq_mul_Lr {α : Type u_1} [measurable_space α] {p q r : } (hp0_lt : 0 < p) (hpq : p < q) (hpqr : 1 / p = 1 / q + 1 / r) (μ : measure_theory.measure α) {f g : α → ℝ≥0∞} (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
(∫⁻ (a : α), (f * g) a ^ p μ) ^ (1 / p) ((∫⁻ (a : α), f a ^ q μ) ^ (1 / q)) * (∫⁻ (a : α), g a ^ r μ) ^ (1 / r)
theorem ennreal.lintegral_mul_rpow_le_lintegral_rpow_mul_lintegral_rpow {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {p q : } (hpq : p.is_conjugate_exponent q) {f g : α → ℝ≥0∞} (hf : ae_measurable f μ) (hg : ae_measurable g μ) (hf_top : ∫⁻ (a : α), f a ^ p μ ) :
∫⁻ (a : α), (f a) * g a ^ (p - 1) μ ((∫⁻ (a : α), f a ^ p μ) ^ (1 / p)) * (∫⁻ (a : α), g a ^ p μ) ^ (1 / q)
theorem ennreal.lintegral_rpow_add_le_add_snorm_mul_lintegral_rpow_add {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {p q : } (hpq : p.is_conjugate_exponent q) {f g : α → ℝ≥0∞} (hf : ae_measurable f μ) (hf_top : ∫⁻ (a : α), f a ^ p μ ) (hg : ae_measurable g μ) (hg_top : ∫⁻ (a : α), g a ^ p μ ) :
∫⁻ (a : α), (f + g) a ^ p μ ((∫⁻ (a : α), f a ^ p μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p μ) ^ (1 / p)) * (∫⁻ (a : α), (f a + g a) ^ p μ) ^ (1 / q)
theorem ennreal.lintegral_Lp_add_le {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {p : } {f g : α → ℝ≥0∞} (hf : ae_measurable f μ) (hg : ae_measurable g μ) (hp1 : 1 p) :
(∫⁻ (a : α), (f + g) a ^ p μ) ^ (1 / p) (∫⁻ (a : α), f a ^ p μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p μ) ^ (1 / p)

Minkowski's inequality for functions α → ℝ≥0∞: the ℒp seminorm of the sum of two functions is bounded by the sum of their ℒp seminorms.

theorem nnreal.lintegral_mul_le_Lp_mul_Lq {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {p q : } (hpq : p.is_conjugate_exponent q) {f g : α → ℝ≥0} (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
∫⁻ (a : α), ((f * g) a) μ ((∫⁻ (a : α), (f a) ^ p μ) ^ (1 / p)) * (∫⁻ (a : α), (g a) ^ q μ) ^ (1 / q)

Hölder's inequality for functions α → ℝ≥0. The integral of the product of two functions is bounded by the product of their ℒp and ℒq seminorms when p and q are conjugate exponents.