# mathlib3documentation

measure_theory.integral.mean_inequalities

# Mean value inequalities for integrals #

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

In this file we prove several inequalities on integrals, notably the Hölder inequality and the Minkowski inequality. The versions for finite sums are in analysis.mean_inequalities.

## Main results #

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,

• ennreal.lintegral_mul_le_Lp_mul_Lq : ℝ≥0∞ functions,
• nnreal.lintegral_mul_le_Lp_mul_Lq : ℝ≥0 functions.

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.

### 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:

• ennreal.lintegral_mul_le_one_of_lintegral_rpow_eq_one : ℝ≥0∞ functions for which the integrals on the right are equal to 1,
• ennreal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top : ℝ≥0∞ functions for which the integrals on the right are neither ⊤ nor 0,
• ennreal.lintegral_mul_le_Lp_mul_Lq : ℝ≥0∞ functions,
• nnreal.lintegral_mul_le_Lp_mul_Lq : nnreal functions.
theorem ennreal.lintegral_mul_le_one_of_lintegral_rpow_eq_one {α : Type u_1} {μ : measure_theory.measure α} {p q : } (hpq : p.is_conjugate_exponent q) {f g : α ennreal} (hf : μ) (hf_norm : ∫⁻ (a : α), f a ^ p μ = 1) (hg_norm : ∫⁻ (a : α), g a ^ q μ = 1) :
∫⁻ (a : α), (f * g) a μ 1
noncomputable def ennreal.fun_mul_inv_snorm {α : Type u_1} (f : α ennreal) (p : ) (μ : measure_theory.measure α) :

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} {μ : measure_theory.measure α} {p : } (f : α ennreal) (hf_nonzero : ∫⁻ (a : α), f a ^ p μ 0) (hf_top : ∫⁻ (a : α), f a ^ p μ ) {a : α} :
f a = a * (∫⁻ (c : α), f c ^ p μ) ^ (1 / p)
theorem ennreal.fun_mul_inv_snorm_rpow {α : Type u_1} {μ : measure_theory.measure α} {p : } (hp0 : 0 < p) {f : α ennreal} {a : α} :
a ^ p = f a ^ p * (∫⁻ (c : α), f c ^ p μ)⁻¹
theorem ennreal.lintegral_rpow_fun_mul_inv_snorm_eq_one {α : Type u_1} {μ : measure_theory.measure α} {p : } (hp0_lt : 0 < p) {f : α ennreal} (hf_nonzero : ∫⁻ (a : α), f a ^ p μ 0) (hf_top : ∫⁻ (a : α), f a ^ p μ ) :
∫⁻ (c : α), c ^ p μ = 1
theorem ennreal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top {α : Type u_1} {μ : measure_theory.measure α} {p q : } (hpq : p.is_conjugate_exponent q) {f g : α ennreal} (hf : μ) (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} {μ : measure_theory.measure α} {p : } (hp0 : 0 p) {f : α ennreal} (hf : μ) (hf_zero : ∫⁻ (a : α), f a ^ p μ = 0) :
f =ᵐ[μ] 0
theorem ennreal.lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero {α : Type u_1} {μ : measure_theory.measure α} {p : } (hp0 : 0 p) {f g : α ennreal} (hf : μ) (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} {μ : measure_theory.measure α} {p q : } (hp0_lt : 0 < p) (hq0 : 0 q) {f g : α ennreal} (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} (μ : measure_theory.measure α) {p q : } (hpq : p.is_conjugate_exponent q) {f g : α ennreal} (hf : μ) (hg : μ) :
∫⁻ (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} {μ : measure_theory.measure α} {p : } {f g : α ennreal} (hf : μ) (hf_top : ∫⁻ (a : α), f a ^ p μ < ) (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} {p q r : } (hp0_lt : 0 < p) (hpq : p < q) (hpqr : 1 / p = 1 / q + 1 / r) (μ : measure_theory.measure α) {f g : α ennreal} (hf : μ) (hg : μ) :
(∫⁻ (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} {μ : measure_theory.measure α} {p q : } (hpq : p.is_conjugate_exponent q) {f g : α ennreal} (hf : μ) (hg : μ) (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} {μ : measure_theory.measure α} {p q : } (hpq : p.is_conjugate_exponent q) {f g : α ennreal} (hf : μ) (hf_top : ∫⁻ (a : α), f a ^ p μ ) (hg : μ) (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} {μ : measure_theory.measure α} {p : } {f g : α ennreal} (hf : μ) (hg : μ) (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 ennreal.lintegral_Lp_add_le_of_le_one {α : Type u_1} {μ : measure_theory.measure α} {p : } {f g : α ennreal} (hf : μ) (hp0 : 0 p) (hp1 : p 1) :
(∫⁻ (a : α), (f + g) a ^ p μ) ^ (1 / p) 2 ^ (1 / p - 1) * ((∫⁻ (a : α), f a ^ p μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p μ) ^ (1 / p))

Variant of Minkowski's inequality for functions α → ℝ≥0∞ in ℒp with p ≤ 1: the ℒp seminorm of the sum of two functions is bounded by a constant multiple of the sum of their ℒp seminorms.

theorem nnreal.lintegral_mul_le_Lp_mul_Lq {α : Type u_1} {μ : measure_theory.measure α} {p q : } (hpq : p.is_conjugate_exponent q) {f g : α nnreal} (hf : μ) (hg : μ) :
∫⁻ (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.