# 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} [] {μ : } {p : } {q : } (hpq : p.IsConjExponent q) {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

Equations
• = f a * ((∫⁻ (c : α), f c ^ 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 : p.IsConjExponent q) {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) :
f =ᵐ[μ] 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 : p.IsConjExponent q) {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_mul_norm_pow_le {α : Type u_2} [] {μ : } {f : αENNReal} {g : αENNReal} (hf : ) (hg : ) {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} [] {μ : } (s : ) {f : ιαENNReal} (hf : is, AEMeasurable (f i) μ) {p : ι} (hp : is, p i = 1) (h2p : is, 0 p i) :
∫⁻ (a : α), is, f i a ^ p iμ is, (∫⁻ (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} [] {μ : } (s : ) {g : αENNReal} {f : ιαENNReal} (hg : ) (hf : is, AEMeasurable (f i) μ) (q : ) {p : ι} (hpq : q + is, p i = 1) (hq : 0 q) (hp : is, 0 p i) :
∫⁻ (a : α), g a ^ q * is, f i a ^ p iμ (∫⁻ (a : α), g aμ) ^ q * is, (∫⁻ (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} [] {μ : } {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 : p.IsConjExponent q) {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 : p.IsConjExponent q) {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 : p.IsConjExponent q) {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.