A trajectory accumulating on meets every fast plane over at arbitrarily large times
OpenFiniteEnergyPlane.exists_hit_of_tendsto_orbitLet be a strictly star-shaped level, a smooth -compatible complex structure on , and a periodic Reeb orbit with ( may be degenerate unless stated otherwise). Let be a fast finite-energy plane asymptotic to at , and let be a Reeb trajectory with .
- If converges to a point of for some , then for every there is with .
- If converges to a point of for some , then for every there is with .
Formalization Note The hypotheses of 1 and 2 say that the -limit set, respectively the -limit set, of meets . is P.IsCZAtLeast 3, the index of the linearized flow along in the global frame of . Hryniewicz writes and restricts to ; on a strictly star-shaped level has a global frame, which extends over every capping disk, so the index depends only on , , and the condition is not restated. The plane is not assumed to be embedded.
import Definitions.Def_FiniteEnergyPlane_OpenBook
namespace FiniteEnergyPlane
open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real
/-- Hryniewicz (Trans. AMS 2012), Lemma 6.9; Hofer–Wysocki–Zehnder (Ann. of Math. 1998), § 5. Let `u`
be a fast finite-energy plane asymptotic to `P` at `∞`, where the Conley–Zehnder index of `P` is at
least `3`, and let `y` be a Reeb trajectory with `y 0 ∉ x(ℝ)`. If a point of `x(ℝ)` is a limit of
`y(tₖ)` for some `tₖ → +∞` (that is, the `ω`-limit set of `y 0` meets `x(ℝ)`), then `y` meets
`proj H ∘ u` at times larger than any given `n`. The same holds for `tₖ → -∞` (the `α`-limit set)
and times smaller than any given `n`. -/
theorem exists_hit_of_tendsto_orbit (H : V 1 → ℝ) (hH : IsStrictlyStarShapedLevel H)
(J : V 1 → V 1 →L[ℝ] V 1) (hJ : IsCompatibleXiStructure H J)
(P : ReebOrbit H) (hcz : P.IsCZAtLeast 3) (u : ℂ → V 1) (hu : IsFastPlane H J u)
(huP : IsNondegenerateEnd H u cylInf P 1) (y : ℝ → V 1) (hy : IsReebTrajectory H y)
(hy₀ : y 0 ∉ Set.range P.x) :
((∃ (τ₀ : ℝ) (s : ℕ → ℝ), Tendsto s atTop atTop ∧ Tendsto (y ∘ s) atTop (𝓝 (P.x τ₀))) →
∀ n : ℝ, ∃ t > n, y t ∈ Set.range (fun z => proj H (u z))) ∧
((∃ (τ₀ : ℝ) (s : ℕ → ℝ), Tendsto s atTop atBot ∧ Tendsto (y ∘ s) atTop (𝓝 (P.x τ₀))) →
∀ n : ℝ, ∃ t < n, y t ∈ Set.range (fun z => proj H (u z))) := by
sorry
end FiniteEnergyPlane
Read-back
What the Lean code literally says, in plain math · claude-opus-5-5
FiniteEnergyPlane.exists_hit_of_tendsto_orbit
Let have strictly star-shaped level , let be a compatible -structure for , let be a Reeb orbit of with "CZ index of at least ", let be a fast plane having end on (with sign ), and let be a Reeb trajectory with .
Then both of the following implications hold, where :
- Forward. If there exist and a real sequence with , then for every there is with .
- Backward. If there exist and a real sequence with , then for every there is with .
is not assumed embedded, and no base point or energy value of is prescribed. No nondegeneracy of any orbit and no compactness hypothesis is assumed. The sequence need not be monotone. The conclusion only concerns membership of in the image; no statement about transversality or the number of hits is made.
Background notions
Conventions. with coordinates ; below mostly , so . denotes the real Fréchet derivative, which is the zero map by convention where is not differentiable. For on : , . Also , and is the image of .
Symplectic data on . for even, for odd. . . has components ; .
Reeb field. (the zero vector where ). -membership: "" means and .
Strictly star-shaped level. ; for every there is exactly one with ; and whenever . The last clause forces .
Compatible -structure. is on all of , and for all with and all : ; ; if then ; .
Radial coordinates. is a chosen with if one exists, and otherwise. and . (For star-shaped : at the is unique; at the value is .)
Almost complex structure on . For with , , set , , and . Then
Finite energy curve on (only itself is used here). with: ; for all ; is differentiable at each with ; and , where
with , , the supremum over monotone (non-decreasing) , and the positive part (the integral is a -valued Lebesgue integral).
-energy. For : , with .
Reeb orbit. A Reeb orbit of is a pair with , , , and for all . is any positive period, not necessarily the minimal one, so covers are orbits. is prime when for all .
Reeb trajectory. Any such that for every : and is differentiable at with . Nothing excludes from being periodic or from running along a Reeb orbit.
Nondegenerate orbit. For every with and for all , and every : implies . (Vacuous if no such exists.)
Nondegenerate end at infinity on (with sign ; written " has end on "). There exist reals and such that, as and uniformly in ,
Fast plane. such that:
- is a finite energy curve on ;
- there exists a prime Reeb orbit of on which has an end in the above sense;
- with and , the zero set of is finite, and there are integers , , summing to , such that for each there is with on and, for each , the loop has winding number .
Here a loop "has winding number " when is continuous, -periodic, nowhere zero, and there is a continuous with and . An empty satisfies clause 3; the definition allows nonempty with indices of mixed sign summing to .
The coordinate is
for , with the Euclidean norm, and .
Embedded plane. is injective and is an injective linear map for every .
Set of embedded fast planes (, ). All that are fast planes, have end on , are embedded planes, have , and satisfy
When this says the energy on is . is not itself required to be prime; the prime orbit of the fast plane condition is a separate existential.
convergence on . means: for every compact and every , the -th iterated Fréchet derivatives of converge uniformly on to that of .
Sequential compactness of a set of maps . Every sequence in has a subsequence (strictly increasing reindexing) converging in on to some element of . The empty set has this property.
Hypothesis "CZ index of is at least " (for a Reeb orbit of , ). Identify with and let be any periodic orbit of for the Hamiltonian field: , , , , , where . Then, for every such with the same image as and with action , and for every with , , one has . Here has entries
with the real pair , , , and at . The integer is: let be the set of numbers over and continuous on with and for some for each ; let , (with the convention that both equal if is empty, and each equals if unbounded on its side). Then if , and otherwise. The hypothesis is universally quantified over and and so is vacuous if no such pair exists.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.