Long finite-energy cylinders of small area are close to periodic orbits

Proved

FiniteEnergyPlane.exists_loop_near_reebOrbit_of_small_area

by Mazecto · Nov 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

compactnessfast-planespseudoholomorphic-curvesreeb-dynamicssymplectic-geometrysymplectization

Let $S=H^{-1}(1)\subset\mathbb{R}^{2n+2}$ be a strictly star-shaped level and $J$ a smooth $d\lambda_0$ -compatible complex structure on $\xi$ . Let $C,e,\eta>0$ , suppose every periodic Reeb orbit of period at most $C$ is nondegenerate, and that $e$ is smaller than every such period and than every difference of two distinct such periods. Then for every $m\in\mathbb{N}$ and $\varepsilon>0$ there is $h>0$ with the following property. Let $R>0$ and let $u$ be a finite-energy $\tilde J$ -holomorphic curve on $\{|z|>R\}$ with

$E(u)\le C$ and $\int_{\{|z|>R\}}u^*d\lambda\le e$ ,
$\int_{|z|=\rho}u^*\lambda\ge\eta$ for every counterclockwise circle of radius $\rho>R$ .

Then for every $\rho\ge Re^{2\pi h}$ there are a periodic orbit $(x,T)$ with $T\le C$ and a phase $c$ such that the loop $t\mapsto\mathrm{proj}(u(\rho e^{2\pi it}))$ and $t\mapsto x(Tt+c)$ differ by at most $\varepsilon$ in $C^m$ : all derivatives of order $\le m$ differ by at most $\varepsilon$ at every $t$ .

Formalization Note $h$ depends only on $C,e,\eta,m,\varepsilon$ (it is chosen before $R$ and $u$ ). In cylindrical coordinates $z=e^{2\pi(s+it)}$ the condition $\rho\ge Re^{2\pi h}$ is $s\ge r+h$ with $R=e^{2\pi r}$ . Compared with Hryniewicz's Lemma 4.11, no convergence of $u(s,\cdot)$ as $s\to\infty$ is assumed, and the neighbourhood of the orbits is the explicit $C^m$ - $\varepsilon$ one.

Preamble

import Definitions.Def_FiniteEnergyPlane_Compactness

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- Hryniewicz (Trans. AMS 2012), Lemma 4.11; Hofer–Wysocki–Zehnder (ETDS 2002), Theorem 1.1. Fix
`C, e, η > 0` such that every periodic Reeb orbit of period at most `C` is nondegenerate, and `e` is
smaller than each such period and than each difference of two distinct such periods. Then for all
`m` and `ε > 0` there is `h > 0` with the following property. If `u` is a finite-energy
`J̃`-holomorphic curve on `{|z| > R}` with energy at most `C`, `dλ`-energy at most `e`, and action
`∫_{|z| = ρ} u*λ ≥ η` on every counterclockwise circle `|z| = ρ > R`, then for every
`ρ ≥ R e^{2πh}` the loop `t ↦ proj(u(ρ e^{2πit}))` is `C^m`-`ε`-close to `t ↦ x(Tt + c)` for some
periodic orbit `(x, T)` with `T ≤ C` and some phase `c`. -/
theorem exists_loop_near_reebOrbit_of_small_area {n : ℕ} (H : V n → ℝ) (hH : IsStrictlyStarShapedLevel H)
    (J : V n → V n →L[ℝ] V n) (hJ : IsCompatibleXiStructure H J)
    (C e η : ℝ) (hnd : ∀ Q : ReebOrbit H, Q.T ≤ C → Q.IsNondegenerate) (he : 0 < e)
    (he₁ : ∀ Q : ReebOrbit H, Q.T ≤ C → e < Q.T)
    (he₂ : ∀ Q₁ Q₂ : ReebOrbit H, Q₁.T ≤ C → Q₂.T ≤ C → Q₁.T ≠ Q₂.T → e < |Q₁.T - Q₂.T|)
    (hη : 0 < η) (m : ℕ) (ε : ℝ) (hε : 0 < ε) :
    ∃ h : ℝ, 0 < h ∧ ∀ (R : ℝ) (u : ℂ → V n), 0 < R →
      IsFiniteEnergyCurve H J {z | R < ‖z‖} u →
      energy H {z | R < ‖z‖} u ≤ ENNReal.ofReal C →
      dlambdaEnergy H {z | R < ‖z‖} u ≤ ENNReal.ofReal e →
      (∀ ρ : ℝ, R < ρ → η ≤ loopAction H u (ccwLoop ρ)) →
      ∀ ρ : ℝ, R * Real.exp (2 * π * h) ≤ ρ →
        ∃ Q : ReebOrbit H, Q.T ≤ C ∧ ∃ c : ℝ, ∀ k ≤ m, ∀ t : ℝ,
          ‖iteratedDeriv k (loopInS H u (ccwLoop ρ)) t -
            iteratedDeriv k (fun t => Q.x (Q.T * t + c)) t‖ ≤ ε := by
  sorry

