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

theorem ENNReal.lintegral_mul_le_one_of_lintegral_rpow_eq_one {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : } {q : } (hpq : p.IsConjExponent 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
Instances For
    theorem ENNReal.fun_eq_funMulInvSnorm_mul_eLpNorm {α : 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)
    @[deprecated ENNReal.fun_eq_funMulInvSnorm_mul_eLpNorm]
    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)

    Alias of ENNReal.fun_eq_funMulInvSnorm_mul_eLpNorm.

    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 : p.IsConjExponent 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 =ᵐ[μ] 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 : p.IsConjExponent 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 : 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} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (s : Finset ι) {g : αENNReal} {f : ιαENNReal} (hg : AEMeasurable g μ) (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} [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 : p.IsConjExponent 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_eLpNorm_mul_lintegral_rpow_add {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : } {q : } (hpq : p.IsConjExponent 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)
    @[deprecated ENNReal.lintegral_rpow_add_le_add_eLpNorm_mul_lintegral_rpow_add]
    theorem ENNReal.lintegral_rpow_add_le_add_snorm_mul_lintegral_rpow_add {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : } {q : } (hpq : p.IsConjExponent 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)

    Alias of ENNReal.lintegral_rpow_add_le_add_eLpNorm_mul_lintegral_rpow_add.

    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 : p.IsConjExponent 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.