Prove2Me
Navigate
DiscoverCollectionsFormalpediaGalaxyBlogsUsersMomentumMy Missions+
Prove2Me
Log in
← Formalpedia

Ends converging along a sequence to a nondegenerate orbit are asymptotically cylindrical

Proved
FiniteEnergyPlane.isAsymptoticallyCylindricalEnd_of_isNondegenerate

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

asymptotic-operatorpseudoholomorphic-curvesreeb-dynamicssymplectic-geometrysymplectization

Let S=H−1(1)⊂R2n+2S=H^{-1}(1)\subset\mathbb{R}^{2n+2}S=H−1(1)⊂R2n+2 be a strictly star-shaped level, JJJ a smooth dλ0d\lambda_0dλ0​-compatible complex structure on ξ\xiξ, and uuu a finite-energy J~\tilde JJ~-holomorphic curve on D∖{0}D\setminus\{0\}D∖{0}, DDD the open unit disk. Let P=(x,T)P=(x,T)P=(x,T) be a nondegenerate periodic Reeb orbit, σ=±1\sigma=\pm1σ=±1, c∈Rc\in\mathbb{R}c∈R, and ρk→0+\rho_k\to0^+ρk​→0+ such that the loops t↦proj u(ρke−2πit)t\mapsto\mathrm{proj}\,u(\rho_ke^{-2\pi it})t↦proju(ρk​e−2πit) converge in C∞(R,V)C^\infty(\mathbb{R},V)C∞(R,V) to t↦x(σTt+c)t\mapsto x(\sigma Tt+c)t↦x(σTt+c). Then, in the cylindrical coordinates e−2π(s+it)e^{-2\pi(s+it)}e−2π(s+it) at 000, uuu is asymptotically cylindrical over PPP with sign σ\sigmaσ.

Formalization Note The conclusion is IsAsymptoticallyCylindricalEnd H u cylEnd P σ; the constant ccc in it need not be the given one.

Preamble
import Definitions.Def_FiniteEnergyPlane_Asymptotics
Formal statement
namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- Hofer–Wysocki–Zehnder: let `u` be a finite-energy `J̃`-holomorphic curve on the punctured disk
`D \ {0}` such that, along some sequence of radii `ρₖ → 0`, the loops `t ↦ proj(u(ρₖ e^{-2πit}))`
converge in `C^∞` to `t ↦ x(σTt + c)` for a nondegenerate periodic Reeb orbit `P = (x, T)` and
`σ = ±1`. Then `u` is asymptotically cylindrical over `P` with sign `σ` at the puncture, in the
cylindrical coordinates `cylEnd`. -/
theorem isAsymptoticallyCylindricalEnd_of_isNondegenerate {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 (ball 0 1 \ {0}) u) (P : ReebOrbit H) (hP : P.IsNondegenerate)
    (σ : ℝ) (hσ : σ = 1 ∨ σ = -1) (ρ : ℕ → ℝ) (hρ : ∀ k, 0 < ρ k) (hρ0 : Tendsto ρ atTop (𝓝 0))
    (c : ℝ) (hconv : TendstoCInfty (fun k => loopInS H u (cwLoop 0 (ρ k)))
      (fun t => P.x (σ * P.T * t + c))) :
    IsAsymptoticallyCylindricalEnd H u cylEnd P σ := by
  sorry

end FiniteEnergyPlane
Source
H. Hofer, K. Wysocki, E. Zehnder, Properties of pseudoholomorphic curves in symplectisations I: Asymptotics, Ann. Inst. H. Poincaré Anal. Non Linéaire 13 (1996), 337–379, with the Correction, ibid. 15 (1998), 535–538, Theorem 1.3; C. Wendl, Lectures on Symplectic Field Theory, lecture notes, Humboldt-Universität zu Berlin (2026 version); earlier version arXiv:1612.01009, Definition 6.4.1
Read-back

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

Read-back: FiniteEnergyPlane.isAsymptoticallyCylindricalEnd_of_isNondegenerate

