The first homological equation

This file verifies the product-rule step in Poincaré's perturbative argument. If two families Poisson-commute for all nearby parameter values, differentiating at the Kepler limit gives the sum of the two cross brackets. The hypotheses expose precisely the mixed derivatives which must later be obtained from joint analyticity.

theorem LeanPool.PoincareThreeBody.hasDerivAt_poissonBracket_family {F H : ℝ → PhaseSpace → ℝ} {F₁ H₁ : PhaseSpace → ℝ} {s : PhaseSpace} (hF : ∀ (i : Fin 4), HasDerivAt (fun (mass : ℝ) => (fderiv ℝ (F mass) s) (coordinateVector i)) ((fderiv ℝ F₁ s) (coordinateVector i)) 0) (hH : ∀ (i : Fin 4), HasDerivAt (fun (mass : ℝ) => (fderiv ℝ (H mass) s) (coordinateVector i)) ((fderiv ℝ H₁ s) (coordinateVector i)) 0) : HasDerivAt (fun (mass : ℝ) => poissonBracket (F mass) (H mass) s) (poissonBracket F₁ (H 0) s + poissonBracket (F 0) H₁ s) 0

Differentiating the canonical Poisson bracket with respect to a parameter gives the two cross brackets. The derivative hypotheses are stated coordinatewise to isolate the required interchange of the mass derivative and the phase derivative.

theorem LeanPool.PoincareThreeBody.firstHomologicalEquation_of_poissonBracket_zero {F H : ℝ → PhaseSpace → ℝ} {F₁ H₁ : PhaseSpace → ℝ} {s : PhaseSpace} (hF : ∀ (i : Fin 4), HasDerivAt (fun (mass : ℝ) => (fderiv ℝ (F mass) s) (coordinateVector i)) ((fderiv ℝ F₁ s) (coordinateVector i)) 0) (hH : ∀ (i : Fin 4), HasDerivAt (fun (mass : ℝ) => (fderiv ℝ (H mass) s) (coordinateVector i)) ((fderiv ℝ H₁ s) (coordinateVector i)) 0) (hcommutes : ∀ᶠ (mass : ℝ) in nhds 0, poissonBracket (F mass) (H mass) s = 0) : poissonBracket F₁ (H 0) s + poissonBracket (F 0) H₁ s = 0

The coefficient of the parameter in a vanishing Poisson bracket is the first homological equation.

theorem LeanPool.PoincareThreeBody.firstHomologicalEquation_cr3bp {F : ℝ → PhaseSpace → ℝ} {F₁ : PhaseSpace → ℝ} {s : PhaseSpace} (hF : ∀ (i : Fin 4), HasDerivAt (fun (mass : ℝ) => (fderiv ℝ (F mass) s) (coordinateVector i)) ((fderiv ℝ F₁ s) (coordinateVector i)) 0) (hH : ∀ (i : Fin 4), HasDerivAt (fun (mass : ℝ) => (fderiv ℝ (hamiltonian mass) s) (coordinateVector i)) ((fderiv ℝ firstMassPerturbation s) (coordinateVector i)) 0) (hcommutes : ∀ᶠ (mass : ℝ) in nhds 0, poissonBracket (F mass) (hamiltonian mass) s = 0) : poissonBracket F₁ (hamiltonian 0) s + poissonBracket (F 0) firstMassPerturbation s = 0

For the restricted three-body Hamiltonian, the Hamiltonian cross term in the first homological equation is the explicit first mass perturbation.