Polar canonical coordinates for the rotating Kepler limit

This file defines the standard canonical polar-coordinate map and verifies directly that it sends the zero-mass Cartesian Hamiltonian to the rotating Kepler Hamiltonian. This is the first coordinate change on the route to Delaunay action-angle variables.

@[reducible, inline]

abbrev LeanPool.PoincareThreeBody.PolarState : Type

Polar canonical state ordered as (r, φ, pᵣ, pφ).

Equations

• LeanPool.PoincareThreeBody.PolarState = (Fin 4 → ℝ)

noncomputable def LeanPool.PoincareThreeBody.polarToCartesian (state : PolarState) : PhaseSpace

The canonical polar-to-Cartesian coordinate map.

Equations

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

noncomputable def LeanPool.PoincareThreeBody.polarKeplerHamiltonian (state : PolarState) : ℝ

The rotating Kepler Hamiltonian in canonical polar coordinates.

Equations

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

noncomputable def LeanPool.PoincareThreeBody.polarKeplerEnergy (state : PolarState) : ℝ

The inertial Kepler energy in canonical polar coordinates.

Equations

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

noncomputable def LeanPool.PoincareThreeBody.delaunayRadialMomentumSq (radius firstAction secondAction : ℝ) : ℝ

The squared radial momentum prescribed by a Kepler energy -1 / (2 * firstAction²) and angular momentum secondAction.

Equations

• LeanPool.PoincareThreeBody.delaunayRadialMomentumSq radius firstAction secondAction = 2 / radius - 1 / firstAction ^ 2 - secondAction ^ 2 / radius ^ 2

theorem LeanPool.PoincareThreeBody.polarKeplerHamiltonian_eq_energy_sub_angularMomentum (state : PolarState) : polarKeplerHamiltonian state = polarKeplerEnergy state - state 3

theorem LeanPool.PoincareThreeBody.polarKeplerEnergy_eq_delaunay_iff {radius radialMomentum firstAction secondAction : ℝ} (hradius : radius ≠ 0) (hfirstAction : firstAction ≠ 0) : (radialMomentum ^ 2 + secondAction ^ 2 / radius ^ 2) / 2 - 1 / radius = -1 / (2 * firstAction ^ 2) ↔ radialMomentum ^ 2 = delaunayRadialMomentumSq radius firstAction secondAction

On a negative Kepler energy shell, the radial momentum satisfies the radicand appearing in the Delaunay generating function.

theorem LeanPool.PoincareThreeBody.delaunayHamiltonian_eq_keplerEnergy_sub_angularMomentum (firstAction secondAction : ℝ) : delaunayHamiltonian ![firstAction, secondAction] = -1 / (2 * firstAction ^ 2) - secondAction

The Delaunay Hamiltonian is the inertial Kepler energy minus angular momentum.

theorem LeanPool.PoincareThreeBody.polar_position_sq (state : PolarState) : polarToCartesian state 0 ^ 2 + polarToCartesian state 1 ^ 2 = state 0 ^ 2

theorem LeanPool.PoincareThreeBody.polar_momentum_sq {state : PolarState} (hr : state 0 ≠ 0) : polarToCartesian state 2 ^ 2 + polarToCartesian state 3 ^ 2 = state 2 ^ 2 + state 3 ^ 2 / state 0 ^ 2

theorem LeanPool.PoincareThreeBody.polar_angular_term {state : PolarState} (hr : state 0 ≠ 0) : polarToCartesian state 2 * polarToCartesian state 1 - polarToCartesian state 3 * polarToCartesian state 0 = -state 3

theorem LeanPool.PoincareThreeBody.polar_radial_momentum_identity {state : PolarState} (hr : state 0 ≠ 0) : polarToCartesian state 2 * Real.cos (state 1) + polarToCartesian state 3 * Real.sin (state 1) = state 2

The Cartesian momentum paired with the radial coordinate differential is pᵣ.

theorem LeanPool.PoincareThreeBody.polar_angular_momentum_identity {state : PolarState} (hr : state 0 ≠ 0) : polarToCartesian state 2 * (-state 0 * Real.sin (state 1)) + polarToCartesian state 3 * (state 0 * Real.cos (state 1)) = state 3

The Cartesian momentum paired with the angular coordinate differential is pφ. Together with polar_radial_momentum_identity, this verifies the canonical one-form under the polar formulas.

theorem LeanPool.PoincareThreeBody.hamiltonian_zero_comp_polarToCartesian {state : PolarState} (hr : 0 < state 0) : hamiltonian 0 (polarToCartesian state) = polarKeplerHamiltonian state

The Cartesian zero-mass Hamiltonian becomes the rotating Kepler Hamiltonian under the canonical polar-coordinate formulas.