The resonant ellipse as a Hamiltonian flow line

This file assembles the four scalar Kepler equations into a derivative of the full phase-space curve and provides the chain-rule interface used to differentiate a candidate first integral along that curve.

noncomputable def LeanPool.PoincareThreeBody.rotatingKeplerVectorField (s : PhaseSpace) : PhaseSpace

Explicit rotating Kepler vector field away from the origin.

Equations

• LeanPool.PoincareThreeBody.rotatingKeplerVectorField s = ![s 2 + s 1, s 3 - s 0, s 3 - s 0 / √(s 0 ^ 2 + s 1 ^ 2) ^ 3, -s 2 - s 1 / √(s 0 ^ 2 + s 1 ^ 2) ^ 3]

theorem LeanPool.PoincareThreeBody.sqrt_positionSq_orientedResonantKeplerPhasePoint {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity orientation time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : √(orientedResonantKeplerPhasePoint p q eccentricity orientation time 0 ^ 2 + orientedResonantKeplerPhasePoint p q eccentricity orientation time 1 ^ 2) = eccentricRadius (resonantFirstAction p q) eccentricity (resonantEccentricAnomaly p q eccentricity time)

theorem LeanPool.PoincareThreeBody.hasDerivAt_orientedResonantKeplerPhasePoint {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity orientation time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : HasDerivAt (orientedResonantKeplerPhasePoint p q eccentricity orientation) (rotatingKeplerVectorField (orientedResonantKeplerPhasePoint p q eccentricity orientation time)) time

The derivative of the full resonant phase-space curve is the rotating Kepler vector field.

theorem LeanPool.PoincareThreeBody.HasFDerivAt.hasDerivAt_comp_orientedResonantKeplerPhasePoint {F : PhaseSpace → ℝ} {F' : PhaseSpace →L[ℝ] ℝ} {s : PhaseSpace} (hF : HasFDerivAt F F' s) {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity orientation time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hs : s = orientedResonantKeplerPhasePoint p q eccentricity orientation time) : HasDerivAt (fun (t : ℝ) => F (orientedResonantKeplerPhasePoint p q eccentricity orientation t)) (F' (rotatingKeplerVectorField s)) time

Chain rule for a scalar observable along the full resonant Kepler orbit.