Mixed derivatives of the restricted three-body Hamiltonian

Joint analyticity permits the mass and phase derivatives of the Hamiltonian to be interchanged. Combining this fact with the explicit mass derivative identifies the Hamiltonian term in Poincaré's first homological equation.

theorem LeanPool.PoincareThreeBody.parameterCoefficient_hamiltonian_eventuallyEq {s : PhaseSpace} (hs : (0, s) ∈ collisionFree) : parameterCoefficient (Function.uncurry hamiltonian) =ᶠ[nhds s] firstMassPerturbation

Near a collision-free phase point, the joint parameter coefficient of the Hamiltonian is the explicit first mass perturbation.

theorem LeanPool.PoincareThreeBody.hasDerivAt_hamiltonian_phasePartial_mass_zero {s : PhaseSpace} (hs : (0, s) ∈ collisionFree) (i : Fin 4) : HasDerivAt (fun (mass : ℝ) => (fderiv ℝ (hamiltonian mass) s) (coordinateVector i)) ((fderiv ℝ firstMassPerturbation s) (coordinateVector i)) 0

The mass derivative of every phase partial of the Hamiltonian is the corresponding phase partial of the explicit perturbation.

theorem LeanPool.PoincareThreeBody.firstHomologicalEquation_cr3bp_of_contDiffAt {F : ℝ → PhaseSpace → ℝ} {s : PhaseSpace} (hs : (0, s) ∈ collisionFree) (hF : ContDiffAt ℝ 2 (Function.uncurry F) (0, s)) (hcommutes : ∀ᶠ (mass : ℝ) in nhds 0, poissonBracket (F mass) (hamiltonian mass) s = 0) : poissonBracket (parameterCoefficient (Function.uncurry F)) (hamiltonian 0) s + poissonBracket (F 0) firstMassPerturbation s = 0

A jointly C² candidate which commutes with the physical Hamiltonian satisfies the explicit first homological equation at every collision-free phase point over μ = 0.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.firstHomologicalEquation_mass_zero {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) {s : PhaseSpace} (hs : (0, s) ∈ collisionFree) : poissonBracket (parameterCoefficient (Function.uncurry F)) (hamiltonian 0) s + poissonBracket (F 0) firstMassPerturbation s = 0

The hypotheses used in the challenge imply the explicit first homological equation at every collision-free phase point over the Kepler limit.