The apoapsis collision boundary of an interior resonance

For resonant semimajor axes between 1 / 2 and 1, increasing eccentricity reaches the unit primary before the parabolic limit. This file identifies the boundary eccentricity, apoapsis time, and orientation at which the limiting ellipse meets the primary exactly.

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

Semimajor axis of the normalized Kepler ellipse at the (p,q) resonance.

Equations

• LeanPool.PoincareThreeBody.resonantSemimajorAxis p q = LeanPool.PoincareThreeBody.resonantFirstAction p q ^ 2

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

Eccentricity at which the resonant apoapsis reaches radius one.

Equations

• LeanPool.PoincareThreeBody.resonantCollisionEccentricity p q = 1 / LeanPool.PoincareThreeBody.resonantSemimajorAxis p q - 1

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

The first time at which the resonant orbit reaches apoapsis.

Equations

• LeanPool.PoincareThreeBody.resonantApoapsisTime p q = Real.pi * ↑p / ↑q

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

Orientation which places that apoapsis at the unit primary.

Equations

• LeanPool.PoincareThreeBody.resonantCollisionOrientation p q = LeanPool.PoincareThreeBody.resonantApoapsisTime p q - Real.pi

theorem LeanPool.PoincareThreeBody.resonantSemimajorAxis_pos {p q : ℕ} (hp : 0 < p) (hq : 0 < q) : 0 < resonantSemimajorAxis p q

theorem LeanPool.PoincareThreeBody.resonantCollisionEccentricity_pos {p q : ℕ} (hp : 0 < p) (hq : 0 < q) (haxisOne : resonantSemimajorAxis p q < 1) : 0 < resonantCollisionEccentricity p q

theorem LeanPool.PoincareThreeBody.resonantCollisionEccentricity_lt_one {p q : ℕ} (hp : 0 < p) (hq : 0 < q) (haxisHalf : 1 / 2 < resonantSemimajorAxis p q) : resonantCollisionEccentricity p q < 1

theorem LeanPool.PoincareThreeBody.resonantMeanAnomaly_apoapsisTime {p q : ℕ} (hp : 0 < p) (hq : 0 < q) : resonantMeanAnomaly p q (resonantApoapsisTime p q) = Real.pi

theorem LeanPool.PoincareThreeBody.resonantEccentricAnomaly_apoapsisTime {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : resonantEccentricAnomaly p q eccentricity (resonantApoapsisTime p q) = Real.pi

theorem LeanPool.PoincareThreeBody.resonantApoapsisTime_lt_orbitPeriod {p q : ℕ} (hp : 0 < p) (hq : 0 < q) : resonantApoapsisTime p q < resonantOrbitPeriod p

theorem LeanPool.PoincareThreeBody.orientedResonantEllipsePosition_alignedApoapsis {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : orientedResonantEllipsePosition p q eccentricity (resonantCollisionOrientation p q) (resonantApoapsisTime p q) = ![resonantSemimajorAxis p q * (1 + eccentricity), 0]

At the collision-aligned orientation, every admissible ellipse places its apoapsis on the positive rotating x-axis.

theorem LeanPool.PoincareThreeBody.alignedApoapsis_primaryDistance {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantSemimajorAxis p q * (1 + eccentricity) < 1) : √((orientedResonantEllipsePosition p q eccentricity (resonantCollisionOrientation p q) (resonantApoapsisTime p q) 0 - 1) ^ 2 + orientedResonantEllipsePosition p q eccentricity (resonantCollisionOrientation p q) (resonantApoapsisTime p q) 1 ^ 2) = 1 - resonantSemimajorAxis p q * (1 + eccentricity)

The distance from aligned apoapsis to the unit primary is the remaining apoapsis gap.

theorem LeanPool.PoincareThreeBody.resonantDisturbingFunction_alignedApoapsis {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantSemimajorAxis p q * (1 + eccentricity) < 1) : resonantDisturbingFunction p q eccentricity (resonantCollisionOrientation p q) (resonantApoapsisTime p q) = have radius := resonantSemimajorAxis p q * (1 + eccentricity); 1 / radius + 1 / radius ^ 2 - 1 / (1 - radius)

At aligned apoapsis the singular part of the disturbing function is exactly the reciprocal of the remaining gap to collision.

theorem LeanPool.PoincareThreeBody.orientedResonantEllipsePosition_collisionBoundary {p q : ℕ} (hp : 0 < p) (hq : 0 < q) (haxisHalf : 1 / 2 < resonantSemimajorAxis p q) (haxisOne : resonantSemimajorAxis p q < 1) : orientedResonantEllipsePosition p q (resonantCollisionEccentricity p q) (resonantCollisionOrientation p q) (resonantApoapsisTime p q) = ![1, 0]

At the boundary eccentricity and aligned orientation, apoapsis is exactly the unit primary.

theorem LeanPool.PoincareThreeBody.collisionAlignedPosition_isBigO {p q : ℕ} (hp : 0 < p) (hq : 0 < q) (haxisHalf : 1 / 2 < resonantSemimajorAxis p q) (haxisOne : resonantSemimajorAxis p q < 1) : (fun (parameters : ℝ × ℝ) => orientedResonantEllipsePosition p q parameters.1 (resonantCollisionOrientation p q) parameters.2 - ![1, 0]) =O[nhds (resonantCollisionEccentricity p q, resonantApoapsisTime p q)] fun (parameters : ℝ × ℝ) => parameters - (resonantCollisionEccentricity p q, resonantApoapsisTime p q)

The collision-aligned position approaches the unit primary at most linearly in the joint eccentricity/time displacement. This is the local estimate behind the logarithmic blowup of the averaged Newtonian singularity.

theorem LeanPool.PoincareThreeBody.exists_collisionAlignedPosition_local_bound {p q : ℕ} (hp : 0 < p) (hq : 0 < q) (haxisHalf : 1 / 2 < resonantSemimajorAxis p q) (haxisOne : resonantSemimajorAxis p q < 1) : ∃ (lipConstant : ℝ), 0 < lipConstant ∧ ∃ (radius : ℝ), 0 < radius ∧ ∀ (parameters : ℝ × ℝ), dist parameters (resonantCollisionEccentricity p q, resonantApoapsisTime p q) < radius → ‖orientedResonantEllipsePosition p q parameters.1 (resonantCollisionOrientation p q) parameters.2 - ![1, 0]‖ ≤ lipConstant * ‖parameters - (resonantCollisionEccentricity p q, resonantApoapsisTime p q)‖

Quantitative neighborhood form of collisionAlignedPosition_isBigO.

theorem LeanPool.PoincareThreeBody.sqrt_sq_add_sq_le_two_norm (vector : ActionSpace) : √(vector 0 ^ 2 + vector 1 ^ 2) ≤ 2 * ‖vector‖

The Euclidean distance used by the Newtonian potential is controlled by twice the ambient sup norm on the concrete two-dimensional action space.