Hölder's inequality with Young's exponents

For 1 ≤ p ≤ q and 1/p + 1/r = 1 + 1/q, and functions k g : β → ℝ≥0∞,

∫⁻ k g ≤ (∫⁻ k ^ r g ^ p) ^ (1/q) (∫⁻ k ^ r) ^ (1 - 1/p) (∫⁻ g ^ p) ^ (1/p - 1/q).

This is the pointwise step in the proof of Young's inequality for integral kernels, TauCeti.lintegral_rpow_lintegral_mul_le_of_inv_add_inv_eq: integrating it in the remaining variable and applying Tonelli's theorem gives the Lᵖ → L^q bound for the integral operator.

The statement is in ℝ≥0∞, so it needs no integrability hypotheses.

Main declarations

• TauCeti.lintegral_mul_le_of_inv_add_inv_eq: the three-exponent Hölder inequality.

References

• G. B. Folland, Real Analysis: Modern Techniques and Their Applications, 2nd ed., proof of Proposition 6.36.

theorem TauCeti.lintegral_mul_le_of_inv_add_inv_eq {β : Type u_1} [MeasurableSpace β] {ν : MeasureTheory.Measure β} {k g : β → ENNReal} (hk : AEMeasurable k ν) (hg : AEMeasurable g ν) {p q r : ℝ} (hp : 1 ≤ p) (hpq : p ≤ q) (hr : p⁻¹ + r⁻¹ = 1 + q⁻¹) : ∫⁻ (y : β), k y * g y ∂ν ≤ (∫⁻ (y : β), k y ^ r * g y ^ p ∂ν) ^ q⁻¹ * (∫⁻ (y : β), k y ^ r ∂ν) ^ (1 - p⁻¹) * (∫⁻ (y : β), g y ^ p ∂ν) ^ (p⁻¹ - q⁻¹)

Hölder's inequality for Young's exponents. Let 1 ≤ p ≤ q and let r be the exponent with 1/p + 1/r = 1 + 1/q. Then ∫⁻ k g ≤ (∫⁻ k ^ r g ^ p) ^ (1/q) (∫⁻ k ^ r) ^ (1 - 1/p) (∫⁻ g ^ p) ^ (1/p - 1/q).