Exponential convergence in all derivatives at the puncture at infinity of a plane

Proved

FiniteEnergyPlane.exists_hasExpAsymptoticsEnd_of_isNondegenerateEnd

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

pseudoholomorphic-curvessymplectic-geometry

Let $u$ be a finite-energy $\tilde J$ -holomorphic plane with a nondegenerate positive puncture at $\infty$ over a periodic Reeb orbit $P$ in the sense of Hryniewicz, Definition 2.9 (so $P$ itself is not assumed nondegenerate). Then, in the cylindrical coordinates $\mathtt{cylInf}$ at $\infty$ , $u$ converges to the trivial cylinder over $P$ exponentially fast in $C^\infty$ .

Role. Upgrades the $C^0$ hypothesis of Definition 2.9 to $C^\infty$ control on the end of a plane, for possibly degenerate orbits.

Preamble

import Definitions.Def_FiniteEnergyPlane_Asymptotics

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- A finite-energy plane with a nondegenerate positive puncture at `∞` over a Reeb orbit `P` (not
assumed nondegenerate) converges to the trivial cylinder over `P` exponentially fast in `C^∞`. -/
theorem exists_hasExpAsymptoticsEnd_of_isNondegenerateEnd {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 Set.univ u)
    (P : ReebOrbit H) (huP : IsNondegenerateEnd H u cylInf P 1) :
    ∃ b > 0, HasExpAsymptoticsEnd H u cylInf P 1 b := by
  sorry

end FiniteEnergyPlane

Source

U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. AMS 364 (2012), arXiv:0812.4076, used with Lemmas 6.10 and 6.20

View graph