Ambient space and standard structures. Here n≥0n \ge 0n≥0 is an arbitrary natural number and V=R2(n+1)V = \mathbb{R}^{2(n+1)}V=R2(n+1), with coordinates v0,…,v2n+1v_0, \dots, v_{2n+1}v0​,…,v2n+1​. VVV carries the sup norm ∥v∥=max⁡k∣vk∣\|v\| = \max_k |v_k|∥v∥=maxk​∣vk​∣ (this is the norm in every estimate below on VVV-valued quantities). Define:

  • j0vj_0 vj0​v by (j0v)k=−vk+1(j_0 v)_k = -v_{k+1}(j0​v)k​=−vk+1​ for even kkk and (j0v)k=vk−1(j_0 v)_k = v_{k-1}(j0​v)k​=vk−1​ for odd kkk;
  • ⟨u,v⟩=∑kukvk\langle u, v \rangle = \sum_k u_k v_k⟨u,v⟩=∑k​uk​vk​,  ω0(u,v)=⟨j0u,v⟩\ \omega_0(u, v) = \langle j_0 u, v \rangle ω0​(u,v)=⟨j0​u,v⟩, and λx(v)=12 ω0(x,v)\lambda_x(v) = \tfrac12\, \omega_0(x, v)λx​(v)=21​ω0​(x,v);
  • for H:V→RH : V \to \mathbb{R}H:V→R: ∇H(x)=(dH(x)ek)k\nabla H(x) = (dH(x) e_k)_k∇H(x)=(dH(x)ek​)k​,  XH(x)=j0∇H(x)\ X_H(x) = j_0 \nabla H(x) XH​(x)=j0​∇H(x), and RH(x)=λx(XH(x))−1 XH(x)R_H(x) = \lambda_x(X_H(x))^{-1}\, X_H(x)RH​(x)=λx​(XH​(x))−1XH​(x), with the convention 0−1=00^{-1} = 00−1=0 (so RH(x)=0R_H(x) = 0RH​(x)=0 wherever λx(XH(x))=0\lambda_x(X_H(x)) = 0λx​(XH​(x))=0);
  • ξx={v∈V:λx(v)=0 and dH(x)v=0}\xi_x = \{ v \in V : \lambda_x(v) = 0 \text{ and } dH(x) v = 0 \}ξx​={v∈V:λx​(v)=0 and dH(x)v=0}.

Throughout, dH(x)dH(x)dH(x), DRH(x)DR_H(x)DRH​(x), ∂s\partial_s∂s​, ∂t\partial_t∂t​, DmD^mDm denote Fréchet derivatives, with the convention that the derivative of a function at a point where it is not differentiable is 000.

Hypothesis on HHH ("strictly star-shaped level"). HHH is C∞C^\inftyC∞; for every y≠0y \ne 0y=0 there is exactly one r>0r > 0r>0 with H(ry)=1H(r y) = 1H(ry)=1; and dH(x) x>0dH(x)\,x > 0dH(x)x>0 whenever H(x)=1H(x) = 1H(x)=1.

Hypothesis on JJJ ("compatible ξ\xiξ-structure"). JJJ is a map from VVV to continuous linear maps V→VV \to VV→V; it is C∞C^\inftyC∞, and for every xxx with H(x)=1H(x) = 1H(x)=1 and all v,w∈ξxv, w \in \xi_xv,w∈ξx​: J(x)v∈ξxJ(x) v \in \xi_xJ(x)v∈ξx​; J(x)J(x)v=−vJ(x) J(x) v = -vJ(x)J(x)v=−v; ω0(v,J(x)v)>0\omega_0(v, J(x) v) > 0ω0​(v,J(x)v)>0 if v≠0v \ne 0v=0; and ω0(J(x)v,J(x)w)=ω0(v,w)\omega_0(J(x) v, J(x) w) = \omega_0(v, w)ω0​(J(x)v,J(x)w)=ω0​(v,w). Nothing is required of J(x)J(x)J(x) outside ξx\xi_xξx​ or at points with H(x)≠1H(x) \ne 1H(x)=1.

Radial coordinates. For y∈Vy \in Vy∈V, let r(y)r(y)r(y) be a fixed (choice-selected) r>0r > 0r>0 with H(ry)=1H(r y) = 1H(ry)=1 if such rrr exists, and r(y)=1r(y) = 1r(y)=1 otherwise. Put pr(y)=r(y) y\mathrm{pr}(y) = r(y)\, ypr(y)=r(y)y and a(y)=−12log⁡r(y)a(y) = -\tfrac12 \log r(y)a(y)=−21​logr(y).

