First mass perturbation of the planar Hamiltonian

This file differentiates the rotating-frame Hamiltonian with respect to the mass parameter at the Kepler limit. The resulting disturbing function is the explicit input to Poincaré's first homological equation.

theorem LeanPool.PoincareThreeBody.hasDerivAt_firstPrimaryDistanceSq (μ : ℝ) (s : PhaseSpace) : HasDerivAt (fun (mass : ℝ) => firstPrimaryDistanceSq mass s) (2 * (s 0 - 1 + μ)) μ

theorem LeanPool.PoincareThreeBody.hasDerivAt_secondPrimaryDistanceSq (μ : ℝ) (s : PhaseSpace) : HasDerivAt (fun (mass : ℝ) => secondPrimaryDistanceSq mass s) (2 * (s 0 + μ)) μ

theorem LeanPool.PoincareThreeBody.hasDerivAt_inverseSqrt_comp {f : ℝ → ℝ} {f' x : ℝ} (hf : HasDerivAt f f' x) (hpositive : 0 < f x) : HasDerivAt (fun (y : ℝ) => 1 / √(f y)) (-(f' / (2 * √(f x))) / √(f x) ^ 2) x

noncomputable def LeanPool.PoincareThreeBody.firstMassPerturbation (s : PhaseSpace) : ℝ

The coefficient of μ in the planar Hamiltonian at the Kepler limit.

Equations

• LeanPool.PoincareThreeBody.firstMassPerturbation s = 1 / √(s 0 ^ 2 + s 1 ^ 2) + s 0 / √(s 0 ^ 2 + s 1 ^ 2) ^ 3 - 1 / √((s 0 - 1) ^ 2 + s 1 ^ 2)

theorem LeanPool.PoincareThreeBody.firstMassPerturbation_eq_source_form {s : PhaseSpace} (hsecond : secondPrimaryDistanceSq 0 s ≠ 0) : firstMassPerturbation s = (s 0 ^ 2 + s 1 ^ 2 + s 0) / √(s 0 ^ 2 + s 1 ^ 2) ^ 3 - 1 / √((s 0 - 1) ^ 2 + s 1 ^ 2)

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

The explicit disturbing function is the mass derivative of the Hamiltonian at μ = 0.

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