Documentation

LeanPool.PoincareThreeBody.DelaunayChart

The lifted planar Delaunay chart #

This file packages the position and canonical rotating-frame momentum as a function of the first action, eccentricity, mean anomaly, and rotating periapsis angle. The angles are initially lifted to real numbers; periodicity will allow the chart to descend to the angle torus.

source
noncomputable def LeanPool.PoincareThreeBody.liftedDelaunayEccentricAnomaly (eccentricity meanAnomaly : ℝ) :
ℝ

Eccentric anomaly in the lifted Delaunay chart.

Equations
Instances For
    source
    noncomputable def LeanPool.PoincareThreeBody.liftedDelaunayPosition (firstAction eccentricity meanAnomaly periapsisAngle : ℝ) :
    ActionSpace

    Position in rotating Cartesian coordinates in the lifted Delaunay chart.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def LeanPool.PoincareThreeBody.liftedDelaunayMomentum (firstAction eccentricity meanAnomaly periapsisAngle : ℝ) :
      ActionSpace

      Canonical rotating-frame momentum in the lifted Delaunay chart.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def LeanPool.PoincareThreeBody.liftedDelaunayPhasePoint (firstAction eccentricity meanAnomaly periapsisAngle : ℝ) :
        PhaseSpace

        Full phase-space point in lifted Delaunay variables.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem LeanPool.PoincareThreeBody.liftedDelaunayPhasePoint_resonant {p q : ℕ} (hp : 0 < p) (hq : 0 < q) (eccentricity orientation time : ℝ) :
          liftedDelaunayPhasePoint (resonantFirstAction p q) eccentricity (resonantMeanAnomaly p q time) (orientation - time) = orientedResonantKeplerPhasePoint p q eccentricity orientation time

          The chart agrees exactly with the previously constructed resonant Kepler orbit.

          source
          theorem LeanPool.PoincareThreeBody.liftedDelaunayPhasePoint_add_mean_period {firstAction eccentricity meanAnomaly periapsisAngle : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) :
          liftedDelaunayPhasePoint firstAction eccentricity (meanAnomaly + 2 * Real.pi) periapsisAngle = liftedDelaunayPhasePoint firstAction eccentricity meanAnomaly periapsisAngle

          The lifted chart is periodic in mean anomaly.

          source
          theorem LeanPool.PoincareThreeBody.positionInRotatingFrame_neg_add_two_pi (periapsisAngle : ℝ) (vector : ActionSpace) :
          positionInRotatingFrame (-(periapsisAngle + 2 * Real.pi)) vector = positionInRotatingFrame (-periapsisAngle) vector

          Rotating a vector through a negated angle is unchanged when a full turn is added to that angle.

          source
          theorem LeanPool.PoincareThreeBody.liftedDelaunayPhasePoint_add_periapsis_period (firstAction eccentricity meanAnomaly periapsisAngle : ℝ) :
          liftedDelaunayPhasePoint firstAction eccentricity meanAnomaly (periapsisAngle + 2 * Real.pi) = liftedDelaunayPhasePoint firstAction eccentricity meanAnomaly periapsisAngle

          The lifted chart is periodic in the rotating periapsis angle.

          source
          noncomputable def LeanPool.PoincareThreeBody.liftedDelaunayFlowLine (firstAction eccentricity meanAnomaly periapsisAngle time : ℝ) :
          PhaseSpace

          Along the unperturbed flow, the first Delaunay angle advances with frequency I₁⁻³ and the rotating periapsis angle decreases with unit speed.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem LeanPool.PoincareThreeBody.liftedDelaunayFlowLine_resonant {p q : ℕ} (hp : 0 < p) (hq : 0 < q) (eccentricity orientation time : ℝ) :
            liftedDelaunayFlowLine (resonantFirstAction p q) eccentricity 0 orientation time = orientedResonantKeplerPhasePoint p q eccentricity orientation time

            At a rational Kepler resonance and zero initial mean anomaly, the general lifted flow line is the previously verified resonant trajectory.

            source
            theorem LeanPool.PoincareThreeBody.analyticAt_liftedDelaunayPhasePoint_angles {firstAction eccentricity : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (angles : ℝ × ℝ) :
            AnalyticAt ℝ (fun (angle : ℝ × ℝ) => liftedDelaunayPhasePoint firstAction eccentricity angle.1 angle.2) angles

            For fixed elliptic actions, the lifted Delaunay chart is jointly analytic in its two angle variables.

            source
            theorem LeanPool.PoincareThreeBody.continuous_liftedDelaunayPhasePoint_angles {firstAction eccentricity : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) :
            Continuous fun (angle : ℝ × ℝ) => liftedDelaunayPhasePoint firstAction eccentricity angle.1 angle.2

            Continuity form of the angle chart.

            source
            theorem LeanPool.PoincareThreeBody.continuousAt_liftedDelaunayPhasePoint_firstAction {firstAction eccentricity meanAnomaly periapsisAngle : ℝ} (hfirstAction : firstAction ≠ 0) :
            ContinuousAt (fun (action : ℝ) => liftedDelaunayPhasePoint action eccentricity meanAnomaly periapsisAngle) firstAction

            Away from the degenerate value I₁ = 0, the lifted chart varies continuously with the first Delaunay action.