Compactness of fast finite-energy planes
ProvedFiniteEnergyPlane.isSeqCompact_fastPlaneSetLet have a strictly star-shaped level (in the sense of HryniewiczCriterion), the same function on , a smooth -compatible complex structure on and a periodic Reeb orbit of . Suppose every periodic orbit of HryniewiczCriterion of action at most is nondegenerate and has . Let be smaller than every period at most and than every difference of two distinct such periods, and let be compact with , where . Then is sequentially compact in .
Formalization Note The orbit hypotheses have the form of exists_transverse_disk_open_book_of_approx at a single level: for every R : PeriodicOrbit H₀ and Y with IsLinearizedFlow H₀ R.x Y and action , linearizedXiPath H₀ R Y 1 fixes no nonzero vector and 3 ≤ czIndexOfPath (linearizedXiPath H₀ R Y). is ∀ y ∈ K, proj H y ∉ Set.range P.x. is fastPlaneSet H J P K γ.
import Definitions.Def_FiniteEnergyPlane_Compactness
namespace FiniteEnergyPlane
open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real
/-- Hryniewicz (Trans. AMS 2012), Theorem 2.2 (2), for `Θ`; Hryniewicz (J. Symplectic Geom. 2014),
Theorem 3.10. Let `S = H⁻¹(1) ⊂ ℝ⁴` be strictly star-shaped and `P` a periodic Reeb orbit. Suppose
every periodic orbit of `HryniewiczCriterion` of action at most `P.T` is nondegenerate with
Conley–Zehnder index at least `3` (as in `exists_transverse_disk_open_book_of_approx`), let
`0 < γ` be smaller than every period at most `P.T` and every difference of two distinct such
periods, and let `K ⊂ V 1 \ {0}` be a compact set disjoint from the cone `ℝ × x(ℝ)` over the image
of `P`. Then `fastPlaneSet H J P K γ` is sequentially compact in `C^∞_loc(ℂ, V 1)`. -/
theorem isSeqCompact_fastPlaneSet (H₀ : HryniewiczCriterion.R4 → ℝ)
(hH₀ : HryniewiczCriterion.IsStrictlyStarShapedLevel H₀) :
let H : V 1 → ℝ := fun y => H₀ (fun k => y (Fin.cast (by norm_num) k))
∀ J : V 1 → V 1 →L[ℝ] V 1, IsCompatibleXiStructure H J → ∀ P : ReebOrbit H,
(∀ (R : HryniewiczCriterion.PeriodicOrbit H₀)
(Y : ℝ → (HryniewiczCriterion.R4 →L[ℝ] HryniewiczCriterion.R4)),
HryniewiczCriterion.IsLinearizedFlow H₀ R.x Y →
(∫ t in (0 : ℝ)..R.T, HryniewiczCriterion.liouvilleForm (R.x t) (deriv R.x t)) ≤ P.T →
∀ v : Fin 2 → ℝ, (HryniewiczCriterion.linearizedXiPath H₀ R Y 1).mulVec v = v → v = 0) →
(∀ (R : HryniewiczCriterion.PeriodicOrbit H₀)
(Y : ℝ → (HryniewiczCriterion.R4 →L[ℝ] HryniewiczCriterion.R4)),
HryniewiczCriterion.IsLinearizedFlow H₀ R.x Y →
(∫ t in (0 : ℝ)..R.T, HryniewiczCriterion.liouvilleForm (R.x t) (deriv R.x t)) ≤ P.T →
3 ≤ HryniewiczCriterion.czIndexOfPath (HryniewiczCriterion.linearizedXiPath H₀ R Y)) →
∀ γ : ℝ, 0 < γ → (∀ Q : ReebOrbit H, Q.T ≤ P.T → γ < Q.T) →
(∀ Q₁ Q₂ : ReebOrbit H, Q₁.T ≤ P.T → Q₂.T ≤ P.T → Q₁.T ≠ Q₂.T → γ < |Q₁.T - Q₂.T|) →
∀ K : Set (V 1), IsCompact K → (0 : V 1) ∉ K → (∀ y ∈ K, proj H y ∉ Set.range P.x) →
IsSeqCompactCInftyLoc (fastPlaneSet H J P K γ) := by
sorry
end FiniteEnergyPlane
Read-back
What the Lean code literally says, in plain math · claude-opus-5-5
Read-back: FiniteEnergyPlane.isSeqCompact_fastPlaneSet
Ambient notation. Work in with coordinates (the dimension with ). Let , , , , and . The Reeb field is (with ). Write and .
- Strictly star-shaped level : is ; every has exactly one with ; whenever .
- Compatible -structure : is , and for every and : , , if , . Nothing is required off or outside .
- Scaling, projection, -coordinate. is some with if one exists (chosen by choice), otherwise ; ; . As always, , so .
- : for , with , , , , : .
- Derivatives. For on : , (real Fréchet derivative; where not differentiable).
- Energies. Admissible : , non-decreasing, values in . With , and , the energy is , and the -energy is (Lebesgue measure; negative parts of the densities are cut off before integrating).
- Finite-energy curve on : is on , on , at every it is differentiable with , and .
- Reeb orbit : a map and a number with , , . is any period, not necessarily minimal, so multiple covers count as separate orbits. is prime if for . is nondegenerate if for every with and for all , every with is .
- Hamiltonian periodic orbits and the index . A Hamiltonian periodic orbit of a function on is , with , , . A linearized flow along is with , . With , , the Euclidean norm, set , (division by read as multiplication by ), the coordinates , and . The linearized -path is the matrix path
For a matrix path , an angle lift from is , continuous on , with and, for each , for some . Let , , (real infimum/supremum, which take the value when is empty or unbounded on that side), and
- "CZ index at least " for a Reeb orbit of : for every Hamiltonian periodic orbit of with and , and every linearized flow along , . (Vacuous if no such exists.)
- Cylindrical end at infinity , with , . has a nondegenerate end at asymptotic to if there are , with and as .
- Winding and zero index. A loop has winding if it is continuous, -periodic, never , and for some continuous with . has zero index at if and for some , on and every loop , , has winding .
- : with (the frame built from ) and , put with .
- Fast plane: is a finite-energy curve on all of ; there is a prime Reeb orbit such that has a nondegenerate end at asymptotic to ; and the zero set of in is a finite set for which there are integers , each the zero index of at , with .
- The set (for a Reeb orbit , , ): all that are fast planes, have a nondegenerate end at asymptotic to , satisfy , and satisfy .
- convergence on : means that for every compact and every , the -th iterated real Fréchet derivatives converge to uniformly on (the iterated derivatives are total functions, defined at every point).
- Sequential -compactness of a set of maps : for every sequence in there are a strictly increasing and with in on all of .
Statement. Let be a strictly star-shaped level function (same definition as above: , unique positive radial solution of for each , on ). Let be read on through the coordinate identification that matches coordinate with coordinate (so and are the same function of ). Then for every compatible -structure for and every Reeb orbit of , the following holds.
Assume, for every Hamiltonian periodic orbit of (any period , not necessarily prime, not required to be related to ) and every linearized flow along , whenever the action satisfies
(here ):
- (i) every with is (i.e. is not an eigenvalue of ); and
- (ii) .
Let with , for every Reeb orbit of with , and for all Reeb orbits of with and . Let be compact with and with for every .
Then is sequentially -compact: every sequence in has a strictly increasing subsequence converging in on all of to an element of .
Remarks on the literal content. Hypotheses (i) and (ii) are stated for Hamiltonian periodic orbits of parametrized by the Hamiltonian vector field (not the Reeb field), selected by an action bound , and for every linearized flow along them; they are not stated in terms of Reeb orbits of or their nondegeneracy as defined above. In (i), is the matrix built from . and are universally quantified before the hypotheses, so (i), (ii), the conditions on and the condition on all refer to the given . If is empty (for instance ), the conclusion holds vacuously.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.