Young's inequality and weighted ℓ² estimates for discrete convolution

This file proves the basic ℓᵖ estimates for Mathlib's discrete convolution DiscreteConvolution.addConvolution, and the resulting bilinear convolution estimate for weighted ℓ² spaces: for s > 1 / 2, convolution through a continuous bilinear map L : E →L E' →L F sends a pair of sequences a : ℤ → E, b : ℤ → E' with ∑ₙ ((1 + |n|) ^ s ‖a n‖)² < ∞ and ∑ₙ ((1 + |n|) ^ s ‖b n‖)² < ∞ to a sequence ℤ → F with the same property, with an explicit bound. Through Fourier coefficients these are the Sobolev spaces H^s of the circle, and convolution of coefficients is multiplication of functions, so taking E = E' = F and L the multiplication gives the coefficient form of the statement that H^s of the circle is an algebra for s > 1 / 2.

All estimates are first proved for unconditional sums in ℝ≥0∞, where they need no summability hypotheses, and then transferred to real sums.

Main statements

• DiscreteConvolution.addConvolutionExists_of_memℓp: on a right-cancellative additive monoid, the convolution of a bounded family with a summable one exists.
• DiscreteConvolution.enorm_addConvolution_le: on an additive monoid, ‖(f ⋆ g) x‖ₑ ≤ ‖L‖ₑ (‖f‖ₑ ⋆ ‖g‖ₑ) x.
• DiscreteConvolution.tsum_addRingConvolution_sq_le and DiscreteConvolution.tsum_addRingConvolution_sq_le': Young's inequality ‖f ⋆ g‖₂ ≤ ‖g‖₁ ‖f‖₂ and ‖f ⋆ g‖₂ ≤ ‖f‖₁ ‖g‖₂ for ℝ≥0∞-valued families, in squared form.
• DiscreteConvolution.tsum_sq_mul_addRingConvolution_le: the weighted (tame) estimate ‖ω (f ⋆ g)‖₂² ≤ 2 c² (‖g‖₁² ‖ω f‖₂² + ‖f‖₁² ‖ω g‖₂²) for a weight with ω (x + y) ≤ c (ω x + ω y).
• DiscreteConvolution.tsum_sq_one_add_norm_rpow_mul_enorm_addConvolution_le: the weighted ℓ² bilinear convolution estimate with weights (1 + ‖x‖) ^ s, in ℝ≥0∞.
• DiscreteConvolution.tsum_sq_one_add_abs_rpow_mul_norm_addConvolution_le and addConvolutionExists_and_summable_sq_one_add_abs_rpow_mul_norm_addConvolution: for s > 1 / 2 and a complete target, convolution maps the weighted ℓ² spaces of E and E' on ℤ into that of F: the convolution a ⋆ b exists, and ‖(1 + |n|) ^ s (a ⋆ b)‖₂² ≤ 4 ^ (s + 1) ‖L‖² (∑ₙ (1 + |n|) ^ (-2 s)) ‖(1 + |n|) ^ s a‖₂² ‖(1 + |n|) ^ s b‖₂².

References

