$C^1$ -bounded pseudoholomorphic discs have $C^\infty_{\mathrm{loc}}$ -convergent subsequences

Proved

JHolomorphic.exists_subseq_tendstoCInftyLocOn

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 $u_\nu:D\to K_0$ be $C^1$ maps with $\partial_su_\nu+J_\nu(u_\nu)\,\partial_tu_\nu=0$ on $D$ and

\sup_\nu\sup_{z\in D}\|Du_\nu(z)\|<\infty.

Then a subsequence $u_{\nu_k}$ converges in $C^\infty_{\mathrm{loc}}$ on $D$ to a $C^\infty$ map $v:D\to K_0$ with $\partial_sv+J(v)\,\partial_tv=0$ .

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 maps are ContDiffOn ℝ 1 on the disc (Wendl leaves the regularity class implicit), and the derivative bound is ‖fderiv ℝ (u ν) z‖ ≤ C for $z\in D$ . The subsequence is u ∘ φ for a StrictMono map $\mathbb{N}\to\mathbb{N}$ , and the limit satisfies ContDiffOn ℝ ∞, IsJHolomorphicOn J (ball 0 1) and Set.MapsTo v (ball 0 1) K₀.

Preamble

import Definitions.Def_JHolomorphic_Setting

Formal statement

namespace JHolomorphic

open MeasureTheory Metric Filter Topology DbarRegularity
open scoped ContDiff ENNReal NNReal

