Differential of the rotating Kepler Hamiltonian

We compute the Fréchet derivative of the mass-zero Hamiltonian and identify its Hamiltonian vector field with rotatingKeplerVectorField. Consequently, a Poisson bracket with the Kepler Hamiltonian is exactly differentiation along a Kepler flow line.

noncomputable def LeanPool.PoincareThreeBody.rotatingKeplerDifferential (s : PhaseSpace) : PhaseSpace →L[ℝ] ℝ

Explicit differential of the rotating Kepler Hamiltonian.

Equations

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

theorem LeanPool.PoincareThreeBody.hasFDerivAt_hamiltonian_zero {s : PhaseSpace} (horigin : s 0 ^ 2 + s 1 ^ 2 ≠ 0) : HasFDerivAt (hamiltonian 0) (rotatingKeplerDifferential s) s

Fréchet derivative of the mass-zero Hamiltonian away from the Kepler collision.

theorem LeanPool.PoincareThreeBody.fderiv_hamiltonian_zero {s : PhaseSpace} (horigin : s 0 ^ 2 + s 1 ^ 2 ≠ 0) : fderiv ℝ (hamiltonian 0) s = rotatingKeplerDifferential s

theorem LeanPool.PoincareThreeBody.poissonBracket_hamiltonian_zero_eq_fderiv_apply (F : PhaseSpace → ℝ) {s : PhaseSpace} (horigin : s 0 ^ 2 + s 1 ^ 2 ≠ 0) : poissonBracket F (hamiltonian 0) s = (fderiv ℝ F s) (rotatingKeplerVectorField s)

The Poisson bracket with the Kepler Hamiltonian is the directional derivative along its explicit Hamiltonian vector field.

theorem LeanPool.PoincareThreeBody.DifferentiableAt.hasDerivAt_comp_orientedResonantKeplerPhasePoint {F : PhaseSpace → ℝ} {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity orientation time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hF : DifferentiableAt ℝ F (orientedResonantKeplerPhasePoint p q eccentricity orientation time)) : HasDerivAt (fun (t : ℝ) => F (orientedResonantKeplerPhasePoint p q eccentricity orientation t)) (poissonBracket F (hamiltonian 0) (orientedResonantKeplerPhasePoint p q eccentricity orientation time)) time

Along the true resonant orbit, the time derivative of any differentiable observable is its Poisson bracket with the mass-zero Hamiltonian.