Propagating resonant obstructions by density

Positive rational Kepler resonances remain dense after restricting to ellipses inside the unit primary orbit. Consequently, nonconstancy of the disturbing average at every such resonance forces the leading integral differential to be dependent on the Kepler frequency everywhere in the corresponding fixed-eccentricity action interval.

def LeanPool.PoincareThreeBody.resonantInteriorPositiveActions (eccentricity : ℝ) : Set (InteriorPositiveAction eccentricity)

Interior first actions carrying a positive rational Kepler resonance.

Equations

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

theorem LeanPool.PoincareThreeBody.resonantInteriorPositiveActions_dense (eccentricity : ℝ) : Dense (resonantInteriorPositiveActions eccentricity)

Rational Kepler resonances are dense even after imposing the open apoapsis constraint.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.wedge_leadingActionDifferentialAtEccentricity_eq_zero {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) {eccentricity : ℝ} (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) (hnonconstant : ∀ {p q : ℕ}, 0 < p → 0 < q → resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1 → ∃ (orientation : ℝ), deriv (resonantDisturbingAverage p q eccentricity) orientation ≠ 0) (action : InteriorPositiveAction eccentricity) : wedge (delaunayFrequency ↑↑action) (leadingActionDifferentialAtEccentricity F eccentricity action) = 0

Conditional classical density step: nonconstant resonant averages force the frequency and leading differential to have zero wedge at every interior action of fixed eccentricity.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.leadingActionDifferentialAtEccentricity_obstruction {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) {eccentricity : ℝ} (heccentricity : 0 < eccentricity) (heccentricityOne : eccentricity < 1) (hnonconstant : ∀ {p q : ℕ}, 0 < p → 0 < q → resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1 → ∃ (orientation : ℝ), deriv (resonantDisturbingAverage p q eccentricity) orientation ≠ 0) (action : InteriorPositiveAction eccentricity) : ¬LinearIndependent ℝ ![delaunayFrequency ↑↑action, leadingActionDifferentialAtEccentricity F eccentricity action]

Under the same resonant nonconstancy input, the two differentials are dependent at every interior fixed-eccentricity action.