• M. E. Taylor, Partial Differential Equations III, Chapter 13, Section 3 (Sobolev spaces as algebras, and the tame product estimate).
• G. B. Folland, Real Analysis: Modern Techniques and Their Applications, 2nd ed., Proposition 8.9 (Young's inequality).

theorem DiscreteConvolution.addConvolutionExists_of_memℓp {𝕜 : Type u_1} {M : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [AddRightCancelMonoid M] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (L : E →L[𝕜] E' →L[𝕜] F) {f : M → E} {g : M → E'} (hf : Memℓp f ⊤) (hg : Memℓp g 1) : AddConvolutionExists (ContinuousLinearMap.toLinearMap₁₂ L) f g

On a right-cancellative additive monoid, the convolution of a bounded family with a summable family exists.

theorem DiscreteConvolution.tsum_addRingConvolution_sq_le {G : Type u_1} [AddGroup G] (f g : G → ENNReal) : ∑' (x : G), addRingConvolution f g x ^ 2 ≤ (∑' (x : G), g x) ^ 2 * ∑' (x : G), f x ^ 2

Young's inequality ‖f ⋆ g‖₂ ≤ ‖g‖₁ ‖f‖₂ for families in ℝ≥0∞ on an additive group, in squared form. No summability hypotheses are needed.

theorem DiscreteConvolution.tsum_addRingConvolution_sq_le' {G : Type u_1} [AddGroup G] (f g : G → ENNReal) : ∑' (x : G), addRingConvolution f g x ^ 2 ≤ (∑' (x : G), f x) ^ 2 * ∑' (x : G), g x ^ 2

Young's inequality in the other orientation, ‖f ⋆ g‖₂ ≤ ‖f‖₁ ‖g‖₂, for families in ℝ≥0∞ on an additive group, in squared form. On a noncommutative group it does not follow from tsum_addRingConvolution_sq_le by commutativity; it is that inequality on the opposite group.

theorem DiscreteConvolution.tsum_sq_mul_addRingConvolution_le {G : Type u_1} [AddGroup G] {ω : G → ENNReal} {c : ENNReal} (hω : ∀ (x y : G), ω (x + y) ≤ c * (ω x + ω y)) (f g : G → ENNReal) : ∑' (x : G), (ω x * addRingConvolution f g x) ^ 2 ≤ 2 * c ^ 2 * ((∑' (x : G), g x) ^ 2 * ∑' (x : G), (ω x * f x) ^ 2 + (∑' (x : G), f x) ^ 2 * ∑' (x : G), (ω x * g x) ^ 2)

The weighted (tame) convolution estimate. If the weight ω satisfies ω (x + y) ≤ c (ω x + ω y), then ‖ω (f ⋆ g)‖₂² ≤ 2 c² (‖g‖₁² ‖ω f‖₂² + ‖f‖₁² ‖ω g‖₂²).

theorem DiscreteConvolution.enorm_addConvolution_le {𝕜 : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) {M : Type u_5} [AddMonoid M] (f : M → E) (g : M → E') (x : M) : ‖addConvolution (ContinuousLinearMap.toLinearMap₁₂ L) f g x‖ₑ ≤ ‖L‖ₑ * addRingConvolution (fun (x : M) => ‖f x‖ₑ) (fun (x : M) => ‖g x‖ₑ) x

On an additive monoid, the norm of a convolution is bounded by ‖L‖ₑ times the convolution of the norms.

theorem DiscreteConvolution.tsum_sq_one_add_norm_rpow_mul_enorm_addConvolution_le {𝕜 : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_5} [SeminormedAddGroup G] (L : E →L[𝕜] E' →L[𝕜] F) {s : ℝ} (hs : 0 ≤ s) (a : G → E) (b : G → E') : ∑' (x : G), (ENNReal.ofReal ((1 + ‖x‖) ^ s) * ‖addConvolution (ContinuousLinearMap.toLinearMap₁₂ L) a b x‖ₑ) ^ 2 ≤ ((ENNReal.ofReal (4 ^ (s + 1)) * ‖L‖ₑ ^ 2 * ∑' (x : G), ENNReal.ofReal ((1 + ‖x‖) ^ (-2 * s))) * ∑' (x : G), (ENNReal.ofReal ((1 + ‖x‖) ^ s) * ‖a x‖ₑ) ^ 2) * ∑' (x : G), (ENNReal.ofReal ((1 + ‖x‖) ^ s) * ‖b x‖ₑ) ^ 2

