Delaunay frequencies and resonant actions

At zero mass the planar rotating Kepler Hamiltonian in Delaunay actions is -1 / (2 * I₁²) - I₂, with frequency (I₁⁻³, -1). Positive rational frequency ratios give an explicit family of resonant actions.

noncomputable def LeanPool.PoincareThreeBody.delaunayHamiltonian (action : ActionSpace) : ℝ

The rotating Kepler Hamiltonian in planar Delaunay actions.

Equations

• LeanPool.PoincareThreeBody.delaunayHamiltonian action = -1 / (2 * action 0 ^ 2) - action 1

noncomputable def LeanPool.PoincareThreeBody.delaunayFrequency (firstAction : ℝ) : ActionSpace

The frequency of the rotating Kepler Hamiltonian.

Equations

• LeanPool.PoincareThreeBody.delaunayFrequency firstAction = ![1 / firstAction ^ 3, -1]

noncomputable def LeanPool.PoincareThreeBody.resonantFirstAction (p q : ℕ) : ℝ

A positive Delaunay action whose Kepler frequency ratio is the positive rational q / p.

Equations

• LeanPool.PoincareThreeBody.resonantFirstAction p q = (↑p / ↑q) ^ 3⁻¹

def LeanPool.PoincareThreeBody.resonanceVector (p q : ℕ) : ActionSpace

The integer resonance vector, regarded as a real vector.

Equations

• LeanPool.PoincareThreeBody.resonanceVector p q = ![↑p, ↑q]

theorem LeanPool.PoincareThreeBody.hasDerivAt_delaunayHamiltonian_firstAction {firstAction : ℝ} (hfirstAction : firstAction ≠ 0) (secondAction : ℝ) : HasDerivAt (fun (action : ℝ) => -1 / (2 * action ^ 2) - secondAction) (1 / firstAction ^ 3) firstAction

theorem LeanPool.PoincareThreeBody.hasDerivAt_delaunayHamiltonian_secondAction (firstAction secondAction : ℝ) : HasDerivAt (fun (action : ℝ) => -1 / (2 * firstAction ^ 2) - action) (-1) secondAction

theorem LeanPool.PoincareThreeBody.deriv_delaunayHamiltonian_firstAction {firstAction : ℝ} (hfirstAction : firstAction ≠ 0) (secondAction : ℝ) : deriv (fun (action : ℝ) => -1 / (2 * action ^ 2) - secondAction) firstAction = 1 / firstAction ^ 3

theorem LeanPool.PoincareThreeBody.deriv_delaunayHamiltonian_secondAction (firstAction secondAction : ℝ) : deriv (fun (action : ℝ) => -1 / (2 * firstAction ^ 2) - action) secondAction = -1

theorem LeanPool.PoincareThreeBody.delaunayFrequency_eq_coordinateDerivatives {firstAction : ℝ} (hfirstAction : firstAction ≠ 0) (secondAction : ℝ) : delaunayFrequency firstAction = ![deriv (fun (action : ℝ) => delaunayHamiltonian ![action, secondAction]) firstAction, deriv (fun (action : ℝ) => delaunayHamiltonian ![firstAction, action]) secondAction]

The displayed Kepler frequency is the coordinate gradient of the Delaunay Hamiltonian.

theorem LeanPool.PoincareThreeBody.resonantFirstAction_pos {p q : ℕ} (hp : 0 < p) (hq : 0 < q) : 0 < resonantFirstAction p q

theorem LeanPool.PoincareThreeBody.resonantFirstAction_cube {p q : ℕ} (hp : 0 < p) (hq : 0 < q) : resonantFirstAction p q ^ 3 = ↑p / ↑q

theorem LeanPool.PoincareThreeBody.resonanceVector_ne_zero {p q : ℕ} (hp : 0 < p) : resonanceVector p q ≠ 0

theorem LeanPool.PoincareThreeBody.resonantFirstAction_is_resonant {p q : ℕ} (hp : 0 < p) (hq : 0 < q) : dot (resonanceVector p q) (delaunayFrequency (resonantFirstAction p q)) = 0

