A local Delaunay chart at the rational elliptic anchor

We combine the two Delaunay actions, eccentric anomaly, and apsidal orientation into a four-dimensional chart. Its derivative at the rational anchor is nonsingular, so its image contains a phase-space neighborhood of the anchor.

@[reducible, inline]

abbrev LeanPool.PoincareThreeBody.DelaunayAnchorParameters : Type

Action and angle variables for the local four-dimensional chart.

Equations

• LeanPool.PoincareThreeBody.DelaunayAnchorParameters = (LeanPool.PoincareThreeBody.ActionSpace × ℝ × ℝ)

noncomputable def LeanPool.PoincareThreeBody.delaunayAnchorAction : ActionSpace

The action pair at the rational energy -2 anchor.

Equations

• LeanPool.PoincareThreeBody.delaunayAnchorAction = ![1 / √3, 1 / 2]

noncomputable def LeanPool.PoincareThreeBody.delaunayAnchorParameters : DelaunayAnchorParameters

Parameters corresponding to the rational phase point (0, 1/6, -3, 0).

Equations

• LeanPool.PoincareThreeBody.delaunayAnchorParameters = (LeanPool.PoincareThreeBody.delaunayAnchorAction, 0, Real.pi / 2)

noncomputable def LeanPool.PoincareThreeBody.delaunayAnchorChart (parameters : DelaunayAnchorParameters) : PhaseSpace

Full local Delaunay chart using eccentric anomaly as its first angle.

Equations

• LeanPool.PoincareThreeBody.delaunayAnchorChart parameters = LeanPool.PoincareThreeBody.delaunayActionSectionAtAnomaly parameters.2.1 parameters.2.2 parameters.1

theorem LeanPool.PoincareThreeBody.delaunayAnchorAction_prograde : delaunayAnchorAction ∈ ProgradeEllipticActions

theorem LeanPool.PoincareThreeBody.eccentricityFromActions_delaunayAnchorAction : eccentricityFromActions delaunayAnchorAction = 1 / 2

theorem LeanPool.PoincareThreeBody.delaunayAnchorChart_anchor : delaunayAnchorChart delaunayAnchorParameters = globalEnergySection (-2)

theorem LeanPool.PoincareThreeBody.analyticAt_delaunayAnchorChart : AnalyticAt ℝ delaunayAnchorChart delaunayAnchorParameters

The full action/anomaly/orientation chart is analytic at the rational anchor.

theorem LeanPool.PoincareThreeBody.cartesianDelaunayActions_delaunayAnchorChart_eventuallyEq : (fun (parameters : DelaunayAnchorParameters) => cartesianDelaunayActions (delaunayAnchorChart parameters)) =ᶠ[nhds delaunayAnchorParameters] fun (parameters : DelaunayAnchorParameters) => parameters.1

Near the anchor, applying the physical action map to the chart recovers exactly the two action parameters.

theorem LeanPool.PoincareThreeBody.fderiv_cartesianDelaunayActions_comp_delaunayAnchorChart : fderiv ℝ cartesianDelaunayActions (delaunayAnchorChart delaunayAnchorParameters) ∘SL fderiv ℝ delaunayAnchorChart delaunayAnchorParameters = ContinuousLinearMap.fst ℝ ActionSpace (ℝ × ℝ)

The action component of the anchor-chart derivative is the projection to the two action parameters. This is the first half of nonsingularity of Delaunay coordinates.

noncomputable def LeanPool.PoincareThreeBody.delaunayAnchorMeanAngleChart (angles : ℝ × ℝ) : PhaseSpace

The same anchor torus, parametrized by mean anomaly and apsidal orientation.

Equations

• LeanPool.PoincareThreeBody.delaunayAnchorMeanAngleChart angles = LeanPool.PoincareThreeBody.liftedDelaunayPhasePoint (1 / √3) (1 / 2) angles.1 angles.2

noncomputable def LeanPool.PoincareThreeBody.delaunayAnchorMeanAngles : ℝ × ℝ

