Logarithmic growth near a resonant collision

This file develops the real-variable estimate showing that the averaged Newtonian singularity becomes unbounded when an aligned apoapsis approaches the unit primary.

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

Reciprocal distance from the resonant position to the unit primary.

Equations

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

theorem LeanPool.PoincareThreeBody.analyticAt_resonantPrimaryInverse_time {p q : ℕ} {eccentricity orientation time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantSemimajorAxis p q * (1 + eccentricity) < 1) : AnalyticAt ℝ (resonantPrimaryInverse p q eccentricity orientation) time

theorem LeanPool.PoincareThreeBody.continuous_resonantPrimaryInverse {p q : ℕ} {eccentricity orientation : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantSemimajorAxis p q * (1 + eccentricity) < 1) : Continuous (resonantPrimaryInverse p q eccentricity orientation)

theorem LeanPool.PoincareThreeBody.one_div_two_mul_constant_mul_time_le_resonantPrimaryInverse {p q : ℕ} {lipConstant neighborhoodRadius eccentricity time : ℝ} (hlocal : ∀ (parameters : ℝ × ℝ), dist parameters (resonantCollisionEccentricity p q, resonantApoapsisTime p q) < neighborhoodRadius → ‖orientedResonantEllipsePosition p q parameters.1 (resonantCollisionOrientation p q) parameters.2 - ![1, 0]‖ ≤ lipConstant * ‖parameters - (resonantCollisionEccentricity p q, resonantApoapsisTime p q)‖) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantSemimajorAxis p q * (1 + eccentricity) < 1) (heccentricityDisplacement : 0 < resonantCollisionEccentricity p q - eccentricity) (htimeDisplacementLower : resonantCollisionEccentricity p q - eccentricity ≤ time - resonantApoapsisTime p q) (htimeDisplacementUpper : time - resonantApoapsisTime p q < neighborhoodRadius) : 1 / (2 * lipConstant * (time - resonantApoapsisTime p q)) ≤ resonantPrimaryInverse p q eccentricity (resonantCollisionOrientation p q) time

On the one-sided time interval where time displacement dominates eccentricity displacement, the collision inverse is bounded below by a reciprocal linear function.

theorem LeanPool.PoincareThreeBody.log_lower_bound_resonantPrimaryInverse_local_integral {p q : ℕ} {lipConstant neighborhoodRadius eccentricity window : ℝ} (hconstant : 0 < lipConstant) (hlocal : ∀ (parameters : ℝ × ℝ), dist parameters (resonantCollisionEccentricity p q, resonantApoapsisTime p q) < neighborhoodRadius → ‖orientedResonantEllipsePosition p q parameters.1 (resonantCollisionOrientation p q) parameters.2 - ![1, 0]‖ ≤ lipConstant * ‖parameters - (resonantCollisionEccentricity p q, resonantApoapsisTime p q)‖) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantSemimajorAxis p q * (1 + eccentricity) < 1) (hdelta : 0 < resonantCollisionEccentricity p q - eccentricity) (hdeltaWindow : resonantCollisionEccentricity p q - eccentricity < window) (hwindow : window < neighborhoodRadius) : 1 / (2 * lipConstant) * Real.log (window / (resonantCollisionEccentricity p q - eccentricity)) ≤ ∫ (time : ℝ) in resonantApoapsisTime p q + (resonantCollisionEccentricity p q - eccentricity)..resonantApoapsisTime p q + window, resonantPrimaryInverse p q eccentricity (resonantCollisionOrientation p q) time

Integrating the pointwise collision estimate gives the explicit logarithmic lower bound.

theorem LeanPool.PoincareThreeBody.log_lower_bound_resonantPrimaryInverse_period_integral {p q : ℕ} {lipConstant neighborhoodRadius eccentricity window : ℝ} (hconstant : 0 < lipConstant) (hlocal : ∀ (parameters : ℝ × ℝ), dist parameters (resonantCollisionEccentricity p q, resonantApoapsisTime p q) < neighborhoodRadius → ‖orientedResonantEllipsePosition p q parameters.1 (resonantCollisionOrientation p q) parameters.2 - ![1, 0]‖ ≤ lipConstant * ‖parameters - (resonantCollisionEccentricity p q, resonantApoapsisTime p q)‖) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantSemimajorAxis p q * (1 + eccentricity) < 1) (hdelta : 0 < resonantCollisionEccentricity p q - eccentricity) (hdeltaWindow : resonantCollisionEccentricity p q - eccentricity < window) (hwindow : window < neighborhoodRadius) (hwindowPeriod : resonantApoapsisTime p q + window ≤ resonantOrbitPeriod p) : 1 / (2 * lipConstant) * Real.log (window / (resonantCollisionEccentricity p q - eccentricity)) ≤ ∫ (time : ℝ) in 0..resonantOrbitPeriod p, resonantPrimaryInverse p q eccentricity (resonantCollisionOrientation p q) time

The local logarithmic estimate also bounds the inverse-distance integral over the whole resonant period, provided the comparison window lies inside that period.