$\|K*f\|_{L^2}\le B\|f\|_{L^2}$ for $f\in L^1\cap L^2(\mathbb R^d)$ when $K\in L^2$ and $|\hat K|\le B$

Proved

DbarRegularity.eLpNorm_conv_le_of_integrable

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^1\cap L^2(\mathbb R^d)$

\Big\|\,x\mapsto\int_{\mathbb R^d}K(x-y)f(y)\,dy\,\Big\|_{L^2}\;\le\;B\,\|f\|_{L^2}.

This is the $L^2$ boundedness of convolution with $K$ on the dense subspace $L^1\cap L^2$ , with operator norm at most $\sup|\hat K|$ .

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; norms are eLpNorm in ℝ≥0∞.

Preamble

import Mathlib.Analysis.Fourier.LpSpace

Formal statement

namespace DbarRegularity

open MeasureTheory FourierTransform Filter Topology
open scoped ENNReal NNReal Convolution

/-- The `L²` bound for `f ∈ L¹ ∩ L²`. -/
theorem eLpNorm_conv_le_of_integrable {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) → ℂ) (hf1 : Integrable f volume) (hf2 : MemLp f 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​ for f∈L1∩L2(Rd)f\in L^1\cap L^2(\mathbb R^d)f∈L1∩L2(Rd) when K∈L2K\in L^2K∈L2 and ∣K^∣≤B|\hat K|\le B∣K^∣≤B

$\|K*f\|_{L^2}\le B\|f\|_{L^2}$ for $f\in L^1\cap L^2(\mathbb R^d)$ when $K\in L^2$ and $|\hat K|\le B$