end FiniteEnergyPlane

Source

U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. Amer. Math. Soc. 364 (2012), 1859–1931, arXiv:0812.4076, Lemma 4.11; H. Hofer, K. Wysocki, E. Zehnder, Finite energy cylinders of small area, Ergodic Theory Dynam. Systems 22 (2002), 1451–1486, doi:10.1017/S0143385702001013, Theorem 1.1

Read-back

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

Read-back: `FiniteEnergyPlane.exists_loop_near_reebOrbit_of_small_area`

Fix $n\in\mathbb{N}$ and $V_n=\mathbb{R}^{2n+2}$ , with the maximum norm. The theorem takes the following data and hypotheses.

Contact data. $H:V_n\to\mathbb{R}$ has a strictly star-shaped level, and $J:V_n\to L(V_n)$ is a compatible $\xi$ -structure (both defined below).
Parameters. $C,e,\eta\in\mathbb{R}$ , $m\in\mathbb{N}$ , and $\varepsilon>0$ .
Hypotheses on Reeb orbits and parameters.
- every Reeb orbit $Q$ with $T_Q\le C$ is nondegenerate;
- $e>0$ ;
- every Reeb orbit $Q$ with $T_Q\le C$ satisfies $e<T_Q$ ;
- any two Reeb orbits $Q_1,Q_2$ with $T_{Q_1},T_{Q_2}\le C$ and $T_{Q_1}\ne T_{Q_2}$ satisfy $e<|T_{Q_1}-T_{Q_2}|$ ;
- $\eta>0$ .

Conclusion. There is an $h>0$ with the property below. $h$ depends only on $H,J,C,e,\eta,m,\varepsilon$ , not on $R$ or $u$ .

Take any $R>0$ and any $u:\mathbb{C}\to V_n$ such that, with $U_R=\{z\in\mathbb{C}:|z|>R\}$ :

$u$ is a finite-energy curve on $U_R$ ;
$E(U_R,u)\le\max(C,0)$ (the bound is $C$ cast into $[0,\infty]$ );
$E_{d\lambda}(U_R,u)\le\max(e,0)=e$ ;
for every $\rho>R$ , $\mathcal{A}_u(\rho)\ge\eta$ , where

