An analytic periapsis section of the planar Delaunay action map

For prograde elliptic actions 0 < G < L, eccentricity is sqrt (1 - (G / L)²). Setting eccentric anomaly and periapsis angle to zero gives an explicit Cartesian phase point depending analytically on (L,G). This section is a right inverse of the physical action map and supplies the action-space representative of the leading candidate integral.

noncomputable def LeanPool.PoincareThreeBody.eccentricityFromActions (action : ActionSpace) : ℝ

Eccentricity reconstructed from prograde planar actions (L,G).

Equations

• LeanPool.PoincareThreeBody.eccentricityFromActions action = √(1 - (action 1 / action 0) ^ 2)

def LeanPool.PoincareThreeBody.ProgradeEllipticActions : Set ActionSpace

The open prograde elliptic action region.

Equations

• LeanPool.PoincareThreeBody.ProgradeEllipticActions = {action : LeanPool.PoincareThreeBody.ActionSpace | 0 < action 1 ∧ action 1 < action 0}

theorem LeanPool.PoincareThreeBody.isOpen_progradeEllipticActions : IsOpen ProgradeEllipticActions

theorem LeanPool.PoincareThreeBody.eccentricityFromActions_nonneg (action : ActionSpace) : 0 ≤ eccentricityFromActions action

theorem LeanPool.PoincareThreeBody.ratio_actions_pos {action : ActionSpace} (haction : action ∈ ProgradeEllipticActions) : 0 < action 1 / action 0

theorem LeanPool.PoincareThreeBody.ratio_actions_lt_one {action : ActionSpace} (haction : action ∈ ProgradeEllipticActions) : action 1 / action 0 < 1

theorem LeanPool.PoincareThreeBody.eccentricityFromActions_pos {action : ActionSpace} (haction : action ∈ ProgradeEllipticActions) : 0 < eccentricityFromActions action

theorem LeanPool.PoincareThreeBody.eccentricityFromActions_lt_one {action : ActionSpace} (haction : action ∈ ProgradeEllipticActions) : eccentricityFromActions action < 1

theorem LeanPool.PoincareThreeBody.eccentricityFromActions_sq {action : ActionSpace} (haction : action ∈ ProgradeEllipticActions) : eccentricityFromActions action ^ 2 = 1 - (action 1 / action 0) ^ 2

theorem LeanPool.PoincareThreeBody.analyticAt_eccentricityFromActions {action : ActionSpace} (haction : action ∈ ProgradeEllipticActions) : AnalyticAt ℝ eccentricityFromActions action

Reconstructed eccentricity varies analytically throughout the prograde elliptic action region.

theorem LeanPool.PoincareThreeBody.eccentricityFromActions_angularActionFromEccentricity {firstAction eccentricity : ℝ} (hfirstAction : 0 < firstAction) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : eccentricityFromActions ![firstAction, angularActionFromEccentricity firstAction eccentricity] = eccentricity

Recovering eccentricity from the actions of an ellipse returns its original eccentricity.

theorem LeanPool.PoincareThreeBody.actions_from_eccentricityFromActions {action : ActionSpace} (haction : action ∈ ProgradeEllipticActions) : ![action 0, angularActionFromEccentricity (action 0) (eccentricityFromActions action)] = action

Reconstructing eccentricity from a prograde action pair and then rebuilding the angular action returns the original pair.

