Analytic continuation from the collision band

For each fixed eccentricity, the leading wedge is analytic in the first action. Its vanishing on the nonempty collision band therefore extends to the entire connected interior first-action interval.

def LeanPool.PoincareThreeBody.interiorFirstActionSet (eccentricity : ℝ) : Set ℝ

The raw open interval of positive first actions whose apoapsis remains inside the unit orbit.

Equations

• LeanPool.PoincareThreeBody.interiorFirstActionSet eccentricity = {firstAction : ℝ | 0 < firstAction ∧ firstAction ^ 2 * (1 + eccentricity) < 1}

theorem LeanPool.PoincareThreeBody.isOpen_interiorFirstActionSet (eccentricity : ℝ) : IsOpen (interiorFirstActionSet eccentricity)

theorem LeanPool.PoincareThreeBody.isConnected_interiorFirstActionSet {eccentricity : ℝ} (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) : IsConnected (interiorFirstActionSet eccentricity)

noncomputable def LeanPool.PoincareThreeBody.fixedEccentricityWedge (F : ℝ → PhaseSpace → ℝ) (eccentricity firstAction : ℝ) : ℝ

The leading-order wedge obstruction along the action line of fixed eccentricity.

Equations

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

theorem LeanPool.PoincareThreeBody.analyticAt_fixedEccentricityAction (eccentricity firstAction : ℝ) : AnalyticAt ℝ (fixedEccentricityAction eccentricity) firstAction

theorem LeanPool.PoincareThreeBody.analyticAt_delaunayFrequency {firstAction : ℝ} (hfirstAction : firstAction ≠ 0) : AnalyticAt ℝ delaunayFrequency firstAction

theorem LeanPool.PoincareThreeBody.IsJointlyAnalytic.analyticAt_fixedEccentricityWedge {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) {eccentricity firstAction : ℝ} (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) (hfirstAction : firstAction ∈ interiorFirstActionSet eccentricity) : AnalyticAt ℝ (fixedEccentricityWedge F eccentricity) firstAction

theorem LeanPool.PoincareThreeBody.collisionBandInteriorPositiveAction_nonempty {eccentricity : ℝ} (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) : Nonempty (CollisionBandInteriorPositiveAction eccentricity)

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.wedge_leadingActionDifferential_eq_zero_of_collisionBand {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) {eccentricity firstAction : ℝ} (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) (hfirstAction : firstAction ∈ interiorFirstActionSet eccentricity) : fixedEccentricityWedge F eccentricity firstAction = 0

The collision-band obstruction analytically continues to every interior first action.

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

Global action-space form of the collision-band obstruction.