Uniform interior $C^m$ bounds for $W^{1,p}$ -bounded pseudoholomorphic maps

Proved

JHolomorphic.bounded_iteratedFDeriv_of_sobolevNorm_le

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$ and 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

\sup_\nu\|u_\nu\|_{W^{1,p}(D)}<\infty.

Then for every compact $K\subset D$ and every $m\ge0$ there is $M$ with $\|D^mu_\nu(z)\|\le M$ for all $\nu$ and all $z\in K$ .

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 $W^{1,p}$ bound is sobolevNorm 1 (ENNReal.ofReal p) (ball 0 1) (u ν) ≤ C with C : ℝ≥0. The constant $M$ depends on $K$ and $m$ and is chosen before $\nu$ .

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 (2a) (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`, are uniformly bounded in
`W^{1,p}`, then on every compact subset of the disc every derivative `Dᵐ u_ν` is bounded
uniformly in `ν`. (Wendl takes `E = O = ℂⁿ`, where the `W^{1,p}` bound already confines the
images to a compact set.) -/
theorem bounded_iteratedFDeriv_of_sobolevNorm_le {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₀) (C : ℝ≥0)
    (hC : ∀ ν, sobolevNorm 1 (ENNReal.ofReal p) (ball 0 1) (u ν) ≤ C) :
    ∀ K ⊆ ball (0 : ℂ) 1, IsCompact K → ∀ m : ℕ,
      ∃ M : ℝ, ∀ ν, ∀ z ∈ K, ‖iteratedFDeriv ℝ m (u ν) z‖ ≤ M := 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 (2a), p. 35 (case k = 1)

Read-back

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

`JHolomorphic.bounded_iteratedFDeriv_of_sobolevNorm_le`

Setting. Let $E$ be a finite-dimensional real normed vector space (arbitrary norm; $E = \{0\}$ is allowed). Let $p$ be a real number with $p > 2$ . Write $\mathbb{D} = \{z \in \mathbb{C} : |z| < 1\}$ for the open unit disk in $\mathbb{C}$ , with Lebesgue measure on $\mathbb{C} \cong \mathbb{R}^2$ . The data are:

a map $J : E \to \mathcal{L}(E,E)$ (continuous $\mathbb{R}$ -linear endomorphisms of $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}$ ;
a constant $C \in [0,\infty)$ .

Hypotheses.

$J$ is almost complex on $O$ : $O$ is open in $E$ , $J$ is $C^\infty$ (over $\mathbb{R}$ ) on $O$ , and $J(x) \circ J(x) = -\mathrm{id}_E$ for every $x \in O$ .
Each $J_\nu$ is almost complex on $O$ , in the same sense: $O$ open, $J_\nu$ is $C^\infty$ on $O$ , and $J_\nu(x)^2 = -\mathrm{id}_E$ for all $x \in O$ .
$C^\infty_{\mathrm{loc}}$ convergence on $O$ : for every compact $K \subseteq O$ and every $m \in \mathbb{N}$ , the $m$ -th iterated Fréchet derivatives $D^m J_\nu$ converge to $D^m J$ uniformly on $K$ as $\nu \to \infty$ . (These are the derivatives of $J_\nu$ , $J$ viewed as maps on all of $E$ , evaluated at points of $K$ ; since $O$ is open they are the ordinary derivatives at those points.) For $m = 0$ this is uniform convergence $J_\nu \to J$ on $K$ .
$K_0$ is compact and $K_0 \subseteq O$ .
For every $\nu$ , $u_\nu$ is $C^\infty$ (as a map of the real 2-dimensional space $\mathbb{C}$ ) on $\mathbb{D}$ .
$u_\nu$ is $J_\nu$ -holomorphic on $\mathbb{D}$ : for every $\nu$ and every $z \in \mathbb{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,

i.e. $\partial_s u_\nu + J_\nu(u_\nu)\,\partial_t u_\nu = 0$ at $z = s + it$ . 7. For every $\nu$ , $u_\nu$ maps $\mathbb{D}$ into $K_0$ . 8. Uniform $W^{1,p}$ bound: for every $\nu$ ,

\|u_\nu\|_{L^p(\mathbb{D})} + \|Du_\nu\|_{L^p(\mathbb{D})} \le C,

where the left side is computed in $[0,\infty]$ as the sum over $j = 0, 1$ of the $L^p$ norms on $\mathbb{D}$ (Lebesgue measure restricted to $\mathbb{D}$ ) of $z \mapsto \|D^j u_\nu(z)\|$ ; for $j=0$ this is $\|u_\nu(z)\|_E$ , and for $j=1$ it is the operator norm of $Du_\nu(z) : \mathbb{C} \to E$ (with $\mathbb{C}$ carrying the norm $|\cdot|$ ). The exponent is $p$ itself (since $p > 2 > 0$ ). The inequality in particular forces both $L^p$ norms to be finite.

Conclusion. For every compact set $K \subseteq \mathbb{D}$ and every $m \in \mathbb{N}$ there is a real number $M$ (depending on $K$ and $m$ , but not on $\nu$ or $z$ ) such that

\big\|D^m u_\nu(z)\big\| \le M \qquad \text{for all } \nu \in \mathbb{N},\ z \in K,

where $D^m u_\nu(z)$ is the $m$ -th iterated real Fréchet derivative of $u_\nu$ at $z$ , a continuous $m$ -linear map $\mathbb{C}^m \to E$ , measured in the operator (multilinear) norm. For $m = 0$ this is a uniform bound on $\|u_\nu(z)\|$ over $K$ .

Remarks on edge cases.

If $K = \emptyset$ the conclusion is trivially true (any $M$ works).
If $O = \emptyset$ , then $K_0 = \emptyset$ , and hypothesis 7 cannot hold (the disk is nonempty), so the hypotheses are then unsatisfiable. More generally, hypothesis 7 requires $K_0 \neq \emptyset$ , hence $O \ne \emptyset$ .
If $E = \{0\}$ , every map $J$ satisfies $J(x)^2 = -\mathrm{id}$ (all maps are $0$ ), all hypotheses are satisfiable, and the conclusion is trivial. For $E \ne \{0\}$ and $O \ne \emptyset$ , hypothesis 1 forces $\dim_\mathbb{R} E$ to be even.
The behaviour of $J$ , $J_\nu$ off $O$ and of $u_\nu$ off $\mathbb{D}$ is unconstrained; only values on $O$ (resp. on and near points of $\mathbb{D}$ ) enter. The limit $J$ appears only in hypotheses 1 and 3; the conclusion does not mention $J$ , $O$ , $K_0$ , $p$ or $C$ .
The hypothesis $p > 2$ is strict; $p = 2$ is excluded.

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

Uniform interior CmC^mCm bounds for W1,pW^{1,p}W1,p-bounded pseudoholomorphic maps

JHolomorphic.bounded_iteratedFDeriv_of_sobolevNorm_le

Uniform interior $C^m$ bounds for $W^{1,p}$ -bounded pseudoholomorphic maps

`JHolomorphic.bounded_iteratedFDeriv_of_sobolevNorm_le`