Limits of sequences of fast planes
ProvedFiniteEnergyPlane.exists_subseq_tendsto_of_fastPlaneSetLet be a strictly star-shaped level and a smooth -compatible complex structure on . Let be a periodic Reeb orbit such that every periodic Reeb orbit of period at most is nondegenerate with , let be smaller than every such period and than every difference of two distinct such periods, and let be compact. Let be a sequence in and write . Then there are a subsequence , a finite set in the closed unit disk and a finite-energy -holomorphic curve on with such that the shifted planes (the -coordinate shifted by ) converge to in , and one of the following holds:
- , , , and meets the cylinder over ;
- , , , and in , where and .
Formalization Note Periods are those of ReebOrbit H (not necessarily minimal, so multiple covers count); is Q.IsCZAtLeast 3. "" is: for every , eventually some has . "" is: for every , eventually everywhere and somewhere. "" is piDs H w z = 0 for all .
import Definitions.Def_FiniteEnergyPlane_Compactness
namespace FiniteEnergyPlane
open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real
/-- Hryniewicz (Trans. AMS 2012), Lemma 4.17. Let `P` be a periodic Reeb orbit on `S ⊂ ℝ⁴` such
that every periodic orbit of period at most `P.T` is nondegenerate with Conley–Zehnder index at
least `3`, let `0 < γ` be smaller than every such period and every difference of two distinct such
periods, and let `K ⊂ V 1 \ {0}` be compact. For every sequence `uₖ` in `fastPlaneSet H J P K γ`
there are a subsequence, a finite set `Γ` in the closed unit disk and a finite-energy
`J̃`-holomorphic curve `w` on `ℂ \ Γ` with `0 < E(w) ≤ P.T` such that the shifted planes
`e^{-2aₖ(2)} • uₖ` (`aₖ = aCoord H ∘ uₖ`) converge to `w` in `C^∞_loc(ℂ \ Γ)`, and one of the
following holds:
* `inf aₖ → -∞`, `Γ` has one point, `π dw ≡ 0`, and `K` meets the cone over the image of `P`;
* `inf aₖ → A ∈ ℝ`, `Γ = ∅`, `aₖ(2) → c`, and `uₖ → e^{2c} • w` in `C^∞_loc(ℂ)`, where
`e^{2c} • w` belongs to `fastPlaneSet H J P K γ` and its coordinate `a` is at least `A`. -/
theorem exists_subseq_tendsto_of_fastPlaneSet (H : V 1 → ℝ) (hH : IsStrictlyStarShapedLevel H)
(J : V 1 → V 1 →L[ℝ] V 1) (hJ : IsCompatibleXiStructure H J)
(P : ReebOrbit H)
(hP : ∀ Q : ReebOrbit H, Q.T ≤ P.T → Q.IsNondegenerate ∧ Q.IsCZAtLeast 3)
(γ : ℝ) (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|)
(K : Set (V 1)) (hK : IsCompact K) (hK0 : (0 : V 1) ∉ K)
(u : ℕ → ℂ → V 1) (hu : ∀ k, u k ∈ fastPlaneSet H J P K γ) :
∃ φ : ℕ → ℕ, StrictMono φ ∧ ∃ Γ : Finset ℂ, (∀ z ∈ Γ, ‖z‖ ≤ 1) ∧ ∃ w : ℂ → V 1,
IsFiniteEnergyCurve H J (↑Γ)ᶜ w ∧ energy H (↑Γ)ᶜ w ≠ 0 ∧
energy H (↑Γ)ᶜ w ≤ ENNReal.ofReal P.T ∧
JHolomorphic.TendstoCInftyLocOn
(fun k z => Real.exp (-(2 * aCoord H (u (φ k) 2))) • u (φ k) z) w (↑Γ)ᶜ ∧
(((∀ M : ℝ, ∀ᶠ k in atTop, ∃ z, aCoord H (u (φ k) z) ≤ M) ∧ Γ.card = 1 ∧
(∀ z ∉ Γ, piDs H w z = 0) ∧ ∃ y ∈ K, proj H y ∈ Set.range P.x) ∨
∃ A : ℝ, (∀ ε > 0, ∀ᶠ k in atTop, ∀ z, A - ε ≤ aCoord H (u (φ k) z)) ∧
(∀ ε > 0, ∀ᶠ k in atTop, ∃ z, aCoord H (u (φ k) z) ≤ A + ε) ∧ Γ = ∅ ∧
∃ c : ℝ, Tendsto (fun k => aCoord H (u (φ k) 2)) atTop (𝓝 c) ∧
JHolomorphic.TendstoCInftyLocOn (fun k => u (φ k))
(fun z => Real.exp (2 * c) • w z) Set.univ ∧
(fun z => Real.exp (2 * c) • w z) ∈ fastPlaneSet H J P K γ ∧
∀ z, A ≤ aCoord H (Real.exp (2 * c) • w z)) := by
sorry
end FiniteEnergyPlane
Read-back
What the Lean code literally says, in plain math · claude-opus-5-5
Read-back: FiniteEnergyPlane.exists_subseq_tendsto_of_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 .
Common hypotheses. is a strictly star-shaped level function and is a compatible -structure. is a Reeb orbit of such that every Reeb orbit with (including itself and all multiple covers with period ) is nondegenerate and has CZ index at least in the sense above. satisfies , for every Reeb orbit with , and for all Reeb orbits with and . is compact with ( is allowed).
Statement. Under the common hypotheses, let be a sequence with for every . Then there exist a strictly increasing , a finite set with for every , and a map such that:
- is a finite-energy curve on ;
- ;
- the rescaled maps
(rescaling by the constant attached to the value at the point ) converge to in on ;
and at least one of the following two alternatives holds (inclusive "or"):
(a) for every , for all sufficiently large there is with ; has exactly one element; for every ; and there is with .
(b) there is such that
- for every , for all sufficiently large : for all ;
- for every , for all sufficiently large : there is with ;
- ;
and there is such that , the unrescaled subsequence converges in on all of to , the map belongs to , and for every .
Remarks on the literal content. The energy bound in 2 compares an element of with the real number . In (a), the first clause says eventually drops below every bound; nothing is said there about convergence of itself. In (a), " off " is computed from the total-function definition of . The common hypotheses on Reeb orbits only concern orbits with period .
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.