Blow-up of the collision-aligned disturbing average #

Combining the logarithmic singular estimate with the uniform regular bound gives an explicit upper bound on the aligned disturbing average.

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

resonantDisturbingAverage p q eccentricity orientation = (∫ (time : ℝ) in 0..resonantOrbitPeriod p, resonantRegularPart p q eccentricity orientation time) - ∫ (time : ℝ) in 0..resonantOrbitPeriod p, resonantPrimaryInverse p q eccentricity orientation time

theorem LeanPool.PoincareThreeBody.resonantDisturbingAverage_collisionAligned_le {p q : ℕ} (hp : 0 < p) (hq : 0 < q) (haxisHalf : 1 / 2 < resonantSemimajorAxis 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) (heccentricityBoundary : eccentricity < resonantCollisionEccentricity p q) (hdeltaWindow : resonantCollisionEccentricity p q - eccentricity < window) (hwindow : window < neighborhoodRadius) (hwindowPeriod : resonantApoapsisTime p q + window ≤ resonantOrbitPeriod p) :

Explicit upper bound which tends to negative infinity as the eccentricity approaches the collision value from below.

theorem LeanPool.PoincareThreeBody.exists_collisionAligned_resonantDisturbingAverage_between {p q : ℕ} (hp : 0 < p) (hq : 0 < q) (haxisHalf : 1 / 2 < resonantSemimajorAxis p q) (haxisOne : resonantSemimajorAxis p q < 1) {lowerEccentricity : ℝ} (hlowerEccentricity : lowerEccentricity < resonantCollisionEccentricity p q) (target : ℝ) :

∃ (eccentricity : ℝ), lowerEccentricity < eccentricity ∧ 0 < eccentricity ∧ eccentricity < resonantCollisionEccentricity p q ∧ eccentricity < 1 ∧ resonantDisturbingAverage p q eccentricity (resonantCollisionOrientation p q) < target

Collision alignment makes the resonant disturbing average arbitrarily negative, at an eccentricity arbitrarily close to the collision boundary.

∃ (eccentricity : ℝ), 0 ≤ eccentricity ∧ eccentricity < resonantCollisionEccentricity p q ∧ eccentricity < 1 ∧ resonantDisturbingAverage p q eccentricity (resonantCollisionOrientation p q) < target

In particular, a positive admissible collision-aligned eccentricity realizes every negative target.

Documentation