Mean value inequalities for integrals

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.MeanInequalities.

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.

ENNReal.lintegral_mul_norm_pow_le is a variant where the exponents are not reciprocals: ∫ (f ^ p * g ^ q) ∂μ ≤ (∫ f ∂μ) ^ p * (∫ g ∂μ) ^ q where p, q ≥ 0 and p + q = 1. ENNReal.lintegral_prod_norm_pow_le generalizes this to a finite family of functions: ∫ (∏ i, f i ^ p i) ∂μ ≤ ∏ i, (∫ f i ∂μ) ^ p i when the p is a collection of nonnegative weights with sum 1.

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 ℝ≥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 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 : ℝ≥0 functions.

theorem ENNReal.lintegral_mul_le_one_of_lintegral_rpow_eq_one {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ℝ} {q : ℝ} (hpq : Real.IsConjExponent p q) {f : α → ENNReal} {g : α → ENNReal} (hf : AEMeasurable f μ) (hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1) (hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1) : ∫⁻ (a : α), (f * g) a ∂μ ≤ 1

def ENNReal.funMulInvSnorm {α : Type u_1} [MeasurableSpace α] (f : α → ENNReal) (p : ℝ) (μ : MeasureTheory.Measure α) : α → ENNReal

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

Equations

• ENNReal.funMulInvSnorm f p μ a = f a * ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹

theorem ENNReal.fun_eq_funMulInvSnorm_mul_snorm {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ℝ} (f : α → ENNReal) (hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0) (hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤) {a : α} : f a = ENNReal.funMulInvSnorm f p μ a * (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)

theorem ENNReal.funMulInvSnorm_rpow {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ℝ} (hp0 : 0 < p) {f : α → ENNReal} {a : α} : ENNReal.funMulInvSnorm f p μ a ^ p = f a ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹

theorem ENNReal.lintegral_rpow_funMulInvSnorm_eq_one {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ℝ} (hp0_lt : 0 < p) {f : α → ENNReal} (hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0) (hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤) : ∫⁻ (c : α), ENNReal.funMulInvSnorm f p μ c ^ p ∂μ = 1

theorem ENNReal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ℝ} {q : ℝ} (hpq : Real.IsConjExponent p q) {f : α → ENNReal} {g : α → ENNReal} (hf : AEMeasurable 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} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ℝ} (hp0 : 0 ≤ p) {f : α → ENNReal} (hf : AEMeasurable f μ) (hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0) : f =ᶠ[MeasureTheory.Measure.ae μ] 0

theorem ENNReal.lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ℝ} (hp0 : 0 ≤ p) {f : α → ENNReal} {g : α → ENNReal} (hf : AEMeasurable 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} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ℝ} {q : ℝ} (hp0_lt : 0 < p) (hq0 : 0 ≤ q) {f : α → ENNReal} {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} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {p : ℝ} {q : ℝ} (hpq : Real.IsConjExponent p q) {f : α → ENNReal} {g : α → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable 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_mul_norm_pow_le {α : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ENNReal} {g : α → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) {p : ℝ} {q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) (hpq : p + q = 1) : ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q

A different formulation of Hölder's inequality for two functions, with two exponents that sum to 1, instead of reciprocals of

theorem ENNReal.lintegral_prod_norm_pow_le {α : Type u_2} {ι : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (s : Finset ι) {f : ι → α → ENNReal} (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : (Finset.sum s fun (i : ι) => p i) = 1) (h2p : ∀ i ∈ s, 0 ≤ p i) : ∫⁻ (a : α), Finset.prod s fun (i : ι) => f i a ^ p i ∂μ ≤ Finset.prod s fun (i : ι) => (∫⁻ (a : α), f i a ∂μ) ^ p i

A version of Hölder with multiple arguments

theorem ENNReal.lintegral_mul_prod_norm_pow_le {α : Type u_2} {ι : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (s : Finset ι) {g : α → ENNReal} {f : ι → α → ENNReal} (hg : AEMeasurable g μ) (hf : ∀ i ∈ s, AEMeasurable (f i) μ) (q : ℝ) {p : ι → ℝ} (hpq : (q + Finset.sum s fun (i : ι) => p i) = 1) (hq : 0 ≤ q) (hp : ∀ i ∈ s, 0 ≤ p i) : ∫⁻ (a : α), g a ^ q * Finset.prod s fun (i : ι) => f i a ^ p i ∂μ ≤ (∫⁻ (a : α), g a ∂μ) ^ q * Finset.prod s fun (i : ι) => (∫⁻ (a : α), f i a ∂μ) ^ p i

A version of Hölder with multiple arguments, one of which plays a distinguished role.

theorem ENNReal.lintegral_rpow_add_lt_top_of_lintegral_rpow_lt_top {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ℝ} {f : α → ENNReal} {g : α → ENNReal} (hf : AEMeasurable 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_2} [MeasurableSpace α] {p : ℝ} {q : ℝ} {r : ℝ} (hp0_lt : 0 < p) (hpq : p < q) (hpqr : 1 / p = 1 / q + 1 / r) (μ : MeasureTheory.Measure α) {f : α → ENNReal} {g : α → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable 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} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ℝ} {q : ℝ} (hpq : Real.IsConjExponent p q) {f : α → ENNReal} {g : α → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable 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} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ℝ} {q : ℝ} (hpq : Real.IsConjExponent p q) {f : α → ENNReal} {g : α → ENNReal} (hf : AEMeasurable f μ) (hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤) (hg : AEMeasurable 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} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ℝ} {f : α → ENNReal} {g : α → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable 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} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ℝ} {f : α → ENNReal} {g : α → ENNReal} (hf : AEMeasurable 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} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ℝ} {q : ℝ} (hpq : Real.IsConjExponent p q) {f : α → NNReal} {g : α → NNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable 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.