Physical realization of the planar Delaunay actions

This file identifies the two actions carried by the explicit lifted ellipse. The second action is Cartesian angular momentum, while the first action is determined by the negative inertial Kepler energy. Consequently the physical mass-zero Hamiltonian pulls back to the displayed Delaunay Hamiltonian.

noncomputable def LeanPool.PoincareThreeBody.actionCovector (vector : ActionSpace) : ActionSpace →L[ℝ] ℝ

A frequency vector regarded as the corresponding Euclidean action covector.

Equations

• LeanPool.PoincareThreeBody.actionCovector vector = (ContinuousLinearMap.proj 0).smulRight (vector 0) + (ContinuousLinearMap.proj 1).smulRight (vector 1)

theorem LeanPool.PoincareThreeBody.actionCovector_apply (vector direction : ActionSpace) : (actionCovector vector) direction = dot vector direction

def LeanPool.PoincareThreeBody.actionCoordinateVector (coordinate : Fin 2) : ActionSpace

Coordinate tangent vectors in the two-dimensional action space.

Equations

• LeanPool.PoincareThreeBody.actionCoordinateVector coordinate index = if index = coordinate then 1 else 0

noncomputable def LeanPool.PoincareThreeBody.cartesianKeplerEnergy (state : PhaseSpace) : ℝ

Inertial Kepler energy written in rotating Cartesian canonical variables.

Equations

• LeanPool.PoincareThreeBody.cartesianKeplerEnergy state = (state 2 ^ 2 + state 3 ^ 2) / 2 - 1 / √(state 0 ^ 2 + state 1 ^ 2)

noncomputable def LeanPool.PoincareThreeBody.cartesianFirstAction (state : PhaseSpace) : ℝ

The first Delaunay action reconstructed from negative inertial Kepler energy.

Equations

• LeanPool.PoincareThreeBody.cartesianFirstAction state = 1 / √(-2 * LeanPool.PoincareThreeBody.cartesianKeplerEnergy state)

def LeanPool.PoincareThreeBody.cartesianAngularAction (state : PhaseSpace) : ℝ

The planar angular action G = x pᵧ - y pₓ.

Equations

• LeanPool.PoincareThreeBody.cartesianAngularAction state = state 0 * state 3 - state 1 * state 2

noncomputable def LeanPool.PoincareThreeBody.cartesianDelaunayActions (state : PhaseSpace) : ActionSpace

Both Cartesian Delaunay actions, ordered as (L, G).

Equations

• LeanPool.PoincareThreeBody.cartesianDelaunayActions state = ![LeanPool.PoincareThreeBody.cartesianFirstAction state, LeanPool.PoincareThreeBody.cartesianAngularAction state]

theorem LeanPool.PoincareThreeBody.analyticAt_cartesianKeplerEnergy {state : PhaseSpace} (hposition : state 0 ^ 2 + state 1 ^ 2 ≠ 0) : AnalyticAt ℝ cartesianKeplerEnergy state

The inertial Kepler energy is analytic away from the central collision.

theorem LeanPool.PoincareThreeBody.analyticAt_cartesianAngularAction (state : PhaseSpace) : AnalyticAt ℝ cartesianAngularAction state

Angular action is an analytic polynomial in Cartesian phase variables.

theorem LeanPool.PoincareThreeBody.analyticAt_cartesianFirstAction {state : PhaseSpace} (hposition : state 0 ^ 2 + state 1 ^ 2 ≠ 0) (henergy : cartesianKeplerEnergy state < 0) : AnalyticAt ℝ cartesianFirstAction state

The reconstructed first action is analytic wherever the central distance is nonzero and the inertial Kepler energy is negative.

theorem LeanPool.PoincareThreeBody.analyticAt_cartesianDelaunayActions {state : PhaseSpace} (hposition : state 0 ^ 2 + state 1 ^ 2 ≠ 0) (henergy : cartesianKeplerEnergy state < 0) : AnalyticAt ℝ cartesianDelaunayActions state

The Cartesian Delaunay action map is analytic on the negative-energy, noncollision region.

