Non-degenerate approximations of a star-shaped Hamiltonian, agreeing with it to first order along two given non-degenerate periodic orbits
OpenHryniewiczCriterion.exists_nondegenerate_approx_of_nondegenerate_along_orbitsLet be a strictly star-shaped level and let , be periodic orbits of on such that every periodic orbit of on whose image lies in (that is, , and all their iterates) is non-degenerate. Then there is a sequence of Hamiltonians such that
- every level is strictly star-shaped;
- every is non-degenerate: every periodic orbit of on , prime or multiply covered, is non-degenerate;
- and at every point of ;
- in .
in means: for every and every compact , uniformly on . A periodic orbit on (prime or not) is non-degenerate when, for its linearized flow , the linearized return map on , written in the global frame as the matrix of linearizedXiPath, does not have as an eigenvalue. A Hamiltonian is non-degenerate when all its periodic orbits on the level are.
Only the orbits and are assumed non-degenerate; the other periodic orbits of may be degenerate. In contact language this is the density, relative to a prescribed -jet along two non-degenerate closed orbits, of non-degenerate contact forms near (Kupka–Smale for Reeb flows).
import Definitions.Def_HryniewiczCriterion_ConleyZehnder import Definitions.Def_HryniewiczCriterion_GlobalSection import Definitions.Def_HryniewiczCriterion_SelfLinking open HryniewiczCriterion
theorem HryniewiczCriterion.exists_nondegenerate_approx_of_nondegenerate_along_orbits (H : R4 → ℝ) (hS : IsStrictlyStarShapedLevel H) (P Q : PeriodicOrbit H)
(hPQ : ∀ (R : PeriodicOrbit H), R.image ⊆ P.image ∪ Q.image →
∀ (Y : ℝ → (R4 →L[ℝ] R4)), IsLinearizedFlow H R.x Y →
∀ v : Fin 2 → ℝ, (linearizedXiPath H R Y 1).mulVec v = v → v = 0) :
∃ Hs : ℕ → R4 → ℝ, (∀ k, IsStrictlyStarShapedLevel (Hs k)) ∧
(∀ k (R : PeriodicOrbit (Hs k)) (Y : ℝ → (R4 →L[ℝ] R4)), IsLinearizedFlow (Hs k) R.x Y →
∀ v : Fin 2 → ℝ, (linearizedXiPath (Hs k) R Y 1).mulVec v = v → v = 0) ∧
(∀ k, ∀ y ∈ P.image ∪ Q.image, Hs k y = H y ∧ fderiv ℝ (Hs k) y = fderiv ℝ H y) ∧
(∀ m : ℕ, ∀ K : Set R4, IsCompact K →
TendstoUniformlyOn (fun k => iteratedFDeriv ℝ m (Hs k)) (iteratedFDeriv ℝ m H) Filter.atTop K) := by sorry