Pointwise factorization of the leading integral through the Delaunay actions

The mass-zero leading coefficient is constant on every interior Kepler torus. This file upgrades that value-level statement to a differential identity: at every noncircular elliptic point, its phase differential is the pullback of the differential of the action-space representative.

theorem LeanPool.PoincareThreeBody.actionDerivativeCovector_cartesianDelaunayActions {state : PhaseSpace} (hposition : state 0 ^ 2 + state 1 ^ 2 ≠ 0) (henergy : cartesianKeplerEnergy state < 0) (coordinate : Fin 2) : actionDerivativeCovector (fderiv ℝ cartesianDelaunayActions state) coordinate = fderiv ℝ (fun (candidate : PhaseSpace) => cartesianDelaunayActions candidate coordinate) state

The rows of the derivative of the physical action map are the derivatives of its two scalar components.

theorem LeanPool.PoincareThreeBody.phaseHamiltonianVector_fderiv_cartesianAngularAction (state : PhaseSpace) : phaseHamiltonianVector (fderiv ℝ cartesianAngularAction state) = angularActionVectorField state

The Hamiltonian vector of the angular-action differential is simultaneous planar rotation.

theorem LeanPool.PoincareThreeBody.phaseHamiltonianVector_actionDerivativeCovector_one {firstAction eccentricity meanAnomaly periapsisAngle : ℝ} (hfirstAction : 0 < firstAction) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : have state := liftedDelaunayPhasePoint firstAction eccentricity meanAnomaly periapsisAngle; phaseHamiltonianVector (actionDerivativeCovector (fderiv ℝ cartesianDelaunayActions state) 1) = angularActionVectorField state

At a lifted elliptic point, the Hamiltonian vector of the second row of the action derivative is the angular-action vector field.

theorem LeanPool.PoincareThreeBody.fderiv_cartesianDelaunayActions_angularActionVectorField_eq_zero {firstAction eccentricity meanAnomaly periapsisAngle : ℝ} (hfirstAction : 0 < firstAction) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : have state := liftedDelaunayPhasePoint firstAction eccentricity meanAnomaly periapsisAngle; (fderiv ℝ cartesianDelaunayActions state) (angularActionVectorField state) = 0

The physical action derivative kills the angular-action Hamiltonian vector at every lifted elliptic point.

theorem LeanPool.PoincareThreeBody.phasePoissonPairing_actionDerivativeCovectors_eq_zero {firstAction eccentricity meanAnomaly periapsisAngle : ℝ} (hfirstAction : 0 < firstAction) (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) : have state := liftedDelaunayPhasePoint firstAction eccentricity meanAnomaly periapsisAngle; phasePoissonPairing (actionDerivativeCovector (fderiv ℝ cartesianDelaunayActions state) 0) (actionDerivativeCovector (fderiv ℝ cartesianDelaunayActions state) 1) = 0

The two rows of the physical action derivative are symplectically orthogonal on every lifted elliptic point.

theorem LeanPool.PoincareThreeBody.phasePoissonPairing_actionDerivativeCovector_eq_actionPoissonVector {state : PhaseSpace} (hposition : state 0 ^ 2 + state 1 ^ 2 ≠ 0) (henergy : cartesianKeplerEnergy state < 0) (f : PhaseSpace → ℝ) (coordinate : Fin 2) : phasePoissonPairing (fderiv ℝ f state) (actionDerivativeCovector (fderiv ℝ cartesianDelaunayActions state) coordinate) = actionPoissonVector f state coordinate

Pairing a phase differential with a row of the physical action derivative recovers the corresponding component of the action Poisson vector.

theorem LeanPool.PoincareThreeBody.poissonBracket_eq_neg_dot_actionPoissonVector_of_fderiv_factors {state : PhaseSpace} (hposition : state 0 ^ 2 + state 1 ^ 2 ≠ 0) (henergy : cartesianKeplerEnergy state < 0) {f h : PhaseSpace → ℝ} {differential : ActionSpace} (hfactor : fderiv ℝ f state = actionCovector differential ∘SL fderiv ℝ cartesianDelaunayActions state) : poissonBracket f h state = -dot differential (actionPoissonVector h state)

Once an observable differential factors through the action map, its bracket with any second observable is contraction against the negative action Poisson vector of that observable.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.fderiv_mass_zero_factors_through_actions_section {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) {firstAction eccentricity meanAnomaly periapsisAngle : ℝ} (hfirstAction : 0 < firstAction) (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : firstAction ^ 2 * (1 + eccentricity) < 1) : have state := liftedDelaunayPhasePoint firstAction eccentricity meanAnomaly periapsisAngle; have action := ![firstAction, angularActionFromEccentricity firstAction eccentricity]; have movingSection := delaunayActionSectionAtAnomaly (eccentricAnomaly eccentricity meanAnomaly) periapsisAngle; fderiv ℝ (F 0) state = (fderiv ℝ (F 0) state ∘SL fderiv ℝ movingSection action) ∘SL fderiv ℝ cartesianDelaunayActions state

The differential of the leading integral factors through the physical action derivative at every interior noncircular lifted elliptic point. This form records the factor using an explicit moving action section through the point.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.fderiv_mass_zero_comp_section_eq_leadingActionCoefficient {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) {firstAction eccentricity meanAnomaly periapsisAngle : ℝ} (hfirstAction : 0 < firstAction) (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : firstAction ^ 2 * (1 + eccentricity) < 1) : have state := liftedDelaunayPhasePoint firstAction eccentricity meanAnomaly periapsisAngle; have action := ![firstAction, angularActionFromEccentricity firstAction eccentricity]; have movingSection := delaunayActionSectionAtAnomaly (eccentricAnomaly eccentricity meanAnomaly) periapsisAngle; fderiv ℝ (F 0) state ∘SL fderiv ℝ movingSection action = fderiv ℝ (leadingActionCoefficient F) action

Differentiating the moving action section through a lifted point gives exactly the differential of the action-space leading coefficient.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.fderiv_mass_zero_eq_actionDifferential_comp_actions {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) {firstAction eccentricity meanAnomaly periapsisAngle : ℝ} (hfirstAction : 0 < firstAction) (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : firstAction ^ 2 * (1 + eccentricity) < 1) : have state := liftedDelaunayPhasePoint firstAction eccentricity meanAnomaly periapsisAngle; have action := ![firstAction, angularActionFromEccentricity firstAction eccentricity]; fderiv ℝ (F 0) state = actionCovector (leadingActionDifferential F action) ∘SL fderiv ℝ cartesianDelaunayActions state

Pointwise differential form of angle-independence: the leading phase differential is the pullback of the represented action differential.