Elliptic Kepler positions in the rotating frame

The eccentric-anomaly ellipse has a simple Cartesian parameterization in the inertial frame. Rotating it through minus the physical time gives the position used in the circular restricted three-body Hamiltonian. This file verifies the radius and distance identities needed to restrict the first mass perturbation to a resonant Kepler orbit.

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

Cartesian position on an inertial Kepler ellipse, with periapsis on the positive x-axis.

Equations

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

noncomputable def LeanPool.PoincareThreeBody.positionInRotatingFrame (time : ℝ) (position : ActionSpace) : ActionSpace

A planar position expressed in coordinates rotating counterclockwise through angle time.

Equations

• LeanPool.PoincareThreeBody.positionInRotatingFrame time position = ![Real.cos time * position 0 + Real.sin time * position 1, -Real.sin time * position 0 + Real.cos time * position 1]

noncomputable def LeanPool.PoincareThreeBody.rotatingEllipsePosition (firstAction eccentricity anomaly time : ℝ) : ActionSpace

Position of the Kepler ellipse in the rotating frame.

Equations

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

def LeanPool.PoincareThreeBody.positionPhasePoint (position : ActionSpace) : PhaseSpace

Embed a planar position into phase space with zero placeholder momenta. The first mass perturbation depends only on position, so these momentum entries are immaterial.

Equations

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

noncomputable def LeanPool.PoincareThreeBody.rotatingEllipsePhasePoint (firstAction eccentricity anomaly time : ℝ) : PhaseSpace

A rotating elliptic position embedded in the restricted three-body phase space.

Equations

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

theorem LeanPool.PoincareThreeBody.inertialEllipsePosition_sq {firstAction eccentricity anomaly : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity ≤ 1) : inertialEllipsePosition firstAction eccentricity anomaly 0 ^ 2 + inertialEllipsePosition firstAction eccentricity anomaly 1 ^ 2 = eccentricRadius firstAction eccentricity anomaly ^ 2

theorem LeanPool.PoincareThreeBody.positionInRotatingFrame_sq (time : ℝ) (position : ActionSpace) : positionInRotatingFrame time position 0 ^ 2 + positionInRotatingFrame time position 1 ^ 2 = position 0 ^ 2 + position 1 ^ 2

theorem LeanPool.PoincareThreeBody.positionInRotatingFrame_add (firstAngle secondAngle : ℝ) (position : ActionSpace) : positionInRotatingFrame (firstAngle + secondAngle) position = positionInRotatingFrame firstAngle (positionInRotatingFrame secondAngle position)

theorem LeanPool.PoincareThreeBody.rotatingEllipsePosition_sq {firstAction eccentricity anomaly time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity ≤ 1) : rotatingEllipsePosition firstAction eccentricity anomaly time 0 ^ 2 + rotatingEllipsePosition firstAction eccentricity anomaly time 1 ^ 2 = eccentricRadius firstAction eccentricity anomaly ^ 2

theorem LeanPool.PoincareThreeBody.rotatingEllipse_primaryDistance_ne_zero_of_apoapsis_lt_one {firstAction eccentricity anomaly time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : firstAction ^ 2 * (1 + eccentricity) < 1) : (rotatingEllipsePosition firstAction eccentricity anomaly time 0 - 1) ^ 2 + rotatingEllipsePosition firstAction eccentricity anomaly time 1 ^ 2 ≠ 0

An ellipse whose apoapsis is strictly inside the unit circle cannot meet the unit primary.

theorem LeanPool.PoincareThreeBody.primaryDistanceSq_positionPhasePoint (position : ActionSpace) : (positionPhasePoint position 0 - 1) ^ 2 + positionPhasePoint position 1 ^ 2 = position 0 ^ 2 + position 1 ^ 2 - 2 * position 0 + 1

theorem LeanPool.PoincareThreeBody.firstMassPerturbation_rotatingEllipse {firstAction eccentricity anomaly time : ℝ} (hfirstAction : firstAction ≠ 0) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : firstMassPerturbation (rotatingEllipsePhasePoint firstAction eccentricity anomaly time) = 1 / eccentricRadius firstAction eccentricity anomaly + rotatingEllipsePosition firstAction eccentricity anomaly time 0 / eccentricRadius firstAction eccentricity anomaly ^ 3 - 1 / √(eccentricRadius firstAction eccentricity anomaly ^ 2 - 2 * rotatingEllipsePosition firstAction eccentricity anomaly time 0 + 1)

Restriction of the first mass perturbation to an elliptic Kepler position, written in terms of its radius and rotating x-coordinate.

theorem LeanPool.PoincareThreeBody.firstMassPerturbation_rotatingEllipse_sourceForm {firstAction eccentricity anomaly time : ℝ} (hfirstAction : firstAction ≠ 0) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : firstMassPerturbation (rotatingEllipsePhasePoint firstAction eccentricity anomaly time) = (eccentricRadius firstAction eccentricity anomaly ^ 2 + rotatingEllipsePosition firstAction eccentricity anomaly time 0) / eccentricRadius firstAction eccentricity anomaly ^ 3 - 1 / √(eccentricRadius firstAction eccentricity anomaly ^ 2 - 2 * rotatingEllipsePosition firstAction eccentricity anomaly time 0 + 1)

Equivalent source form of the restricted perturbation, combining its first two terms over the cube of the Kepler radius.