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

Open

DbarRegularity.dbar_l2_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 $R>0$ and let $\varphi:\mathbb{C}\to\mathbb{C}^n$ be smooth with compact support in the open disc $B_R(0)$ . Then

\|\varphi_s\|_{L^2}^2+\|\varphi_t\|_{L^2}^2+\|\varphi\|_{L^2}^2\le(4R^2+1)\,\|\bar\partial\varphi\|_{L^2}^2 .

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 squared norms are the Bochner integrals ∫ z, ‖·‖ ^ 2.

Retired (2026-10-12). As formalized, the three integrals on the left nest (∫ z, (A + ∫ w, (B + ∫ u, C))), so the statement is weaker than intended. The corrected statement is DbarRegularity.dbar_l2_bound.

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.1
(p. 101): for a smooth `φ : ℂ → ℂⁿ` with compact support in the open disc `B_R(0)`,
`‖φ_s‖²_{L²} + ‖φ_t‖²_{L²} + ‖φ‖²_{L²} ≤ (4R² + 1) ‖∂̄φ‖²_{L²}`, where `z = s + i t`. -/
theorem dbar_l2_estimate {n : ℕ} (R : ℝ) (φ : ℂ → EuclideanSpace ℂ (Fin n))
    (hφ : ContDiff ℝ ∞ φ) (hsupp : tsupport φ ⊆ ball 0 R) :
    ∫ z, ‖fderiv ℝ φ z 1‖ ^ 2 + ∫ z, ‖fderiv ℝ φ z Complex.I‖ ^ 2 + ∫ z, ‖φ z‖ ^ 2
      ≤ (4 * R ^ 2 + 1) * ∫ z, ‖dbar φ z‖ ^ 2 := 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.1, p. 101

Read-back

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

Read-back: `DbarRegularity.dbar_l2_estimate`

Setting. $n\in\mathbb N$ , $R\in\mathbb R$ , $\varphi:\mathbb C\to\mathbb C^n$ , $z=s+it$ , Lebesgue measure on $\mathbb C$ .

Hypotheses. $\varphi\in C^\infty$ over $\mathbb R$ , and $\operatorname{tsupport}\varphi$ (the closure of $\{\varphi\ne0\}$ ) is contained in the open disc $B_R(0)$ . There is no hypothesis on the sign of $R$ .

Definitions used. $\varphi_s$ = fderiv ℝ φ z 1, $\varphi_t$ = fderiv ℝ φ z Complex.I, $\bar\partial\varphi=\varphi_s+i\varphi_t$ (dbar).

Conclusion.

\int|\varphi_s|^2+\int|\varphi_t|^2+\int|\varphi|^2\le(4R^2+1)\int|\bar\partial\varphi|^2 .

Degenerate cases. If $R\le0$ , the disc is empty, so $\varphi\equiv0$ and the inequality reads $0\le0$ . This is harmless. $n=0$ is trivial.

Soundness checks.

Lean defaults. ∞ means $C^\infty$ , not analytic (see the ContDiff scoped notation), so the statement is not vacuous. Since $\operatorname{tsupport}\varphi$ is closed and contained in a bounded set in $\mathbb C$ , it is compact. All integrands are therefore continuous with compact support and integrable, and no Bochner integral defaults to 0. Directional derivatives along $1$ and $i$ are $\partial_s$ and $\partial_t$ . There is no rpow, toReal or ℕ subtraction, and the constant $4R^2+1$ is a finite real.
There is no existential constant; the explicit constant depends only on $R$ . The statement is true. By the $L^2$ identity, $\int|\varphi_s|^2+\int|\varphi_t|^2=\int|\bar\partial\varphi|^2$ . The Poincaré inequality on a disc (or on an interval of length $2R$ in $s$ ) gives $\int|\varphi|^2\le c R^2\int|\nabla\varphi|^2$ with $c=(2/\pi)^2\le4$ , so $\int|\varphi|^2\le4R^2\int|\bar\partial\varphi|^2$ .

Remarks. The support condition uses tsupport, which is stronger than "support in the closed disc" and matches "compact support inside the open disc".

Verdict: no mis-formalization observed

View graph

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

Read-back: DbarRegularity.dbar_l2_estimate

Read-back: `DbarRegularity.dbar_l2_estimate`