Exponential decay of the normal component of a nondegenerate end in tube coordinates
ProvedFiniteEnergyPlane.exists_expDecay_tubeNormalLet be a strictly star-shaped level with contact planes , a smooth -compatible complex structure on , a finite-energy -holomorphic curve on and a periodic Reeb orbit, , . In the cylindrical coordinates at write for the symplectization coordinate and for the radial projection of . Suppose that for
with and , where and in , uniformly in , as . If is nondegenerate, then decays exponentially: there are , and with for all and all .
This is the exponential decay of the normal part of an asymptotically cylindrical end at a nondegenerate orbit (Wendl, Proposition 6.7.1).
Formalization Note proj H is the radial projection onto , IsInXi H x v means , and convergence is TendstoZeroCInfty (smooth on some , every derivative tends to uniformly in ). and are endA H u cylEnd and endW H u cylEnd; norms on are sup norms.
import Definitions.Def_FiniteEnergyPlane_Asymptotics
namespace FiniteEnergyPlane
open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real
/-- Let `u` be a finite-energy `J̃`-holomorphic curve on `D \ {0}` and `P = (x, T)` a nondegenerate
periodic Reeb orbit. Suppose that, in the cylindrical coordinates `cylEnd` at `0` and for `s ≥ s₀`,
`w = proj H (x(τ) + h)` with `h ∈ ξ_{x(τ)}`, `τ(s, t + 1) = τ(s, t) + εT` and `h` `1`-periodic,
where `τ(s, t) - εTt - c → 0` and `h → 0` in `C^∞`. Then the normal component `h` decays
exponentially: `‖h(s, t)‖ ≤ C e^{-δs}` for some `δ > 0`. -/
theorem exists_expDecay_tubeNormal {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) (hP : P.IsNondegenerate)
(ε : ℝ) (hε : ε = 1 ∨ ε = -1) (c : ℝ) (τ : ℝ × ℝ → ℝ) (h : ℝ × ℝ → V n) (s₀ : ℝ)
(hτ : TendstoZeroCInfty (fun p : ℝ × ℝ => τ p - ε * P.T * p.2 - c))
(hh : TendstoZeroCInfty h)
(hrep : ∀ s ≥ s₀, ∀ t : ℝ,
τ (s, t + 1) = τ (s, t) + ε * P.T ∧ h (s, t + 1) = h (s, t) ∧
IsInXi H (P.x (τ (s, t))) (h (s, t)) ∧
endW H u cylEnd (s, t) = proj H (P.x (τ (s, t)) + h (s, t))) :
∃ δ > 0, ∃ C s₁ : ℝ, ∀ s ≥ s₁, ∀ t : ℝ, ‖h (s, t)‖ ≤ C * Real.exp (-(δ * s)) := by
sorry
end FiniteEnergyPlane