mathlib3 documentation

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} [measurable_space α] {μ : measure_theory.measure α} {p q : ℝ} (hpq : p.is_conjugate_exponent q) {f g : α → ennreal} (hf : ae_measurable f μ) (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} [measurable_space α] (f : α → ennreal) (p : ℝ) (μ : measure_theory.measure α) :

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

Equations

ennreal.fun_mul_inv_snorm f p μ = λ (a : α), f a * ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹

theorem ennreal.fun_eq_fun_mul_inv_snorm_mul_snorm {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {p : ℝ} (f : α → ennreal) (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 : α → ennreal} {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 : α → ennreal} (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 : α → ennreal} (hf : ae_measurable f μ) (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 : 0 ≤ p) {f : α → ennreal} (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 : 0 ≤ p) {f g : α → ennreal} (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 : α → 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} [measurable_space α] (μ : measure_theory.measure α) {p q : ℝ} (hpq : p.is_conjugate_exponent q) {f g : α → ennreal} (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 : α → ennreal} (hf : ae_measurable f μ) (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} [measurable_space α] {p q r : ℝ} (hp0_lt : 0 < p) (hpq : p < q) (hpqr : 1 / p = 1 / q + 1 / r) (μ : measure_theory.measure α) {f g : α → ennreal} (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 : α → ennreal} (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 : α → ennreal} (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 : α → ennreal} (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 ennreal.lintegral_Lp_add_le_of_le_one {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {p : ℝ} {f g : α → ennreal} (hf : ae_measurable f μ) (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} [measurable_space α] {μ : measure_theory.measure α} {p q : ℝ} (hpq : p.is_conjugate_exponent q) {f g : α → nnreal} (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.