\mathcal{A}_u(\rho)=\int_0^1\lambda_{\gamma_\rho(t)}\big(\gamma_\rho'(t)\big)\,dt,\qquad \gamma_\rho(t)=\mathrm{proj}\big(u(\rho e^{2\pi it})\big).

Here $\gamma_\rho'$ is the derivative, taken to be $0$ wherever it does not exist.

Then for every $\rho\ge Re^{2\pi h}$ there are a Reeb orbit $Q$ with $T_Q\le C$ and a constant $c\in\mathbb{R}$ such that

\Big\| \frac{d^k}{dt^k}\gamma_\rho(t) - \frac{d^k}{dt^k}\,x_Q(T_Qt+c)\Big\| \le \varepsilon \qquad\text{for all }k\le m\text{ and all }t\in\mathbb{R}.

The case $k=0$ is included. Iterated derivatives are again $0$ where they do not exist. $Q$ and $c$ may depend on $\rho$ .

Definitions used

Forms. Coordinates of $V_n$ are indexed $0,\dots,2n+1$ .

$(j_0v)_{2i}=-v_{2i+1}$ and $(j_0v)_{2i+1}=v_{2i}$ .
$\omega_0(u,v)=\sum_i(u_{2i}v_{2i+1}-u_{2i+1}v_{2i})$ .
$\lambda_x(v)=\tfrac12\omega_0(x,v)$ .
$X_H=j_0\nabla H$ , with $\nabla H(x)_k=DH(x)e_k$ .
$R_H(x)=\lambda_x(X_H(x))^{-1}X_H(x)$ , with $0^{-1}=0$ .
$\xi_x=\{v:\lambda_x(v)=0,\ DH(x)v=0\}$ .

Strictly star-shaped level. $H$ is $C^\infty$ ; every $u\ne0$ has exactly one $r>0$ with $H(ru)=1$ ; and $DH(x)x>0$ whenever $H(x)=1$ .

Compatible $\xi$ -structure. $J$ is $C^\infty$ , and for every $x$ with $H(x)=1$ and all $v,w\in\xi_x$ :

$J(x)v\in\xi_x$ ;
$J(x)J(x)v=-v$ ;
$\omega_0(v,J(x)v)>0$ if $v\ne0$ ;
$\omega_0(J(x)v,J(x)w)=\omega_0(v,w)$ .

Reeb orbit. $Q=(x_Q,T_Q)$ with $T_Q>0$ , $H(x_Q(\tau))=1$ , $x_Q'=R_H(x_Q)$ , and $x_Q(\tau+T_Q)=x_Q(\tau)$ . The period $T_Q$ is not necessarily minimal.

Nondegenerate. For every $\Phi$ with $\Phi(0)=\mathrm{id}$ and $\Phi'(\tau)=DR_H(x_Q(\tau))\Phi(\tau)$ , the only $v\in\xi_{x_Q(0)}$ with $\Phi(T_Q)v=v$ is $v=0$ .

Radial coordinates. $r(y)$ is a chosen $r>0$ with $H(ry)=1$ if one exists, and $r(y)=1$ otherwise. Then $\mathrm{proj}(y)=r(y)y$ and $a(y)=-\tfrac12\log r(y)$ .

$\tilde J$ . For $y\in V_n$ put $x=\mathrm{proj}(y)$ , $r=r(y)$ , $\alpha(v)=\frac{r}{2DH(x)x}DH(x)v$ and $\beta(v)=r\lambda_x(v)$ . Then

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

Energies. Write $a_u=a\circ u$ and $w_u=\mathrm{proj}\circ u$ , with $\partial_s f=Df(z)1$ and $\partial_tf=Df(z)i$ (both $0$ where $f$ is not differentiable).

$E_{d\lambda}(U,u)=\int_U\max(\omega_0(\partial_sw_u,\partial_tw_u),0)\,dz$ .
$E(U,u)$ is the supremum, over $C^\infty$ nondecreasing $\phi:\mathbb{R}\to[0,1]$ , of

\int_U\max\Big(\phi'(a_u)\big(\partial_sa_u\,\lambda_{w_u}(\partial_tw_u)-\partial_ta_u\,\lambda_{w_u}(\partial_sw_u)\big)+\phi(a_u)\,\omega_0(\partial_sw_u,\partial_tw_u),0\Big)\,dz.

Finite-energy curve on $U$ . This means all of the following:

$u$ is $C^\infty$ on $U$ and nonvanishing there;
at every $z\in U$ , $u$ is differentiable with $\partial_su+\tilde J(u)\partial_tu=0$ ;
$E(U,u)<\infty$ .

Human review

Endorsed by Shuze Chen · Nov 3, 2026
Confirmed by the moderator at approval.
Endorsed by Mazecto · Nov 3, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Long finite-energy cylinders of small area are close to periodic orbits

Read-back: FiniteEnergyPlane.exists_loop_near_reebOrbit_of_small_area

Definitions used

Read-back: `FiniteEnergyPlane.exists_loop_near_reebOrbit_of_small_area`