Removal of singularities for pseudoholomorphic maps of finite energy

Proved

FiniteEnergyPlane.exists_extension_of_energy_lt_top

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

finite-energypseudoholomorphic-curvesreeb-dynamicssymplectic-geometrysymplectization

Let $E$ be a finite-dimensional real normed space, $J$ a smooth almost complex structure on an open set $O\subseteq E$ , and $K\subseteq O$ compact. Let $D\subset\mathbb{C}$ be the open unit disc and $u$ a $C^\infty$ $J$ -holomorphic map on $D\setminus\{0\}$ with $u(D\setminus\{0\})\subseteq K$ and

\int_{D\setminus\{0\}}\|Du(z)\|^2\,dz<\infty.

Then there is a $C^\infty$ $J$ -holomorphic map $v$ on $D$ with $v(D)\subseteq K$ and $v=u$ on $D\setminus\{0\}$ .

Formalization Note The energy is a lower integral in ℝ≥0∞ of the squared operator norm. Wendl and Zinger assume a compact target manifold (or a compact image); here the image lies in a compact subset $K$ of the domain $O$ of $J$ .

Preamble

import Definitions.Def_FiniteEnergyPlane_Setting

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- Removal of singularities: Zinger, *Notes on J-holomorphic maps*, Proposition 5.1; Wendl,
Theorem 9.2 (p. 152). Let `J` be a smooth almost complex structure on an open set `O ⊆ E` and
`K ⊆ O` compact. A smooth `J`-holomorphic map on the punctured unit disc with values in `K` and
finite Dirichlet energy `∫ ‖Du‖²` extends to a smooth `J`-holomorphic map on the disc with values
in `K`. (Zinger assumes the target manifold compact; here the image lies in a compact `K ⊆ O`.) -/
theorem exists_extension_of_energy_lt_top {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (J : E → E →L[ℝ] E) (O : Set E)
    (hJ : JHolomorphic.IsAlmostComplexOn J O) (K : Set E) (hK : IsCompact K) (hKO : K ⊆ O)
    (u : ℂ → E) (hu : ContDiffOn ℝ ∞ u (ball 0 1 \ {0}))
    (hhol : JHolomorphic.IsJHolomorphicOn J (ball 0 1 \ {0}) u)
    (hmaps : Set.MapsTo u (ball 0 1 \ {0}) K)
    (hE : ∫⁻ z in ball 0 1 \ {0}, ENNReal.ofReal (‖fderiv ℝ u z‖ ^ 2) < ⊤) :
    ∃ v : ℂ → E, ContDiffOn ℝ ∞ v (ball 0 1) ∧ JHolomorphic.IsJHolomorphicOn J (ball 0 1) v ∧
      Set.MapsTo v (ball 0 1) K ∧ ∀ z ∈ ball (0 : ℂ) 1, z ≠ 0 → v z = u z := by
  sorry

end FiniteEnergyPlane

Source

C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Theorem 9.2, p. 152; A. Zinger, Notes on J-holomorphic maps, arXiv:1706.00331, Proposition 5.1

Read-back

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

Read-back: `FiniteEnergyPlane.exists_extension_of_energy_lt_top`

Data. Let $E$ be a finite-dimensional real normed vector space (any norm). Let $J : E \to \mathcal L(E)$ assign to each $x \in E$ a continuous $\mathbb R$ -linear map $J_x : E \to E$ , and let $O \subseteq E$ be such that

$O$ is open,
$x \mapsto J_x$ is $C^\infty$ on $O$ ,
$J_x \circ J_x = -\mathrm{id}_E$ for every $x \in O$ .

Nothing is assumed about $J_x$ for $x \notin O$ . Let $K \subseteq E$ be compact with $K \subseteq O$ . Write $D = \{ z \in \mathbb C : |z| < 1\}$ for the open unit disk and $D^* = D \setminus \{0\}$ for the punctured disk. Let $u : \mathbb C \to E$ be a map (its values at $0$ and outside $D$ play no role in the hypotheses) such that:

$u$ is $C^\infty$ on $D^*$ (as a map of $\mathbb C \cong \mathbb R^2$ );
$u$ is $J$ -holomorphic on $D^*$ : for every $z \in D^*$ , $u$ is real-differentiable at $z$ and

\partial_s u(z) + J_{u(z)}\,\partial_t u(z) = 0, \qquad \partial_s u(z) = Du(z)\cdot 1,\quad \partial_t u(z) = Du(z)\cdot i;

$u(D^*) \subseteq K$ ;
the energy is finite:

\int_{D^*} \|Du(z)\|^2\, dz < \infty,

the Lebesgue integral (in $[0,\infty]$ ) over $D^*$ with respect to area measure, where $\|Du(z)\|$ is the operator norm of the real derivative $Du(z) : \mathbb C \to E$ ( $\mathbb C$ normed by the modulus).

Conclusion. There exists a map $v : \mathbb C \to E$ such that

$v$ is $C^\infty$ on the full disk $D$ ;
$v$ is $J$ -holomorphic on $D$ (for every $z \in D$ , including $z = 0$ : $v$ is real-differentiable at $z$ and $\partial_s v(z) + J_{v(z)}\,\partial_t v(z) = 0$ );
$v(D) \subseteq K$ (in particular $v(0) \in K$ );
$v(z) = u(z)$ for every $z \in D$ with $z \neq 0$ .

Nothing is asserted about $v$ outside $D$ , and $v(0)$ need not equal $u(0)$ .

Remarks on edge cases. If $K$ is empty, hypothesis 3 cannot hold (since $D^*$ is nonempty), so the statement is vacuous. If $E$ has odd positive dimension, $J_x^2 = -\mathrm{id}$ is impossible on a nonempty set, so $O = K = \emptyset$ and again the statement is vacuous. If $E = \{0\}$ , all hypotheses on $J$ hold trivially and the conclusion is satisfied by the zero map.

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

Removal of singularities for pseudoholomorphic maps of finite energy

Read-back: FiniteEnergyPlane.exists_extension_of_energy_lt_top

Read-back: `FiniteEnergyPlane.exists_extension_of_energy_lt_top`