Uniform L^p bounds and L^p convergence of truncated singular integrals

Proved

DbarRegularity.truncatedSingularIntegral_lp

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

calderon-zygmundcauchy-riemannelliptic-regularityharmonic-analysissingular-integrals

Let $K$ be a measurable function on $\mathbb{R}^d$ and $B\ge0$ such that

|K(x)|\le B|x|^{-d}\ (x\ne0),\qquad \int_{|x|\ge2|y|}|K(x-y)-K(x)|\,dx\le B\ (y\ne0),\qquad \int_{R_1<|x|<R_2}K(x)\,dx=0\ (0<R_1<R_2<\infty).

$\mathbb{R}^d$ carries Lebesgue measure $m$ , and $\|\cdot\|_p$ is the $L^p(\mathbb{R}^d)$ norm. Let $1<p<\infty$ and for $f\in L^p(\mathbb{R}^d)$ and $\varepsilon>0$ put

T_\varepsilon f(x)=\int_{|y|\ge\varepsilon}f(x-y)K(y)\,dy .

Then there is a constant $A_p$ , independent of $f$ and $\varepsilon$ , such that $\|T_\varepsilon f\|_p\le A_p\|f\|_p$ for all $f\in L^p$ and $\varepsilon>0$ . Moreover, for each $f\in L^p$ the limit $Tf=\lim_{\varepsilon\to0}T_\varepsilon f$ exists in the $L^p$ norm, and $\|Tf\|_p\le A_p\|f\|_p$ .

Formalization Note $T_\varepsilon f$ is the Bochner integral ∫ y in {y | ε ≤ ‖y‖}, …; for $f\in L^p$ it converges absolutely at every $x$ . The limit $\varepsilon\to0$ is taken along 𝓝[>] 0, and the limit operator is the function g. ENNReal.ofReal p is the exponent, so $p<\infty$ . The second condition on $K$ is a lower Lebesgue integral ∫⁻, so it also asserts integrability. Measurability of $K$ is assumed as AEStronglyMeasurable K volume. The constant A : ℝ≥0 depends on $K$ and $p$ (Stein: independent of $f$ and $\varepsilon$ ).

Preamble

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

Formal statement

namespace DbarRegularity

open MeasureTheory Metric Filter Topology
open scoped ENNReal NNReal ContDiff

