$\|K*f\|_{L^2}\le B\|f\|_{L^2}$ on $L^2(\mathbb R^d)$ when $K\in L^2$ has $|\hat K|\le B$

Proved

DbarRegularity.convolution_l2_bound

by Mazecto · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

convolutionfourier-analysisharmonic-analysislp-spaces

Let $d\ge0$ , $B\in\mathbb R$ , and let $K\in L^2(\mathbb R^d)$ be complex valued whose $L^2$ Fourier transform satisfies $|\hat K(\xi)|\le B$ for almost every $\xi$ . Then for every $f\in L^2(\mathbb R^d)$ the convolution $Tf(x)=\int K(x-y)f(y)\,dy$ belongs to $L^2(\mathbb R^d)$ and

\|Tf\|_{L^2}\;\le\;B\,\|f\|_{L^2}.

This is the $L^2$ theory of convolution operators with bounded Fourier multiplier, for the convolution defined pointwise, which is finite at every point since $K,f\in L^2$ .

Formalization Note. $\mathbb R^d$ is EuclideanSpace ℝ (Fin d) with Lebesgue measure volume. $\hat K$ is Lp.fourierTransformₗᵢ applied to hK.toLp K, and $B$ enters as ENNReal.ofReal B. The convolution is the Bochner integral ∫ y, K (x - y) * f y; norms are eLpNorm · 2 volume.

Preamble

import Mathlib.Analysis.Fourier.LpSpace

Formal statement

namespace DbarRegularity

open MeasureTheory FourierTransform Filter Topology
open scoped ENNReal NNReal Convolution

/-- **`L²` bound.** If `K ∈ L²(ℝ^d)` has `L²` Fourier transform bounded by `B`, then
`f ↦ ∫ K(· - y) f(y) dy` maps `L²` to `L²` with norm at most `B`. -/
theorem convolution_l2_bound {d : ℕ} (K : EuclideanSpace ℝ (Fin d) → ℂ) (hK : MemLp K 2 volume) (B : ℝ)
    (hB : ∀ᵐ ξ, ‖Lp.fourierTransformₗᵢ (EuclideanSpace ℝ (Fin d)) ℂ (hK.toLp K) ξ‖ ≤ B)
    (f : EuclideanSpace ℝ (Fin d) → ℂ) (hf : MemLp f 2 volume) :
    MemLp (fun x => ∫ y, K (x - y) * f y) 2 volume ∧
      eLpNorm (fun x => ∫ y, K (x - y) * f y) 2 volume ≤ ENNReal.ofReal B * eLpNorm f 2 volume := by sorry

end DbarRegularity

Source

E. M. Stein, Singular Integrals and Differentiability Properties of Functions, Princeton University Press (1970), Chapter II, § 2.2, p. 29

View graph

∥K∗f∥L2≤B∥f∥L2\|K*f\|_{L^2}\le B\|f\|_{L^2}∥K∗f∥L2​≤B∥f∥L2​ on L2(Rd)L^2(\mathbb R^d)L2(Rd) when K∈L2K\in L^2K∈L2 has ∣K^∣≤B|\hat K|\le B∣K^∣≤B

$\|K*f\|_{L^2}\le B\|f\|_{L^2}$ on $L^2(\mathbb R^d)$ when $K\in L^2$ has $|\hat K|\le B$