theorem LeanPool.PoincareThreeBody.eccentricAnomaly_zero {eccentricity : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : eccentricAnomaly eccentricity 0 = 0

Zero mean anomaly has zero eccentric anomaly throughout the elliptic range.

noncomputable def LeanPool.PoincareThreeBody.delaunayActionSection (action : ActionSpace) : PhaseSpace

Explicit phase point at periapsis, used as a section of the action map.

Equations

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

theorem LeanPool.PoincareThreeBody.delaunayActionSection_eq_liftedDelaunayPhasePoint {action : ActionSpace} (haction : action ∈ ProgradeEllipticActions) : delaunayActionSection action = liftedDelaunayPhasePoint (action 0) (eccentricityFromActions action) 0 0

On the prograde elliptic region, the explicit section is the lifted Delaunay point with both angles zero.

theorem LeanPool.PoincareThreeBody.cartesianDelaunayActions_delaunayActionSection {action : ActionSpace} (haction : action ∈ ProgradeEllipticActions) : cartesianDelaunayActions (delaunayActionSection action) = action

The periapsis section realizes the prescribed action pair.

theorem LeanPool.PoincareThreeBody.analyticAt_delaunayActionSection {action : ActionSpace} (haction : action ∈ ProgradeEllipticActions) : AnalyticAt ℝ delaunayActionSection action

The explicit periapsis section is analytic on the prograde elliptic action region.

noncomputable def LeanPool.PoincareThreeBody.delaunayActionSectionAtAnomaly (anomaly periapsisAngle : ℝ) (action : ActionSpace) : PhaseSpace

An action section through a prescribed eccentric anomaly and periapsis angle. Fixing the eccentric anomaly, rather than the mean anomaly, makes the dependence on the two actions explicitly analytic.

Equations

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

theorem LeanPool.PoincareThreeBody.delaunayActionSectionAtAnomaly_eq_liftedDelaunayPhasePoint {action : ActionSpace} (haction : action ∈ ProgradeEllipticActions) (anomaly periapsisAngle : ℝ) : delaunayActionSectionAtAnomaly anomaly periapsisAngle action = liftedDelaunayPhasePoint (action 0) (eccentricityFromActions action) (eccentricMeanAnomaly (eccentricityFromActions action) anomaly) periapsisAngle

The fixed-eccentric-anomaly section is a lifted Delaunay point whose mean anomaly is obtained from Kepler's equation.

theorem LeanPool.PoincareThreeBody.cartesianDelaunayActions_delaunayActionSectionAtAnomaly {action : ActionSpace} (haction : action ∈ ProgradeEllipticActions) (anomaly periapsisAngle : ℝ) : cartesianDelaunayActions (delaunayActionSectionAtAnomaly anomaly periapsisAngle action) = action

Every fixed-eccentric-anomaly section is a right inverse of the Cartesian action map.

theorem LeanPool.PoincareThreeBody.analyticAt_delaunayActionSectionAtAnomaly {action : ActionSpace} (haction : action ∈ ProgradeEllipticActions) (anomaly periapsisAngle : ℝ) : AnalyticAt ℝ (delaunayActionSectionAtAnomaly anomaly periapsisAngle) action

With anomaly and periapsis held fixed, the moving action section is analytic throughout the prograde elliptic action region.

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

Choosing the anomaly of a lifted point makes the moving action section pass through that point.

theorem LeanPool.PoincareThreeBody.fderiv_cartesianDelaunayActions_comp_sectionAtAnomaly {action : ActionSpace} (haction : action ∈ ProgradeEllipticActions) (anomaly periapsisAngle : ℝ) : fderiv ℝ cartesianDelaunayActions (delaunayActionSectionAtAnomaly anomaly periapsisAngle action) ∘SL fderiv ℝ (delaunayActionSectionAtAnomaly anomaly periapsisAngle) action = ContinuousLinearMap.id ℝ ActionSpace

The derivative of every moving action section is a linear right inverse of the derivative of the physical action map.

noncomputable def LeanPool.PoincareThreeBody.leadingActionCoefficient (F : ℝ → PhaseSpace → ℝ) (action : ActionSpace) : ℝ

The leading, mass-zero candidate integral represented on the explicit action section.

Equations

• LeanPool.PoincareThreeBody.leadingActionCoefficient F action = F 0 (LeanPool.PoincareThreeBody.delaunayActionSection action)

theorem LeanPool.PoincareThreeBody.IsJointlyAnalytic.analyticAt_leadingActionCoefficient {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) {action : ActionSpace} (haction : action ∈ ProgradeEllipticActions) (hapoapsis : action 0 ^ 2 * (1 + eccentricityFromActions action) < 1) : AnalyticAt ℝ (leadingActionCoefficient F) action

On an interior prograde elliptic action, the leading action coefficient is analytic.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.leadingActionCoefficient_eq_liftedDelaunayPhasePoint {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) {firstAction eccentricity : ℝ} (hfirstAction : 0 < firstAction) (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : firstAction ^ 2 * (1 + eccentricity) < 1) (angles : ℝ × ℝ) : leadingActionCoefficient F ![firstAction, angularActionFromEccentricity firstAction eccentricity] = F 0 (liftedDelaunayPhasePoint firstAction eccentricity angles.1 angles.2)

The action-section representative equals the leading candidate on every lifted point with the same prograde elliptic actions.

noncomputable def LeanPool.PoincareThreeBody.leadingActionDifferential (F : ℝ → PhaseSpace → ℝ) (action : ActionSpace) : ActionSpace

The coordinate vector representing the differential of the leading action coefficient.

Equations

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

theorem LeanPool.PoincareThreeBody.fderiv_leadingActionCoefficient_eq_actionCovector (F : ℝ → PhaseSpace → ℝ) (action : ActionSpace) : fderiv ℝ (leadingActionCoefficient F) action = actionCovector (leadingActionDifferential F action)

The Fréchet differential of the leading action coefficient is its represented Euclidean action covector.

theorem LeanPool.PoincareThreeBody.IsJointlyAnalytic.continuousAt_leadingActionDifferential {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) {action : ActionSpace} (haction : action ∈ ProgradeEllipticActions) (hapoapsis : action 0 ^ 2 * (1 + eccentricityFromActions action) < 1) : ContinuousAt (leadingActionDifferential F) action

The represented leading differential varies continuously at every interior prograde action.

theorem LeanPool.PoincareThreeBody.IsJointlyAnalytic.analyticAt_leadingActionDifferential {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) {action : ActionSpace} (haction : action ∈ ProgradeEllipticActions) (hapoapsis : action 0 ^ 2 * (1 + eccentricityFromActions action) < 1) : AnalyticAt ℝ (leadingActionDifferential F) action

The represented leading differential is itself analytic on the interior action region.

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

The action pair (L, L sqrt(1-e²)) along a fixed-eccentricity family.

Equations

• LeanPool.PoincareThreeBody.fixedEccentricityAction eccentricity firstAction = ![firstAction, LeanPool.PoincareThreeBody.angularActionFromEccentricity firstAction eccentricity]

noncomputable def LeanPool.PoincareThreeBody.leadingActionDifferentialAtEccentricity (F : ℝ → PhaseSpace → ℝ) (eccentricity : ℝ) (firstAction : InteriorPositiveAction eccentricity) : ActionSpace

The leading action differential restricted to a fixed-eccentricity interior family.

Equations

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

theorem LeanPool.PoincareThreeBody.IsJointlyAnalytic.continuous_leadingActionDifferentialAtEccentricity {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) {eccentricity : ℝ} (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) : Continuous (leadingActionDifferentialAtEccentricity F eccentricity)

Along every fixed noncircular eccentricity family inside the unit primary orbit, the leading action differential is continuous in L.