A plane asymptotic to an orbit stays away from its value at the origin

Proved

FiniteEnergyPlane.exists_pos_le_aCoord_add_proj_of_isNondegenerateEnd

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

pseudoholomorphic-curvessymplectic-geometry

Let $H$ be a strictly star-shaped level function on $V_n$ , $P$ a Reeb orbit, and $u : \mathbb{C} \to V_n$ continuous, injective, avoiding $0$ , and asymptotic to $P$ at $\infty$ in the sense of IsNondegenerateEnd H u cylInf P 1. For every $\rho > 0$ there is $\eta > 0$ such that for all $z$ with $|z| \ge \rho$ ,

\eta \le |a_H(u(z)) - a_H(u(0))| + \|\mathrm{proj}_H(u(z)) - \mathrm{proj}_H(u(0))\|.

Role. A uniform separation of $u(0)$ from the part of the plane outside a ball, measured in the coordinates of the symplectization. These are the coordinates used by IsCylCloseTo.

Preamble

import Definitions.Def_FiniteEnergyPlane_Asymptotics

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- An injective continuous plane avoiding `0` and asymptotic to a Reeb orbit at `∞` stays away from
its value at `0` in the symplectization coordinates, outside any ball around `0`. -/
theorem exists_pos_le_aCoord_add_proj_of_isNondegenerateEnd {n : ℕ} (H : V n → ℝ)
    (hH : IsStrictlyStarShapedLevel H) (P : ReebOrbit H) (u : ℂ → V n) (hu0 : ∀ z, u z ≠ 0)
    (huc : Continuous u) (hui : Function.Injective u) (huP : IsNondegenerateEnd H u cylInf P 1)
    (ρ : ℝ) (hρ : 0 < ρ) :
    ∃ η > 0, ∀ z, ρ ≤ ‖z‖ →
      η ≤ |aCoord H (u z) - aCoord H (u 0)| + ‖proj H (u z) - proj H (u 0)‖ := by
  sorry

end FiniteEnergyPlane

Source

Elementary lemma in the setting of U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. AMS 364 (2012), arXiv:0812.4076

View graph