Interpolation of Lᵖ seminorms

For an exponent q between r and s, with 1/q = θ/r + (1-θ)/s and θ ∈ (0,1), the L^q seminorm is bounded by the geometric mean

‖f‖_q ≤ ‖f‖_r^θ ‖f‖_s^{1-θ}.

The proof is Hölder's inequality applied to the splitting |f|^q = |f|^{qθ} · |f|^{q(1-θ)} at the conjugate pair r/(qθ) and s/(q(1-θ)), whose reciprocals sum to q(θ/r + (1-θ)/s) = 1.

Mathlib's Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean supplies Hölder's inequality and the bounds that compare two exponents on a finite measure, and stops short of this one.

The consumer is compactness of the Sobolev embedding below the critical exponent: a sequence converging in L² and bounded in L^{2⋆} converges at every exponent between them, which is the step Guo's proof of Rellich-Kondrachov takes between L¹ and L^{p⋆}.

Main declarations

• EllipticPdes.Analysis.eLpNorm_le_rpow_mul_rpow: the interpolation inequality.
• EllipticPdes.Analysis.eLpNorm_le_of_le_of_le: the form the compactness argument uses, bounding the L^q seminorm by a bound at each end.

References

James Guo, Partial Differential Equations, proof of Theorem IV.2.10; H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Remark 2 after Theorem 4.16.

theorem EllipticPdes.Analysis.eLpNorm_le_rpow_mul_rpow {α : Type u_1} {E : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} {r s q : ENNReal} (hr : r ≠ 0) (hr' : r ≠ ⊤) (hs : s ≠ 0) (hs' : s ≠ ⊤) (hq : q ≠ 0) (hq' : q ≠ ⊤) {θ : ℝ} (hθ0 : 0 < θ) (hθ1 : θ < 1) (hqrs : q.toReal⁻¹ = θ * r.toReal⁻¹ + (1 - θ) * s.toReal⁻¹) (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.eLpNorm f q μ ≤ MeasureTheory.eLpNorm f r μ ^ θ * MeasureTheory.eLpNorm f s μ ^ (1 - θ)

Interpolation of Lᵖ seminorms. With 1/q = θ/r + (1-θ)/s and θ ∈ (0,1), the L^q seminorm is bounded by the geometric mean of the seminorms at r and at s.

theorem EllipticPdes.Analysis.eLpNorm_le_of_le_of_le {α : Type u_1} {E : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] {f : α → E} {r s q : ENNReal} (hr : r ≠ 0) (hr' : r ≠ ⊤) (hs : s ≠ 0) (hs' : s ≠ ⊤) (hq : q ≠ 0) (hq' : q ≠ ⊤) {θ : ℝ} (hθ0 : 0 < θ) (hθ1 : θ < 1) (hqrs : q.toReal⁻¹ = θ * r.toReal⁻¹ + (1 - θ) * s.toReal⁻¹) (hf : MeasureTheory.AEStronglyMeasurable f μ) {A B : ENNReal} (hA : MeasureTheory.eLpNorm f r μ ≤ A) (hB : MeasureTheory.eLpNorm f s μ ≤ B) : MeasureTheory.eLpNorm f q μ ≤ A ^ θ * B ^ (1 - θ)

The form the compactness argument uses: a bound at each end bounds the middle.