Poisson brackets and the Cartesian Delaunay action map

This file rewrites the physical Poisson bracket with the zero-mass Hamiltonian as contraction of the Kepler frequency with the two Poisson brackets against the Cartesian actions (L,G).

def LeanPool.PoincareThreeBody.phasePoissonPairing (first second : PhaseSpace →L[ℝ] ℝ) : ℝ

Canonical symplectic pairing of two phase covectors.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.PoincareThreeBody.phaseHamiltonianVector (covector : PhaseSpace →L[ℝ] ℝ) : PhaseSpace

The canonical Hamiltonian vector associated with a phase covector.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.PoincareThreeBody.phasePoissonPairing_eq_apply_phaseHamiltonianVector (first second : PhaseSpace →L[ℝ] ℝ) : phasePoissonPairing first second = first (phaseHamiltonianVector second)

theorem LeanPool.PoincareThreeBody.phaseHamiltonianVector_add (first second : PhaseSpace →L[ℝ] ℝ) : phaseHamiltonianVector (first + second) = phaseHamiltonianVector first + phaseHamiltonianVector second

theorem LeanPool.PoincareThreeBody.phaseHamiltonianVector_smul (scalar : ℝ) (covector : PhaseSpace →L[ℝ] ℝ) : phaseHamiltonianVector (scalar • covector) = scalar • phaseHamiltonianVector covector

theorem LeanPool.PoincareThreeBody.phaseHamiltonianVector_injective : Function.Injective phaseHamiltonianVector

The canonical sharp map from covectors to Hamiltonian vectors is injective.

theorem LeanPool.PoincareThreeBody.phasePoissonPairing_skew (first second : PhaseSpace →L[ℝ] ℝ) : phasePoissonPairing first second = -phasePoissonPairing second first

theorem LeanPool.PoincareThreeBody.phasePoissonPairing_self (covector : PhaseSpace →L[ℝ] ℝ) : phasePoissonPairing covector covector = 0

def LeanPool.PoincareThreeBody.actionDerivativeCovector (actionDerivative : PhaseSpace →L[ℝ] ActionSpace) (coordinate : Fin 2) : PhaseSpace →L[ℝ] ℝ

A coordinate row of a phase-to-action linear map.

Equations

• LeanPool.PoincareThreeBody.actionDerivativeCovector actionDerivative coordinate = ContinuousLinearMap.proj coordinate ∘SL actionDerivative

theorem LeanPool.PoincareThreeBody.actionDerivativeCovector_apply (actionDerivative : PhaseSpace →L[ℝ] ActionSpace) (coordinate : Fin 2) (direction : PhaseSpace) : (actionDerivativeCovector actionDerivative coordinate) direction = actionDerivative direction coordinate

def LeanPool.PoincareThreeBody.actionHamiltonianTangentMap (actionDerivative : PhaseSpace →L[ℝ] ActionSpace) : ActionSpace →ₗ[ℝ] PhaseSpace

The two Hamiltonian tangent vectors associated with the rows of an action derivative.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.PoincareThreeBody.actionHamiltonianTangentMap_apply (actionDerivative : PhaseSpace →L[ℝ] ActionSpace) (vector : ActionSpace) : (actionHamiltonianTangentMap actionDerivative) vector = vector 0 • phaseHamiltonianVector (actionDerivativeCovector actionDerivative 0) + vector 1 • phaseHamiltonianVector (actionDerivativeCovector actionDerivative 1)

theorem LeanPool.PoincareThreeBody.actionHamiltonianTangentMap_injective_of_rightInverse {actionDerivative : PhaseSpace →L[ℝ] ActionSpace} {actionSectionDerivative : ActionSpace →L[ℝ] PhaseSpace} (hright : actionDerivative ∘SL actionSectionDerivative = ContinuousLinearMap.id ℝ ActionSpace) : Function.Injective ⇑(actionHamiltonianTangentMap actionDerivative)

A right inverse makes the two Hamiltonian row vectors linearly independent.

theorem LeanPool.PoincareThreeBody.range_actionHamiltonianTangentMap_eq_ker {actionDerivative : PhaseSpace →L[ℝ] ActionSpace} {actionSectionDerivative : ActionSpace →L[ℝ] PhaseSpace} (hright : actionDerivative ∘SL actionSectionDerivative = ContinuousLinearMap.id ℝ ActionSpace) (hisotropic : phasePoissonPairing (actionDerivativeCovector actionDerivative 0) (actionDerivativeCovector actionDerivative 1) = 0) : (actionHamiltonianTangentMap actionDerivative).range = (↑actionDerivative).ker

In four-dimensional canonical phase space, an isotropic surjective two-action derivative has kernel exactly the span of its two Hamiltonian row vectors.

theorem LeanPool.PoincareThreeBody.phaseCovector_eq_comp_actionDerivative {actionDerivative : PhaseSpace →L[ℝ] ActionSpace} {actionSectionDerivative : ActionSpace →L[ℝ] PhaseSpace} (hright : actionDerivative ∘SL actionSectionDerivative = ContinuousLinearMap.id ℝ ActionSpace) (hisotropic : phasePoissonPairing (actionDerivativeCovector actionDerivative 0) (actionDerivativeCovector actionDerivative 1) = 0) (phaseCovector : PhaseSpace →L[ℝ] ℝ) (hzero : ∀ (coordinate : Fin 2), phasePoissonPairing phaseCovector (actionDerivativeCovector actionDerivative coordinate) = 0) : phaseCovector = (phaseCovector ∘SL actionSectionDerivative) ∘SL actionDerivative

