L^p bounds for convolution with a kernel whose Fourier transform is bounded and whose gradient decays like |x|^{-d-1}

Proved

DbarRegularity.convolution_lp_bound

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

calderon-zygmundcauchy-riemannelliptic-regularityharmonic-analysissingular-integrals

Let $K\in L^2(\mathbb{R}^d)$ and $B\ge0$ . $\mathbb{R}^d$ carries Lebesgue measure $m$ , and $\|\cdot\|_p$ is the $L^p(\mathbb{R}^d)$ norm. Assume

the Fourier transform of $K$ is essentially bounded: $|\hat K(\xi)|\le B$ for almost every $\xi$ ;
$K$ is of class $C^1$ on $\mathbb{R}^d\setminus\{0\}$ and $|\nabla K(x)|\le B/|x|^{d+1}$ for $x\ne0$ .

For $f\in L^1\cap L^p$ let $Tf(x)=\int_{\mathbb{R}^d}K(x-y)f(y)\,dy$ . Then for every $1<p<\infty$ there is a constant $A_p$ , depending only on $p$ , $B$ and $d$ (in particular not on the $L^2$ norm of $K$ ), such that $Tf\in L^p$ and

\|Tf\|_p\le A_p\|f\|_p\qquad\text{for all }f\in L^1\cap L^p .

Formalization Note $\hat K$ is Mathlib's Fourier transform on $L^2$ , Lp.fourierTransformₗᵢ, applied to hK.toLp K; it is normalized as $\hat K(\xi)=\int K(x)e^{-2\pi i x\cdot\xi}dx$ , while Stein uses $e^{+2\pi i x\cdot\xi}$ ; the two differ by $\xi\mapsto-\xi$ , which does not change the bound $|\hat K|\le B$ . $|\nabla K(x)|$ is written as the operator norm ‖fderiv ℝ K x‖, which is at most the Euclidean norm of the gradient, so the hypothesis here is implied by Stein's with the same $B$ . $Tf(x)$ is the Bochner integral ∫ y, K (x - y) * f y. The constant A : ℝ≥0 is chosen before $K$ and $f$ .

Preamble

import Definitions.Def_DbarRegularity_Setting
import Mathlib.Analysis.Calculus.ContDiff.Basic
import Mathlib.Analysis.Fourier.LpSpace

Formal statement

namespace DbarRegularity

open MeasureTheory Metric Filter Topology
open scoped ENNReal NNReal ContDiff

/-- Stein, *Singular Integrals*, Chapter II, § 2.2, Theorem 1 (p. 29): let `K ∈ L²(ℝ^d)` with
essentially bounded Fourier transform, `|K̂| ≤ B`, and let `K` be of class `C¹` outside the origin
with `|∇K(x)| ≤ B / |x|^{d+1}`. For `f ∈ L¹ ∩ L^p`, `1 < p < ∞`, the convolution
`T f (x) = ∫ K(x - y) f(y) dy` satisfies `‖T f‖_p ≤ A_p ‖f‖_p`, where `A_p` depends only on `p`,
`B` and `d` (not on the `L²` norm of `K`). -/
theorem convolution_lp_bound (d : ℕ) (p : ℝ) (hp : 1 < p) (B : ℝ) :
    ∃ A : ℝ≥0, ∀ (K : EuclideanSpace ℝ (Fin d) → ℂ) (hK : MemLp K 2 volume),
      (∀ᵐ ξ, ‖Lp.fourierTransformₗᵢ (EuclideanSpace ℝ (Fin d)) ℂ (hK.toLp K) ξ‖ ≤ B) →
      ContDiffOn ℝ 1 K {0}ᶜ →
      (∀ x, x ≠ 0 → ‖fderiv ℝ K x‖ ≤ B / ‖x‖ ^ (d + 1)) →
      ∀ f : EuclideanSpace ℝ (Fin d) → ℂ, MemLp f 1 volume → MemLp f (ENNReal.ofReal p) volume →
        MemLp (fun x => ∫ y, K (x - y) * f y) (ENNReal.ofReal p) volume ∧
        eLpNorm (fun x => ∫ y, K (x - y) * f y) (ENNReal.ofReal p) volume
          ≤ A * eLpNorm f (ENNReal.ofReal p) volume := by sorry

