Documentation

LeanPool.PoincareThreeBody.DisturbingRegularBound

Uniform control of the regular disturbing terms near collision #

The two nonsingular terms in the first mass perturbation stay uniformly bounded as an interior resonant ellipse approaches its apoapsis collision boundary.

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

The part of the resonant disturbing function which is regular at the unit primary.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem LeanPool.PoincareThreeBody.resonantDisturbingFunction_eq_regularPart_sub_primaryInverse (p q : ℕ) (eccentricity orientation time : ℝ) :
    resonantDisturbingFunction p q eccentricity orientation time = resonantRegularPart p q eccentricity orientation time - resonantPrimaryInverse p q eccentricity orientation time
    source
    theorem LeanPool.PoincareThreeBody.sqrt_orientedResonantEllipse_origin_sq {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity orientation time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) :
    √(orientedResonantEllipsePosition p q eccentricity orientation time 0 ^ 2 + orientedResonantEllipsePosition p q eccentricity orientation time 1 ^ 2) = eccentricRadius (resonantFirstAction p q) eccentricity (resonantEccentricAnomaly p q eccentricity time)
    source
    theorem LeanPool.PoincareThreeBody.collision_radius_floor_pos {p q : ℕ} (haxisHalf : 1 / 2 < resonantSemimajorAxis p q) :
    0 < 2 * resonantSemimajorAxis p q - 1

    The pericenter radius at the collision boundary is 2a - 1, which is positive precisely in the interior band a > 1/2.

    source
    theorem LeanPool.PoincareThreeBody.collision_radius_floor_le_eccentricRadius {p q : ℕ} (hp : 0 < p) (hq : 0 < q) (haxisHalf : 1 / 2 < resonantSemimajorAxis p q) {eccentricity anomaly : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityBoundary : eccentricity ≤ resonantCollisionEccentricity p q) :
    2 * resonantSemimajorAxis p q - 1 ≤ eccentricRadius (resonantFirstAction p q) eccentricity anomaly

    Every radius before collision is bounded below by the boundary pericenter radius.

    source
    theorem LeanPool.PoincareThreeBody.resonant_apoapsis_lt_one_of_eccentricity_lt_collision {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity : ℝ} (heccentricityBoundary : eccentricity < resonantCollisionEccentricity p q) :
    resonantSemimajorAxis p q * (1 + eccentricity) < 1
    source
    theorem LeanPool.PoincareThreeBody.abs_resonantRegularPart_le_collision_bound {p q : ℕ} (hp : 0 < p) (hq : 0 < q) (haxisHalf : 1 / 2 < resonantSemimajorAxis p q) {eccentricity orientation time : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (heccentricityBoundary : eccentricity ≤ resonantCollisionEccentricity p q) :
    |resonantRegularPart p q eccentricity orientation time| ≤ 1 / (2 * resonantSemimajorAxis p q - 1) + 1 / (2 * resonantSemimajorAxis p q - 1) ^ 2

    Explicit uniform absolute bound for the regular part throughout the pre-collision family.

    source
    theorem LeanPool.PoincareThreeBody.intervalIntegrable_resonantRegularPart {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity orientation start finish : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantSemimajorAxis p q * (1 + eccentricity) < 1) :
    IntervalIntegrable (resonantRegularPart p q eccentricity orientation) MeasureTheory.volume start finish
    source
    theorem LeanPool.PoincareThreeBody.abs_integral_resonantRegularPart_le_collision_bound {p q : ℕ} (hp : 0 < p) (hq : 0 < q) (haxisHalf : 1 / 2 < resonantSemimajorAxis p q) {eccentricity orientation : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (heccentricityBoundary : eccentricity < resonantCollisionEccentricity p q) :
    |∫ (time : ℝ) in 0..resonantOrbitPeriod p, resonantRegularPart p q eccentricity orientation time| ≤ resonantOrbitPeriod p * (1 / (2 * resonantSemimajorAxis p q - 1) + 1 / (2 * resonantSemimajorAxis p q - 1) ^ 2)

    The integral of the regular part is uniformly bounded throughout the pre-collision family.