/-- Wendl, Proposition 9.1 (p. 151): let `J_ν → J` in `C^∞_loc` be smooth almost complex
structures on an open set `O ⊆ E`. Every sequence of `C¹` maps `u_ν` on the open unit disc that are
`J_ν`-holomorphic, take values in a fixed compact `K₀ ⊆ O` and have uniformly bounded first
derivative has a subsequence converging in `C^∞_loc` on the disc; the limit is a `C^∞`
`J`-holomorphic map with values in `K₀`. -/
theorem exists_subseq_tendstoCInftyLocOn {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    (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 ℝ 1 (u ν) (ball 0 1))
    (hhol : ∀ ν, IsJHolomorphicOn (Jν ν) (ball 0 1) (u ν))
    (hmaps : ∀ ν, Set.MapsTo (u ν) (ball 0 1) K₀) (C : ℝ)
    (hC : ∀ ν, ∀ z ∈ ball (0 : ℂ) 1, ‖fderiv ℝ (u ν) z‖ ≤ C) :
    ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∃ v : ℂ → E, ContDiffOn ℝ ∞ v (ball 0 1) ∧
      IsJHolomorphicOn J (ball 0 1) v ∧ Set.MapsTo v (ball 0 1) K₀ ∧
      TendstoCInftyLocOn (fun ν => 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 9, Proposition 9.1, p. 151

Read-back

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

`JHolomorphic.exists_subseq_tendstoCInftyLocOn`

Setting. Let $E$ be a finite-dimensional real normed vector space, and write $\mathcal L(E)$ for the continuous $\mathbb R$ -linear maps $E \to E$ . Let $D = \{ z \in \mathbb C : |z| < 1 \}$ be the open unit disc in $\mathbb C$ , viewed as a real 2-dimensional space with real basis $1, i$ . The data are:

a map $J : E \to \mathcal L(E)$ and a sequence of maps $J_\nu : E \to \mathcal L(E)$ , $\nu \in \mathbb N = \{0,1,2,\dots\}$ ;
two subsets $O, K_0 \subseteq E$ ;
a sequence of maps $u_\nu : \mathbb C \to E$ , $\nu \in \mathbb N$ ;
a real number $C$ .

Definitions used (expanded).

Almost complex on $O$ . A map $A : E \to \mathcal L(E)$ is "almost complex on $O$ " iff (i) $O$ is open in $E$ , (ii) $A$ is $C^\infty$ (infinitely often real-differentiable, smoothness order $\infty$ , not analyticity) on $O$ , and (iii) $A(x) \circ A(x) = -\mathrm{id}_E$ for every $x \in O$ .
$\bar\partial_A$ operator. For $A : E \to \mathcal L(E)$ , $w : \mathbb C \to E$ and $z \in \mathbb C$ ,

\bar\partial_A w(z) = Dw(z)[1] + A\big(w(z)\big)\big(Dw(z)[i]\big),

where $Dw(z)$ is the real Fréchet derivative of $w$ at $z$ (by convention the zero map if $w$ is not differentiable at $z$ ). Writing $z = s + it$ this is $\partial_s w + A(w)\,\partial_t w$ .

$A$ -holomorphic on $U$ . $w$ is " $A$ -holomorphic on $U \subseteq \mathbb C$ " iff for every $z \in U$ , $w$ is real-differentiable at $z$ and $\bar\partial_A w(z) = 0$ .
$C^\infty_{\mathrm{loc}}$ convergence on $S$ . For normed real spaces $X, Y$ , maps $f_\nu, g : X \to Y$ and $S \subseteq X$ , " $f_\nu \to g$ in $C^\infty_{\mathrm{loc}}$ on $S$ " means: for every compact $K \subseteq S$ and every $m \in \mathbb N$ , $D^m f_\nu \to D^m g$ uniformly on $K$ as $\nu \to \infty$ (with respect to the operator norm on $m$ -multilinear maps). Here $D^m$ is the $m$ -th iterated Fréchet derivative taken on the whole space $X$ ( $D^0 f = f$ ); at any point where a lower-order derivative is not differentiable, the next derivative is by convention $0$ . In particular $m = 0$ requires uniform convergence of the functions themselves on $K$ .

Hypotheses.

$J$ is almost complex on $O$ (so in particular $O$ is open).
For every $\nu$ , $J_\nu$ is almost complex on $O$ .
$J_\nu \to J$ in $C^\infty_{\mathrm{loc}}$ on $O$ (in the sense above, with $X = E$ , $Y = \mathcal L(E)$ ).
$K_0$ is compact and $K_0 \subseteq O$ .
For every $\nu$ , $u_\nu$ is $C^1$ (real) on $D$ .
For every $\nu$ , $u_\nu$ is $J_\nu$ -holomorphic on $D$ : for all $z \in D$ , $u_\nu$ is differentiable at $z$ and

Du_\nu(z)[1] + J_\nu\big(u_\nu(z)\big)\big(Du_\nu(z)[i]\big) = 0.

For every $\nu$ , $u_\nu(D) \subseteq K_0$ .
For every $\nu$ and every $z \in D$ , $\|Du_\nu(z)\| \le C$ (operator norm of the real derivative $\mathbb C \to E$ ).

Conclusion. There exist a strictly increasing map $\varphi : \mathbb N \to \mathbb N$ and a map $v : \mathbb C \to E$ such that

$v$ is $C^\infty$ on $D$ ;
$v$ is $J$ -holomorphic on $D$ , i.e. for every $z \in D$ , $v$ is differentiable at $z$ and $Dv(z)[1] + J(v(z))(Dv(z)[i]) = 0$ ;
$v(D) \subseteq K_0$ ;
$u_{\varphi(\nu)} \to v$ in $C^\infty_{\mathrm{loc}}$ on $D$ : for every compact $K \subseteq D$ and every $m \in \mathbb N$ ,

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

Remarks on edge cases (literal content).

The values of $J$ , $J_\nu$ , $u_\nu$ , $v$ outside $O$ resp. $D$ are unconstrained; only their behaviour on $O$ resp. $D$ enters, except that $D^m$ is the global derivative (on the open sets $O$ and $D$ this agrees with the derivative of the restriction).
The hypotheses give only $C^1$ regularity of $u_\nu$ on $D$ ; for $m \ge 2$ the objects $D^m u_{\varphi(\nu)}$ in the conclusion are the global iterated derivatives as defined above, which take the conventional value $0$ at points where $D^{m-1}u_{\varphi(\nu)}$ is not differentiable.
If $C < 0$ , hypothesis 8 cannot hold (since $D \neq \emptyset$ and norms are $\ge 0$ ), and the statement is vacuously true. If $K_0 = \emptyset$ , hypothesis 7 cannot hold (since $D \ne \emptyset$ ), and the statement is again vacuous. If $E = \{0\}$ , then $\mathrm{id}_E = 0 = -\mathrm{id}_E$ , so the almost-complex condition (iii) holds for every $J$ .
The theorem does not assert uniqueness of $v$ or of $\varphi$ , and does not relate $v$ to the full sequence $(u_\nu)$ , only to the subsequence $(u_{\varphi(\nu)})$ .

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

C1C^1C1-bounded pseudoholomorphic discs have Cloc∞C^\infty_{\mathrm{loc}}Cloc∞​-convergent subsequences

JHolomorphic.exists_subseq_tendstoCInftyLocOn

$C^1$ -bounded pseudoholomorphic discs have $C^\infty_{\mathrm{loc}}$ -convergent subsequences

`JHolomorphic.exists_subseq_tendstoCInftyLocOn`