The angle pair at the rational anchor.

Equations

• LeanPool.PoincareThreeBody.delaunayAnchorMeanAngles = (0, Real.pi / 2)

theorem LeanPool.PoincareThreeBody.analyticAt_delaunayAnchorMeanAngleChart : AnalyticAt ℝ delaunayAnchorMeanAngleChart delaunayAnchorMeanAngles

theorem LeanPool.PoincareThreeBody.delaunayAnchorMeanAngleChart_anchor : delaunayAnchorMeanAngleChart delaunayAnchorMeanAngles = globalEnergySection (-2)

theorem LeanPool.PoincareThreeBody.phaseHamiltonianVector_actionCovector_comp (actionDerivative : PhaseSpace →L[ℝ] ActionSpace) (vector : ActionSpace) : phaseHamiltonianVector (actionCovector vector ∘SL actionDerivative) = (actionHamiltonianTangentMap actionDerivative) vector

Hamiltonian vectors commute with pulling an action covector back along an action derivative.

theorem LeanPool.PoincareThreeBody.phaseHamiltonianVector_fderiv_hamiltonian_zero {state : PhaseSpace} (hposition : state 0 ^ 2 + state 1 ^ 2 ≠ 0) : phaseHamiltonianVector (fderiv ℝ (hamiltonian 0) state) = rotatingKeplerVectorField state

The Hamiltonian vector of the mass-zero Hamiltonian differential is its explicit rotating Kepler vector field.

theorem LeanPool.PoincareThreeBody.fderiv_delaunayAnchorMeanAngleChart_orientation : (fderiv ℝ delaunayAnchorMeanAngleChart delaunayAnchorMeanAngles) (0, 1) = angularActionVectorField (globalEnergySection (-2))

The second angle direction is the Hamiltonian vector of angular momentum.

theorem LeanPool.PoincareThreeBody.fderiv_delaunayAnchorMeanAngleChart_frequency : (fderiv ℝ delaunayAnchorMeanAngleChart delaunayAnchorMeanAngles) (1 / (1 / √3) ^ 3, -1) = rotatingKeplerVectorField (globalEnergySection (-2))

Advancing mean anomaly at Kepler frequency while decreasing the apsidal angle at unit speed is the mass-zero Hamiltonian vector field.

theorem LeanPool.PoincareThreeBody.actionHamiltonianTangentMap_anchor_orientation : (actionHamiltonianTangentMap (fderiv ℝ cartesianDelaunayActions (globalEnergySection (-2)))) ![0, 1] = angularActionVectorField (globalEnergySection (-2))

At the anchor, the second basis vector of the action Hamiltonian tangent map is the angular action flow.

theorem LeanPool.PoincareThreeBody.actionHamiltonianTangentMap_anchor_frequency : (actionHamiltonianTangentMap (fderiv ℝ cartesianDelaunayActions (globalEnergySection (-2)))) ![1 / (1 / √3) ^ 3, -1] = rotatingKeplerVectorField (globalEnergySection (-2))

At the anchor, the Kepler frequency vector maps to the rotating Kepler flow.

theorem LeanPool.PoincareThreeBody.actionHamiltonianTangentMap_anchor_injective : Function.Injective ⇑(actionHamiltonianTangentMap (fderiv ℝ cartesianDelaunayActions (globalEnergySection (-2))))

theorem LeanPool.PoincareThreeBody.injective_fderiv_delaunayAnchorMeanAngleChart : Function.Injective ⇑(fderiv ℝ delaunayAnchorMeanAngleChart delaunayAnchorMeanAngles)

The two mean-angle directions are linearly independent at the anchor.

noncomputable def LeanPool.PoincareThreeBody.delaunayAnchorMeanFromEccentricAngles (angles : ℝ × ℝ) : ℝ × ℝ

Convert eccentric anomaly to mean anomaly at the anchor eccentricity.

Equations

• LeanPool.PoincareThreeBody.delaunayAnchorMeanFromEccentricAngles angles = (LeanPool.PoincareThreeBody.eccentricMeanAnomaly (1 / 2) angles.1, angles.2)

