Pseudoholomorphic maps converging in $W^{1,p}$ converge in $C^\infty_{\mathrm{loc}}$

Proved

JHolomorphic.tendstoCInftyLocOn_of_sobolevNorm_tendsto

by Mazecto · Oct 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

elliptic-regularitypseudoholomorphic-curvessobolev-spacessymplectic-geometryunique-continuation

Let $E$ be a finite-dimensional real vector space, $O\subseteq E$ open, and let $J_\nu$ , $J$ be smooth almost complex structures on $O$ with $J_\nu\to J$ in $C^\infty_{\mathrm{loc}}$ on $O$ . Let $K_0\subseteq O$ be compact and let $D\subset\mathbb{C}$ be the open unit disc. Let $p>2$ , let $u_\nu:D\to K_0$ be $C^\infty$ maps with $\partial_su_\nu+J_\nu(u_\nu)\,\partial_tu_\nu=0$ on $D$ , and let $v$ be $C^\infty$ on $D$ . If $\|u_\nu-v\|_{W^{1,p}(D)}\to0$ , then $u_\nu\to v$ in $C^\infty_{\mathrm{loc}}$ on $D$ .

Formalization Note The hypotheses on the structures are IsAlmostComplexOn J O, ∀ ν, IsAlmostComplexOn (Jν ν) O and TendstoCInftyLocOn Jν J O. Because $J$ is only defined on $O$ , the maps are required to take values in the fixed compact set $K_0\subseteq O$ (Set.MapsTo (u ν) (ball 0 1) K₀). The convergence hypothesis is Tendsto (fun ν => sobolevNorm 1 (ENNReal.ofReal p) (ball 0 1) (u ν - v)) atTop (𝓝 0); the conclusion is TendstoCInftyLocOn u v (ball 0 1).

Preamble

import Definitions.Def_JHolomorphic_Setting

Formal statement

namespace JHolomorphic

open MeasureTheory Metric Filter Topology DbarRegularity
open scoped ContDiff ENNReal NNReal

