The $L^p$ estimate for $\partial_s+J_0\partial_t$ on the cylinder $\mathbb R\times S^1$, up to a lower-order term

Let $1<p<\infty$ and $n\in\mathbb N$, and let $J_0=\begin{pmatrix}0&-\mathrm{Id}\\ \mathrm{Id}&0\end{pmatrix}$. There is a constant $A$ such that every continuously differentiable map $u:\mathbb R\times\mathbb R\to\mathbb R^{2n}$ which is $1$-periodic in the second variable, $u(s,t+1)=u(s,t)$, and vanishes for $|s|$ large satisfies

where all norms are taken over the cylinder $\mathbb R\times S^1$, i.e. over the strip $\mathbb R\times[0,1)$ with Lebesgue measure.

It is the $L^p$ estimate for the standard Cauchy–Riemann operator on the cylinder, the case $S=0$ of the local estimate for Cauchy–Riemann type operators $\partial_s+J_0\partial_t+S$ (Wendl, Proposition 4.8). The constant does not depend on the size of the support of $u$.

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$. Lebesgue measure on the strip is cylMeasure. Vanishing for large $|s|$ means: there is $R$ with $u(s,t)=0$ whenever $R<|s|$. The constant $A$ is chosen before $u$ (and before $R$).