Lᵖ membership at an intermediate exponent

A function lying in both L^{p₀} and L^{p₁} lies in Lᵖ for every 0 < p₀ ≤ p ≤ p₁, on an arbitrary measure space. Pointwise, ‖f‖ ^ p ≤ ‖f‖ ^ {p₀} + ‖f‖ ^ {p₁} when p₁ is finite, according as ‖f‖ ≤ 1 or not, and ‖f‖ ^ p ≤ ‖f‖_∞ ^ {p - p₀} ‖f‖ ^ {p₀} when p₁ = ∞.

This inclusion L^{p₀} ∩ L^{p₁} ⊆ Lᵖ for 0 < p₀ ≤ p ≤ p₁ is what lets an operator bounded into two Lᵖ spaces be compared with its values in the intermediate space, as in the Riesz–Thorin theorem.

Quantitatively, the Lᵖ norms are logarithmically convex in 1 / p: if 1 / p = (1 - θ) / p₀ + θ / p₁ with 0 ≤ θ ≤ 1, then

‖f‖_p ≤ ‖f‖_{p₀} ^ (1 - θ) ‖f‖_{p₁} ^ θ

(MeasureTheory.eLpNorm_le_eLpNorm_rpow_mul_eLpNorm_rpow), by Hölder's inequality applied to ‖f‖ = ‖f‖ ^ (1 - θ) ‖f‖ ^ θ. The same bound for elements of Lᵖ spaces representing one function is MeasureTheory.Lp.norm_le_norm_rpow_mul_norm_rpow_of_ae_eq. Since the exponent 1 - θ is positive for θ < 1, smallness in L^{p₀} and boundedness in L^{p₁} give smallness in Lᵖ; this is how compactness into L^{p₀} passes to the intermediate exponents.

References

• G. B. Folland, Real Analysis, 2nd ed., Proposition 6.10.

theorem MeasureTheory.MemLp.of_le_of_le {α : Type u_1} {ε : Type u_2} {mα : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} {p₀ p p₁ : ENNReal} (hf₀ : MemLp f p₀ μ) (hf₁ : MemLp f p₁ μ) (hp₀ : p₀ ≠ 0) (h₀ : p₀ ≤ p) (h₁ : p ≤ p₁) : MemLp f p μ

A function in L^{p₀} and in L^{p₁} is in Lᵖ for every p₀ ≤ p ≤ p₁, provided p₀ ≠ 0.

theorem MeasureTheory.eLpNorm_le_eLpNorm_rpow_mul_eLpNorm_rpow {α : Type u_1} {ε : Type u_2} {mα : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} {p₀ p₁ p : ENNReal} {θ : ℝ} (hθ : θ ∈ Set.Icc 0 1) (hp : p⁻¹ = ENNReal.ofReal (1 - θ) * p₀⁻¹ + ENNReal.ofReal θ * p₁⁻¹) : eLpNorm f p μ ≤ eLpNorm f p₀ μ ^ (1 - θ) * eLpNorm f p₁ μ ^ θ

Logarithmic convexity of the Lᵖ norms. If 0 ≤ θ ≤ 1 and 1 / p = (1 - θ) / p₀ + θ / p₁, then ‖f‖_p ≤ ‖f‖_{p₀} ^ (1 - θ) ‖f‖_{p₁} ^ θ.

theorem MeasureTheory.Lp.norm_le_norm_rpow_mul_norm_rpow_of_ae_eq {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {E : Type u_3} [NormedAddCommGroup E] {p₀ p₁ p : ENNReal} {θ : ℝ} (hθ : θ ∈ Set.Icc 0 1) (hp : p⁻¹ = ENNReal.ofReal (1 - θ) * p₀⁻¹ + ENNReal.ofReal θ * p₁⁻¹) {f : ↥(Lp E p μ)} {f₀ : ↥(Lp E p₀ μ)} {f₁ : ↥(Lp E p₁ μ)} (h₀ : ↑↑f =ᵐ[μ] ↑↑f₀) (h₁ : ↑↑f =ᵐ[μ] ↑↑f₁) : ‖f‖ ≤ ‖f₀‖ ^ (1 - θ) * ‖f₁‖ ^ θ

Logarithmic convexity of the Lᵖ norms, for elements f ∈ Lᵖ, f₀ ∈ L^{p₀} and f₁ ∈ L^{p₁} representing the same function: if 0 ≤ θ ≤ 1 and 1 / p = (1 - θ) / p₀ + θ / p₁, then ‖f‖ ≤ ‖f₀‖ ^ (1 - θ) ‖f₁‖ ^ θ.