The Calderón–Zygmund decomposition of a non-negative integrable function

Proved

DbarRegularity.calderonZygmund_decomposition

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

calderon-zygmundcauchy-riemannelliptic-regularityharmonic-analysissingular-integrals

Let $d\ge1$ , let $f\ge0$ be an integrable function on $\mathbb{R}^d$ and let $\alpha>0$ . $\mathbb{R}^d$ carries Lebesgue measure $m$ , and $\|\cdot\|_p$ is the $L^p(\mathbb{R}^d)$ norm. Then there is a decomposition $\mathbb{R}^d=F\cup\Omega$ , $F\cap\Omega=\emptyset$ , such that

$f(x)\le\alpha$ for almost every $x\in F$ ;
$\Omega=\bigcup_k Q_k$ is a countable union of closed cubes $Q_k$ (with positive side lengths) whose interiors are pairwise disjoint, and for every $k$

\alpha<\frac{1}{m(Q_k)}\int_{Q_k}f(x)\,dx\le 2^d\alpha .

Formalization Note A cube is closedCube a s $=\{x: a_i\le x_i\le a_i+s\}$ with $s>0$ . The family of cubes is indexed by a countable type ι; Stein does not say "countable", but cubes with disjoint interiors are automatically countably many. The average is (∫ x in Q, f x) / (volume Q).toReal, where volume Q is finite and positive. The hypothesis $d\ge1$ is implicit in Stein: for $d=0$ the space is a point of measure $1$ and the statement fails when $f>\alpha$ .

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 I, § 3.2, Theorem 4 (p. 17): for a non-negative integrable
`f` on `ℝ^d` (`d ≥ 1`) and `α > 0` there is a decomposition `ℝ^d = F ∪ Ω`, `F ∩ Ω = ∅`, with
`f ≤ α` almost everywhere on `F` and `Ω` a union of closed cubes `Q_k` with pairwise disjoint
interiors such that `α < (1 / |Q_k|) ∫_{Q_k} f ≤ 2^d α` for every `k`. -/
theorem calderonZygmund_decomposition {d : ℕ} (hd : 0 < d)
    (f : EuclideanSpace ℝ (Fin d) → ℝ) (hf0 : ∀ x, 0 ≤ f x) (hf : Integrable f)
    (α : ℝ) (hα : 0 < α) :
    ∃ (F Ω : Set (EuclideanSpace ℝ (Fin d))) (ι : Type) (_ : Countable ι)
      (a : ι → EuclideanSpace ℝ (Fin d)) (s : ι → ℝ),
      F ∪ Ω = Set.univ ∧ Disjoint F Ω ∧
      (∀ᵐ x, x ∈ F → f x ≤ α) ∧
      Ω = ⋃ k, closedCube (a k) (s k) ∧
      (∀ k, 0 < s k) ∧
      Pairwise (fun k l => Disjoint (interior (closedCube (a k) (s k)))
        (interior (closedCube (a l) (s l)))) ∧
      ∀ k, α < (∫ x in closedCube (a k) (s k), f x) / (volume (closedCube (a k) (s k))).toReal ∧
        (∫ x in closedCube (a k) (s k), f x) / (volume (closedCube (a k) (s k))).toReal
          ≤ 2 ^ d * α := 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 I, § 3.2, Theorem 4, pp. 17–18

Read-back

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

Read-back: `DbarRegularity.calderonZygmund_decomposition`

Setting. $d\ge1$ ; $f:\mathbb R^d\to\mathbb R$ ; Lebesgue measure.

Hypotheses. $0<d$ ; $f(x)\ge0$ for all $x$ ; $f\in L^1(\mathbb R^d)$ ; $\alpha\in\mathbb R$ , $\alpha>0$ .

Definitions used. closedCube a s $=\prod_i[a_i,a_i+s]$ ; Bochner set integral; ENNReal.toReal of the cube's volume.

Conclusion. There exist sets $F,\Omega\subseteq\mathbb R^d$ , a countable index type $\iota$ (in Type), corners $a:\iota\to\mathbb R^d$ and sides $s:\iota\to\mathbb R$ such that

$F\cup\Omega=\mathbb R^d$ and $F\cap\Omega=\emptyset$ ;
for a.e. $x$ : $x\in F\Rightarrow f(x)\le\alpha$ ;
$\Omega=\bigcup_k Q_k$ with $Q_k=$ closedCube (a k) (s k);
$s_k>0$ for all $k$ ;
$\operatorname{int}Q_k\cap\operatorname{int}Q_l=\emptyset$ for $k\ne l$ ;
for all $k$ : $\alpha<\dfrac{\int_{Q_k}f}{|Q_k|}\le 2^d\alpha$ (with $|Q_k|$ = (volume Q_k).toReal).

Degenerate cases. $\iota$ may be empty (then $\Omega=\emptyset$ , $F=\mathbb R^d$ and one must have $f\le\alpha$ a.e.; not a loophole). $d=0$ is excluded by hd; this is necessary (on a point with $f>\alpha$ the bound $\le 2^0\alpha$ would fail).

Remarks. $F=\Omega^c$ is forced. Since $s_k>0$ , $|Q_k|=s_k^d\in(0,\infty)$ , so toReal is the true volume and the division is genuine. $f$ integrable implies integrable on $Q_k$ , so the Bochner integral is the true integral.

Soundness checks.

Bochner junk: excluded ( $f$ integrable). toReal ⊤ = 0: excluded (bounded cubes). Division by $0$ : excluded by $s_k>0$ . 2 ^ d is a real power of a natural, fine. No Nat subtraction. Hypotheses are satisfiable; the conclusion is not trivially true (the average bounds and the a.e. bound on $F$ are real constraints).
All objects are chosen after $f,\alpha$ , as in the standard lemma. The statement is the Calderón–Zygmund decomposition (Stein Ch. I, Thm 4, dyadic stopping-time cubes): 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

The Calderón–Zygmund decomposition of a non-negative integrable function

Read-back: DbarRegularity.calderonZygmund_decomposition

Read-back: `DbarRegularity.calderonZygmund_decomposition`