# Documentation

Mathlib.MeasureTheory.Integral.MeanInequalities

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

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} [] {μ : } {p : } {q : } (hpq : ) {f : αENNReal} {g : αENNReal} (hf : ) (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} [] (f : αENNReal) (p : ) (μ : ) :
αENNReal

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

Instances For
theorem ENNReal.fun_eq_funMulInvSnorm_mul_snorm {α : Type u_1} [] {μ : } {p : } (f : αENNReal) (hf_nonzero : ∫⁻ (a : α), f a ^ pμ 0) (hf_top : ∫⁻ (a : α), f a ^ pμ ) {a : α} :
f a = * (∫⁻ (c : α), f c ^ pμ) ^ (1 / p)
theorem ENNReal.funMulInvSnorm_rpow {α : Type u_1} [] {μ : } {p : } (hp0 : 0 < p) {f : αENNReal} {a : α} :
^ p = f a ^ p * (∫⁻ (c : α), f c ^ pμ)⁻¹
theorem ENNReal.lintegral_rpow_funMulInvSnorm_eq_one {α : Type u_1} [] {μ : } {p : } (hp0_lt : 0 < p) {f : αENNReal} (hf_nonzero : ∫⁻ (a : α), f a ^ pμ 0) (hf_top : ∫⁻ (a : α), f a ^ pμ ) :
∫⁻ (c : α), ^ pμ = 1
theorem ENNReal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top {α : Type u_1} [] {μ : } {p : } {q : } (hpq : ) {f : αENNReal} {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} [] {μ : } {p : } (hp0 : 0 p) {f : αENNReal} (hf : ) (hf_zero : ∫⁻ (a : α), f a ^ pμ = 0) :
theorem ENNReal.lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero {α : Type u_1} [] {μ : } {p : } (hp0 : 0 p) {f : αENNReal} {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} [] {μ : } {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} [] (μ : ) {p : } {q : } (hpq : ) {f : αENNReal} {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} [] {μ : } {p : } {f : αENNReal} {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_2} [] {p : } {q : } {r : } (hp0_lt : 0 < p) (hpq : p < q) (hpqr : 1 / p = 1 / q + 1 / r) (μ : ) {f : αENNReal} {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} [] {μ : } {p : } {q : } (hpq : ) {f : αENNReal} {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} [] {μ : } {p : } {q : } (hpq : ) {f : αENNReal} {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} [] {μ : } {p : } {f : αENNReal} {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} [] {μ : } {p : } {f : αENNReal} {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} [] {μ : } {p : } {q : } (hpq : ) {f : αNNReal} {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.