The $L^p$ estimate for $\partial_s+J_0\partial_t$ on compactly supported maps $\mathbb R^2\to\mathbb R^{2n}$

Let $1<p<\infty$ and $n\in\mathbb N$, and let $J_0=\begin{pmatrix}0&-\mathrm{Id}\\ \mathrm{Id}&0\end{pmatrix}$ be the standard complex structure on $\mathbb R^{2n}$. There is a constant $A$ such that every continuously differentiable map $v:\mathbb R^2\to\mathbb R^{2n}$ with compact support satisfies

where $(s,t)$ are the coordinates of $\mathbb R^2$ and the measure is Lebesgue measure.

This is the basic $L^p$ elliptic estimate for the Cauchy–Riemann operator $\partial_s+J_0\partial_t$ in real notation, in the form used for linear Cauchy–Riemann type operators on Riemann surfaces and cylinders (Wendl, Lecture 4).

Formalization Note. $\mathbb R^{2n}$ is EuclideanSpace ℝ (Fin n ⊕ Fin n), $J_0$ is Matrix.J, acting through Matrix.toEuclideanLin. Points of the plane are pairs $(s,t)\in\mathbb R\times\mathbb R$; $\partial_s v$ and $\partial_t v$ are partialS v x = fderiv ℝ v x (1, 0) and partialT v x = fderiv ℝ v x (0, 1). $C^1$ means ContDiff ℝ 1. Norms are eLpNorm with values in $[0,\infty]$, for an exponent p : ℝ≥0∞ with $1<p$ and $p\ne\infty$. The constant $A$ is chosen before $v$; the measure on $\mathbb R\times\mathbb R$ is volume.