The Marcinkiewicz interpolation theorem for sub-additive operators

Proved

DbarRegularity.marcinkiewicz_interpolation

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

calderon-zygmundcauchy-riemannelliptic-regularityharmonic-analysissingular-integrals

Let $1<r\le\infty$ and let $T$ be a map from $L^1(\mathbb{R}^d)+L^r(\mathbb{R}^d)$ to measurable functions on $\mathbb{R}^d$ . $\mathbb{R}^d$ carries Lebesgue measure $m$ , and $\|\cdot\|_p$ is the $L^p(\mathbb{R}^d)$ norm. Assume that for all $f,g\in L^1+L^r$ :

$|T(f+g)(x)|\le|Tf(x)|+|Tg(x)|$ for almost every $x$ ;
$m\{x:|Tf(x)|>\alpha\}\le\dfrac{A_1}{\alpha}\|f\|_1$ for $f\in L^1$ and $\alpha>0$ ;
if $r<\infty$ : $m\{x:|Tf(x)|>\alpha\}\le\Big(\dfrac{A_r}{\alpha}\|f\|_r\Big)^r$ for $f\in L^r$ and $\alpha>0$ ; if $r=\infty$ : $\|Tf\|_\infty\le A_r\|f\|_\infty$ for $f\in L^\infty$ .

Then for every $1<p<r$ there is a constant $A_p$ , depending only on $A_1$ , $A_r$ , $p$ and $r$ , such that $\|Tf\|_p\le A_p\|f\|_p$ for every $f\in L^p(\mathbb{R}^d)$ .

