Loops near a puncture of nonzero charge converge to a Reeb orbit
ProvedFiniteEnergyPlane.exists_subseq_tendstoCInfty_cwLoopfinite-energypseudoholomorphic-curvesreeb-dynamicssymplectic-geometry
Let be a strictly star-shaped level with contact form and -compatible complex structure on , and let be a finite-energy -holomorphic curve on the punctured unit disc. Write for the action of the clockwise loop , and call for the gradient bound near the puncture, where (-invariant). Assume the gradient bound near the puncture and . Then for every sequence there are a subsequence , a periodic Reeb orbit (period ) and such that the loops converge in to . (The gradient bound gives -compactness of the shifted cylinders ; the limit has zero -energy, hence is an orbit cylinder, and its loop action is .)
Preamble
import Definitions.Def_FiniteEnergyPlane_Setting
Formal statement
namespace FiniteEnergyPlane
open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real
/-- (d) Nonzero charge: under the gradient bound, along any `ρ_k → 0⁺` a subsequence of the loops
`t ↦ proj(u(ρ_k e^{-2π i t}))` converges in `C^∞` to `t ↦ x(Q t + c)` for a periodic Reeb orbit
`(x, |Q|)`. -/
theorem exists_subseq_tendstoCInfty_cwLoop {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)
(hG : ∃ r : ℝ, 0 < r ∧ ∃ C : ℝ, ∀ z : ℂ, z ≠ 0 → ‖z‖ < r → ‖z‖ * gradNorm H u z ≤ C)
(Q : ℝ) (hQ0 : Q ≠ 0) (hQ : Tendsto (fun ρ => loopAction H u (cwLoop 0 ρ)) (𝓝[>] 0) (𝓝 Q))
(ρ : ℕ → ℝ) (hρ : ∀ k, 0 < ρ k) (hρ0 : Tendsto ρ atTop (𝓝 0)) :
∃ φ : ℕ → ℕ, StrictMono φ ∧ ∃ P : ReebOrbit H, P.T = |Q| ∧ ∃ c : ℝ,
TendstoCInfty (fun k => loopInS H u (cwLoop 0 (ρ (φ k)))) (fun t => P.x (Q * t + c)) := by
sorry
end FiniteEnergyPlaneSource
H. Hofer, Pseudoholomorphic curves in symplectizations with applications to the Weinstein conjecture in dimension three, Invent. Math. 114 (1993), 515-563, Section 3 (convergence to periodic orbits); C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Theorem 9.8 and its proof, pp. 157-160