Analyticity of the collision-avoiding average at the boundary

Compactness of one resonant period upgrades pointwise collision avoidance to a uniform parameter neighborhood. The compact parameter-integral theorem then gives analyticity of the safe average through the collision eccentricity.

noncomputable def LeanPool.PoincareThreeBody.safePrimaryDistanceSq (p q : ℕ) (parameters : ℝ × ℝ) : ℝ

Squared distance from the primary along the collision-avoiding resonant orientation.

Equations

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

theorem LeanPool.PoincareThreeBody.analyticAt_safePrimaryDistanceSq (p q : ℕ) {eccentricity time : ℝ} (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) : AnalyticAt ℝ (safePrimaryDistanceSq p q) (eccentricity, time)

theorem LeanPool.PoincareThreeBody.isOpen_safeCollisionFreeParameters (p q : ℕ) : IsOpen {parameters : ℝ × ℝ | 0 < parameters.1 ∧ parameters.1 < 1 ∧ safePrimaryDistanceSq p q parameters ≠ 0}

theorem LeanPool.PoincareThreeBody.analyticAt_resonantDisturbingAverage_safe_collisionBoundary {p q : ℕ} (hp : 0 < p) (hq : 0 < q) (haxisHalf : 1 / 2 < resonantSemimajorAxis p q) (haxisOne : resonantSemimajorAxis p q < 1) : AnalyticAt ℝ (fun (eccentricity : ℝ) => resonantDisturbingAverage p q eccentricity (resonantSafeOrientation p q)) (resonantCollisionEccentricity p q)

The safe disturbing average extends analytically through the aligned collision boundary.