Constancy of the leading coefficient on Kepler energy leaves

The coordinate change (L,E) ↦ (L,-1/(2L²)-E) straightens the level sets of the rotating Kepler Hamiltonian. The dense-resonance obstruction says exactly that the derivative of the leading coefficient in the L direction at fixed E vanishes. The mean-value inequality then makes that coefficient constant on every connected energy-leaf segment contained in the interior elliptic region.

noncomputable def LeanPool.PoincareThreeBody.energyLeafAction (energy firstAction : ℝ) : ActionSpace

The Delaunay action on the Kepler energy leaf E with first action L.

Equations

• LeanPool.PoincareThreeBody.energyLeafAction energy firstAction = ![firstAction, -1 / (2 * firstAction ^ 2) - energy]

@[simp]

theorem LeanPool.PoincareThreeBody.energyLeafAction_zero (energy firstAction : ℝ) : energyLeafAction energy firstAction 0 = firstAction

@[simp]

theorem LeanPool.PoincareThreeBody.energyLeafAction_one (energy firstAction : ℝ) : energyLeafAction energy firstAction 1 = -1 / (2 * firstAction ^ 2) - energy

theorem LeanPool.PoincareThreeBody.delaunayHamiltonian_energyLeafAction {energy firstAction : ℝ} (_hfirstAction : firstAction ≠ 0) : delaunayHamiltonian (energyLeafAction energy firstAction) = energy

The straightened leaf really has the prescribed Delaunay energy.

theorem LeanPool.PoincareThreeBody.hasDerivAt_energyLeafAction (energy : ℝ) {firstAction : ℝ} (hfirstAction : firstAction ≠ 0) : HasDerivAt (energyLeafAction energy) ![1, 1 / firstAction ^ 3] firstAction

Tangent vector to a straightened Kepler energy leaf.

theorem LeanPool.PoincareThreeBody.dot_energyLeafTangent_eq_zero_of_wedge_frequency_eq_zero {firstAction : ℝ} {differential : ActionSpace} (hwedge : wedge (delaunayFrequency firstAction) differential = 0) : dot differential ![1, 1 / firstAction ^ 3] = 0

The wedge obstruction is precisely vanishing of the candidate differential along a fixed-energy tangent.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.hasDerivAt_leadingActionCoefficient_energyLeaf_zero {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) {energy firstAction : ℝ} (haction : energyLeafAction energy firstAction ∈ ProgradeEllipticActions) (hapoapsis : firstAction ^ 2 * (1 + eccentricityFromActions (energyLeafAction energy firstAction)) < 1) : HasDerivAt (fun (candidate : ℝ) => leadingActionCoefficient F (energyLeafAction energy candidate)) 0 firstAction

Under density of the classical Poincaré set, the leading coefficient has zero derivative in the L direction while its Kepler energy is held fixed.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.leadingActionCoefficient_eq_of_same_energyLeaf {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) {energy firstAction₁ firstAction₂ : ℝ} (haction : ∀ firstAction ∈ Set.uIcc firstAction₁ firstAction₂, energyLeafAction energy firstAction ∈ ProgradeEllipticActions) (hapoapsis : ∀ firstAction ∈ Set.uIcc firstAction₁ firstAction₂, firstAction ^ 2 * (1 + eccentricityFromActions (energyLeafAction energy firstAction)) < 1) : leadingActionCoefficient F (energyLeafAction energy firstAction₁) = leadingActionCoefficient F (energyLeafAction energy firstAction₂)

The leading coefficient is constant between two actions on the same Kepler energy leaf, provided the whole intervening leaf segment stays in the interior collision-free elliptic chart.

theorem LeanPool.PoincareThreeBody.energyLeafAction_delaunayHamiltonian (action : ActionSpace) : energyLeafAction (delaunayHamiltonian action) (action 0) = action

The explicit inverse relation between the original action coordinates and the straightened (L,E) coordinates.

noncomputable def LeanPool.PoincareThreeBody.leadingEnergyCoefficient (F : ℝ → PhaseSpace → ℝ) (referenceFirstAction energy : ℝ) : ℝ

A one-variable representative of the leading coefficient, obtained by meeting each nearby energy leaf at one fixed reference value of the first action.

Equations

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

theorem LeanPool.PoincareThreeBody.analyticAt_energyLeafAction (referenceFirstAction energy : ℝ) : AnalyticAt ℝ (fun (candidateEnergy : ℝ) => energyLeafAction candidateEnergy referenceFirstAction) energy

The explicit fixed-L energy section is analytic.

theorem LeanPool.PoincareThreeBody.IsJointlyAnalytic.analyticAt_leadingEnergyCoefficient {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) {referenceFirstAction energy : ℝ} (haction : energyLeafAction energy referenceFirstAction ∈ ProgradeEllipticActions) (hapoapsis : referenceFirstAction ^ 2 * (1 + eccentricityFromActions (energyLeafAction energy referenceFirstAction)) < 1) : AnalyticAt ℝ (leadingEnergyCoefficient F referenceFirstAction) energy

The energy representative is analytic wherever its reference section remains in the interior elliptic chart.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.leadingActionCoefficient_eq_leadingEnergyCoefficient {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) {action : ActionSpace} {referenceFirstAction : ℝ} (haction : ∀ firstAction ∈ Set.uIcc (action 0) referenceFirstAction, energyLeafAction (delaunayHamiltonian action) firstAction ∈ ProgradeEllipticActions) (hapoapsis : ∀ firstAction ∈ Set.uIcc (action 0) referenceFirstAction, firstAction ^ 2 * (1 + eccentricityFromActions (energyLeafAction (delaunayHamiltonian action) firstAction)) < 1) : leadingActionCoefficient F action = leadingEnergyCoefficient F referenceFirstAction (delaunayHamiltonian action)

On any connected energy-leaf segment inside the chart, the leading action coefficient is the analytic one-variable energy representative based at the other endpoint. This is the local functional-dependence statement used in Poincaré's coefficient normalization.