Every pair of positive natural numbers determines an exact Kepler resonance.

theorem LeanPool.PoincareThreeBody.exists_resonantFirstAction_between {a b : ℝ} (ha : 0 < a) (hab : a < b) : ∃ (p : ℕ) (q : ℕ), 0 < p ∧ 0 < q ∧ a < resonantFirstAction p q ∧ resonantFirstAction p q < b

Positive rational Kepler resonances occur in every positive open interval.

@[reducible, inline]

abbrev LeanPool.PoincareThreeBody.PositiveAction : Set ℝ

The positive first Delaunay action axis.

Equations

• LeanPool.PoincareThreeBody.PositiveAction = Set.Ioi 0

def LeanPool.PoincareThreeBody.irrationalFrequencyPositiveActions : Set ↑PositiveAction

The positive actions whose Kepler frequency is irrational.

Equations

• LeanPool.PoincareThreeBody.irrationalFrequencyPositiveActions = {action : ↑LeanPool.PoincareThreeBody.PositiveAction | Irrational (1 / ↑action ^ 3)}

theorem LeanPool.PoincareThreeBody.exists_irrationalFrequencyAction_between {a b : ℝ} (ha : 0 < a) (hab : a < b) : ∃ (action : ℝ), a < action ∧ action < b ∧ Irrational (1 / action ^ 3)

Actions with irrational Kepler frequency occur in every positive open interval.

theorem LeanPool.PoincareThreeBody.irrationalFrequencyPositiveActions_dense : Dense irrationalFrequencyPositiveActions

Positive actions with irrational Kepler frequency form a dense set.

def LeanPool.PoincareThreeBody.resonantPositiveActions : Set ↑PositiveAction

The positive actions with a rational Kepler frequency ratio.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.PoincareThreeBody.resonantPositiveActions_dense : Dense resonantPositiveActions

theorem LeanPool.PoincareThreeBody.continuous_delaunayFrequencyOnPositive : Continuous fun (action : ↑PositiveAction) => delaunayFrequency ↑action

theorem LeanPool.PoincareThreeBody.delaunayDenseResonance_obstruction {differential : ↑PositiveAction → ActionSpace} (hdifferential : Continuous differential) (hresonant : ∀ {p q : ℕ} (hp : 0 < p) (hq : 0 < q), dot (resonanceVector p q) (differential ⟨resonantFirstAction p q, ⋯⟩) = 0) (action : ↑PositiveAction) : ¬LinearIndependent ℝ ![delaunayFrequency ↑action, differential action]

Orthogonality at every rational Kepler resonance forces dependence at every positive action.

theorem LeanPool.PoincareThreeBody.delaunayHomological_obstruction {differential : ↑PositiveAction → ActionSpace} (hdifferential : Continuous differential) (correction perturbation : ℕ → ℕ → ℝ) (hperturbation : ∀ (p q : ℕ), 0 < p → 0 < q → perturbation p q ≠ 0) (hequation : ∀ (p q : ℕ) (hp : 0 < p) (hq : 0 < q), dot (resonanceVector p q) (delaunayFrequency (resonantFirstAction p q)) * correction p q + dot (resonanceVector p q) (differential ⟨resonantFirstAction p q, ⋯⟩) * perturbation p q = 0) (action : ↑PositiveAction) : ¬LinearIndependent ℝ ![delaunayFrequency ↑action, differential action]

The first homological equation and nonvanishing perturbing modes at all rational resonances exclude an independent leading integral throughout the positive Delaunay action axis.

theorem LeanPool.PoincareThreeBody.rationalKeplerResonance_obstruction {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {differential : ActionSpace} (hdifferential : dot (resonanceVector p q) differential = 0) : ¬LinearIndependent ℝ ![delaunayFrequency (resonantFirstAction p q), differential]

The abstract linear-algebra obstruction at every positive rational Kepler resonance.