noncomputable def LeanPool.PoincareThreeBody.delaunayAnchorEccentricAngleChart (angles : ℝ × ℝ) : PhaseSpace

The angle slice of the full anchor chart.

Equations

• LeanPool.PoincareThreeBody.delaunayAnchorEccentricAngleChart angles = LeanPool.PoincareThreeBody.delaunayAnchorChart (LeanPool.PoincareThreeBody.delaunayAnchorAction, angles)

theorem LeanPool.PoincareThreeBody.delaunayAnchorEccentricAngleChart_eq_mean : delaunayAnchorEccentricAngleChart = delaunayAnchorMeanAngleChart ∘ delaunayAnchorMeanFromEccentricAngles

theorem LeanPool.PoincareThreeBody.analyticAt_delaunayAnchorEccentricAngleChart : AnalyticAt ℝ delaunayAnchorEccentricAngleChart delaunayAnchorMeanAngles

theorem LeanPool.PoincareThreeBody.hasFDerivAt_delaunayAnchorMeanFromEccentricAngles : HasFDerivAt delaunayAnchorMeanFromEccentricAngles ((ContinuousLinearMap.toSpanSingleton ℝ (1 / 2) ∘SL ContinuousLinearMap.fst ℝ ℝ ℝ).prod (ContinuousLinearMap.snd ℝ ℝ ℝ)) delaunayAnchorMeanAngles

theorem LeanPool.PoincareThreeBody.injective_fderiv_delaunayAnchorMeanFromEccentricAngles : Function.Injective ⇑(fderiv ℝ delaunayAnchorMeanFromEccentricAngles delaunayAnchorMeanAngles)

theorem LeanPool.PoincareThreeBody.injective_fderiv_delaunayAnchorEccentricAngleChart : Function.Injective ⇑(fderiv ℝ delaunayAnchorEccentricAngleChart delaunayAnchorMeanAngles)

Replacing eccentric anomaly by mean anomaly preserves nonsingularity of the two angle directions.

theorem LeanPool.PoincareThreeBody.fderiv_delaunayAnchorChart_comp_angleEmbedding : fderiv ℝ delaunayAnchorChart delaunayAnchorParameters ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (ℝ × ℝ)) = fderiv ℝ delaunayAnchorEccentricAngleChart delaunayAnchorMeanAngles

Restricting the full chart derivative to pure angle directions gives the derivative of the two-angle slice.

theorem LeanPool.PoincareThreeBody.injective_fderiv_delaunayAnchorChart : Function.Injective ⇑(fderiv ℝ delaunayAnchorChart delaunayAnchorParameters)

The full four-dimensional Delaunay chart has injective derivative at the rational anchor.

theorem LeanPool.PoincareThreeBody.surjective_fderiv_delaunayAnchorChart : Function.Surjective ⇑(fderiv ℝ delaunayAnchorChart delaunayAnchorParameters)

The full derivative is onto because its four-dimensional domain and codomain have equal finite dimension.

theorem LeanPool.PoincareThreeBody.map_delaunayAnchorChart_nhds : Filter.map delaunayAnchorChart (nhds delaunayAnchorParameters) = nhds (globalEnergySection (-2))

The analytic anchor chart maps the parameter-space neighborhood filter onto the phase-space neighborhood filter. Thus any identity proved for all nearby Delaunay parameters holds on an actual open phase-space neighborhood of the rational anchor.

theorem LeanPool.PoincareThreeBody.eventually_exists_delaunayAnchorChart_preimage {parameterNeighborhood : Set DelaunayAnchorParameters} (hneighborhood : parameterNeighborhood ∈ nhds delaunayAnchorParameters) : ∀ᶠ (state : PhaseSpace) in nhds (globalEnergySection (-2)), ∃ parameters ∈ parameterNeighborhood, delaunayAnchorChart parameters = state

Every sufficiently nearby phase point has a chart preimage in any prescribed parameter neighborhood of the anchor.