Documentation

LeanPool.PoincareThreeBody.DelaunayFlow

The unperturbed Hamiltonian flow in lifted Delaunay variables #

The lifted Delaunay chart evolves by advancing the mean anomaly at rate I₁⁻³ and decreasing the rotating periapsis angle at unit speed. Here we verify directly that this curve satisfies all four Hamilton equations for the mass-zero rotating Kepler Hamiltonian.

source
noncomputable def LeanPool.PoincareThreeBody.liftedDelaunayMeanAnomalyAlongFlow (firstAction meanAnomaly time : ℝ) :
ℝ

Mean anomaly along a general lifted Delaunay flow line.

Equations
Instances For
    source
    noncomputable def LeanPool.PoincareThreeBody.liftedDelaunayEccentricAnomalyAlongFlow (firstAction eccentricity meanAnomaly time : ℝ) :
    ℝ

    Eccentric anomaly along a general lifted Delaunay flow line.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem LeanPool.PoincareThreeBody.liftedDelaunayEccentricAnomaly_flow_argument (firstAction eccentricity meanAnomaly time : ℝ) :
      liftedDelaunayEccentricAnomaly eccentricity (meanAnomaly + time / firstAction ^ 3) = liftedDelaunayEccentricAnomalyAlongFlow firstAction eccentricity meanAnomaly time
      source
      theorem LeanPool.PoincareThreeBody.hasDerivAt_liftedDelaunayMeanAnomalyAlongFlow (firstAction meanAnomaly time : ℝ) :
      HasDerivAt (liftedDelaunayMeanAnomalyAlongFlow firstAction meanAnomaly) (1 / firstAction ^ 3) time
      source
      theorem LeanPool.PoincareThreeBody.hasDerivAt_liftedDelaunayEccentricAnomalyAlongFlow {firstAction eccentricity meanAnomaly time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) :
      HasDerivAt (liftedDelaunayEccentricAnomalyAlongFlow firstAction eccentricity meanAnomaly) (1 / firstAction ^ 3 / (1 - eccentricity * Real.cos (liftedDelaunayEccentricAnomalyAlongFlow firstAction eccentricity meanAnomaly time))) time
      source
      theorem LeanPool.PoincareThreeBody.hasDerivAt_liftedDelaunayFlowLine_position {firstAction eccentricity meanAnomaly periapsisAngle time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) :
      HasDerivAt (fun (t : ℝ) => liftedDelaunayFlowLine firstAction eccentricity meanAnomaly periapsisAngle t 0) (liftedDelaunayFlowLine firstAction eccentricity meanAnomaly periapsisAngle time 2 + liftedDelaunayFlowLine firstAction eccentricity meanAnomaly periapsisAngle time 1) time ∧ HasDerivAt (fun (t : ℝ) => liftedDelaunayFlowLine firstAction eccentricity meanAnomaly periapsisAngle t 1) (liftedDelaunayFlowLine firstAction eccentricity meanAnomaly periapsisAngle time 3 - liftedDelaunayFlowLine firstAction eccentricity meanAnomaly periapsisAngle time 0) time

      The position coordinates of a general Delaunay flow line satisfy the first two Hamilton equations.

      source
      theorem LeanPool.PoincareThreeBody.hasDerivAt_inertialEllipseVelocity_liftedDelaunayFlow {firstAction eccentricity meanAnomaly time : ℝ} (hfirstAction : firstAction ≠ 0) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (coordinate : Fin 2) :
      HasDerivAt (fun (t : ℝ) => inertialEllipseVelocity firstAction eccentricity (1 / firstAction ^ 3) (liftedDelaunayEccentricAnomalyAlongFlow firstAction eccentricity meanAnomaly t) coordinate) (-inertialEllipsePosition firstAction eccentricity (liftedDelaunayEccentricAnomalyAlongFlow firstAction eccentricity meanAnomaly time) coordinate / eccentricRadius firstAction eccentricity (liftedDelaunayEccentricAnomalyAlongFlow firstAction eccentricity meanAnomaly time) ^ 3) time

      In inertial coordinates, a general Delaunay ellipse satisfies the inverse-square acceleration law.

      source
      theorem LeanPool.PoincareThreeBody.hasDerivAt_liftedDelaunayFlowLine_momentum {firstAction eccentricity meanAnomaly periapsisAngle time : ℝ} (hfirstAction : firstAction ≠ 0) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) :
      have radius := eccentricRadius firstAction eccentricity (liftedDelaunayEccentricAnomalyAlongFlow firstAction eccentricity meanAnomaly time); HasDerivAt (fun (t : ℝ) => liftedDelaunayFlowLine firstAction eccentricity meanAnomaly periapsisAngle t 2) (liftedDelaunayFlowLine firstAction eccentricity meanAnomaly periapsisAngle time 3 - liftedDelaunayFlowLine firstAction eccentricity meanAnomaly periapsisAngle time 0 / radius ^ 3) time ∧ HasDerivAt (fun (t : ℝ) => liftedDelaunayFlowLine firstAction eccentricity meanAnomaly periapsisAngle t 3) (-liftedDelaunayFlowLine firstAction eccentricity meanAnomaly periapsisAngle time 2 - liftedDelaunayFlowLine firstAction eccentricity meanAnomaly periapsisAngle time 1 / radius ^ 3) time

      The momentum coordinates of a general Delaunay flow line satisfy the remaining two Hamilton equations.

      source
      theorem LeanPool.PoincareThreeBody.sqrt_positionSq_liftedDelaunayFlowLine {firstAction eccentricity meanAnomaly periapsisAngle time : ℝ} (hfirstAction : firstAction ≠ 0) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) :
      √(liftedDelaunayFlowLine firstAction eccentricity meanAnomaly periapsisAngle time 0 ^ 2 + liftedDelaunayFlowLine firstAction eccentricity meanAnomaly periapsisAngle time 1 ^ 2) = eccentricRadius firstAction eccentricity (liftedDelaunayEccentricAnomalyAlongFlow firstAction eccentricity meanAnomaly time)

      The position norm of a lifted Delaunay flow point is its eccentric radius.

      source
      theorem LeanPool.PoincareThreeBody.hasDerivAt_liftedDelaunayFlowLine {firstAction eccentricity meanAnomaly periapsisAngle time : ℝ} (hfirstAction : firstAction ≠ 0) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) :
      HasDerivAt (liftedDelaunayFlowLine firstAction eccentricity meanAnomaly periapsisAngle) (rotatingKeplerVectorField (liftedDelaunayFlowLine firstAction eccentricity meanAnomaly periapsisAngle time)) time

      A general lifted Delaunay flow line has derivative equal to the rotating Kepler vector field.

      source
      theorem LeanPool.PoincareThreeBody.DifferentiableAt.hasDerivAt_comp_liftedDelaunayFlowLine {F : PhaseSpace → ℝ} {firstAction eccentricity meanAnomaly periapsisAngle time : ℝ} (hfirstAction : firstAction ≠ 0) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hF : DifferentiableAt ℝ F (liftedDelaunayFlowLine firstAction eccentricity meanAnomaly periapsisAngle time)) :
      HasDerivAt (fun (t : ℝ) => F (liftedDelaunayFlowLine firstAction eccentricity meanAnomaly periapsisAngle t)) (poissonBracket F (hamiltonian 0) (liftedDelaunayFlowLine firstAction eccentricity meanAnomaly periapsisAngle time)) time

      Along a general lifted Delaunay flow line, the derivative of any differentiable observable is its Poisson bracket with the mass-zero Hamiltonian.

      source
      theorem LeanPool.PoincareThreeBody.liftedDelaunayFlowLine_collisionFree_mass_zero {firstAction eccentricity meanAnomaly periapsisAngle time : ℝ} (hfirstAction : firstAction ≠ 0) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : firstAction ^ 2 * (1 + eccentricity) < 1) :
      (0, liftedDelaunayFlowLine firstAction eccentricity meanAnomaly periapsisAngle time) ∈ collisionFree

      A lifted Delaunay ellipse lying strictly inside the unit primary's orbit is collision-free at mass zero for all time.

      source
      theorem LeanPool.PoincareThreeBody.liftedDelaunayPhasePoint_collisionFree_mass_zero {firstAction eccentricity meanAnomaly periapsisAngle : ℝ} (hfirstAction : firstAction ≠ 0) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : firstAction ^ 2 * (1 + eccentricity) < 1) :
      (0, liftedDelaunayPhasePoint firstAction eccentricity meanAnomaly periapsisAngle) ∈ collisionFree

      Collision-freeness of a static lifted Delaunay chart point.

      source
      @[reducible, inline]
      abbrev LeanPool.PoincareThreeBody.InteriorPositiveAction (eccentricity : ℝ) :
      Type

      Positive first actions whose Kepler ellipses stay strictly inside the unit primary orbit.

      Equations
      Instances For
        source
        def LeanPool.PoincareThreeBody.irrationalFrequencyInteriorPositiveActions (eccentricity : ℝ) :
        Set (InteriorPositiveAction eccentricity)

        The interior actions with irrational Kepler frequency.

        Equations
        Instances For
          source
          theorem LeanPool.PoincareThreeBody.irrationalFrequencyInteriorPositiveActions_dense (eccentricity : ℝ) :
          Dense (irrationalFrequencyInteriorPositiveActions eccentricity)

          Irrational Kepler tori are dense among the ellipses staying inside the primary orbit.

          source
          theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.liftedDelaunayFlowLine_invariant {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) {firstAction eccentricity meanAnomaly periapsisAngle : ℝ} (hfirstAction : firstAction ≠ 0) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : firstAction ^ 2 * (1 + eccentricity) < 1) (time : ℝ) :
          F 0 (liftedDelaunayFlowLine firstAction eccentricity meanAnomaly periapsisAngle time) = F 0 (liftedDelaunayFlowLine firstAction eccentricity meanAnomaly periapsisAngle 0)

          The mass-zero member of an exact analytic first-integral family is invariant along every interior lifted Delaunay flow line.

          source
          theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.mass_zero_liftedDelaunayPhasePoint_eq_of_irrational {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) {firstAction eccentricity : ℝ} (hfirstAction : firstAction ≠ 0) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : firstAction ^ 2 * (1 + eccentricity) < 1) (hirrational : Irrational (1 / firstAction ^ 3)) (firstAngles secondAngles : ℝ × ℝ) :
          F 0 (liftedDelaunayPhasePoint firstAction eccentricity firstAngles.1 firstAngles.2) = F 0 (liftedDelaunayPhasePoint firstAction eccentricity secondAngles.1 secondAngles.2)

          On every irrational interior Kepler torus, the mass-zero term of a candidate exact analytic first integral is independent of both Delaunay angles.

          source
          theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.mass_zero_liftedDelaunayPhasePoint_eq {δ : ℝ} {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) (firstAngles secondAngles : ℝ × ℝ) :
          F 0 (liftedDelaunayPhasePoint firstAction eccentricity firstAngles.1 firstAngles.2) = F 0 (liftedDelaunayPhasePoint firstAction eccentricity secondAngles.1 secondAngles.2)

          On every interior Kepler torus, including the rationally resonant ones, the mass-zero term of an exact analytic first-integral family is independent of both Delaunay angles. This is the continuity extension of the irrational-torus theorem.