The L^p a priori estimate for the Cauchy–Riemann operator on the plane

Proved

DbarRegularity.cauchyRiemann_lp_plane

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

calderon-zygmundcauchy-riemannelliptic-regularityharmonic-analysissingular-integrals

For every $1<p<\infty$ there is a constant $A_p$ such that every complex-valued function $f$ of class $C^1$ with compact support in $\mathbb{R}^2$ satisfies

\Big\|\frac{\partial f}{\partial x_1}\Big\|_p+\Big\|\frac{\partial f}{\partial x_2}\Big\|_p\le A_p\Big\|\frac{\partial f}{\partial x_1}+i\frac{\partial f}{\partial x_2}\Big\|_p,

where $\|\cdot\|_p$ is the $L^p(\mathbb{R}^2)$ norm.

Formalization Note $\mathbb{R}^2$ is EuclideanSpace ℝ (Fin 2) and $\partial f/\partial x_j$ is fderiv ℝ f x (EuclideanSpace.single j 1). ContDiff ℝ 1 f and HasCompactSupport f are the hypotheses. The exponent is ENNReal.ofReal p with $p>1$ real, and the constant A : ℝ≥0 is chosen before $f$ .

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 III, § 1.3, Proposition 4 (p. 60): for `1 < p < ∞` there is
`A_p` such that every complex-valued `f` of class `C¹` with compact support in `ℝ²` satisfies
`‖∂f/∂x₁‖_p + ‖∂f/∂x₂‖_p ≤ A_p ‖∂f/∂x₁ + i ∂f/∂x₂‖_p`. -/
theorem cauchyRiemann_lp_plane (p : ℝ) (hp : 1 < p) :
    ∃ A : ℝ≥0, ∀ f : EuclideanSpace ℝ (Fin 2) → ℂ, ContDiff ℝ 1 f → HasCompactSupport f →
      eLpNorm (fun x => fderiv ℝ f x (EuclideanSpace.single 0 1)) (ENNReal.ofReal p) volume +
          eLpNorm (fun x => fderiv ℝ f x (EuclideanSpace.single 1 1)) (ENNReal.ofReal p) volume
        ≤ A * eLpNorm (fun x => fderiv ℝ f x (EuclideanSpace.single 0 1) +
            Complex.I * fderiv ℝ f x (EuclideanSpace.single 1 1)) (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 III, § 1.3, Proposition 4, p. 60

Read-back

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

Read-back: `DbarRegularity.cauchyRiemann_lp_plane`

Setting. $\mathbb R^2$ = EuclideanSpace ℝ (Fin 2) with Lebesgue measure; functions $f:\mathbb R^2\to\mathbb C$ ; a real $p$ .

Hypotheses. $1<p$ (real, hence finite).

Definitions used. fderiv ℝ f x (EuclideanSpace.single 0 1) $=\partial f/\partial x_1(x)$ , and ... (single 1 1) $=\partial f/\partial x_2(x)$ (the Fréchet derivative applied to the standard basis vectors $e_1,e_2$ ). eLpNorm · (ofReal p) volume $=\|\cdot\|_{L^p(\mathbb R^2)}$ .

Conclusion.

\exists A\in[0,\infty)\ \forall f\in C^1(\mathbb R^2;\mathbb C)\text{ with compact support}:\quad \Big\|\tfrac{\partial f}{\partial x_1}\Big\|_p+\Big\|\tfrac{\partial f}{\partial x_2}\Big\|_p\le A\,\Big\|\tfrac{\partial f}{\partial x_1}+i\,\tfrac{\partial f}{\partial x_2}\Big\|_p .

Degenerate cases. $f=0$ gives $0\le0$ . A holomorphic-type $f$ with $\partial_1 f+i\partial_2 f\equiv0$ and compact support is $0$ (Liouville/identity), so the right-hand side vanishes only when the left-hand side does. This is consistent.

Soundness checks.

Lean defaults. ContDiff ℝ 1 is genuinely $C^1$ . Here the exponent is the numeral 1, not $\omega$ and not $\top$ , so analyticity is not involved. No Bochner integrals, toReal, rpow, ENNReal division or ℕ subtraction occur. $A:\mathbb R_{\ge0}$ is finite. The derivatives are continuous and compactly supported, so every $L^p$ norm is finite and the inequality is not trivially true through $\top$ on the right. Complex.I * ... is multiplication in $\mathbb C$ , as intended.
Quantifiers: $A$ is chosen after $p$ and before $f$ . The statement is the classical $L^p$ bound of $\nabla f$ by $\bar\partial f$ in the plane (Beurling–Ahlfors / Riesz transforms), which is true for $1<p<\infty$ .

Remarks. The operator here is $\partial_1+i\partial_2$ , without the factor $1/2$ , which only changes $A$ .

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 L^p a priori estimate for the Cauchy–Riemann operator on the plane

Read-back: DbarRegularity.cauchyRiemann_lp_plane

Read-back: `DbarRegularity.cauchyRiemann_lp_plane`