The L² norm of the Cauchy–Riemann operator equals the L² norm of the gradient for compactly supported maps

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. For every smooth compactly supported map $\varphi:\mathbb{C}\to\mathbb{C}^n$,

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). Each squared $L^2$ norm is its own Bochner integral ∫ z, ‖·‖ ^ 2; the first integral on the right is parenthesized so that the two integrals are added, not nested. This statement replaces DbarRegularity.dbar_l2_identity, whose right-hand side lacked these parentheses and therefore read $\int_{\mathbb{C}}\big(\|\varphi_s\|^2+\mathrm{const}\big)$.