Analyticity of the Newtonian potential away from collision

Mathlib provides the real binomial series at one but does not package the resulting local analyticity of arbitrary real powers on the positive half-line. We establish that bridge and apply it to the inverse square roots in the restricted three-body potential.

theorem LeanPool.PoincareThreeBody.analyticAt_rpow_of_pos (a : ℝ) {x₀ : ℝ} (hx₀ : 0 < x₀) : AnalyticAt ℝ (fun (x : ℝ) => x ^ a) x₀

A real power is analytic at every positive base.

theorem LeanPool.PoincareThreeBody.analyticAt_inv_sqrt {x₀ : ℝ} (hx₀ : 0 < x₀) : AnalyticAt ℝ (fun (x : ℝ) => 1 / √x) x₀

The inverse square-root function is analytic at every positive real number.

theorem LeanPool.PoincareThreeBody.analyticAt_sqrt_of_pos {x₀ : ℝ} (hx₀ : 0 < x₀) : AnalyticAt ℝ Real.sqrt x₀

The square-root function is analytic at every positive real number.

theorem LeanPool.PoincareThreeBody.mass_analyticAt (z : ℝ × PhaseSpace) : AnalyticAt ℝ (fun (w : ℝ × PhaseSpace) => w.1) z

theorem LeanPool.PoincareThreeBody.phaseCoordinate_analyticAt (z : ℝ × PhaseSpace) (i : Fin 4) : AnalyticAt ℝ (fun (w : ℝ × PhaseSpace) => w.2 i) z

theorem LeanPool.PoincareThreeBody.firstPrimaryDistanceSq_analyticAt (z : ℝ × PhaseSpace) : AnalyticAt ℝ (Function.uncurry firstPrimaryDistanceSq) z

theorem LeanPool.PoincareThreeBody.secondPrimaryDistanceSq_analyticAt (z : ℝ × PhaseSpace) : AnalyticAt ℝ (Function.uncurry secondPrimaryDistanceSq) z

theorem LeanPool.PoincareThreeBody.inverseFirstDistance_analyticAt {z : ℝ × PhaseSpace} (hz : firstPrimaryDistanceSq z.1 z.2 ≠ 0) : AnalyticAt ℝ (fun (w : ℝ × PhaseSpace) => 1 / √(firstPrimaryDistanceSq w.1 w.2)) z

theorem LeanPool.PoincareThreeBody.inverseSecondDistance_analyticAt {z : ℝ × PhaseSpace} (hz : secondPrimaryDistanceSq z.1 z.2 ≠ 0) : AnalyticAt ℝ (fun (w : ℝ × PhaseSpace) => 1 / √(secondPrimaryDistanceSq w.1 w.2)) z

theorem LeanPool.PoincareThreeBody.potential_analyticAt {z : ℝ × PhaseSpace} (hz : z ∈ collisionFree) : AnalyticAt ℝ (Function.uncurry potential) z

The Newtonian potential is jointly analytic in mass and phase away from both collisions.

theorem LeanPool.PoincareThreeBody.hamiltonian_analyticAt {z : ℝ × PhaseSpace} (hz : z ∈ collisionFree) : AnalyticAt ℝ (Function.uncurry hamiltonian) z

The rotating-frame Hamiltonian is jointly analytic away from collision.

theorem LeanPool.PoincareThreeBody.potential_analyticOn_collisionFree : AnalyticOnNhd ℝ (Function.uncurry potential) collisionFree

theorem LeanPool.PoincareThreeBody.hamiltonian_analyticOn_collisionFree : AnalyticOnNhd ℝ (Function.uncurry hamiltonian) collisionFree

theorem LeanPool.PoincareThreeBody.analyticAt_mass_zero_of_jointlyAnalytic {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hF : IsJointlyAnalytic δ F) {s : PhaseSpace} (hs : (0, s) ∈ collisionFree) : AnalyticAt ℝ (fun (μ : ℝ) => F μ s) 0

Joint analyticity supplies an ordinary analytic mass-parameter germ at every collision-free phase point over μ = 0.

theorem LeanPool.PoincareThreeBody.exists_massPowerSeries_of_jointlyAnalytic {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hF : IsJointlyAnalytic δ F) {s : PhaseSpace} (hs : (0, s) ∈ collisionFree) : ∃ (series : FormalMultilinearSeries ℝ ℝ ℝ), HasFPowerSeriesAt (fun (μ : ℝ) => F μ s) series 0

A jointly analytic candidate integral has a convergent mass-parameter power series at every collision-free phase point over the Kepler limit.

theorem LeanPool.PoincareThreeBody.hamiltonian_analyticAt_mass_zero {s : PhaseSpace} (hs : (0, s) ∈ collisionFree) : AnalyticAt ℝ (fun (μ : ℝ) => hamiltonian μ s) 0