Analytic eccentricity dependence of the disturbing function

Away from collisions, the Newtonian disturbing function along a fixed point of a resonant orbit is real analytic in eccentricity. This is the pointwise analytic input for the subsequent parameter-integral argument.

theorem LeanPool.PoincareThreeBody.analyticAt_resonantEccentricAnomaly_eccentricity (p q : ℕ) {eccentricity time : ℝ} (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) : AnalyticAt ℝ (fun (candidate : ℝ) => resonantEccentricAnomaly p q candidate time) eccentricity

theorem LeanPool.PoincareThreeBody.analyticAt_orientedResonantEllipsePosition_eccentricity_coordinate (p q : ℕ) {eccentricity orientation time : ℝ} (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) (coordinate : Fin 2) : AnalyticAt ℝ (fun (candidate : ℝ) => orientedResonantEllipsePosition p q candidate orientation time coordinate) eccentricity

Each rotating Cartesian coordinate of the oriented resonant ellipse is analytic in eccentricity.

theorem LeanPool.PoincareThreeBody.analyticAt_resonantDisturbingFunction_eccentricity {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity orientation time : ℝ} (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) : AnalyticAt ℝ (fun (candidate : ℝ) => resonantDisturbingFunction p q candidate orientation time) eccentricity

At every fixed orientation and time, the resonant disturbing function is analytic in eccentricity throughout the collision-free interior range.

theorem LeanPool.PoincareThreeBody.analyticOnNhd_resonantDisturbingFunction_eccentricity {p q : ℕ} (hp : 0 < p) (hq : 0 < q) (orientation time : ℝ) : AnalyticOnNhd ℝ (fun (eccentricity : ℝ) => resonantDisturbingFunction p q eccentricity orientation time) {eccentricity : ℝ | 0 < eccentricity ∧ eccentricity < 1 ∧ resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1}

Pointwise analyticity assembled over the whole collision-free eccentricity interval.

theorem LeanPool.PoincareThreeBody.analyticAt_resonantEccentricAnomaly_eccentricity_time (p q : ℕ) {eccentricity time : ℝ} (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) : AnalyticAt ℝ (fun (parameters : ℝ × ℝ) => resonantEccentricAnomaly p q parameters.1 parameters.2) (eccentricity, time)

The resonant eccentric anomaly is jointly analytic in eccentricity and physical time.

theorem LeanPool.PoincareThreeBody.analyticAt_orientedResonantEllipsePosition_eccentricity_time_coordinate (p q : ℕ) {eccentricity orientation time : ℝ} (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) (coordinate : Fin 2) : AnalyticAt ℝ (fun (parameters : ℝ × ℝ) => orientedResonantEllipsePosition p q parameters.1 orientation parameters.2 coordinate) (eccentricity, time)

Each Cartesian coordinate of the oriented resonant ellipse is jointly analytic in eccentricity and time.

theorem LeanPool.PoincareThreeBody.analyticAt_resonantDisturbingFunction_eccentricity_time_of_primaryDistance_ne_zero {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity orientation time : ℝ} (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) (hprimaryNe : (orientedResonantEllipsePosition p q eccentricity orientation time 0 - 1) ^ 2 + orientedResonantEllipsePosition p q eccentricity orientation time 1 ^ 2 ≠ 0) : AnalyticAt ℝ (fun (parameters : ℝ × ℝ) => resonantDisturbingFunction p q parameters.1 orientation parameters.2) (eccentricity, time)

The disturbing function is jointly analytic at every point away from the unit primary.

theorem LeanPool.PoincareThreeBody.analyticAt_resonantDisturbingFunction_eccentricity_time {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity orientation time : ℝ} (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) : AnalyticAt ℝ (fun (parameters : ℝ × ℝ) => resonantDisturbingFunction p q parameters.1 orientation parameters.2) (eccentricity, time)

The collision-free disturbing function is jointly analytic in eccentricity and time.

theorem LeanPool.PoincareThreeBody.analyticOnNhd_resonantDisturbingFunction_eccentricity_time {p q : ℕ} (hp : 0 < p) (hq : 0 < q) (orientation : ℝ) : AnalyticOnNhd ℝ (fun (parameters : ℝ × ℝ) => resonantDisturbingFunction p q parameters.1 orientation parameters.2) {parameters : ℝ × ℝ | 0 < parameters.1 ∧ parameters.1 < 1 ∧ resonantFirstAction p q ^ 2 * (1 + parameters.1) < 1}

Joint analyticity assembled over the full admissible eccentricity/time cylinder.