end DbarRegularity

Source

E. M. Stein, Singular Integrals and Differentiability Properties of Functions, Princeton Mathematical Series 30, Princeton University Press (1970), ISBN 0-691-08079-8, Chapter II, § 2.2, Theorem 1, p. 29

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Read-back: `DbarRegularity.convolution_lp_bound`

Setting. $d\in\mathbb N$ , real $p>1$ (used as ENNReal.ofReal p $\in(1,\infty)$ ), real $B$ ; kernels and functions $\mathbb R^d\to\mathbb C$ , Lebesgue measure.

Hypotheses. $1<p$ ; $B\in\mathbb R$ arbitrary.

Definitions used. MemLp, eLpNorm; MemLp.toLp (the $L^2$ class of $K$ ); Lp.fourierTransformₗᵢ = Mathlib's $L^2$ Fourier transform (unitary extension of the Schwartz Fourier transform $\hat K(\xi)=\int K(x)e^{-2\pi i\langle x,\xi\rangle}dx$ ); ContDiffOn ℝ 1; fderiv ℝ (operator norm of the real derivative); Bochner integral for the convolution.

Conclusion. $\exists A\in[0,\infty)$ such that for every $K:\mathbb R^d\to\mathbb C$ with $K\in L^2$ and

$|\hat K(\xi)|\le B$ for a.e. $\xi$ ,
$K\in C^1(\mathbb R^d\setminus\{0\})$ ,
$\|DK(x)\|\le B/|x|^{d+1}$ for all $x\ne0$ ,

and every $f\in L^1\cap L^p$ , the function $Tf(x)=\int K(x-y)f(y)\,dy$ (Bochner) satisfies $Tf\in L^p$ and $\|Tf\|_p\le A\|f\|_p$ .

Quantifier order: $d,p,B$ $\to$ $A$ $\to$ $K$ $\to$ $f$ . So $A=A(d,p,B)$ , independent of $K$ (in particular of $\|K\|_2$ ) and $f$ .

Degenerate cases. $B<0$ : the a.e. bound $|\hat K|\le B$ is impossible (the space has positive measure), so the statement is vacuous for $B<0$ (harmless). $d=0$ : $\{0\}^c=\emptyset$ , so the $C^1$ and gradient hypotheses are vacuous; $Tf=K(0)f(0)$ , $|K(0)|=|\hat K|\le B$ , true with $A=\max(B,0)$ . $p=\infty$ and $p=1$ are excluded.

Remarks. For $K\in L^2$ , $f\in L^1$ , Minkowski gives $\int|K(x-y)||f(y)|dy<\infty$ for a.e. $x$ , so the Bochner integral equals the true convolution a.e. (the junk value $0$ only occurs on a null set, which does not affect eLpNorm). The gradient bound implies Hörmander's condition $\int_{|x|\ge2|y|}|K(x-y)-K(x)|dx\le c_dB$ , so this is Stein's Ch. II Thm 1 hypothesis up to a dimensional constant. The Fourier normalization is the $2\pi$ -in-the-exponent one (Stein's), unitary on $L^2$ .

Soundness checks.

Bochner junk: only on a null set (see above), no effect. ofReal p with $p>1$ is a genuine finite exponent $>1$ . Real division $B/\|x\|^{d+1}$ with $x\ne0$ is genuine. ContDiffOn ℝ 1 is $C^1$ (not the analytic ω). $A$ is ℝ≥0. Hypotheses satisfiable for $B\ge0$ (e.g. $K=0$ ; or smooth truncations of Riesz-type kernels); conclusion non-trivial.
$A$ before $K$ and $f$ , depending only on $d,p,B$ : matches the standard statement and is true (Calderón–Zygmund $L^p$ bound with constants depending on $B$ , $p$ , $d$ ). Plausibly TRUE as written.

Verdict: no mis-formalization observed

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Mazecto · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

L^p bounds for convolution with a kernel whose Fourier transform is bounded and whose gradient decays like |x|^{-d-1}

Read-back: DbarRegularity.convolution_lp_bound

Read-back: `DbarRegularity.convolution_lp_bound`