Young's inequality for convolution

This file proves three forms of Young's inequality for convolution.

L¹ ⋆ L² ⊆ L² for the Lebesgue-integral convolution

Let μ be a left-invariant measure on a measurable additive group and let (f ⋆ₗ[μ] g) x = ∫⁻ y, f y * g (-y + x) ∂μ be the convolution of extended nonnegative functions (MeasureTheory.lconvolution). Young's inequality in the case L¹ ⋆ L² ⊆ L² reads

∫⁻ (f ⋆ₗ[μ] g) ^ 2 ≤ (∫⁻ f) ^ 2 * ∫⁻ g ^ 2

(MeasureTheory.lintegral_lconvolution_sq_le). It follows from the pointwise Cauchy–Schwarz inequality for the measure with density f,

(f ⋆ₗ[μ] g) x ^ 2 ≤ (∫⁻ f) * ∫⁻ y, f y * g (-y + x) ^ 2

(MeasureTheory.lconvolution_sq_le), by integrating in x, exchanging the integrals and using the left invariance of μ. Being stated for extended nonnegative functions, neither inequality needs any integrability hypothesis.

L¹ ⋆ Lᵖ ⊆ Lᵖ for the Bochner convolution

Let μ be a σ-finite right-invariant measure on a measurable additive group G, and let L : E →L[𝕜] E' →L[𝕜] F be a continuous bilinear map. For 1 ≤ p ≤ ∞, an integrable f and g ∈ Lᵖ(μ), the convolution (f ⋆[L] g)(x) = ∫ L (f t) (g (x - t)) dμ(t) satisfies

‖f ⋆[L] g‖_p ≤ ‖L‖ ‖f‖₁ ‖g‖_p.

The statement is in ℝ≥0∞ (MeasureTheory.eLpNorm_convolution_le), so it needs no integrability hypotheses: it is informative exactly when the right side is finite. For p < ∞ it is Minkowski's integral inequality (TauCeti.lintegral_Lp_lintegral_le) applied to the pointwise bound ‖(f ⋆[L] g)(x)‖ ≤ ∫ ‖L‖ ‖f t‖ ‖g (x - t)‖ dμ(t), together with the translation invariance ‖g (· - t)‖_p = ‖g‖_p. For p = ∞, ‖g (x - t)‖ ≤ ‖g‖_∞ for almost every t.

The kernel f and the bilinear map L are arbitrary, so the inequality applies to complex kernels acting on vector-valued functions through ContinuousLinearMap.lsmul, as for the kernel 𝓕⁻ σ of a Fourier multiplier with Schwartz symbol σ.

Lᵖ ⋆ Lʳ ⊆ Lᵠ on commutative groups

On a commutative group whose measure is also invariant under negation, the general form of Young's convolution inequality holds: for 1 ≤ p, r ≤ ∞ and 1/p + 1/r = 1 + 1/q,

‖f ⋆ₗ[μ] g‖_q ≤ ‖f‖_p ‖g‖_r

(MeasureTheory.eLpNorm_lconvolution_le). For q < ∞ this is Young's inequality for the integral operator with kernel (x, y) ↦ g (x - y), whose rows and columns all have the same Lʳ norm as g (TauCeti.lintegral_rpow_lintegral_mul_le_of_inv_add_inv_eq); for q = ∞ it is Hölder's inequality at each point.

The norm of a convolution of Bochner-integrable functions is bounded pointwise by the convolution of their norms, so this inequality also bounds the Lᵠ norm of f ⋆[L] g (MeasureTheory.eLpNorm_convolution_le_of_inv_add_inv_eq).

Main declarations

• MeasureTheory.lconvolution_sq_le: pointwise Cauchy–Schwarz for f ⋆ₗ[μ] g.
• MeasureTheory.lintegral_lconvolution_sq_le: Young's inequality L¹ ⋆ L² ⊆ L².
• MeasureTheory.enorm_convolution_le_lintegral: the pointwise bound for f ⋆[L, μ] g.
• MeasureTheory.eLpNorm_convolution_le: Young's inequality ‖f ⋆[L] g‖_p ≤ ‖L‖ ‖f‖₁ ‖g‖_p.
• MeasureTheory.eLpNorm_lconvolution_le: Young's inequality Lᵖ ⋆ Lʳ ⊆ Lᵠ.
• MeasureTheory.eLpNorm_convolution_le_of_inv_add_inv_eq: the same bound for the convolution f ⋆[L, μ] g of vector-valued functions along a continuous bilinear map L.

References

• E. H. Lieb and M. Loss, Analysis, 2nd ed., Graduate Studies in Mathematics 14, AMS, 2001, Theorem 4.2.
• G. B. Folland, Real Analysis: Modern Techniques and Their Applications, 2nd ed., Propositions 8.7 and 8.9.

