Periodic Kepler ellipses at rational Delaunay resonances

At the action I₁³ = p / q, the inertial ellipse makes q revolutions while the rotating frame makes p revolutions during the common period 2πp. This file constructs that orbit and proves its periodicity exactly.

noncomputable def LeanPool.PoincareThreeBody.resonantMeanMotion (p q : ℕ) : ℝ

Mean motion on the (p,q) Kepler resonance.

Equations

• LeanPool.PoincareThreeBody.resonantMeanMotion p q = ↑q / ↑p

noncomputable def LeanPool.PoincareThreeBody.resonantOrbitPeriod (p : ℕ) : ℝ

Common period of the inertial ellipse and rotating frame.

Equations

• LeanPool.PoincareThreeBody.resonantOrbitPeriod p = 2 * Real.pi * ↑p

noncomputable def LeanPool.PoincareThreeBody.resonantMeanAnomaly (p q : ℕ) (time : ℝ) : ℝ

Mean anomaly along a resonant unperturbed orbit.

Equations

• LeanPool.PoincareThreeBody.resonantMeanAnomaly p q time = LeanPool.PoincareThreeBody.resonantMeanMotion p q * time

noncomputable def LeanPool.PoincareThreeBody.resonantEccentricAnomaly (p q : ℕ) (eccentricity time : ℝ) : ℝ

Eccentric anomaly along a resonant unperturbed orbit.

Equations

• LeanPool.PoincareThreeBody.resonantEccentricAnomaly p q eccentricity time = LeanPool.PoincareThreeBody.eccentricAnomaly eccentricity (LeanPool.PoincareThreeBody.resonantMeanAnomaly p q time)

noncomputable def LeanPool.PoincareThreeBody.resonantRotatingEllipsePosition (p q : ℕ) (eccentricity time : ℝ) : ActionSpace

Position of the resonant Kepler ellipse in the rotating frame.

Equations

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

noncomputable def LeanPool.PoincareThreeBody.resonantEllipsePhasePoint (p q : ℕ) (eccentricity time : ℝ) : PhaseSpace

The resonant position embedded into the four-dimensional phase space.

Equations

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

theorem LeanPool.PoincareThreeBody.resonantMeanMotion_eq_delaunayFrequency {p q : ℕ} (hp : 0 < p) (hq : 0 < q) : resonantMeanMotion p q = delaunayFrequency (resonantFirstAction p q) 0

theorem LeanPool.PoincareThreeBody.resonantMeanAnomaly_add_period {p q : ℕ} (hp : 0 < p) (time : ℝ) : resonantMeanAnomaly p q (time + resonantOrbitPeriod p) = resonantMeanAnomaly p q time + ↑q * (2 * Real.pi)

theorem LeanPool.PoincareThreeBody.resonantEccentricAnomaly_add_period {p q : ℕ} (hp : 0 < p) {eccentricity : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (time : ℝ) : resonantEccentricAnomaly p q eccentricity (time + resonantOrbitPeriod p) = resonantEccentricAnomaly p q eccentricity time + ↑q * (2 * Real.pi)

theorem LeanPool.PoincareThreeBody.analyticAt_resonantMeanAnomaly (p q : ℕ) (time : ℝ) : AnalyticAt ℝ (resonantMeanAnomaly p q) time

theorem LeanPool.PoincareThreeBody.analyticAt_resonantEccentricAnomaly (p q : ℕ) {eccentricity time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : AnalyticAt ℝ (resonantEccentricAnomaly p q eccentricity) time

theorem LeanPool.PoincareThreeBody.analyticAt_resonantRotatingEllipsePosition_coordinate (p q : ℕ) {eccentricity time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (coordinate : Fin 2) : AnalyticAt ℝ (fun (argument : ℝ) => resonantRotatingEllipsePosition p q eccentricity argument coordinate) time

theorem LeanPool.PoincareThreeBody.analyticAt_firstMassPerturbation_resonantOrbit {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hprimary : (resonantRotatingEllipsePosition p q eccentricity time 0 - 1) ^ 2 + resonantRotatingEllipsePosition p q eccentricity time 1 ^ 2 ≠ 0) : AnalyticAt ℝ (fun (argument : ℝ) => firstMassPerturbation (resonantEllipsePhasePoint p q eccentricity argument)) time

Away from a collision with the unit primary, the disturbing function restricted to a resonant ellipse is real analytic in time.

theorem LeanPool.PoincareThreeBody.intervalIntegrable_firstMassPerturbation_resonantOrbit {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity start finish : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hprimary : ∀ time ∈ Set.uIcc start finish, (resonantRotatingEllipsePosition p q eccentricity time 0 - 1) ^ 2 + resonantRotatingEllipsePosition p q eccentricity time 1 ^ 2 ≠ 0) : IntervalIntegrable (fun (time : ℝ) => firstMassPerturbation (resonantEllipsePhasePoint p q eccentricity time)) MeasureTheory.volume start finish

theorem LeanPool.PoincareThreeBody.resonantRotatingEllipse_primaryDistance_ne_zero_of_apoapsis_lt_one {p q : ℕ} {eccentricity time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) : (resonantRotatingEllipsePosition p q eccentricity time 0 - 1) ^ 2 + resonantRotatingEllipsePosition p q eccentricity time 1 ^ 2 ≠ 0

theorem LeanPool.PoincareThreeBody.analyticAt_firstMassPerturbation_resonantOrbit_of_apoapsis_lt_one {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) : AnalyticAt ℝ (fun (argument : ℝ) => firstMassPerturbation (resonantEllipsePhasePoint p q eccentricity argument)) time

theorem LeanPool.PoincareThreeBody.intervalIntegrable_firstMassPerturbation_resonantOrbit_of_apoapsis_lt_one {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity start finish : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) : IntervalIntegrable (fun (time : ℝ) => firstMassPerturbation (resonantEllipsePhasePoint p q eccentricity time)) MeasureTheory.volume start finish

theorem LeanPool.PoincareThreeBody.resonantEllipsePhasePoint_collisionFree_mass_zero {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hprimary : (resonantRotatingEllipsePosition p q eccentricity time 0 - 1) ^ 2 + resonantRotatingEllipsePosition p q eccentricity time 1 ^ 2 ≠ 0) : (0, resonantEllipsePhasePoint p q eccentricity time) ∈ collisionFree

theorem LeanPool.PoincareThreeBody.resonantRotatingEllipsePosition_add_period {p q : ℕ} (hp : 0 < p) {eccentricity : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (time : ℝ) : resonantRotatingEllipsePosition p q eccentricity (time + resonantOrbitPeriod p) = resonantRotatingEllipsePosition p q eccentricity time

A rational Kepler resonance gives a genuinely periodic orbit in the rotating frame.

theorem LeanPool.PoincareThreeBody.resonantEllipsePhasePoint_add_period {p q : ℕ} (hp : 0 < p) {eccentricity : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (time : ℝ) : resonantEllipsePhasePoint p q eccentricity (time + resonantOrbitPeriod p) = resonantEllipsePhasePoint p q eccentricity time

theorem LeanPool.PoincareThreeBody.firstMassPerturbation_resonantOrbit_periodic {p q : ℕ} (hp : 0 < p) {eccentricity : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (time : ℝ) : firstMassPerturbation (resonantEllipsePhasePoint p q eccentricity (time + resonantOrbitPeriod p)) = firstMassPerturbation (resonantEllipsePhasePoint p q eccentricity time)

The disturbing function restricted to a resonant ellipse has the common resonant period.