The leading obstruction on collision-band resonances #
Fiberwise density in eccentricity propagates each collision-band resonant obstruction from the nondegenerate eccentricities to every admissible eccentricity at that resonance.
@[reducible, inline]
Interior first actions whose semimajor axis lies in the collision band.
Equations
- LeanPool.PoincareThreeBody.CollisionBandInteriorPositiveAction eccentricity = { action : LeanPool.PoincareThreeBody.InteriorPositiveAction eccentricity // 1 / 2 < ↑↑action ^ 2 }
Instances For
def
LeanPool.PoincareThreeBody.resonantCollisionBandActions
(eccentricity : ℝ)
:
Set (CollisionBandInteriorPositiveAction eccentricity)
Positive rational resonances restricted to the collision band.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LeanPool.PoincareThreeBody.resonantCollisionBandActions_dense
(eccentricity : ℝ)
:
Dense (resonantCollisionBandActions eccentricity)
theorem
LeanPool.PoincareThreeBody.IsFirstIntegralFamily.wedge_leadingActionDifferential_eq_zero_at_collisionBandResonance
{δ : ℝ}
{F : ℝ → PhaseSpace → ℝ}
(hδ : 0 < δ)
(hanalytic : IsJointlyAnalytic δ F)
(hfirstIntegral : IsFirstIntegralFamily δ F)
{p q : ℕ}
(hp : 0 < p)
(hq : 0 < q)
(haxisHalf : 1 / 2 < resonantSemimajorAxis p q)
(haxisOne : resonantSemimajorAxis p q < 1)
(eccentricity : AdmissibleResonantEccentricity p q)
:
wedge (delaunayFrequency (resonantFirstAction p q))
(leadingActionDifferential F (fixedEccentricityAction (↑eccentricity) (resonantFirstAction p q))) = 0
theorem
LeanPool.PoincareThreeBody.IsFirstIntegralFamily.wedge_leadingActionDifferential_eq_zero_on_collisionBand
{δ : ℝ}
{F : ℝ → PhaseSpace → ℝ}
(hδ : 0 < δ)
(hanalytic : IsJointlyAnalytic δ F)
(hfirstIntegral : IsFirstIntegralFamily δ F)
{eccentricity : ℝ}
(heccentricity : 0 < eccentricity)
(heccentricityOne : eccentricity < 1)
(action : CollisionBandInteriorPositiveAction eccentricity)
:
wedge (delaunayFrequency ↑↑↑action) (leadingActionDifferential F (fixedEccentricityAction eccentricity ↑↑↑action)) = 0
Collision-band resonances are dense, so the leading wedge vanishes throughout the band at every fixed admissible eccentricity.