/-- Stein, *Singular Integrals*, Chapter II, § 3.2, Theorem 2 (p. 35): let `K` on `ℝ^d` satisfy
`|K(x)| ≤ B |x|^{-d}` for `x ≠ 0`, `∫_{|x| ≥ 2|y|} |K(x - y) - K(x)| dx ≤ B` for `y ≠ 0`
(conditions (18)), and `∫_{R₁ < |x| < R₂} K(x) dx = 0` for `0 < R₁ < R₂` (condition (19)). For
`1 < p < ∞` and `f ∈ L^p` let `T_ε f (x) = ∫_{|y| ≥ ε} f(x - y) K(y) dy`. Then
`‖T_ε f‖_p ≤ A_p ‖f‖_p` with `A_p` independent of `f` and `ε` (inequality (21)), and for each
`f ∈ L^p` the limit `T f = lim_{ε → 0} T_ε f` exists in `L^p` and also satisfies (21). -/
theorem truncatedSingularIntegral_lp {d : ℕ} (K : EuclideanSpace ℝ (Fin d) → ℂ) (B : ℝ)
    (hKm : AEStronglyMeasurable K volume)
    (hK1 : ∀ x, x ≠ 0 → ‖K x‖ ≤ B / ‖x‖ ^ d)
    (hK2 : ∀ y, y ≠ 0 → ∫⁻ x in {x | 2 * ‖y‖ ≤ ‖x‖}, ‖K (x - y) - K x‖ₑ ≤ ENNReal.ofReal B)
    (hK3 : ∀ R₁ R₂ : ℝ, 0 < R₁ → R₁ < R₂ → ∫ x in {x | R₁ < ‖x‖ ∧ ‖x‖ < R₂}, K x = 0)
    (p : ℝ) (hp : 1 < p) :
    ∃ A : ℝ≥0,
      (∀ ε : ℝ, 0 < ε → ∀ f : EuclideanSpace ℝ (Fin d) → ℂ, MemLp f (ENNReal.ofReal p) volume →
        eLpNorm (fun x => ∫ y in {y | ε ≤ ‖y‖}, f (x - y) * K y) (ENNReal.ofReal p) volume
          ≤ A * eLpNorm f (ENNReal.ofReal p) volume) ∧
      ∀ f : EuclideanSpace ℝ (Fin d) → ℂ, MemLp f (ENNReal.ofReal p) volume →
        ∃ g : EuclideanSpace ℝ (Fin d) → ℂ, MemLp g (ENNReal.ofReal p) volume ∧
          Tendsto (fun ε : ℝ => eLpNorm
              ((fun x => ∫ y in {y | ε ≤ ‖y‖}, f (x - y) * K y) - g) (ENNReal.ofReal p) volume)
            (𝓝[>] 0) (𝓝 0) ∧
          eLpNorm g (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, § 3.2, Theorem 2, p. 35

Read-back

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

Read-back: `DbarRegularity.truncatedSingularIntegral_lp`

Setting. $d\in\mathbb N$ (implicit), kernel $K:\mathbb R^d\to\mathbb C$ , real $B$ , real $p>1$ (used as ENNReal.ofReal p $\in(1,\infty)$ ), Lebesgue measure.

Hypotheses.

$K$ a.e.-strongly measurable;
(size) $|K(x)|\le B/|x|^d$ for all $x\ne0$ ;
(Hörmander) for all $y\ne0$ : $\int^-_{\{x:\,2|y|\le|x|\}}|K(x-y)-K(x)|\,dx\le\max(B,0)$ (lower integral, so a true $[0,\infty]$ value);
(cancellation) for all $0<R_1<R_2$ : $\int_{\{R_1<|x|<R_2\}}K(x)\,dx=0$ (Bochner);
$p>1$ .

Definitions used. MemLp, eLpNorm, Bochner set integral, Tendsto … (𝓝[>] 0) (𝓝 0) in $[0,\infty]$ . Write $T_\varepsilon f(x)=\int_{\{|y|\ge\varepsilon\}}f(x-y)K(y)\,dy$ .

Quantifier order: $K,B,d,p$ (and hypotheses) $\to$ $A$ $\to$ $\varepsilon$ , $f$ $\to$ $g$ . So $A$ is uniform in $\varepsilon$ and $f$ (it may depend on $K$ ; Stein's dependence only on $p,B,d$ is stronger, but the weaker form is still the standard content).

Degenerate cases. $B<0$ , $d\ge1$ : the size bound is impossible, so the statement is vacuous (harmless). $d=0$ : the space is the point $\{0\}$ ; the size and Hörmander hypotheses are vacuous, the annulus $\{R_1<0<R_2\}$ is empty so cancellation holds; $\{|y|\ge\varepsilon\}=\emptyset$ , so $T_\varepsilon f=0$ , and (i),(ii) hold with $g=0$ . Harmless and true.

Remarks. For $d\ge1$ , $\varepsilon>0$ : $|K|\mathbf 1_{|y|\ge\varepsilon}\le B|y|^{-d}\mathbf 1_{|y|\ge\varepsilon}\in L^{p'}$ ( $p'<\infty$ , $dp'>d$ ), so by Hölder $y\mapsto f(x-y)K(y)$ is integrable on $\{|y|\ge\varepsilon\}$ for every $x$ : the Bochner integral is genuine, no junk. On annuli $K$ is bounded and the annulus has finite measure, so the cancellation integral is genuine. The Hörmander set includes only $x$ with $|x|\ge2|y|>0$ , so $x\ne0\ne x-y$ .

Soundness checks.

Bochner junk: none (shown above for both integrals). ENNReal.ofReal B $=0$ for $B<0$ is consistent with the vacuous case. ofReal p with $p>1$ is a genuine exponent; $p=\infty$ excluded. Real division by $\|x\|^d$ only for $x\ne0$ . $A$ is ℝ≥0, so finite. Hypotheses satisfiable for $B\ge0$ (e.g. $K=0$ ; or Riesz kernels $x_j/|x|^{d+1}$ with $B$ large); conclusion non-trivial.
$A$ chosen before $\varepsilon$ and $f$ : uniform bound as in Stein Ch. II Thm 2, inequality (21); existence of the $L^p$ limit as $\varepsilon\to0^+$ with the same bound is the second part of that theorem. 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

Uniform L^p bounds and L^p convergence of truncated singular integrals

Read-back: DbarRegularity.truncatedSingularIntegral_lp

Read-back: `DbarRegularity.truncatedSingularIntegral_lp`