Finite-energy curves. For fff defined on C=R2\mathbb{C} = \mathbb{R}^2C=R2 write ∂sf(z)=Df(z)⋅1\partial_s f(z) = Df(z)\cdot 1∂s​f(z)=Df(z)⋅1 and ∂tf(z)=Df(z)⋅i\partial_t f(z) = Df(z)\cdot i∂t​f(z)=Df(z)⋅i. For y∈Vy \in Vy∈V let x=pr(y)x = \mathrm{pr}(y)x=pr(y), r=r(y)r = r(y)r=r(y), α(v)=r2 dH(x)x dH(x)v\alpha(v) = \dfrac{r}{2\, dH(x) x}\, dH(x) vα(v)=2dH(x)xr​dH(x)v, β(v)=r λx(v)\beta(v) = r\, \lambda_x(v)β(v)=rλx​(v), w(v)=v−2α(v) y−β(v) r−1RH(x)w(v) = v - 2\alpha(v)\, y - \beta(v)\, r^{-1} R_H(x)w(v)=v−2α(v)y−β(v)r−1RH​(x), and

J~(y)v=α(v) r−1RH(x)−2β(v) y+J(x) w(v).\tilde J(y) v = \alpha(v)\, r^{-1} R_H(x) - 2 \beta(v)\, y + J(x)\, w(v).J~(y)v=α(v)r−1RH​(x)−2β(v)y+J(x)w(v).

For u:C→Vu : \mathbb{C} \to Vu:C→V put au=a∘ua_u = a \circ uau​=a∘u and wu=pr∘uw_u = \mathrm{pr} \circ uwu​=pr∘u. A function φ:R→R\varphi : \mathbb{R} \to \mathbb{R}φ:R→R is admissible if it is C∞C^\inftyC∞, nondecreasing, and takes values in [0,1][0, 1][0,1]. For U⊆CU \subseteq \mathbb{C}U⊆C the energy is the value in [0,∞][0, \infty][0,∞]

EU(u)=sup⁡φ admissible∫Umax⁡{0,eφ(z)} dz,eφ=φ′(au)(∂sau λwu(∂twu)−∂tau λwu(∂swu))+φ(au) ω0(∂swu,∂twu),E_U(u) = \sup_{\varphi \text{ admissible}} \int_U \max\{0, e_\varphi(z)\}\, dz, \qquad e_\varphi = \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),EU​(u)=φ admissiblesup​∫U​max{0,eφ​(z)}dz,eφ​=φ′(au​)(∂s​au​λwu​​(∂t​wu​)−∂t​au​λwu​​(∂s​wu​))+φ(au​)ω0​(∂s​wu​,∂t​wu​),

the integral being the Lebesgue integral of a nonnegative extended-real function. "uuu is a finite-energy curve on UUU" means: uuu is C∞C^\inftyC∞ on UUU; u(z)≠0u(z) \ne 0u(z)=0 for all z∈Uz \in Uz∈U; at every z∈Uz \in Uz∈U, uuu is differentiable and ∂su(z)+J~(u(z)) ∂tu(z)=0\partial_s u(z) + \tilde J(u(z))\, \partial_t u(z) = 0∂s​u(z)+J~(u(z))∂t​u(z)=0; and EU(u)<∞E_U(u) < \inftyEU​(u)<∞.

Reeb orbits. A Reeb orbit PPP of HHH consists of a map xP:R→Vx_P : \mathbb{R} \to VxP​:R→V and a number TP>0T_P > 0TP​>0 such that, for all τ\tauτ, H(xP(τ))=1H(x_P(\tau)) = 1H(xP​(τ))=1, xPx_PxP​ has derivative RH(xP(τ))R_H(x_P(\tau))RH​(xP​(τ)) at τ\tauτ, and xP(τ+TP)=xP(τ)x_P(\tau + T_P) = x_P(\tau)xP​(τ+TP​)=xP​(τ). (TPT_PTP​ is a period of xPx_PxP​, not required to be the minimal one.)

Nondegenerate Reeb orbit. "PPP is nondegenerate" means: for every map Φ:R→{continuous linear maps V→V}\Phi : \mathbb{R} \to \{\text{continuous linear maps } V \to V\}Φ:R→{continuous linear maps V→V} with Φ(0)=id\Phi(0) = \mathrm{id}Φ(0)=id and Φ′(τ)=DRH(xP(τ))∘Φ(τ)\Phi'(\tau) = DR_H(x_P(\tau)) \circ \Phi(\tau)Φ′(τ)=DRH​(xP​(τ))∘Φ(τ) for all τ∈R\tau \in \mathbb{R}τ∈R, and every v∈ξxP(0)v \in \xi_{x_P(0)}v∈ξxP​(0)​ with Φ(TP)v=v\Phi(T_P) v = vΦ(TP​)v=v, one has v=0v = 0v=0. (The condition quantifies over all such Φ\PhiΦ; if none exists it holds vacuously.)

