Algebraic foundations of the planar Delaunay generating function

For negative Kepler energy -1 / (2 * I₁²) and angular momentum I₂, the radial Hamilton–Jacobi equation has two turning radii. This file verifies their sum, product, and the factorization of the squared radial momentum. These identities underlie the square root integrated in the Delaunay generating function.

noncomputable def LeanPool.PoincareThreeBody.periapsisRadius (firstAction secondAction : ℝ) : ℝ

The periapsis radius associated with Delaunay actions.

Equations

• LeanPool.PoincareThreeBody.periapsisRadius firstAction secondAction = firstAction * (firstAction - √(firstAction ^ 2 - secondAction ^ 2))

noncomputable def LeanPool.PoincareThreeBody.apoapsisRadius (firstAction secondAction : ℝ) : ℝ

The apoapsis radius associated with Delaunay actions.

Equations

• LeanPool.PoincareThreeBody.apoapsisRadius firstAction secondAction = firstAction * (firstAction + √(firstAction ^ 2 - secondAction ^ 2))

noncomputable def LeanPool.PoincareThreeBody.angularActionFromEccentricity (firstAction eccentricity : ℝ) : ℝ

Angular action of an elliptic Kepler orbit with first action I₁ and eccentricity e.

Equations

• LeanPool.PoincareThreeBody.angularActionFromEccentricity firstAction eccentricity = firstAction * √(1 - eccentricity ^ 2)

theorem LeanPool.PoincareThreeBody.periapsis_add_apoapsis (firstAction secondAction : ℝ) : periapsisRadius firstAction secondAction + apoapsisRadius firstAction secondAction = 2 * firstAction ^ 2

theorem LeanPool.PoincareThreeBody.periapsis_mul_apoapsis {firstAction secondAction : ℝ} (hactions : secondAction ^ 2 ≤ firstAction ^ 2) : periapsisRadius firstAction secondAction * apoapsisRadius firstAction secondAction = firstAction ^ 2 * secondAction ^ 2

theorem LeanPool.PoincareThreeBody.angularActionFromEccentricity_pos {firstAction eccentricity : ℝ} (hfirstAction : 0 < firstAction) (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) : 0 < angularActionFromEccentricity firstAction eccentricity

theorem LeanPool.PoincareThreeBody.angularActionFromEccentricity_lt_firstAction {firstAction eccentricity : ℝ} (hfirstAction : 0 < firstAction) (heccentricity : 0 < eccentricity) : angularActionFromEccentricity firstAction eccentricity < firstAction

theorem LeanPool.PoincareThreeBody.delaunayDiscriminant_angularActionFromEccentricity {firstAction eccentricity : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity ≤ 1) : firstAction ^ 2 - angularActionFromEccentricity firstAction eccentricity ^ 2 = (firstAction * eccentricity) ^ 2

theorem LeanPool.PoincareThreeBody.sqrt_delaunayDiscriminant_angularActionFromEccentricity {firstAction eccentricity : ℝ} (hfirstAction : 0 ≤ firstAction) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity ≤ 1) : √(firstAction ^ 2 - angularActionFromEccentricity firstAction eccentricity ^ 2) = firstAction * eccentricity

theorem LeanPool.PoincareThreeBody.periapsisRadius_angularActionFromEccentricity {firstAction eccentricity : ℝ} (hfirstAction : 0 ≤ firstAction) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity ≤ 1) : periapsisRadius firstAction (angularActionFromEccentricity firstAction eccentricity) = firstAction ^ 2 * (1 - eccentricity)

theorem LeanPool.PoincareThreeBody.apoapsisRadius_angularActionFromEccentricity {firstAction eccentricity : ℝ} (hfirstAction : 0 ≤ firstAction) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity ≤ 1) : apoapsisRadius firstAction (angularActionFromEccentricity firstAction eccentricity) = firstAction ^ 2 * (1 + eccentricity)

theorem LeanPool.PoincareThreeBody.delaunayRadialMomentumSq_factorization {radius firstAction secondAction : ℝ} (hradius : radius ≠ 0) (hfirstAction : firstAction ≠ 0) (hactions : secondAction ^ 2 ≤ firstAction ^ 2) : delaunayRadialMomentumSq radius firstAction secondAction = (apoapsisRadius firstAction secondAction - radius) * (radius - periapsisRadius firstAction secondAction) / (firstAction ^ 2 * radius ^ 2)

The radial momentum radicand factors through the two Kepler turning radii.

theorem LeanPool.PoincareThreeBody.periapsis_le_apoapsis {firstAction secondAction : ℝ} (hfirstAction : 0 ≤ firstAction) : periapsisRadius firstAction secondAction ≤ apoapsisRadius firstAction secondAction

theorem LeanPool.PoincareThreeBody.delaunayAction_discriminant_pos {firstAction secondAction : ℝ} (hsecondAction : 0 < secondAction) (hactions : secondAction < firstAction) : 0 < firstAction ^ 2 - secondAction ^ 2

theorem LeanPool.PoincareThreeBody.sqrt_delaunayAction_discriminant_lt {firstAction secondAction : ℝ} (hsecondAction : 0 < secondAction) (hactions : secondAction < firstAction) : √(firstAction ^ 2 - secondAction ^ 2) < firstAction

theorem LeanPool.PoincareThreeBody.periapsisRadius_pos {firstAction secondAction : ℝ} (hsecondAction : 0 < secondAction) (hactions : secondAction < firstAction) : 0 < periapsisRadius firstAction secondAction

theorem LeanPool.PoincareThreeBody.apoapsisRadius_pos {firstAction secondAction : ℝ} (hsecondAction : 0 < secondAction) (hactions : secondAction < firstAction) : 0 < apoapsisRadius firstAction secondAction

theorem LeanPool.PoincareThreeBody.periapsisRadius_lt_apoapsisRadius {firstAction secondAction : ℝ} (hsecondAction : 0 < secondAction) (hactions : secondAction < firstAction) : periapsisRadius firstAction secondAction < apoapsisRadius firstAction secondAction

theorem LeanPool.PoincareThreeBody.delaunayRadialMomentumSq_nonneg_of_mem_turningInterval {radius firstAction secondAction : ℝ} (hsecondAction : 0 < secondAction) (hactions : secondAction < firstAction) (hlower : periapsisRadius firstAction secondAction ≤ radius) (hupper : radius ≤ apoapsisRadius firstAction secondAction) : 0 ≤ delaunayRadialMomentumSq radius firstAction secondAction

Between periapsis and apoapsis, the radial momentum square prescribed by the Delaunay actions is nonnegative.