Formalization Note $T$ acts on functions EuclideanSpace ℝ (Fin d) → ℂ. Membership in $L^1+L^r$ is written out as ∃ f₁ f₂, MemLp f₁ 1 ∧ MemLp f₂ r ∧ f = f₁ + f₂, and measurability of $Tf$ is assumed for such $f$ . Sub-additivity is assumed almost everywhere (Stein writes it pointwise). The exponents $r,p$ are in ℝ≥0∞; the case $r=\infty$ uses Stein's form (17) in place of a weak-type bound. $A_1,A_r,A_p\in$ ℝ≥0, and $A_p$ is chosen before $d$ and $T$ .

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, § 4.2, Theorem 5 (p. 21), Marcinkiewicz interpolation:
let `1 < r ≤ ∞` and let `T` map `L¹(ℝ^d) + L^r(ℝ^d)` to measurable functions. Suppose `T` is
sub-additive, of weak type `(1, 1)` with constant `A₁`, and of weak type `(r, r)` with constant
`A_r` (for `r = ∞`: `‖T f‖_∞ ≤ A_r ‖f‖_∞`, Stein's form (17)). Then `‖T f‖_p ≤ A_p ‖f‖_p` for
`f ∈ L^p`, `1 < p < r`, where `A_p` depends only on `A₁`, `A_r`, `p` and `r`. -/
theorem marcinkiewicz_interpolation (r p : ℝ≥0∞) (hr : 1 < r) (hp : 1 < p) (hpr : p < r)
    (A₁ Ar : ℝ≥0) :
    ∃ A : ℝ≥0, ∀ (d : ℕ)
      (T : (EuclideanSpace ℝ (Fin d) → ℂ) → EuclideanSpace ℝ (Fin d) → ℂ),
      (∀ f, (∃ f₁ f₂, MemLp f₁ 1 volume ∧ MemLp f₂ r volume ∧ f = f₁ + f₂) →
        AEStronglyMeasurable (T f) volume) →
      (∀ f g, (∃ f₁ f₂, MemLp f₁ 1 volume ∧ MemLp f₂ r volume ∧ f = f₁ + f₂) →
        (∃ g₁ g₂, MemLp g₁ 1 volume ∧ MemLp g₂ r volume ∧ g = g₁ + g₂) →
        ∀ᵐ x, ‖T (f + g) x‖ ≤ ‖T f x‖ + ‖T g x‖) →
      (∀ f, MemLp f 1 volume → ∀ α : ℝ≥0, 0 < α →
        volume {x | (α : ℝ≥0∞) < ‖T f x‖ₑ} ≤ (A₁ : ℝ≥0∞) / α * eLpNorm f 1 volume) →
      (r ≠ ⊤ → ∀ f, MemLp f r volume → ∀ α : ℝ≥0, 0 < α →
        volume {x | (α : ℝ≥0∞) < ‖T f x‖ₑ} ≤ ((Ar : ℝ≥0∞) / α * eLpNorm f r volume) ^ r.toReal) →
      (r = ⊤ → ∀ f, MemLp f ⊤ volume → eLpNorm (T f) ⊤ volume ≤ Ar * eLpNorm f ⊤ volume) →
      ∀ f, MemLp f p volume → eLpNorm (T f) p volume ≤ A * eLpNorm f 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 I, § 4.2, Theorem 5, p. 21 (with the definitions (17), (18) of § 4.1, p. 20)

Read-back

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

Read-back: `DbarRegularity.marcinkiewicz_interpolation`

Setting. Exponents $r,p\in[0,\infty]$ with $1<p<r$ (so $r>1$ , $p<\infty$ , $r=\infty$ allowed); constants $A_1,A_r\in[0,\infty)$ .

Hypotheses. $1<r$ , $1<p$ , $p<r$ ; $A_1,A_r\ge0$ real (ℝ≥0).

Definitions used. MemLp, eLpNorm (Lebesgue measure), AEStronglyMeasurable. Write $L^1+L^r$ for $\{f_1+f_2: f_1\in L^1, f_2\in L^r\}$ (pointwise sums of genuine functions).

Conclusion. $\exists A\in[0,\infty)$ such that for every $d\in\mathbb N$ and every map $T:(\mathbb R^d\to\mathbb C)\to(\mathbb R^d\to\mathbb C)$ satisfying

$Tf$ is a.e.-strongly measurable for every $f\in L^1+L^r$ ;
for $f,g\in L^1+L^r$ : $|T(f+g)(x)|\le|Tf(x)|+|Tg(x)|$ for a.e. $x$ ;
for $f\in L^1$ , $\alpha>0$ : $|\{x:\alpha<|Tf(x)|\}|\le\dfrac{A_1}{\alpha}\|f\|_1$ ;
if $r<\infty$ : for $f\in L^r$ , $\alpha>0$ : $|\{x:\alpha<|Tf(x)|\}|\le\Big(\dfrac{A_r}{\alpha}\|f\|_r\Big)^{r}$ ;
if $r=\infty$ : for $f\in L^\infty$ : $\|Tf\|_\infty\le A_r\|f\|_\infty$ ;

one has $\|Tf\|_p\le A\,\|f\|_p$ for all $f\in L^p(\mathbb R^d)$ .

Quantifier order: $r,p,A_1,A_r$ $\to$ $A$ $\to$ $d$ , $T$ $\to$ $f$ . So $A=A(A_1,A_r,p,r)$ is independent of $d$ and $T$ .

Degenerate cases. $r=\infty$ : hypothesis 4 is vacuous and 5 is active; when $r<\infty$ , 5 is vacuous. $A_1=0$ forces $Tf=0$ a.e. on $L^1$ ; fine. $d=0$ is allowed (one-point probability space); the Marcinkiewicz theorem holds on any measure space, so no problem.

Remarks. $T$ acts on functions, not a.e.-classes; hypotheses and conclusion are all about the same representatives, which is enough for the standard proof (split $f=f\mathbf 1_{|f|>c\alpha}+f\mathbf 1_{|f|\le c\alpha}$ , the pieces are in $L^1$ and $L^r$ respectively, apply 2 for each fixed $\alpha$ , integrate the distribution function). No homogeneity of $T$ is assumed, and none is needed.

Soundness checks.

ENNReal: $\alpha>0$ so $A_1/\alpha,A_r/\alpha<\infty$ ; $\|f\|_1,\|f\|_r,\|f\|_p<\infty$ under the MemLp hypotheses, so no $0\cdot\infty$ issue. In 4, $r\ne\infty$ and $r>1$ , so r.toReal $=r>1$ (the toReal ⊤ = 0 trap is avoided by the guard r ≠ ⊤). $A$ is ℝ≥0, so finite. No Bochner integrals. Hypotheses are satisfiable (e.g. $T=0$ , or $T$ = identity); the conclusion is non-trivial.
$A$ is chosen before $d$ and $T$ : correct and true, since the Marcinkiewicz constant depends only on $p,r,A_1,A_r$ (Stein Ch. I, Thm 5). 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 Marcinkiewicz interpolation theorem for sub-additive operators

Read-back: DbarRegularity.marcinkiewicz_interpolation

Read-back: `DbarRegularity.marcinkiewicz_interpolation`