Loops and C∞C^\inftyC∞ convergence of loops. γρcw(t)=ρ e−2πit\gamma^{\mathrm{cw}}_\rho(t) = \rho\, e^{-2\pi i t}γρcw​(t)=ρe−2πit and γRccw(t)=R e2πit\gamma^{\mathrm{ccw}}_R(t) = R\, e^{2\pi i t}γRccw​(t)=Re2πit. For γ:R→C\gamma : \mathbb{R} \to \mathbb{C}γ:R→C the loop of uuu along γ\gammaγ is t↦pr(u(γ(t)))t \mapsto \mathrm{pr}(u(\gamma(t)))t↦pr(u(γ(t))). A sequence fk:R→Vf_k : \mathbb{R} \to Vfk​:R→V converges in C∞C^\inftyC∞ to ggg if for every m∈Nm \in \mathbb{N}m∈N the mmm-th derivatives fk(m)f_k^{(m)}fk(m)​ converge to g(m)g^{(m)}g(m) uniformly on all of R\mathbb{R}R as k→∞k \to \inftyk→∞ (with the zero-derivative convention).

Decay notions on half-cylinders. For f:R2→Ff : \mathbb{R}^2 \to Ff:R2→F (with F=RF = \mathbb{R}F=R or F=VF = VF=V), Dmf(s,t)D^m f(s, t)Dmf(s,t) is the mmm-th Fréchet derivative, measured in the operator norm of mmm-linear maps, where R2\mathbb{R}^2R2 carries the max norm ∥(s,t)∥=max⁡(∣s∣,∣t∣)\|(s, t)\| = \max(|s|, |t|)∥(s,t)∥=max(∣s∣,∣t∣); D0f=fD^0 f = fD0f=f.

  • f→0f \to 0f→0 uniformly: for every ϵ>0\epsilon > 0ϵ>0 there is s0s_0s0​ with ∥f(s,t)∥≤ϵ\|f(s, t)\| \le \epsilon∥f(s,t)∥≤ϵ for all s≥s0s \ge s_0s≥s0​ and all t∈Rt \in \mathbb{R}t∈R.
  • f→0f \to 0f→0 in C∞C^\inftyC∞: there is s0s_0s0​ such that fff is C∞C^\inftyC∞ on (s0,∞)×R(s_0, \infty) \times \mathbb{R}(s0​,∞)×R, and for every m∈Nm \in \mathbb{N}m∈N and every ϵ>0\epsilon > 0ϵ>0 there is s1s_1s1​ with ∥Dmf(s,t)∥≤ϵ\|D^m f(s, t)\| \le \epsilon∥Dmf(s,t)∥≤ϵ for all s≥s1s \ge s_1s≥s1​, t∈Rt \in \mathbb{R}t∈R.
  • fff decays at rate bbb in C∞C^\inftyC∞: there is s0s_0s0​ such that fff is C∞C^\inftyC∞ on (s0,∞)×R(s_0, \infty) \times \mathbb{R}(s0​,∞)×R, and for every m∈Nm \in \mathbb{N}m∈N there are reals Cm,smC_m, s_mCm​,sm​ with ∥Dmf(s,t)∥≤Cm e−bs\|D^m f(s, t)\| \le C_m\, e^{-b s}∥Dmf(s,t)∥≤Cm​e−bs for all s≥sms \ge s_ms≥sm​, t∈Rt \in \mathbb{R}t∈R.