theorem MeasureTheory.lconvolution_sq_le {G : Type u_1} {mG : MeasurableSpace G} [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] {μ : Measure G} [SFinite μ] [μ.IsAddLeftInvariant] {f g : G → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) (x : G) : lconvolution f g μ x ^ 2 ≤ (∫⁻ (y : G), f y ∂μ) * ∫⁻ (y : G), f y * g (-y + x) ^ 2 ∂μ

Pointwise Cauchy–Schwarz for a convolution. Cauchy–Schwarz for the measure with density f gives (f ⋆ₗ[μ] g) x ^ 2 ≤ (∫⁻ f) * ∫⁻ y, f y * g (-y + x) ^ 2.

theorem MeasureTheory.lintegral_lconvolution_sq_le {G : Type u_1} {mG : MeasurableSpace G} [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] {μ : Measure G} [SFinite μ] [μ.IsAddLeftInvariant] {f g : G → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : ∫⁻ (x : G), lconvolution f g μ x ^ 2 ∂μ ≤ (∫⁻ (y : G), f y ∂μ) ^ 2 * ∫⁻ (x : G), g x ^ 2 ∂μ

Young's inequality L¹ ⋆ L² ⊆ L². For extended nonnegative functions on a group with a left-invariant measure, ∫⁻ (f ⋆ₗ[μ] g) ^ 2 ≤ (∫⁻ f) ^ 2 * ∫⁻ g ^ 2.

theorem MeasureTheory.enorm_convolution_le_lintegral {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] (L : E →L[𝕜] E' →L[𝕜] F) {f : G → E} {g : G → E'} [Sub G] [MeasurableSpace G] (μ : Measure G) (x : G) : ‖convolution f g L μ x‖ₑ ≤ ∫⁻ (t : G), ‖L‖ₑ * ‖f t‖ₑ * ‖g (x - t)‖ₑ ∂μ

The pointwise bound behind Young's inequality: ‖(f ⋆[L] g)(x)‖ ≤ ∫ ‖L‖ ‖f t‖ ‖g (x - t)‖ dμ(t), in extended nonnegative form.

theorem MeasureTheory.eLpNorm_convolution_le {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] (L : E →L[𝕜] E' →L[𝕜] F) {f : G → E} {g : G → E'} [AddGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] {μ : Measure G} [SigmaFinite μ] [μ.IsAddRightInvariant] (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) {p : ENNReal} (hp : 1 ≤ p) : eLpNorm (convolution f g L μ) p μ ≤ ‖L‖ₑ * eLpNorm f 1 μ * eLpNorm g p μ

Young's inequality for convolution with an integrable function: for 1 ≤ p ≤ ∞, ‖f ⋆[L] g‖_p ≤ ‖L‖ ‖f‖₁ ‖g‖_p.

theorem MeasureTheory.eLpNorm_lconvolution_le {G : Type u_1} {mG : MeasurableSpace G} [AddCommGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] {μ : Measure G} [SFinite μ] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] {f g : G → ENNReal} {p q r : ENNReal} (hp : 1 ≤ p) (hr : 1 ≤ r) (hpqr : p⁻¹ + r⁻¹ = 1 + q⁻¹) (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : eLpNorm (lconvolution f g μ) q μ ≤ eLpNorm f p μ * eLpNorm g r μ

Young's convolution inequality. On a commutative group whose measure is invariant under translation and negation, for 1 ≤ p, r ≤ ∞ and 1/p + 1/r = 1 + 1/q, the convolution of extended nonnegative functions satisfies ‖f ⋆ₗ[μ] g‖_q ≤ ‖f‖_p ‖g‖_r.

theorem MeasureTheory.eLpNorm_convolution_le_of_inv_add_inv_eq {G : Type u_1} {mG : MeasurableSpace G} [AddCommGroup G] [MeasurableAdd₂ G] [MeasurableNeg G] {μ : Measure G} [SFinite μ] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] {𝕜 : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) {f : G → E} {g : G → E'} {p q r : ENNReal} (hp : 1 ≤ p) (hr : 1 ≤ r) (hpqr : p⁻¹ + r⁻¹ = 1 + q⁻¹) (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) : eLpNorm (convolution f g L μ) q μ ≤ ‖L‖ₑ * eLpNorm f p μ * eLpNorm g r μ

Young's convolution inequality for the convolution f ⋆[L, μ] g along a continuous bilinear map L: for 1 ≤ p, r ≤ ∞ and 1/p + 1/r = 1 + 1/q, ‖f ⋆[L, μ] g‖_q ≤ ‖L‖ ‖f‖_p ‖g‖_r. Where the integral defining the convolution does not converge, its value is 0, so no integrability hypothesis is needed.