theorem LeanPool.PoincareThreeBody.positionInRotatingFrame_cross (angle : ℝ) (first second : ActionSpace) : positionInRotatingFrame angle first 0 * positionInRotatingFrame angle second 1 - positionInRotatingFrame angle first 1 * positionInRotatingFrame angle second 0 = first 0 * second 1 - first 1 * second 0

A common planar rotation preserves the determinant of two vectors.

theorem LeanPool.PoincareThreeBody.positionInRotatingFrame_momentum_sq (angle : ℝ) (momentum : ActionSpace) : positionInRotatingFrame angle momentum 0 ^ 2 + positionInRotatingFrame angle momentum 1 ^ 2 = momentum 0 ^ 2 + momentum 1 ^ 2

A common planar rotation preserves the squared norm.

theorem LeanPool.PoincareThreeBody.inertialEllipsePosition_velocity_cross {firstAction eccentricity anomaly : ℝ} (hfirstAction : firstAction ≠ 0) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : inertialEllipsePosition firstAction eccentricity anomaly 0 * inertialEllipseVelocity firstAction eccentricity (1 / firstAction ^ 3) anomaly 1 - inertialEllipsePosition firstAction eccentricity anomaly 1 * inertialEllipseVelocity firstAction eccentricity (1 / firstAction ^ 3) anomaly 0 = angularActionFromEccentricity firstAction eccentricity

The eccentric-anomaly position and velocity carry angular action L * sqrt (1 - e²).

theorem LeanPool.PoincareThreeBody.inertialEllipseVelocity_energy_identity {firstAction eccentricity anomaly : ℝ} (hfirstAction : firstAction ≠ 0) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : (inertialEllipseVelocity firstAction eccentricity (1 / firstAction ^ 3) anomaly 0 ^ 2 + inertialEllipseVelocity firstAction eccentricity (1 / firstAction ^ 3) anomaly 1 ^ 2) / 2 - 1 / eccentricRadius firstAction eccentricity anomaly = -1 / (2 * firstAction ^ 2)

The velocity norm on an elliptic Kepler orbit has the vis-viva value needed for its energy shell.

theorem LeanPool.PoincareThreeBody.cartesianAngularAction_liftedDelaunayPhasePoint {firstAction eccentricity meanAnomaly periapsisAngle : ℝ} (hfirstAction : firstAction ≠ 0) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : cartesianAngularAction (liftedDelaunayPhasePoint firstAction eccentricity meanAnomaly periapsisAngle) = angularActionFromEccentricity firstAction eccentricity

The explicit lifted Delaunay chart realizes its prescribed second action.

theorem LeanPool.PoincareThreeBody.cartesianKeplerEnergy_liftedDelaunayPhasePoint {firstAction eccentricity meanAnomaly periapsisAngle : ℝ} (hfirstAction : firstAction ≠ 0) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : cartesianKeplerEnergy (liftedDelaunayPhasePoint firstAction eccentricity meanAnomaly periapsisAngle) = -1 / (2 * firstAction ^ 2)

The first action of the lifted chart is its negative Kepler energy action.

theorem LeanPool.PoincareThreeBody.cartesianFirstAction_liftedDelaunayPhasePoint {firstAction eccentricity meanAnomaly periapsisAngle : ℝ} (hfirstAction : 0 < firstAction) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : cartesianFirstAction (liftedDelaunayPhasePoint firstAction eccentricity meanAnomaly periapsisAngle) = firstAction

Reconstructing the first action from the energy of a positive-action lifted ellipse returns the original L.

theorem LeanPool.PoincareThreeBody.cartesianDelaunayActions_liftedDelaunayPhasePoint {firstAction eccentricity meanAnomaly periapsisAngle : ℝ} (hfirstAction : 0 < firstAction) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : cartesianDelaunayActions (liftedDelaunayPhasePoint firstAction eccentricity meanAnomaly periapsisAngle) = ![firstAction, angularActionFromEccentricity firstAction eccentricity]

The complete Cartesian action map is a left inverse of the lifted Delaunay chart.

