The L² norm of the Cauchy–Riemann operator for maps into a complex Hilbert space

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$. Let $E$ be a complex Hilbert space. For every smooth compactly supported map $\varphi:\mathbb{C}\to E$,

with respect to Lebesgue measure on $\mathbb{C}$. This is the identity $\|\bar\partial\varphi\|_{L^2}^2=\|\varphi_s\|_{L^2}^2+\|\varphi_t\|_{L^2}^2$ for an arbitrary Hilbert-space target.

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 φ. $E$ is a complete complex inner product space (InnerProductSpace ℂ E, CompleteSpace E). Each squared 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.