A phase covector which Poisson-annihilates both rows of an isotropic action derivative factors through that derivative. The factor is computed by any linear right inverse.

theorem LeanPool.PoincareThreeBody.poissonBracket_eq_phasePoissonPairing (f g : PhaseSpace → ℝ) (state : PhaseSpace) : poissonBracket f g state = phasePoissonPairing (fderiv ℝ f state) (fderiv ℝ g state)

noncomputable def LeanPool.PoincareThreeBody.actionPoissonVector (f : PhaseSpace → ℝ) (state : PhaseSpace) : ActionSpace

The two Poisson brackets of an observable with the reconstructed actions.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.PoincareThreeBody.angularActionVectorField (state : PhaseSpace) : PhaseSpace

Hamiltonian vector field of the angular action.

Equations

• LeanPool.PoincareThreeBody.angularActionVectorField state = ![-state 1, state 0, -state 3, state 2]

theorem LeanPool.PoincareThreeBody.hasDerivAt_positionInRotatingFrame_neg (angle : ℝ) (vector : ActionSpace) : HasDerivAt (fun (argument : ℝ) => positionInRotatingFrame (-argument) vector) ![-positionInRotatingFrame (-angle) vector 1, positionInRotatingFrame (-angle) vector 0] angle

Varying the negated rotation angle generates the angular-action Hamiltonian flow.

theorem LeanPool.PoincareThreeBody.hasDerivAt_liftedDelaunayPhasePoint_periapsisAngle (firstAction eccentricity meanAnomaly periapsisAngle : ℝ) : HasDerivAt (fun (angle : ℝ) => liftedDelaunayPhasePoint firstAction eccentricity meanAnomaly angle) (angularActionVectorField (liftedDelaunayPhasePoint firstAction eccentricity meanAnomaly periapsisAngle)) periapsisAngle

Varying the lifted periapsis angle follows the angular-action Hamiltonian vector field.

theorem LeanPool.PoincareThreeBody.fderiv_cartesianAngularAction (state : PhaseSpace) : fderiv ℝ cartesianAngularAction state = state 0 • ContinuousLinearMap.proj 3 + state 3 • ContinuousLinearMap.proj 0 - (state 1 • ContinuousLinearMap.proj 2 + state 2 • ContinuousLinearMap.proj 1)

Differential of the Cartesian angular action.

theorem LeanPool.PoincareThreeBody.poissonBracket_cartesianAngularAction (f : PhaseSpace → ℝ) (state : PhaseSpace) : poissonBracket f cartesianAngularAction state = (fderiv ℝ f state) (angularActionVectorField state)

Bracketing with angular action differentiates along simultaneous rotation of position and momentum.

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

theorem LeanPool.PoincareThreeBody.phasePoissonPairing_actionCovector_comp_actions {state : PhaseSpace} (hposition : state 0 ^ 2 + state 1 ^ 2 ≠ 0) (henergy : cartesianKeplerEnergy state < 0) (phaseCovector : PhaseSpace →L[ℝ] ℝ) (vector : ActionSpace) : phasePoissonPairing phaseCovector (actionCovector vector ∘SL fderiv ℝ cartesianDelaunayActions state) = dot vector ![phasePoissonPairing phaseCovector (fderiv ℝ cartesianFirstAction state), phasePoissonPairing phaseCovector (fderiv ℝ cartesianAngularAction state)]

Pairing a phase covector with a pulled-back action covector contracts the represented action vector with the two action Poisson brackets.

theorem LeanPool.PoincareThreeBody.poissonBracket_hamiltonian_zero_eq_frequency_dot_actionPoisson {state : PhaseSpace} (hposition : state 0 ^ 2 + state 1 ^ 2 ≠ 0) (henergy : cartesianKeplerEnergy state < 0) (f : PhaseSpace → ℝ) : poissonBracket f (hamiltonian 0) state = dot (delaunayFrequency (cartesianDelaunayActions state 0)) (actionPoissonVector f state)

Bracketing any observable with the zero-mass Hamiltonian is contraction of the Delaunay frequency with its two action brackets.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.poissonBracket_cartesianAngularAction_mass_zero {δ : ℝ} {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) : poissonBracket (F 0) cartesianAngularAction (liftedDelaunayPhasePoint firstAction eccentricity meanAnomaly periapsisAngle) = 0

Angle-independence of the leading candidate implies that it Poisson-commutes with angular action at every interior lifted elliptic point.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.actionPoissonVector_mass_zero_eq_zero {δ : ℝ} {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) : actionPoissonVector (F 0) (liftedDelaunayPhasePoint firstAction eccentricity meanAnomaly periapsisAngle) = 0

The leading candidate Poisson-commutes with both reconstructed Delaunay actions throughout the interior elliptic chart.