The W^{k,p} estimate for the Cauchy–Riemann operator on a disc

Proved

DbarRegularity.dbar_sobolev_estimate

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

calderon-zygmundcauchy-riemannelliptic-regularityharmonic-analysissingular-integrals

Let $k\ge1$ be an integer, $p>1$ and $R>0$ . Then there is a constant $M=M(k,p,R)$ such that for every disc $B\subset\mathbb{C}$ of radius $R$ and every smooth map $\varphi:\mathbb{C}\to\mathbb{C}^n$ whose support lies in the interior of $B$ ,

\|\varphi\|_{W^{k,p}(B)}\le M\,\|\bar\partial\varphi\|_{W^{k-1,p}(B)} .

Here $\bar\partial\varphi=\partial\varphi/\partial s+i\,\partial\varphi/\partial t$ for $z=s+it$ , and $\|\psi\|_{W^{k,p}(B)}=\sum_{j=0}^{k}\|D^j\psi\|_{L^p(B)}$ is the Sobolev norm of the definition module.

This is the elliptic estimate for $\bar\partial$ that Hofer–Wysocki–Zehnder use to bound the derivatives of pseudoholomorphic half-cylinders, and the basic a priori estimate of the regularity theory of pseudoholomorphic curves.

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). "Support in the interior of $B$ " is tsupport φ ⊆ ball c R. The norms are sobolevNorm k (ENNReal.ofReal p) (ball c R), valued in ℝ≥0∞; any other choice of equivalent $W^{k,p}$ norm changes only $M$ . The constant M : ℝ≥0 is chosen before the centre $c$ of the disc and before $\varphi$ , and it may depend on $n$ . Hofer–Wysocki–Zehnder take $\varphi$ with values in $\mathbb{R}^2$ and $\bar\partial=\partial_s+J_0\partial_t$ with $J_0^2=-1$ ; identifying $\mathbb{R}^2$ with $\mathbb{C}$ so that $J_0$ is multiplication by $i$ gives the case $n=1$ , and the statement here allows $\mathbb{C}^n$ , as in Abbas–Hofer, § 4.2.

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

/-- Hofer–Wysocki–Zehnder, *Properties of pseudoholomorphic curves in symplectisations I*, estimate (49)
(p. 366): for an integer `k ≥ 1`, `p > 1` and `R > 0` there is `M = M(k, p, R)` such that for
every disc `B` of radius `R` and every smooth `φ : ℂ → ℂⁿ` with support in the interior of `B`,
`‖φ‖_{W^{k,p}(B)} ≤ M ‖∂̄φ‖_{W^{k-1,p}(B)}`. -/
theorem dbar_sobolev_estimate (n k : ℕ) (p R : ℝ) (hk : 1 ≤ k) (hp : 1 < p) (hR : 0 < R) :
    ∃ M : ℝ≥0, ∀ (c : ℂ) (φ : ℂ → EuclideanSpace ℂ (Fin n)), ContDiff ℝ ∞ φ →
      tsupport φ ⊆ ball c R →
      sobolevNorm k (ENNReal.ofReal p) (ball c R) φ
        ≤ M * sobolevNorm (k - 1) (ENNReal.ofReal p) (ball c R) (dbar φ) := by sorry

end DbarRegularity

Source

H. Hofer, K. Wysocki, E. Zehnder, Properties of pseudoholomorphic curves in symplectisations I: asymptotics, Ann. Inst. H. Poincaré Anal. Non Linéaire 13(3) (1996) 337–379, http://www.numdam.org/item/AIHPC_1996__13_3_337_0/, estimate (49), p. 366, § 3

Read-back

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

Read-back: `DbarRegularity.dbar_sobolev_estimate`

Setting. $n,k\in\mathbb N$ , real $p,R$ ; centre $c\in\mathbb C$ ; $\varphi:\mathbb C\to\mathbb C^n$ .

Hypotheses. $k\ge1$ , $1<p$ (finite), $0<R$ .

Definitions used. sobolevNorm k p U ψ $=\sum_{j=0}^{k}\|D^j\psi\|_{L^p(U)}\in[0,\infty]$ . Here $D^j\psi$ = iteratedFDeriv ℝ j ψ is the $j$ -th real Fréchet derivative, a continuous $j$ -linear map $\mathbb C^j\to\mathbb C^n$ , and $|D^j\psi(z)|$ is its operator norm. The $L^p(U)$ norm is taken with respect to Lebesgue measure restricted to $U$ . $\bar\partial\varphi=\varphi_s+i\varphi_t$ (dbar).

Conclusion.

\exists M\in[0,\infty)\ \forall c\in\mathbb C\ \forall\varphi\in C^\infty(\mathbb C;\mathbb C^n)\text{ with }\operatorname{tsupport}\varphi\subseteq B_R(c):\quad \sum_{j=0}^{k}\|D^j\varphi\|_{L^p(B_R(c))}\le M\sum_{j=0}^{k-1}\|D^j\bar\partial\varphi\|_{L^p(B_R(c))} .

The constant $M$ depends on $n,k,p,R$ only, and is uniform in the centre $c$ .

Degenerate cases. $k-1$ is ℕ subtraction, but $k\ge1$ , so it is the genuine $k-1\ge0$ . For $k=1$ the right-hand side is $M\|\bar\partial\varphi\|_{L^p(B)}$ . $\varphi=0$ gives $0\le0$ . $n=0$ is trivial.

Soundness checks.

Lean defaults.
- ∞ means $C^\infty$ , not analytic.
- ℕ subtraction is guarded by $k\ge1$ .
- $M:\mathbb R_{\ge0}$ is finite.
- All $D^j\varphi$ and $D^j\bar\partial\varphi$ are continuous and vanish outside the compact set $\operatorname{tsupport}\varphi$ , so every norm is finite and the right-hand side is not $\top$ .
- There is no Bochner integral, toReal or rpow.
- dbar φ is smooth because $\varphi$ is, so iteratedFDeriv of it is meaningful.
- The ℂ-normed space $\mathbb C^n$ is used as an ℝ-normed space through scalar restriction, which is the intended real derivative.
Quantifiers: $M$ is chosen after $n,k,p,R$ and before $c$ and $\varphi$ . Uniformity in $c$ is consistent by translation invariance. The statement is true. Since $\varphi$ and all its derivatives vanish outside $B$ , the norms over $B$ equal the norms over $\mathbb C$ . Calderón–Zygmund applied to $D^{j-1}\varphi$ (since $\bar\partial$ commutes with $D$ ) bounds $\|D^j\varphi\|_p$ by $\|D^{j-1}\bar\partial\varphi\|_p$ for $1\le j\le k$ , and Poincaré on $B_R$ handles $j=0$ .

Remarks. The norm uses the operator norm of $D^j$ rather than a sum over multi-indices, which is an equivalent norm (finite dimension, fixed $j$ ).

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 W^{k,p} estimate for the Cauchy–Riemann operator on a disc

Read-back: DbarRegularity.dbar_sobolev_estimate

Read-back: `DbarRegularity.dbar_sobolev_estimate`