A weakly $J$-holomorphic map is $J$-holomorphic, and $(u,\partial_s u)$ is weakly $J^T$-holomorphic

Let $p>2$, let $E$ be a finite-dimensional real normed space and let $J$ be a smooth almost complex structure on an open set $O\subseteq E$. Let $U\subseteq\mathbb{C}$ be open and let $u:U\to O$ be continuous, with $u\in W^{1,p}_{\mathrm{loc}}(U)$ and $\partial_su+J(u)\,\partial_tu=0$ almost everywhere on $U$ for its weak partial derivatives. Then:

1. $u$ is differentiable at every point of $U$ and $\partial_su+J(u)\,\partial_tu=0$ holds at every point of $U$ (classical derivatives);
2. the map $w(z)=(u(z),\partial_su(z))$ is continuous on $U$ with values in $O\times E$, lies in $W^{1,p}_{\mathrm{loc}}(U)$, and satisfies $\partial_sw+J^T(w)\,\partial_tw=0$ almost everywhere on $U$, where $J^T(x,y)(a,b)=\big(J(x)a,\;J(x)b+DJ(x)[y]\,a\big)$ is the tangent almost complex structure on $O\times E$.

Formalization Note The hypothesis is IsWeakJHolomorphicOn p J O U u. Conclusion 1 is IsJHolomorphicOn J U u; conclusion 2 is IsWeakJHolomorphicOn p J^T (O ×ˢ Set.univ) U (fun z => (u z, fderiv ℝ u z 1)), with $\partial_su(z)$ the classical derivative fderiv ℝ u z 1 and $J^T$ written inline as ((J x.1).comp fst).prod ((J x.1).comp snd + (fderiv ℝ J x.1 x.2).comp fst). $E\times E$ carries the product norm. As in Wendl, the case $E=\mathbb{C}^n$ on a disc is the classical one; here the domain is any open $U$ and $J$ is only defined on $O$.