L^p boundedness of singular integrals with homogeneous Dini-continuous kernels of mean zero

Proved

DbarRegularity.homogeneousSingularIntegral_lp

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

calderon-zygmundcauchy-riemannelliptic-regularityharmonic-analysissingular-integrals

Let $\Omega:\mathbb{R}^d\to\mathbb{C}$ be homogeneous of degree $0$ , i.e. $\Omega(tx)=\Omega(x)$ for $t>0$ , and assume

$\displaystyle\int_{S^{d-1}}\Omega\,d\sigma=0$ , where $\sigma$ is the surface measure on the unit sphere $S^{d-1}$ (condition (24));
the modulus $w(\delta)=\sup\{|\Omega(x)-\Omega(x')|: |x|=|x'|=1,\ |x-x'|\le\delta\}$ satisfies $\displaystyle\int_0^1\frac{w(\delta)}{\delta}\,d\delta<\infty$ (condition (25)).

$\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}\frac{\Omega(y)}{|y|^d}f(x-y)\,dy .

Then

(a) there is a constant $A_p$ , independent of $f$ and $\varepsilon$ , such that $\|T_\varepsilon f\|_p\le A_p\|f\|_p$ ;

(b) 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 The sphere measure is Mathlib's volume.toSphere on sphere (0 : EuclideanSpace ℝ (Fin d)) 1; condition (24) does not change if the measure is multiplied by a positive constant. The modulus $w(\delta)$ is the supremum ⨆ … ‖Ω x - Ω x'‖ₑ in ℝ≥0∞, and condition (25) is ∫⁻ δ in Ioc 0 1, w δ / ENNReal.ofReal δ < ⊤. $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 constant A : ℝ≥0 depends on $\Omega$ and $p$ . Part (c) of Stein's theorem, an explicit formula for the Fourier transform of $Tf$ when $f\in L^2$ , is not included.

Preamble

import Definitions.Def_DbarRegularity_Setting
import Mathlib.Analysis.Calculus.ContDiff.Basic
import Mathlib.MeasureTheory.Constructions.HaarToSphere

Formal statement

namespace DbarRegularity

open MeasureTheory Metric Filter Topology
open scoped ENNReal NNReal ContDiff

/-- Stein, *Singular Integrals*, Chapter II, § 4.2, Theorem 3 (a), (b) (p. 39): let `Ω` on `ℝ^d` be
homogeneous of degree `0`, with mean zero on the unit sphere `S^{d-1}` (condition (24)) and with
modulus of continuity `w(δ) = sup {|Ω(x) - Ω(x')| : |x| = |x'| = 1, |x - x'| ≤ δ}` satisfying
`∫₀¹ w(δ) / δ dδ < ∞` (condition (25)). For `1 < p < ∞`, `f ∈ L^p` and
`T_ε f (x) = ∫_{|y| ≥ ε} Ω(y) / |y|^d · f(x - y) dy`:
(a) `‖T_ε f‖_p ≤ A_p ‖f‖_p` with `A_p` independent of `f` and `ε`;
(b) `T f = lim_{ε → 0} T_ε f` exists in `L^p` and `‖T f‖_p ≤ A_p ‖f‖_p`. -/
theorem homogeneousSingularIntegral_lp {d : ℕ} (Ω : EuclideanSpace ℝ (Fin d) → ℂ)
    (hhom : ∀ x, ∀ t : ℝ, 0 < t → Ω (t • x) = Ω x)
    (hmean : ∫ x : sphere (0 : EuclideanSpace ℝ (Fin d)) 1, Ω x ∂(volume.toSphere) = 0)
    (hdini : ∫⁻ δ in Set.Ioc (0 : ℝ) 1,
      (⨆ (x : EuclideanSpace ℝ (Fin d)) (x' : EuclideanSpace ℝ (Fin d)) (_ : ‖x‖ = 1)
        (_ : ‖x'‖ = 1) (_ : ‖x - x'‖ ≤ δ), ‖Ω x - Ω x'‖ₑ) / ENNReal.ofReal δ < ⊤)
    (p : ℝ) (hp : 1 < p) :
    ∃ A : ℝ≥0,
      (∀ ε : ℝ, 0 < ε → ∀ f : EuclideanSpace ℝ (Fin d) → ℂ, MemLp f (ENNReal.ofReal p) volume →
        eLpNorm (fun x => ∫ y in {y | ε ≤ ‖y‖}, Ω y / ((‖y‖ ^ d : ℝ) : ℂ) * f (x - 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‖}, Ω y / ((‖y‖ ^ d : ℝ) : ℂ) * f (x - 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, § 4.2, Theorem 3 (a), (b), p. 39 (conditions (24), (25) on the same page)

Read-back

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

Read-back: `DbarRegularity.homogeneousSingularIntegral_lp`

Setting. $d\in\mathbb N$ , $\mathbb R^d$ = EuclideanSpace ℝ (Fin d) with Lebesgue measure. A function $\Omega:\mathbb R^d\to\mathbb C$ and a real $p$ .

Hypotheses.

(hom) $\Omega(tx)=\Omega(x)$ for all $x\in\mathbb R^d$ , $t>0$ (homogeneous of degree 0; $\Omega(0)$ unconstrained).
(mean) $\displaystyle\int_{S^{d-1}}\Omega\,d\sigma = 0$ , where $\sigma$ = volume.toSphere (Mathlib's surface measure on the unit sphere induced from Lebesgue measure, $\sigma(A)=d\cdot|\{rx: x\in A,\ 0<r<1\}|$ ); Bochner integral.
(Dini) $\displaystyle\int^{-}_{(0,1]} \frac{w(\delta)}{\delta}\,d\delta<\infty$ (lower Lebesgue integral in $[0,\infty]$ ), where $w(\delta)=\sup\{|\Omega(x)-\Omega(x')| : |x|=|x'|=1,\ |x-x'|\le\delta\}\in[0,\infty]$ .
$1<p$ (real, so $p<\infty$ ).

Definitions used. eLpNorm · (ofReal p) volume = $\|\cdot\|_{L^p(\mathbb R^d)}\in[0,\infty]$ ; MemLp f p = a.e.-strongly measurable with finite $L^p$ norm. For $\varepsilon>0$ : $T_\varepsilon f(x)=\displaystyle\int_{|y|\ge\varepsilon}\frac{\Omega(y)}{|y|^d}f(x-y)\,dy$ (Bochner; $|y|^d$ is a natural-number power of a real, cast to $\mathbb C$ ).

Conclusion. There is $A\in[0,\infty)$ (depending on $d,\Omega,p$ only) such that

(a) $\forall\varepsilon>0\ \forall f\in L^p(\mathbb R^d;\mathbb C):\ \|T_\varepsilon f\|_p\le A\|f\|_p$ ;

(b) $\forall f\in L^p\ \exists g\in L^p:\ \|T_\varepsilon f-g\|_p\to0$ as $\varepsilon\to0^+$ , and $\|g\|_p\le A\|f\|_p$ .

Quantifier order: $\exists A\ \forall\varepsilon\ \forall f$ in (a); $\exists A$ ( $\forall f\ \exists g$ ) in (b), same $A$ .

Degenerate cases.

$d=0$ : the space is one point, the sphere is empty, (mean) and (Dini) hold trivially, $\{|y|\ge\varepsilon\}=\emptyset$ so $T_\varepsilon f=0$ ; conclusion holds with $g=0$ . Harmless.
$d=1$ : sphere $=\{\pm1\}$ , $w\equiv0$ on $(0,1]$ , (mean) says (a positive multiple of) $\Omega(1)+\Omega(-1)=0$ : the Hilbert-transform case, which is true.

Soundness checks.

Lean defaults.
- Bochner integral in (mean): $w$ is monotone in $\delta$ , so the Dini condition forces $w(\delta)\to0$ (otherwise $\int c/\delta=\infty$ ), hence $\Omega|_{S^{d-1}}$ is uniformly continuous and bounded. It is therefore integrable for the finite measure $\sigma$ , so (mean) is a genuine mean-zero condition, not something that holds automatically by the "non-integrable gives 0" default.
- iSup over an empty set: for $\delta>0$ and $d\ge1$ the pair $x=x'$ is admissible, so the sup is over a nonempty set. When $d=0$ it is $0$ , which is harmless.
- Division in ℝ≥0∞: $\delta\in(0,1]$ , so ofReal δ lies in $(0,1]$ , with no division by 0 or $\top$ . If $w=\top$ the hypothesis fails, which is correct.
- $T_\varepsilon f(x)$ : $\Omega$ is bounded and $|y|^{-d}\mathbf 1_{|y|\ge\varepsilon}\in L^{p'}$ (since $dp'>d$ ), so by Hölder the integrand is integrable for every $x$ . The Bochner value is the true value and not a default 0. $\Omega$ is continuous off $0$ , hence measurable.
- The cast $((\|y\|^d:\mathbb R):\mathbb C)$ is the real $|y|^d$ with $\mathbb N$ -exponent, as intended. It is nonzero on $|y|\ge\varepsilon>0$ .
- No toReal, no rpow at exponent 0, no ContDiff, no ℕ subtraction. $A:\mathbb R_{\ge0}$ , so it cannot be $\top$ . The exponent ofReal p lies in $(1,\infty)$ .
Quantifiers: $A$ is chosen after $d,\Omega,p$ and before $\varepsilon$ and $f$ ; $g$ is chosen after $f$ . This is exactly the uniform-in- $\varepsilon$ $L^p$ bound for truncated homogeneous Calderón–Zygmund kernels with Dini-continuous mean-zero angular part, together with $L^p$ convergence of the truncations. It is a standard true theorem, and the hypotheses are satisfiable non-trivially (e.g. Riesz kernels $\Omega(x)=x_j/|x|$ ).

Remarks. $\Omega$ carries no measurability hypothesis, but measurability follows from the hypotheses as shown above. Part (b) uses the same constant $A$ as (a), which is consistent because the $L^p$ limit inherits the bound.

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 boundedness of singular integrals with homogeneous Dini-continuous kernels of mean zero

Read-back: DbarRegularity.homogeneousSingularIntegral_lp

Read-back: `DbarRegularity.homogeneousSingularIntegral_lp`