Finite-energy cylinders with vanishing $d\lambda$ -energy are trivial cylinders

Proved

FiniteEnergyPlane.eq_trivialCylinder_of_dlambdaEnergy_eq_zero

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

finite-energypseudoholomorphic-curvesreeb-dynamicssymplectic-geometrysymplectization

Let $S=H^{-1}(1)$ be a strictly star-shaped level, $J$ a smooth $d\lambda_0$ -compatible complex structure on $\xi$ , and $u$ a nonconstant finite-energy $\tilde J$ -holomorphic curve on $\mathbb{C}\setminus\{0\}$ with $\int_{\mathbb{C}\setminus\{0\}}u^*d\lambda_0=0$ . Then there are a periodic Reeb orbit $P$ , an integer $k\neq0$ and $c\in\mathbb{C}\setminus\{0\}$ with

u(z)=F_P(c\,z^k)\qquad\text{for all }z\neq0.

Formalization Note The cylinder $\mathbb{R}\times S^1$ is $\mathbb{C}\setminus\{0\}$ , $(s,t)\mapsto e^{2\pi(s+it)}$ ; Wendl's "biholomorphically equivalent to a trivial cylinder over a closed Reeb orbit" is the explicit form $F_P(cz^k)$ , with $F_P$ as in the setting and $z^k$ an integer power. Wendl's lemma also covers the plane and general stable Hamiltonian structures; this item is the cylinder case in the symplectization of a star-shaped level.

Preamble

import Definitions.Def_FiniteEnergyPlane_Setting

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- Wendl, Lemma 9.9 (p. 158), cylinder case. A nonconstant finite-energy `J̃`-holomorphic
cylinder `u : ℂ \ {0} → V n \ {0}` with vanishing `dλ`-energy is a trivial cylinder: there are a
periodic Reeb orbit `P`, an integer `k ≠ 0` and `c ≠ 0` with `u(z) = F_P(c zᵏ)`. (The cylinder
`ℝ × S¹` is `ℂ \ {0}` by `e^{2π(s+it)}`; `F_P(w) = |w|^{T/π} x(T arg w / 2π)` in the coordinate
`y = e^{2a} x`.) -/
theorem eq_trivialCylinder_of_dlambdaEnergy_eq_zero {n : ℕ} (H : V n → ℝ) (hH : IsStrictlyStarShapedLevel H)
    (J : V n → V n →L[ℝ] V n) (hJ : IsCompatibleXiStructure H J) (u : ℂ → V n)
    (hu : IsFiniteEnergyCurve H J {z | z ≠ 0} u)
    (hnc : ∃ z₁ : ℂ, z₁ ≠ 0 ∧ ∃ z₂ : ℂ, z₂ ≠ 0 ∧ u z₁ ≠ u z₂)
    (hzero : dlambdaEnergy H {z | z ≠ 0} u = 0) :
    ∃ P : ReebOrbit H, ∃ k : ℤ, k ≠ 0 ∧ ∃ c : ℂ, c ≠ 0 ∧
      ∀ z : ℂ, z ≠ 0 → u z = trivialCylinder P (c * z ^ k) := by
  sorry

end FiniteEnergyPlane

Source

C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Lemma 9.9, p. 158 (case of the cylinder)

Read-back

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

FiniteEnergyPlane.eq_trivialCylinder_of_dlambdaEnergy_eq_zero

Statement. Let $n \in \mathbb{N}$ , $H : V \to \mathbb{R}$ satisfying the star-shaped level conditions, and $J$ a compatible structure (both defined below). Let $u : \mathbb{C} \to V$ be such that:

$u$ is a finite-energy curve on the punctured plane $\mathbb{C} \setminus \{0\}$ (as defined below, with respect to $H$ and $J$ );
$u$ is non-constant on $\mathbb{C} \setminus \{0\}$ : there are $z_1 \neq 0$ and $z_2 \neq 0$ with $u(z_1) \neq u(z_2)$ ;
$E_{d\lambda}(\mathbb{C} \setminus \{0\}, u) = 0$ .

Then there exist a Reeb orbit $P$ (with no condition on its period $T_P$ ), an integer $k \in \mathbb{Z}$ with $k \neq 0$ (either sign allowed; $z^k$ is the integer power, so $z^{k} = (z^{-1})^{|k|}$ for $k < 0$ ), and a complex number $c \neq 0$ , such that

u(z) = \mathrm{Cyl}_P\big(c\, z^{k}\big) \quad \text{for every } z \in \mathbb{C} \setminus \{0\}.

No hypothesis is made on the behaviour of $a \circ u$ near $0$ or near $\infty$ , and nothing is asserted about $u(0)$ .

Setting and notation (all definitions unfolded)

Throughout, $n \in \mathbb{N}$ is arbitrary (including $n = 0$ ) and $V = \mathbb{R}^{2(n+1)}$ , with coordinates indexed $0, 1, \dots, 2n+1$ .

