A Reeb trajectory that returns to a leaf
OpenFiniteEnergyPlane.exists_trajectory_returnLet 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 such that is sequentially compact in for every compact with . If there is an embedded fast finite-energy plane asymptotic to at , then there are a Reeb trajectory , a plane and with .
Formalization Note The hypothesis on is exactly the conclusion of isSeqCompact_embeddedFastPlaneSet for the same , quantified over ; the cylinder is the cone . 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. Hryniewicz uses a return of the trajectory to the leaf of the given plane through a suitable point; here the leaf is only required to exist.
import Definitions.Def_FiniteEnergyPlane_OpenBook
namespace FiniteEnergyPlane
open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real
/-- Hryniewicz (Trans. AMS 2012), § 7.2.1 (variant). Let `P` be a periodic Reeb orbit of
Conley–Zehnder index at least `3`, `0 < γ < P.T`, and suppose `Λ(K, P)` is sequentially compact in
`C^∞_loc` for every compact `K ⊂ V 1 \ {0}` disjoint from the cone `ℝ × x(ℝ)`. If there is an
embedded fast finite-energy plane asymptotic to `P` at `∞`, then there are a Reeb trajectory `y`, a
plane `v ∈ Λ({y 0}, P)` and `τ > 0` such that `y τ` lies in the image of `proj H ∘ v`. -/
theorem exists_trajectory_return (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) (γ : ℝ) (hγ : 0 < γ) (hγT : γ < P.T)
(hΛ : ∀ K : Set (V 1), IsCompact K → (0 : V 1) ∉ K → (∀ y ∈ K, proj H y ∉ Set.range P.x) →
IsSeqCompactCInftyLoc (embeddedFastPlaneSet H J P K γ))
(u₀ : ℂ → V 1) (hu₀ : IsFastPlane H J u₀) (hu₀P : IsNondegenerateEnd H u₀ cylInf P 1)
(hu₀e : IsEmbeddedPlane u₀) :
∃ y : ℝ → V 1, IsReebTrajectory H y ∧ ∃ v ∈ embeddedFastPlaneSet H J P {y 0} γ,
∃ τ > 0, y τ ∈ Set.range (fun z => proj H (v z)) := by
sorry
end FiniteEnergyPlane
Read-back
What the Lean code literally says, in plain math · claude-opus-5-5
FiniteEnergyPlane.exists_trajectory_return
Let have strictly star-shaped level , let be a compatible -structure for , let be a Reeb orbit of with "CZ index of at least ", and let with . Assume the compactness hypothesis:
for every compact with and with for all , the set is sequentially compact.
This is an assumption of the statement, not derived from the other data; the statement does not say whether it can be satisfied. Let be a fast plane having end on and being an embedded plane. No value of the -energy of and no base point of is prescribed, and does not appear in the conclusion.
Then there exist a Reeb trajectory , a map , and a real such that
The conclusion is purely existential: , , are not related to in the statement, and is not required to differ from . Since and , star-shapedness gives , so a trajectory with for some meets the condition at . No nondegeneracy of any orbit is assumed, and the only relation between and periods is .
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.