End coordinates. e0(s,t)=e−2πse−2πit∈Ce_0(s, t) = e^{-2\pi s} e^{-2\pi i t} \in \mathbb{C}e0​(s,t)=e−2πse−2πit∈C (it tends to the puncture 000 as s→+∞s \to +\inftys→+∞) and e∞(s,t)=e2πse2πite_\infty(s, t) = e^{2\pi s} e^{2\pi i t}e∞​(s,t)=e2πse2πit. For an end map e∈{e0,e∞}e \in \{e_0, e_\infty\}e∈{e0​,e∞​} put A(s,t)=a(u(e(s,t)))A(s, t) = a(u(e(s, t)))A(s,t)=a(u(e(s,t))) and W(s,t)=pr(u(e(s,t)))W(s, t) = \mathrm{pr}(u(e(s, t)))W(s,t)=pr(u(e(s,t))).

  • Asymptotically cylindrical end (for eee, PPP, a real ε\varepsilonε): there exist d,c∈Rd, c \in \mathbb{R}d,c∈R such that A(s,t)−εTPs−d→0A(s, t) - \varepsilon T_P s - d \to 0A(s,t)−εTP​s−d→0 in C∞C^\inftyC∞ and W(s,t)−xP(εTPt+c)→0W(s, t) - x_P(\varepsilon T_P t + c) \to 0W(s,t)−xP​(εTP​t+c)→0 in C∞C^\inftyC∞.
  • Exponential asymptotics at rate bbb (for eee, PPP, ε\varepsilonε, bbb): there exist d,c∈Rd, c \in \mathbb{R}d,c∈R such that A(s,t)−εTPs−dA(s, t) - \varepsilon T_P s - dA(s,t)−εTP​s−d and W(s,t)−xP(εTPt+c)W(s, t) - x_P(\varepsilon T_P t + c)W(s,t)−xP​(εTP​t+c) both decay at rate bbb in C∞C^\inftyC∞.
  • Nondegenerate end (for eee, PPP, ε\varepsilonε): there exist d,c,b∈Rd, c, b \in \mathbb{R}d,c,b∈R with b>0b > 0b>0 such that A(s,t)−εTPs−d→0A(s, t) - \varepsilon T_P s - d \to 0A(s,t)−εTP​s−d→0 uniformly and ebs(W(s,t)−xP(εTPt+c))→0e^{b s}\big(W(s, t) - x_P(\varepsilon T_P t + c)\big) \to 0ebs(W(s,t)−xP​(εTP​t+c))→0 uniformly.

Statement. D∗={z∈C:0<∣z∣<1}D^* = \{ z \in \mathbb{C} : 0 < |z| < 1 \}D∗={z∈C:0<∣z∣<1} denotes the punctured open unit disk. Let n∈Nn \in \mathbb{N}n∈N, H:V→RH : V \to \mathbb{R}H:V→R a strictly star-shaped level, JJJ a compatible ξ\xiξ-structure for HHH, and u:C→Vu : \mathbb{C} \to Vu:C→V a finite-energy curve on D∗D^*D∗ (nothing is assumed about uuu outside D∗D^*D∗). Let PPP be a Reeb orbit of HHH which is nondegenerate. Let σ∈{1,−1}\sigma \in \{1, -1\}σ∈{1,−1}, let (ρk)k∈N(\rho_k)_{k \in \mathbb{N}}(ρk​)k∈N​ be real numbers with ρk>0\rho_k > 0ρk​>0 for all kkk and ρk→0\rho_k \to 0ρk​→0, and let c∈Rc \in \mathbb{R}c∈R. Assume that the loops

t↦pr(u(ρke−2πit))t \mapsto \mathrm{pr}\big(u(\rho_k e^{-2\pi i t})\big)t↦pr(u(ρk​e−2πit))

converge in C∞C^\inftyC∞ (all derivatives, uniformly on R\mathbb{R}R, as k→∞k \to \inftyk→∞) to t↦xP(σTPt+c)t \mapsto x_P(\sigma T_P t + c)t↦xP​(σTP​t+c).

Then the end at 000 parametrized by e0e_0e0​ is asymptotically cylindrical over PPP with sign σ\sigmaσ: there exist d,c′∈Rd, c' \in \mathbb{R}d,c′∈R such that, with A(s,t)=a(u(e−2πse−2πit))A(s,t) = a\big(u(e^{-2\pi s} e^{-2\pi i t})\big)A(s,t)=a(u(e−2πse−2πit)) and W(s,t)=pr(u(e−2πse−2πit))W(s,t) = \mathrm{pr}\big(u(e^{-2\pi s} e^{-2\pi i t})\big)W(s,t)=pr(u(e−2πse−2πit)),

A(s,t)−σTPs−d→0  in C∞,W(s,t)−xP(σTPt+c′)→0  in C∞A(s,t) - \sigma T_P s - d \to 0 \ \text{ in } C^\infty, \qquad W(s,t) - x_P(\sigma T_P t + c') \to 0 \ \text{ in } C^\inftyA(s,t)−σTP​s−d→0  in C∞,W(s,t)−xP​(σTP​t+c′)→0  in C∞

as s→+∞s \to +\inftys→+∞. The phase c′c'c′ in the conclusion is existentially quantified and is not required to equal the ccc of the hypothesis.

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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paperProve2Me Team
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me