theorem LeanPool.PoincareThreeBody.analyticAt_cartesianDelaunayActions_liftedDelaunayPhasePoint {firstAction eccentricity meanAnomaly periapsisAngle : ℝ} (hfirstAction : 0 < firstAction) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : AnalyticAt ℝ cartesianDelaunayActions (liftedDelaunayPhasePoint firstAction eccentricity meanAnomaly periapsisAngle)

The Cartesian action map is analytic at every nondegenerate lifted elliptic point.

theorem LeanPool.PoincareThreeBody.analyticAt_delaunayHamiltonian {action : ActionSpace} (hfirstAction : action 0 ≠ 0) : AnalyticAt ℝ delaunayHamiltonian action

The Delaunay Hamiltonian is analytic whenever its first action is nonzero.

theorem LeanPool.PoincareThreeBody.fderiv_delaunayHamiltonian_eq_actionCovector {action : ActionSpace} (hfirstAction : action 0 ≠ 0) : fderiv ℝ delaunayHamiltonian action = actionCovector (delaunayFrequency (action 0))

The Fréchet differential of the Delaunay Hamiltonian is the covector represented by its frequency vector.

theorem LeanPool.PoincareThreeBody.hamiltonian_zero_eq_cartesianKeplerEnergy_sub_angularAction (state : PhaseSpace) : hamiltonian 0 state = cartesianKeplerEnergy state - cartesianAngularAction state

At every noncentral phase point, the zero-mass rotating Hamiltonian is inertial Kepler energy minus angular action.

theorem LeanPool.PoincareThreeBody.delaunayHamiltonian_cartesianDelaunayActions {state : PhaseSpace} (henergy : cartesianKeplerEnergy state < 0) : delaunayHamiltonian (cartesianDelaunayActions state) = hamiltonian 0 state

On the negative-energy region, the Cartesian action reconstruction puts the physical Hamiltonian into Delaunay normal form.

theorem LeanPool.PoincareThreeBody.hamiltonian_zero_eventuallyEq_delaunayHamiltonian_comp_actions {state : PhaseSpace} (hposition : state 0 ^ 2 + state 1 ^ 2 ≠ 0) (henergy : cartesianKeplerEnergy state < 0) : hamiltonian 0 =ᶠ[nhds state] fun (candidate : PhaseSpace) => delaunayHamiltonian (cartesianDelaunayActions candidate)

The physical and action-coordinate zero-mass Hamiltonians agree on a whole neighborhood of every negative-energy, noncentral phase point.

theorem LeanPool.PoincareThreeBody.fderiv_hamiltonian_zero_eq_delaunay_comp_actions {state : PhaseSpace} (hposition : state 0 ^ 2 + state 1 ^ 2 ≠ 0) (henergy : cartesianKeplerEnergy state < 0) : fderiv ℝ (hamiltonian 0) state = fderiv ℝ delaunayHamiltonian (cartesianDelaunayActions state) ∘SL fderiv ℝ cartesianDelaunayActions state

Differential form of the action-coordinate normal form for the zero-mass Hamiltonian.

theorem LeanPool.PoincareThreeBody.fderiv_hamiltonian_zero_eq_frequencyCovector_comp_actions {state : PhaseSpace} (hposition : state 0 ^ 2 + state 1 ^ 2 ≠ 0) (henergy : cartesianKeplerEnergy state < 0) : fderiv ℝ (hamiltonian 0) state = actionCovector (delaunayFrequency (cartesianDelaunayActions state 0)) ∘SL fderiv ℝ cartesianDelaunayActions state

The physical Hamiltonian differential is the pullback of the Kepler frequency covector by the Cartesian action map.

theorem LeanPool.PoincareThreeBody.hamiltonian_zero_liftedDelaunayPhasePoint {firstAction eccentricity meanAnomaly periapsisAngle : ℝ} (hfirstAction : firstAction ≠ 0) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : hamiltonian 0 (liftedDelaunayPhasePoint firstAction eccentricity meanAnomaly periapsisAngle) = delaunayHamiltonian ![firstAction, angularActionFromEccentricity firstAction eccentricity]

The physical zero-mass Hamiltonian pulls back to the Delaunay Hamiltonian.