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

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

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 (for $R\le 0$ this forces $\varphi=0$). Each squared $L^2$ norm is its own Bochner integral ∫ z, ‖·‖ ^ 2; the three integrals on the left are parenthesized so that they are added, not nested. This statement replaces DbarRegularity.dbar_l2_estimate, whose left-hand side lacked these parentheses.