Foliating the complement of a leaf and of
OpenFiniteEnergyPlane.exists_page_foliationLet be a strictly star-shaped level, a smooth -compatible complex structure on , and a periodic Reeb orbit with ( may be degenerate unless stated otherwise). Suppose every periodic Reeb orbit of period at most is nondegenerate, is smaller than every such period and than every difference of two distinct such periods, and is sequentially compact in for every compact with . Let be a Reeb trajectory, and with . Then for every there are and a family with IsPageFoliation H J P γ y l L δ U and .
Formalization Note Periods are those of ReebOrbit H (not necessarily minimal, so multiple covers count). 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 assumes every contractible orbit nondegenerate; only orbits of period at most appear here. On a star-shaped level every orbit is contractible.
import Definitions.Def_FiniteEnergyPlane_OpenBook
namespace FiniteEnergyPlane
open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real
/-- Hryniewicz (Trans. AMS 2012), Lemma 7.7. Let `P` be a periodic Reeb orbit of Conley–Zehnder index
at least `3` such that every periodic orbit of period at most `P.T` is nondegenerate; let `0 < γ` be
smaller than every such period and every difference of two distinct such periods, and suppose
`Λ(K, P)` is sequentially compact in `C^∞_loc` for every compact `K ⊂ V 1 \ {0}` disjoint from the
cone `ℝ × x(ℝ)`. Let `y` be a Reeb trajectory and `v ∈ Λ({y 0}, P)` such that `y τ` lies in the image
of `proj H ∘ v` for some `τ > 0`. Then for every `l ≥ 1` there are `L, δ > 0` and a `C^l` family `U`
with `U(0, ·) = v` satisfying `IsPageFoliation`: its leaves at `t = 0` and `t = L` have the same
image, and `(0, L) × ℂ` parametrizes the complement in `S` of this leaf and of `x(ℝ)`. -/
theorem exists_page_foliation (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) (hnd : ∀ Q : ReebOrbit H, Q.T ≤ P.T → Q.IsNondegenerate)
(γ : ℝ) (hγ : 0 < γ) (hγ₁ : ∀ Q : ReebOrbit H, Q.T ≤ P.T → γ < Q.T)
(hγ₂ : ∀ Q₁ Q₂ : ReebOrbit H, Q₁.T ≤ P.T → Q₂.T ≤ P.T → Q₁.T ≠ Q₂.T → γ < |Q₁.T - Q₂.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 γ))
(y : ℝ → V 1) (hy : IsReebTrajectory H y) (v : ℂ → V 1)
(hv : v ∈ embeddedFastPlaneSet H J P {y 0} γ) (τ : ℝ) (hτ : 0 < τ)
(hret : y τ ∈ Set.range (fun z => proj H (v z))) (l : ℕ) (hl : 1 ≤ l) :
∃ L > 0, ∃ δ > 0, ∃ U : ℝ × ℂ → V 1, IsPageFoliation H J P γ y l L δ U ∧
∀ z, U (0, z) = v z := by
sorry
end FiniteEnergyPlane
Read-back
What the Lean code literally says, in plain math · claude-opus-5-5
FiniteEnergyPlane.exists_page_foliation
Let have strictly star-shaped level , let be a compatible -structure for , and let be a Reeb orbit of with "CZ index of at least ". Assume every Reeb orbit of with is nondegenerate (this includes , and any orbit counted with a period at most ). Let with:
- ;
- for every Reeb orbit with ;
- for all Reeb orbits with and .
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 Reeb trajectory, , with , and with .
Then there exist reals , and a map with for all such that, writing , is a page foliation, that is:
- is on , and for each one has (so );
- for every : ; is injective; and there are and with ;
- ;
- restricts to a bijection from onto .
The statement does not relate to . It asserts equality of the images at and but no equality of the maps. The hypotheses on quantify over all Reeb orbits of with period at most , with period meaning the recorded (not necessarily minimal) ; no hypothesis asserts that there are finitely many such orbits or periods, and no hypothesis is imposed on orbits of larger period.
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.