Full phase-space Kepler orbits

The disturbing function only depends on position, so earlier files used zero placeholders for the momenta. The homological equation must instead be evaluated on a genuine Hamiltonian orbit. This file supplies the canonical rotating-frame momentum and embeds the resonant ellipse into the full four-dimensional phase space.

noncomputable def LeanPool.PoincareThreeBody.inertialEllipseVelocity (firstAction eccentricity meanMotion anomaly : ℝ) : ActionSpace

Inertial Cartesian velocity of the eccentric-anomaly ellipse when the mean anomaly advances at rate meanMotion.

Equations

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

noncomputable def LeanPool.PoincareThreeBody.orientedResonantEllipseMomentum (p q : ℕ) (eccentricity orientation time : ℝ) : ActionSpace

Canonical momentum of an oriented resonant ellipse in rotating coordinates.

Equations

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

def LeanPool.PoincareThreeBody.positionMomentumPhasePoint (position momentum : ActionSpace) : PhaseSpace

Embed planar position and canonical momentum into (x,y,pₓ,pᵧ) phase space.

Equations

• LeanPool.PoincareThreeBody.positionMomentumPhasePoint position momentum = ![position 0, position 1, momentum 0, momentum 1]

noncomputable def LeanPool.PoincareThreeBody.orientedResonantKeplerPhasePoint (p q : ℕ) (eccentricity orientation time : ℝ) : PhaseSpace

The genuine full phase-space orbit underlying the oriented resonant disturbing function.

Equations

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

theorem LeanPool.PoincareThreeBody.analyticAt_orientedResonantEllipseMomentum_coordinate (p q : ℕ) {eccentricity orientation time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (coordinate : Fin 2) : AnalyticAt ℝ (fun (argument : ℝ) => orientedResonantEllipseMomentum p q eccentricity orientation argument coordinate) time

Every coordinate of the true rotating-frame momentum is analytic in time.

theorem LeanPool.PoincareThreeBody.analyticAt_orientedResonantKeplerPhasePoint (p q : ℕ) {eccentricity orientation time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : AnalyticAt ℝ (orientedResonantKeplerPhasePoint p q eccentricity orientation) time

The genuine full resonant phase-space trajectory is analytic in time.

theorem LeanPool.PoincareThreeBody.hasDerivAt_resonantMeanAnomaly (p q : ℕ) (time : ℝ) : HasDerivAt (resonantMeanAnomaly p q) (resonantMeanMotion p q) time

theorem LeanPool.PoincareThreeBody.hasDerivAt_resonantEccentricAnomaly (p q : ℕ) {eccentricity time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : HasDerivAt (resonantEccentricAnomaly p q eccentricity) (resonantMeanMotion p q / (1 - eccentricity * Real.cos (resonantEccentricAnomaly p q eccentricity time))) time

theorem LeanPool.PoincareThreeBody.hasDerivAt_orientedResonantKeplerPhasePoint_position (p q : ℕ) {eccentricity orientation time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : HasDerivAt (fun (t : ℝ) => orientedResonantKeplerPhasePoint p q eccentricity orientation t 0) (orientedResonantKeplerPhasePoint p q eccentricity orientation time 2 + orientedResonantKeplerPhasePoint p q eccentricity orientation time 1) time ∧ HasDerivAt (fun (t : ℝ) => orientedResonantKeplerPhasePoint p q eccentricity orientation t 1) (orientedResonantKeplerPhasePoint p q eccentricity orientation time 3 - orientedResonantKeplerPhasePoint p q eccentricity orientation time 0) time

The position part of the full resonant state satisfies the first two canonical Hamilton equations in the rotating frame.

theorem LeanPool.PoincareThreeBody.hasDerivAt_inertialEllipseVelocity_resonant {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (coordinate : Fin 2) : HasDerivAt (fun (t : ℝ) => inertialEllipseVelocity (resonantFirstAction p q) eccentricity (resonantMeanMotion p q) (resonantEccentricAnomaly p q eccentricity t) coordinate) (-inertialEllipsePosition (resonantFirstAction p q) eccentricity (resonantEccentricAnomaly p q eccentricity time) coordinate / eccentricRadius (resonantFirstAction p q) eccentricity (resonantEccentricAnomaly p q eccentricity time) ^ 3) time

In inertial coordinates, the resonant ellipse satisfies Newton's inverse-square acceleration law.

theorem LeanPool.PoincareThreeBody.hasDerivAt_orientedResonantKeplerPhasePoint_momentum {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity orientation time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : have radius := eccentricRadius (resonantFirstAction p q) eccentricity (resonantEccentricAnomaly p q eccentricity time); HasDerivAt (fun (t : ℝ) => orientedResonantKeplerPhasePoint p q eccentricity orientation t 2) (orientedResonantKeplerPhasePoint p q eccentricity orientation time 3 - orientedResonantKeplerPhasePoint p q eccentricity orientation time 0 / radius ^ 3) time ∧ HasDerivAt (fun (t : ℝ) => orientedResonantKeplerPhasePoint p q eccentricity orientation t 3) (-orientedResonantKeplerPhasePoint p q eccentricity orientation time 2 - orientedResonantKeplerPhasePoint p q eccentricity orientation time 1 / radius ^ 3) time

The momentum part of the rotating resonant state satisfies the remaining two Kepler Hamilton equations.

@[simp]

theorem LeanPool.PoincareThreeBody.orientedResonantKeplerPhasePoint_position_zero (p q : ℕ) (eccentricity orientation time : ℝ) : orientedResonantKeplerPhasePoint p q eccentricity orientation time 0 = orientedResonantEllipsePosition p q eccentricity orientation time 0

@[simp]

theorem LeanPool.PoincareThreeBody.orientedResonantKeplerPhasePoint_position_one (p q : ℕ) (eccentricity orientation time : ℝ) : orientedResonantKeplerPhasePoint p q eccentricity orientation time 1 = orientedResonantEllipsePosition p q eccentricity orientation time 1

theorem LeanPool.PoincareThreeBody.orientedResonantEllipseMomentum_add_period {p q : ℕ} (hp : 0 < p) {eccentricity orientation : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (time : ℝ) : orientedResonantEllipseMomentum p q eccentricity orientation (time + resonantOrbitPeriod p) = orientedResonantEllipseMomentum p q eccentricity orientation time

Adding the common resonant period preserves the true canonical momentum.

theorem LeanPool.PoincareThreeBody.orientedResonantKeplerPhasePoint_add_period {p q : ℕ} (hp : 0 < p) {eccentricity orientation : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (time : ℝ) : orientedResonantKeplerPhasePoint p q eccentricity orientation (time + resonantOrbitPeriod p) = orientedResonantKeplerPhasePoint p q eccentricity orientation time

The full resonant phase-space trajectory has the common period.

theorem LeanPool.PoincareThreeBody.firstMassPerturbation_orientedResonantKeplerPhasePoint (p q : ℕ) (eccentricity orientation time : ℝ) : firstMassPerturbation (orientedResonantKeplerPhasePoint p q eccentricity orientation time) = resonantDisturbingFunction p q eccentricity orientation time

Replacing the momentum placeholder by the true momentum does not change the first mass perturbation.

theorem LeanPool.PoincareThreeBody.orientedResonantKeplerPhasePoint_collisionFree_mass_zero {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity orientation time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) : (0, orientedResonantKeplerPhasePoint p q eccentricity orientation time) ∈ collisionFree

Collision-freeness at mass zero depends only on the position, so the full phase-space orbit inherits the collision exclusion proved for the interior ellipse.