Standard structure. $j_0 : V \to V$ is $(j_0 v)_k = -v_{k+1}$ for $k$ even and $(j_0 v)_k = v_{k-1}$ for $k$ odd. With the Euclidean dot product $\langle u, v\rangle = \sum_k u_k v_k$ , set $\omega_0(u, v) = \langle j_0 u, v\rangle$ and $\lambda_x(v) = \tfrac12\,\omega_0(x, v)$ .
Hamiltonian data. For $H : V \to \mathbb{R}$ : $\nabla H(x)$ is the vector of partial derivatives $dH_x(e_k)$ ; $X_H(x) = j_0 \nabla H(x)$ ; $S = \{x : H(x) = 1\}$ ; the "Reeb field" is $R(x) = \lambda_x(X_H(x))^{-1}\, X_H(x)$ , where the inverse of $0$ is taken to be $0$ . Derivatives are Fréchet derivatives, with the convention that the derivative of a non-differentiable map at a point is $0$ .
Star-shaped level (hypothesis $hH$ ): $H$ is $C^\infty$ ; for every $u \neq 0$ there is a unique $r > 0$ with $H(ru) = 1$ ; and $dH_x(x) > 0$ for every $x$ with $H(x) = 1$ .
Compatible structure (hypothesis $hJ$ ): $J : V \to \mathrm{End}_{\mathbb{R}}(V)$ is $C^\infty$ , and for every $x \in S$ and all $v, w$ in $\xi_x = \{v : \lambda_x(v) = 0,\ dH_x(v) = 0\}$ : $J(x)v \in \xi_x$ , $J(x)J(x)v = -v$ , $\omega_0(v, J(x)v) > 0$ if $v \neq 0$ , and $\omega_0(J(x)v, J(x)w) = \omega_0(v, w)$ . Nothing is required of $J(x)$ off $\xi_x$ or for $x \notin S$ .
Radial coordinates. $\rho(y)$ is a chosen $r > 0$ with $H(ry) = 1$ if one exists, and $\rho(y) = 1$ otherwise (under $hH$ , for $y \ne 0$ it is the unique such $r$ ). Then $\pi_S(y) = \rho(y)\, y$ and $a(y) = -\tfrac12 \log \rho(y)$ , so $y = e^{2a(y)}\pi_S(y)$ when $\rho(y)$ is that $r$ .
Almost complex structure $\tilde J$ . For $y \in V$ put $x = \pi_S(y)$ , $r = \rho(y)$ , $\alpha(v) = \dfrac{r}{2\, dH_x(x)}\, dH_x(v)$ , $\beta(v) = r\,\lambda_x(v)$ , $w(v) = v - 2\alpha(v)\, y - \beta(v)\, r^{-1} R(x)$ , and

\tilde J(y)v = \alpha(v)\, r^{-1} R(x) - 2\beta(v)\, y + J(x)\, w(v).

Derivatives of maps $f$ on $\mathbb{C} = \mathbb{R}^2 \ni z = s + it$ . $\partial_s f(z) = Df(z)(1)$ , $\partial_t f(z) = Df(z)(i)$ (each $0$ where $f$ is not differentiable).
Finite-energy curve on $U \subseteq \mathbb{C}$ for $u : \mathbb{C} \to V$ : (1) $u$ is $C^\infty$ on $U$ ; (2) $u(z) \ne 0$ for $z \in U$ ; (3) for every $z \in U$ , $u$ is differentiable at $z$ and $\partial_s u(z) + \tilde J(u(z))\, \partial_t u(z) = 0$ ; (4) $E(U, u) < \infty$ , where, writing $a_u = a \circ u$ and $w_u = \pi_S \circ u$ ,

E(U,u) = \sup_{\varphi}\ \int_U \Big[\varphi'(a_u)\big(\partial_s a_u\, \lambda_{w_u}(\partial_t w_u) - \partial_t a_u\, \lambda_{w_u}(\partial_s w_u)\big) + \varphi(a_u)\, \omega_0(\partial_s w_u, \partial_t w_u)\Big]^+ \, dz \ \in [0, \infty],

the supremum being over $C^\infty$ nondecreasing $\varphi : \mathbb{R} \to [0,1]$ , $[\cdot]^+ = \max(\cdot, 0)$ , and the integral a Lebesgue integral of a nonnegative function with respect to area measure (value in $[0,\infty]$ ).

$d\lambda$ -energy. $E_{d\lambda}(U, u) = \displaystyle\int_U \big[\omega_0(\partial_s w_u, \partial_t w_u)\big]^+\, dz \in [0, \infty]$ .
Reeb orbits. A Reeb orbit $P$ consists of a map $x_P : \mathbb{R} \to V$ and a number $T_P > 0$ such that $x_P(\tau) \in S$ for all $\tau$ , $x_P$ is differentiable with $x_P'(\tau) = R(x_P(\tau))$ , and $x_P(\tau + T_P) = x_P(\tau)$ for all $\tau$ . ( $T_P$ is a period, not required to be the minimal one.)
Trivial cylinder over $P$ . For $w \in \mathbb{C}$ ,

\mathrm{Cyl}_P(w) = |w|^{T_P/\pi}\; x_P\!\Big(\frac{T_P \arg w}{2\pi}\Big),

with $\arg w \in (-\pi, \pi]$ the principal argument ( $\arg 0 = 0$ ); since $T_P/\pi > 0$ , $\mathrm{Cyl}_P(0) = 0$ .

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

Finite-energy cylinders with vanishing dλd\lambdadλ-energy are trivial cylinders

FiniteEnergyPlane.eq_trivialCylinder_of_dlambdaEnergy_eq_zero

Setting and notation (all definitions unfolded)

Finite-energy cylinders with vanishing $d\lambda$ -energy are trivial cylinders