/-- Wendl, Theorem 2.22 (2b) (p. 35), case `k = 1`: let `p > 2` and let `J_ν → J` in `C^∞_loc`
be smooth almost complex structures on an open set `O ⊆ E`. If smooth `J_ν`-holomorphic maps
`u_ν` on the open unit disc, with values in a fixed compact `K₀ ⊆ O`, converge in `W^{1,p}` to a
smooth map `u`, then `u_ν → u` in `C^∞_loc` on the disc. -/
theorem tendstoCInftyLocOn_of_sobolevNorm_tendsto {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (p : ℝ) (hp : 2 < p)
    (J : E → E →L[ℝ] E) (Jν : ℕ → E → E →L[ℝ] E) (O K₀ : Set E)
    (hJ : IsAlmostComplexOn J O) (hJν : ∀ ν, IsAlmostComplexOn (Jν ν) O)
    (hconv : TendstoCInftyLocOn Jν J O) (hK₀ : IsCompact K₀) (hK₀O : K₀ ⊆ O)
    (u : ℕ → ℂ → E) (hu : ∀ ν, ContDiffOn ℝ ∞ (u ν) (ball 0 1))
    (hhol : ∀ ν, IsJHolomorphicOn (Jν ν) (ball 0 1) (u ν))
    (hmaps : ∀ ν, Set.MapsTo (u ν) (ball 0 1) K₀) (v : ℂ → E)
    (hv : ContDiffOn ℝ ∞ v (ball 0 1))
    (hlim : Tendsto (fun ν => sobolevNorm 1 (ENNReal.ofReal p) (ball 0 1) (u ν - v)) atTop
      (𝓝 0)) :
    TendstoCInftyLocOn u v (ball 0 1) := by
  sorry

end JHolomorphic

Source

C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Lecture 2, Theorem 2.22 (2b), p. 35 (case k = 1)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

`JHolomorphic.tendstoCInftyLocOn_of_sobolevNorm_tendsto`

Setting. Let $E$ be a finite-dimensional real normed vector space (any dimension, including $\dim E = 0$ ), with its given norm. Let $D = \{z \in \mathbb{C} : |z| < 1\}$ be the open unit disc in $\mathbb{C}$ , where $\mathbb{C}$ is regarded as the real plane $\mathbb{R}^2$ with Lebesgue measure and all derivatives below are real Fréchet derivatives. For a map $f$ , $D^m f(x)$ denotes the $m$ -th iterated Fréchet derivative of $f$ at $x$ (an $m$ -linear map; $D^0 f(x)$ is $f(x)$ itself), computed for $f$ as a map on its whole domain, and normed by the operator norm of multilinear maps built from the given norms.

Data (all universally quantified).

A real number $p$ with $p > 2$ (strict).
A map $J : E \to \mathcal{L}(E,E)$ (continuous real-linear operators on $E$ ) and a sequence of such maps $J_\nu : E \to \mathcal{L}(E,E)$ , $\nu \in \mathbb{N}$ .
Two subsets $O, K_0 \subseteq E$ .
A sequence of maps $u_\nu : \mathbb{C} \to E$ , $\nu \in \mathbb{N}$ , and a map $v : \mathbb{C} \to E$ .

Hypotheses.

$J$ is almost complex on $O$ : $O$ is open, $J$ is $C^\infty$ on $O$ , and $J(x) \circ J(x) = -\mathrm{id}_E$ for every $x \in O$ .
Each $J_\nu$ is almost complex on $O$ : for every $\nu$ , $J_\nu$ is $C^\infty$ on $O$ and $J_\nu(x) \circ J_\nu(x) = -\mathrm{id}_E$ for every $x \in O$ (openness of $O$ is restated).
$J_\nu \to J$ in $C^\infty_{\mathrm{loc}}$ on $O$ : for every compact $K \subseteq O$ and every $m \in \mathbb{N}$ (including $m = 0$ ),

\sup_{x \in K} \big\| D^m J_\nu(x) - D^m J(x) \big\| \longrightarrow 0 \quad (\nu \to \infty),

i.e. $D^m J_\nu \to D^m J$ uniformly on $K$ . 4. $K_0$ is compact and $K_0 \subseteq O$ . 5. For every $\nu$ , $u_\nu$ is $C^\infty$ on $D$ . 6. Each $u_\nu$ is $J_\nu$ -holomorphic on $D$ : for every $\nu$ and every $z \in D$ , $u_\nu$ is (real) differentiable at $z$ and

Du_\nu(z)\,1 + J_\nu\big(u_\nu(z)\big)\big(Du_\nu(z)\,i\big) = 0,

that is, writing $z = s + it$ , $\partial_s u_\nu + J_\nu(u_\nu)\,\partial_t u_\nu = 0$ at $z$ . 7. For every $\nu$ , $u_\nu$ maps $D$ into $K_0$ . 8. $v$ is $C^\infty$ on $D$ . (No other condition is imposed on $v$ : it is not assumed to take values in $O$ or $K_0$ , nor to satisfy any holomorphicity equation.) 9. $W^{1,p}$ convergence on $D$ :

\|u_\nu - v\|_{L^p(D)} + \big\|D(u_\nu - v)\big\|_{L^p(D)} \longrightarrow 0 \quad (\nu \to \infty),

where $\|g\|_{L^p(D)} = \big(\int_D \|g(z)\|^p \, dz\big)^{1/p} \in [0, \infty]$ with Lebesgue measure on $D$ , the second term uses the operator norm of the derivative $D(u_\nu - v)(z) \in \mathcal{L}(\mathbb{C}, E)$ , and the sum is taken in $[0,\infty]$ . Convergence to $0$ in $[0,\infty]$ means that the sum is finite for all large $\nu$ and tends to $0$ ; nothing is assumed about finiteness for small $\nu$ .

Conclusion. $u_\nu \to v$ in $C^\infty_{\mathrm{loc}}$ on $D$ : for every compact $K \subseteq D$ and every $m \in \mathbb{N}$ (including $m = 0$ , i.e. uniform convergence $u_\nu \to v$ on $K$ ),

\sup_{z \in K} \big\| D^m u_\nu(z) - D^m v(z) \big\| \longrightarrow 0 \quad (\nu \to \infty).

Remarks on edge cases.

Hypothesis 7 together with $D \neq \emptyset$ forces $K_0 \neq \emptyset$ , hence $O \neq \emptyset$ . A linear map with $A \circ A = -\mathrm{id}_E$ exists only when $\dim E$ is even (including $0$ ), so for odd $\dim E$ the hypotheses are jointly unsatisfiable and the statement holds vacuously. For $\dim E = 0$ every condition on $J, J_\nu$ holds trivially and all maps into $E$ are constant $0$ .
The limit structure $J$ enters only through hypotheses 1 and 3; it does not appear in the conclusion. No relation between $v$ and $J$ is assumed.
The number $p$ enters only through hypothesis 9 (via the $L^p$ norms) and the condition $p > 2$ .
Since $D$ is open, $K \subseteq D$ , and the measure in hypothesis 9 is restricted to $D$ , the iterated derivatives in the conclusion and in hypothesis 9 are evaluated only at points of $D$ , where $u_\nu$ and $v$ are $C^\infty$ ; values of $u_\nu$ , $v$ outside $D$ play no role in the $L^p$ norms (the boundary circle has measure zero and is not in $D$ ).

Human review

Endorsed by Shuze Chen · Oct 21, 2026
Confirmed by the moderator at approval.
Endorsed by Mazecto · Oct 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Pseudoholomorphic maps converging in W1,pW^{1,p}W1,p converge in Cloc∞C^\infty_{\mathrm{loc}}Cloc∞​

JHolomorphic.tendstoCInftyLocOn_of_sobolevNorm_tendsto

Pseudoholomorphic maps converging in $W^{1,p}$ converge in $C^\infty_{\mathrm{loc}}$

`JHolomorphic.tendstoCInftyLocOn_of_sobolevNorm_tendsto`