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

Proved

DbarRegularity.dbar_lp_estimate

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

calderon-zygmundcauchy-riemannelliptic-regularityharmonic-analysissingular-integrals

Write $z=s+it$ for $z\in\mathbb{C}$ , $\varphi_s=\partial\varphi/\partial s$ , $\varphi_t=\partial\varphi/\partial t$ and $\bar\partial\varphi=\varphi_s+i\varphi_t$ . $\mathbb{C}^n$ carries the Hermitian norm, and $\|\cdot\|_{L^p}$ is the $L^p$ norm on $\mathbb{C}$ with respect to Lebesgue measure. Let $1<p<\infty$ and $R>0$ . Then there is a constant $c>1$ such that every smooth $\varphi:\mathbb{C}\to\mathbb{C}^n$ with compact support in the open disc $B_R(0)$ satisfies

\|\varphi\|_{1,p}\le c\,\|\bar\partial\varphi\|_{L^p},\qquad \|\varphi\|_{1,p}=\big(\|\varphi_s\|_{L^p}^p+\|\varphi_t\|_{L^p}^p+\|\varphi\|_{L^p}^p\big)^{1/p}.

Formalization Note ContDiff ℝ ∞ φ is $C^\infty$ smoothness over $\mathbb{R}$ (not analyticity). $\varphi_s$ and $\varphi_t$ are fderiv ℝ φ z 1 and fderiv ℝ φ z Complex.I, and $\bar\partial\varphi$ is dbar φ. $\mathbb{C}^n$ is EuclideanSpace ℂ (Fin n). "Compact support in $B_R(0)$ " is tsupport φ ⊆ ball 0 R. The norms are eLpNorm with exponent ENNReal.ofReal p, combined in ℝ≥0∞. Abbas–Hofer write $c=c(p,R)$ ; here $c$ is chosen after $n$ as well, so it may depend on $n$ .

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

/-- Abbas–Hofer, *Holomorphic Curves and Global Questions in Contact Geometry*, § 4.2, Theorem 4.2.2
(p. 102): for `1 < p < ∞` and `R > 0` there is `c > 1` such that every smooth `φ : ℂ → ℂⁿ` with
compact support in the open disc `B_R(0)` satisfies `‖φ‖_{1,p} ≤ c ‖∂̄φ‖_{L^p}`, where
`‖φ‖_{1,p} = (‖φ_s‖_p^p + ‖φ_t‖_p^p + ‖φ‖_p^p)^{1/p}` and `z = s + i t`. -/
theorem dbar_lp_estimate (n : ℕ) (p R : ℝ) (hp : 1 < p) (hR : 0 < R) :
    ∃ c : ℝ, 1 < c ∧ ∀ φ : ℂ → EuclideanSpace ℂ (Fin n), ContDiff ℝ ∞ φ → tsupport φ ⊆ ball 0 R →
      (eLpNorm (fun z => fderiv ℝ φ z 1) (ENNReal.ofReal p) volume ^ p +
          eLpNorm (fun z => fderiv ℝ φ z Complex.I) (ENNReal.ofReal p) volume ^ p +
          eLpNorm φ (ENNReal.ofReal p) volume ^ p) ^ (1 / p)
        ≤ ENNReal.ofReal c * eLpNorm (dbar φ) (ENNReal.ofReal p) volume := by sorry

end DbarRegularity

Source

C. Abbas, H. Hofer, Holomorphic Curves and Global Questions in Contact Geometry, Birkhäuser Advanced Texts Basler Lehrbücher, Birkhäuser (2019), https://doi.org/10.1007/978-3-030-11803-7, § 4.2, Theorem 4.2.2, p. 102

Read-back

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

Read-back: `DbarRegularity.dbar_lp_estimate`

Setting. $n\in\mathbb N$ , real $p,R$ ; $\varphi:\mathbb C\to\mathbb C^n$ (Hermitian norm), $z=s+it$ , Lebesgue measure on $\mathbb C$ .

Hypotheses. $1<p$ (finite) and $0<R$ .

Definitions used. eLpNorm · (ofReal p) volume $=\|\cdot\|_{L^p(\mathbb C)}\in[0,\infty]$ . $\varphi_s$ and $\varphi_t$ are the derivatives along $1$ and $i$ ; $\bar\partial\varphi=\varphi_s+i\varphi_t$ . The exponents ^ p and ^ (1/p) are ENNReal powers with real exponents.

Conclusion.

\exists c\in\mathbb R,\ c>1,\ \forall\varphi\in C^\infty(\mathbb C;\mathbb C^n)\text{ with }\operatorname{tsupport}\varphi\subseteq B_R(0):\quad \big(\|\varphi_s\|_p^p+\|\varphi_t\|_p^p+\|\varphi\|_p^p\big)^{1/p}\le c\,\|\bar\partial\varphi\|_p .

The constant $c$ depends on $n,p,R$ only.

Degenerate cases. $\varphi=0$ gives $0\le0$ . $n=0$ is trivial. $R\le0$ is excluded by hypothesis.

Soundness checks.

Lean defaults.
- ∞ means $C^\infty$ , not analytic.
- All functions are continuous with compact support, so every eLpNorm is finite and the right-hand side is not $\top$ .
- The exponents $p>1$ and $1/p\in(0,1)$ are both nonzero, so the rpow-at-0 degeneracy cannot occur, and $0^{p}=0$ and $0^{1/p}=0$ behave correctly.
- ENNReal.ofReal c with $c>1$ is a finite positive number.
- There is no Bochner integral, toReal or ℕ subtraction.
- 1 / p is real division with $p>0$ .
Quantifiers: $c$ is chosen after $n,p,R$ and before $\varphi$ . The statement is true. Calderón–Zygmund gives $\|\varphi_s\|_p+\|\varphi_t\|_p\le A_p\|\bar\partial\varphi\|_p$ , componentwise and hence with an $n$ -dependent constant. Poincaré on $B_R$ gives $\|\varphi\|_p\le C R\|\nabla\varphi\|_p$ . Requiring $c>1$ costs nothing, since $c$ can always be enlarged.

Remarks. The norm on $\mathbb C^n$ is Euclidean. Pointwise norms are used, not a sum of componentwise $L^p$ norms, which only affects the constant.

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 estimate for the Cauchy–Riemann operator on a disc

Read-back: DbarRegularity.dbar_lp_estimate

Read-back: `DbarRegularity.dbar_lp_estimate`