Analytic eccentricity dependence of the resonant disturbing average

The joint analyticity of the disturbing function and compact parameter-integral theorem imply that averaging over one resonant period preserves real analyticity in eccentricity.

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

The resonant disturbing average is analytic in eccentricity throughout the collision-free interior range.

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

Analyticity assembled over the entire admissible eccentricity interval.