The weighted ℓ² convolution estimate. For s ≥ 0, convolution through a continuous bilinear map L satisfies, with the weights (1 + ‖x‖) ^ s, ‖(1 + ‖x‖) ^ s (a ⋆ b)‖₂² ≤ 4 ^ (s + 1) ‖L‖² (∑' x, (1 + ‖x‖) ^ (-2 s)) ‖(1 + ‖x‖) ^ s a‖₂² ‖(1 + ‖x‖) ^ s b‖₂². The sums are unconditional sums in ℝ≥0∞. On ℤ, the inverse-weight sum ∑' x, (1 + ‖x‖) ^ (-2 s) is finite when s > 1 / 2 (TauCeti.summable_one_add_abs_int_rpow), so the bound is finite whenever the weighted square sums of a and b are also finite.

theorem DiscreteConvolution.summable_sq_one_add_abs_rpow_mul_norm_addConvolution {𝕜 : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) {s : ℝ} (hs : 1 / 2 < s) {a : ℤ → E} {b : ℤ → E'} (ha : Summable fun (n : ℤ) => ((1 + |↑n|) ^ s * ‖a n‖) ^ 2) (hb : Summable fun (n : ℤ) => ((1 + |↑n|) ^ s * ‖b n‖) ^ 2) : Summable fun (n : ℤ) => ((1 + |↑n|) ^ s * ‖addConvolution (ContinuousLinearMap.toLinearMap₁₂ L) a b n‖) ^ 2

The total convolution of two weighted square-summable sequences on ℤ is weighted square-summable for s > 1 / 2, without requiring completeness of its target.

theorem DiscreteConvolution.addConvolutionExists_and_summable_sq_one_add_abs_rpow_mul_norm_addConvolution {𝕜 : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (L : E →L[𝕜] E' →L[𝕜] F) {s : ℝ} (hs : 1 / 2 < s) {a : ℤ → E} {b : ℤ → E'} (ha : Summable fun (n : ℤ) => ((1 + |↑n|) ^ s * ‖a n‖) ^ 2) (hb : Summable fun (n : ℤ) => ((1 + |↑n|) ^ s * ‖b n‖) ^ 2) : AddConvolutionExists (ContinuousLinearMap.toLinearMap₁₂ L) a b ∧ Summable fun (n : ℤ) => ((1 + |↑n|) ^ s * ‖addConvolution (ContinuousLinearMap.toLinearMap₁₂ L) a b n‖) ^ 2

Convolution of weighted ℓ² sequences on ℤ is weighted ℓ². For s > 1 / 2 and a complete target, if (1 + |n|) ^ s ‖a n‖ and (1 + |n|) ^ s ‖b n‖ are square-summable, then the convolution a ⋆ b exists, so it is the pointwise convolution sum, and (1 + |n|) ^ s ‖(a ⋆ b) n‖ is square-summable.

theorem DiscreteConvolution.tsum_sq_one_add_abs_rpow_mul_norm_addConvolution_le {𝕜 : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) {s : ℝ} (hs : 1 / 2 < s) {a : ℤ → E} {b : ℤ → E'} (ha : Summable fun (n : ℤ) => ((1 + |↑n|) ^ s * ‖a n‖) ^ 2) (hb : Summable fun (n : ℤ) => ((1 + |↑n|) ^ s * ‖b n‖) ^ 2) : ∑' (n : ℤ), ((1 + |↑n|) ^ s * ‖addConvolution (ContinuousLinearMap.toLinearMap₁₂ L) a b n‖) ^ 2 ≤ ((4 ^ (s + 1) * ‖L‖ ^ 2 * ∑' (n : ℤ), (1 + |↑n|) ^ (-2 * s)) * ∑' (n : ℤ), ((1 + |↑n|) ^ s * ‖a n‖) ^ 2) * ∑' (n : ℤ), ((1 + |↑n|) ^ s * ‖b n‖) ^ 2

The weighted ℓ² convolution estimate on ℤ. For s > 1 / 2, ∑ₙ ((1 + |n|) ^ s ‖(a ⋆ b) n‖)² ≤ 4 ^ (s + 1) ‖L‖² (∑ₙ (1 + |n|) ^ (-2 s)) (∑ₙ ((1 + |n|) ^ s ‖a n‖)²) (∑ₙ ((1 + |n|) ^ s ‖b n‖)²).