Unique continuation for pseudoholomorphic maps

Proved

JHolomorphic.eventuallyEq_of_iteratedFDeriv_eq

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, let $J$ be a smooth almost complex structure on an open set $O\subseteq E$ , and let $D\subset\mathbb{C}$ be the open unit disc. If $u,v:D\to O$ are $C^\infty$ and $J$ -holomorphic, and all their derivatives of all orders (including order $0$ ) agree at $0$ , then $u=v$ on a neighbourhood of $0$ .

Formalization Note The hypotheses are ContDiffOn ℝ ∞, IsJHolomorphicOn J (ball 0 1) and Set.MapsTo _ (ball 0 1) O for $u$ and $v$ , and ∀ m, iteratedFDeriv ℝ m u 0 = iteratedFDeriv ℝ m v 0. Wendl takes $E=O=\mathbb{C}^n$ and $u(0)=v(0)=0$ . The conclusion is u =ᶠ[𝓝 0] v.

Preamble

import Definitions.Def_JHolomorphic_Setting

Formal statement

namespace JHolomorphic

open MeasureTheory Metric Filter Topology DbarRegularity
open scoped ContDiff ENNReal NNReal

/-- Wendl, Proposition 2.28 (p. 40): let `J` be a smooth almost complex structure on an open set
`O ⊆ E`. Two smooth `J`-holomorphic maps `u`, `v` on the open unit disc with values in `O` whose
derivatives of all orders (including order `0`) agree at `0` coincide on a neighbourhood
of `0`. -/
theorem eventuallyEq_of_iteratedFDeriv_eq {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    (J : E → E →L[ℝ] E) (O : Set E) (hJ : IsAlmostComplexOn J O) (u v : ℂ → E)
    (hu : ContDiffOn ℝ ∞ u (ball 0 1)) (hv : ContDiffOn ℝ ∞ v (ball 0 1))
    (huh : IsJHolomorphicOn J (ball 0 1) u) (hvh : IsJHolomorphicOn J (ball 0 1) v)
    (hum : Set.MapsTo u (ball 0 1) O) (hvm : Set.MapsTo v (ball 0 1) O)
    (hD : ∀ m : ℕ, iteratedFDeriv ℝ m u 0 = iteratedFDeriv ℝ m v 0) :
    u =ᶠ[𝓝 0] v := by
  sorry

end JHolomorphic

Source

C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Lecture 2, Proposition 2.28, p. 40

Read-back

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

`JHolomorphic.eventuallyEq_of_iteratedFDeriv_eq`

Setting. Let $E$ be a finite-dimensional real normed vector space (any dimension, including $\dim E = 0$ ). Let $J$ be an arbitrary map assigning to each point $x \in E$ a continuous real-linear map $J_x : E \to E$ , and let $O \subseteq E$ be a set. Let $u, v : \mathbb{C} \to E$ be arbitrary functions defined on all of $\mathbb{C}$ . Write $D = \{ z \in \mathbb{C} : |z| < 1 \}$ for the open unit disc centred at $0$ .

Hypotheses.

$(J, O)$ is an almost complex structure on $O$ : this unfolds to the conjunction of
- $O$ is open in $E$ ;
- $x \mapsto J_x$ is $C^\infty$ (real-smooth, as a map into the space of continuous linear maps $E \to E$ ) on $O$ ;
- for every $x \in O$ , $J_x \circ J_x = -\mathrm{id}_E$ .
Nothing is required of $J_x$ for $x \notin O$ .
$u$ is real $C^\infty$ on $D$ , and $v$ is real $C^\infty$ on $D$ (smoothness of the restriction to the open set $D$ ; nothing is assumed outside $D$ ).
$u$ is $J$ -holomorphic on $D$ : for every $z \in D$ , $u$ is real-differentiable at $z$ and

\bar\partial_J u(z) := Du(z)[1] + J_{u(z)}\big(Du(z)[i]\big) = 0,

where $Du(z) : \mathbb{C} \to E$ is the real Fréchet derivative of $u$ at $z$ . Writing $z = s + it$ , this is $\partial_s u(z) + J_{u(z)}\,\partial_t u(z) = 0$ . The same condition is assumed for $v$ on $D$ . 4. $u(D) \subseteq O$ and $v(D) \subseteq O$ . 5. For every natural number $m \ge 0$ , the $m$ -th iterated real Fréchet derivatives of $u$ and $v$ at $0$ coincide as symmetric $m$ -linear maps $\mathbb{C}^m \to E$ :

D^m u(0) = D^m v(0) \quad \text{for all } m \in \mathbb{N}.

Here $D^m u(0)$ is the iterated derivative of $u$ as a function on all of $\mathbb{C}$ (not a derivative within $D$ ); since $D$ is an open neighbourhood of $0$ and $u$ is smooth on it, these are the usual higher derivatives at $0$ . The case $m = 0$ says $u(0) = v(0)$ .

Conclusion. $u$ and $v$ agree on some neighbourhood of $0$ : there is an open set $V \ni 0$ in $\mathbb{C}$ with $u(z) = v(z)$ for all $z \in V$ . (No size of $V$ is asserted; in particular it is not asserted that $u = v$ on all of $D$ .)

Remarks on degenerate cases.

If $\dim_{\mathbb{R}} E$ is odd, no linear map $J_x$ with $J_x^2 = -\mathrm{id}$ exists, so the third clause of hypothesis 1 forces $O = \emptyset$ ; but hypothesis 4 requires $u(0) \in O$ (as $0 \in D$ ), so the hypotheses cannot all hold and the statement is vacuous. If $E = \{0\}$ , then $J_x = 0 = -\mathrm{id}_E$ is allowed and $u = v = 0$ trivially.
The real-differentiability clause in hypothesis 3 is already implied by hypothesis 2 on the open set $D$ .
Hypothesis 1 includes a smoothness assumption on $J$ only on $O$ ; the value $J_{u(z)}$ in hypothesis 3 is only ever evaluated at points of $O$ , by hypothesis 4.
The proof of the declaration is not part of this read-back; only the statement is rendered.

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