Asymptotic eigenvalue and eigenvector at a nondegenerate puncture
ProvedFiniteEnergyPlane.asymptotic_eigenvectorLet be a strictly star-shaped level, a smooth -compatible complex structure on , the open unit disk, and a finite-energy -holomorphic curve on . Suppose is a nondegenerate puncture of (Hryniewicz, Definition 2.9 (1), (2), (4)), asymptotic to a periodic Reeb orbit with sign , in the cylindrical coordinates at ; is not assumed nondegenerate. Then:
- there is such that has exponential asymptotics with rate : for some , both and decay like with all derivatives;
- if does not vanish identically on any punctured neighbourhood of , there are an eigenvalue of with and an eigenvector for such that, for large,
with and in as .
Formalization Note The hypothesis is IsNondegenerateEnd H u cylEnd P ε; the conclusions are HasExpAsymptoticsEnd and HasAsymptoticEigenvector (defined in FiniteEnergyPlane_Asymptotics). "Not identically zero near " is: every , , contains with dlambdaDensity H u z ≠ 0. Hryniewicz writes the leading term in a Martinet tube for ; here it is written in the tube , , in any dimension.
import Definitions.Def_FiniteEnergyPlane_Asymptotics
namespace FiniteEnergyPlane
open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real
/-- Hryniewicz, Theorem 2.11 and Lemma 2.12: let `u` be a finite-energy `J̃`-holomorphic curve on
`D \ {0}` whose puncture `0` is nondegenerate in the sense of Definition 2.9, asymptotic to a
periodic Reeb orbit `P` (not assumed nondegenerate) with sign `ε`. Then `u` converges to the
trivial cylinder over `P` exponentially fast in `C^∞`. If moreover `π du` does not vanish
identically near `0`, then `u` has an asymptotic eigenvalue `μ` with `εμ < 0` and an asymptotic
eigenvector `v` of `A_P` at the puncture. -/
theorem asymptotic_eigenvector {n : ℕ} (H : V n → ℝ) (hH : IsStrictlyStarShapedLevel H)
(J : V n → V n →L[ℝ] V n) (hJ : IsCompatibleXiStructure H J) (u : ℂ → V n)
(hu : IsFiniteEnergyCurve H J (ball 0 1 \ {0}) u) (P : ReebOrbit H) (ε : ℝ)
(hε : ε = 1 ∨ ε = -1) (hnd : IsNondegenerateEnd H u cylEnd P ε) :
(∃ b > 0, HasExpAsymptoticsEnd H u cylEnd P ε b) ∧
((∀ r > 0, ∃ z ∈ ball (0 : ℂ) r \ {0}, dlambdaDensity H u z ≠ 0) →
∃ (μ : ℝ) (v : ℝ → V n), HasAsymptoticEigenvector H J u cylEnd P ε μ v) := by
sorry
end FiniteEnergyPlane
Read-back
What the Lean code literally says, in plain math · claude-opus-5-5
Read-back: FiniteEnergyPlane.asymptotic_eigenvector
Ambient space and standard structures. Here is an arbitrary natural number and , with coordinates . carries the sup norm (this is the norm in every estimate below on -valued quantities). Define:
- by for even and for odd ;
- , , and ;
- for : , , and , with the convention (so wherever );
- .
Throughout, , , , , denote Fréchet derivatives, with the convention that the derivative of a function at a point where it is not differentiable is .
Hypothesis on ("strictly star-shaped level"). is ; for every there is exactly one with ; and whenever .
Hypothesis on ("compatible -structure"). is a map from to continuous linear maps ; it is , and for every with and all : ; ; if ; and . Nothing is required of outside or at points with .
Radial coordinates. For , let be a fixed (choice-selected) with if such exists, and otherwise. Put and .
Finite-energy curves. For defined on write and . For let , , , , , and
For put and . A function is admissible if it is , nondecreasing, and takes values in . For the energy is the value in
the integral being the Lebesgue integral of a nonnegative extended-real function. " is a finite-energy curve on " means: is on ; for all ; at every , is differentiable and ; and .
Reeb orbits. A Reeb orbit of consists of a map and a number such that, for all , , has derivative at , and . ( is a period of , not required to be the minimal one.)
Decay notions on half-cylinders. For (with or ), is the -th Fréchet derivative, measured in the operator norm of -linear maps, where carries the max norm ; .
- uniformly: for every there is with for all and all .
- in : there is such that is on , and for every and every there is with for all , .
- decays at rate in : there is such that is on , and for every there are reals with for all , .
End coordinates. (it tends to the puncture as ) and . For an end map put and .
- Asymptotically cylindrical end (for , , a real ): there exist such that in and in .
- Exponential asymptotics at rate (for , , , ): there exist such that and both decay at rate in .
- Nondegenerate end (for , , ): there exist with such that uniformly and uniformly.
Asymptotic eigenvector. For define
For , , an end map and a real , " is an asymptotic eigenvector of the end" means all of:
- is , -periodic, for all , for at least one , and for all ;
- ;
- there exist , , and such that in , in , and for all and all , with
one has and .
Statement. denotes the punctured open unit disk. Let , a strictly star-shaped level, a compatible -structure for , and a finite-energy curve on (nothing is assumed about outside ). Let be a Reeb orbit of (no nondegeneracy assumption on ), and let . Assume the end at parametrized by is a nondegenerate end over with sign : there are and with
uniformly in as , where and (only convergence is assumed).
Then both of the following hold:
- There exists such that the end (for , , ) has exponential asymptotics at rate (with some , existentially quantified).
- If for every there is with and (where ), then there exist and such that is an asymptotic eigenvector of the end for , the orbit and the sign (in particular , and the representation of in item 3 of that definition holds for ).
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.