The classical Poincaré set

The classical proof does not require nonvanishing at every resonant action. It requires the set of resonant actions carrying a nonzero disturbing coefficient to be a uniqueness set; density is a convenient sufficient formulation in the real-analytic setting developed here. This file defines that set intrinsically in the full two-dimensional action region and proves the resulting leading-coefficient obstruction.

def LeanPool.PoincareThreeBody.InteriorProgradeEllipticActions : Set ActionSpace

Prograde, noncircular elliptic actions whose entire ellipse stays inside the unit primary orbit.

Equations

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

@[reducible, inline]

abbrev LeanPool.PoincareThreeBody.InteriorProgradeEllipticAction : Type

An interior prograde elliptic action, as a topological subtype.

Equations

• LeanPool.PoincareThreeBody.InteriorProgradeEllipticAction = { action : LeanPool.PoincareThreeBody.ActionSpace // action ∈ LeanPool.PoincareThreeBody.InteriorProgradeEllipticActions }

def LeanPool.PoincareThreeBody.classicalPoincareSet : Set InteriorProgradeEllipticAction

The classical Poincaré set: rational Kepler resonances at which the disturbing average has a nonzero orientation derivative.

Equations

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

def LeanPool.PoincareThreeBody.HasDenseClassicalPoincareSet : Prop

The exact classical celestial-mechanics input used by the density argument.

Equations

• LeanPool.PoincareThreeBody.HasDenseClassicalPoincareSet = Dense LeanPool.PoincareThreeBody.classicalPoincareSet

def LeanPool.PoincareThreeBody.ClassicalDisturbingNondegeneracy : Prop

A stronger sufficient condition: every interior positive rational resonance has a nonconstant disturbing average as the relative apsidal orientation varies.

Equations

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

def LeanPool.PoincareThreeBody.admissibleResonantEccentricitySet (p q : ℕ) : Set ℝ

The open interval of admissible noncircular eccentricities for one fixed positive rational resonance.

Equations

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

@[reducible, inline]

abbrev LeanPool.PoincareThreeBody.AdmissibleResonantEccentricity (p q : ℕ) : Type

An admissible noncircular eccentricity for one fixed positive rational resonance.

Equations

• LeanPool.PoincareThreeBody.AdmissibleResonantEccentricity p q = { eccentricity : ℝ // eccentricity ∈ LeanPool.PoincareThreeBody.admissibleResonantEccentricitySet p q }

def LeanPool.PoincareThreeBody.nondegenerateResonantEccentricities (p q : ℕ) : Set (AdmissibleResonantEccentricity p q)

Eccentricities at a fixed resonance where the resonant disturbing average is nonconstant.

Equations

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

def LeanPool.PoincareThreeBody.HasDenseNondegenerateResonantEccentricities : Prop

A one-dimensional sufficient form of the classical perturbing-function calculation: at every rational resonance, nondegenerate eccentricities are dense in their admissible interval. Unlike ClassicalDisturbingNondegeneracy, this permits isolated zeros of individual Fourier coefficients.

Equations

• LeanPool.PoincareThreeBody.HasDenseNondegenerateResonantEccentricities = ∀ (p q : ℕ), 0 < p → 0 < q → Dense (LeanPool.PoincareThreeBody.nondegenerateResonantEccentricities p q)

def LeanPool.PoincareThreeBody.HasAnalyticSeparatingResonantAverages : Prop

A sharply localized analytic form of the classical disturbing-function input. For every positive rational resonance, two fixed orientations separate at one admissible eccentricity and their averaged-value difference is analytic throughout the admissible eccentricity interval.

The classical high-rank Fourier-coefficient calculation is precisely what supplies the two orientations and the nonzero witness.

Equations

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

def LeanPool.PoincareThreeBody.HasSeparatingResonantAverages : Prop

The remaining classical disturbing-function calculation, stripped of analyticity: at every positive rational resonance, two orientations give different averaged perturbations at one admissible eccentricity.

Equations

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

theorem LeanPool.PoincareThreeBody.hasAnalyticSeparatingResonantAverages_of_separation (hseparation : HasSeparatingResonantAverages) : HasAnalyticSeparatingResonantAverages

Compact parameter integration supplies the analytic clause automatically, so the classical Fourier calculation only has to provide a separating value at each resonance.

theorem LeanPool.PoincareThreeBody.isOpen_admissibleResonantEccentricitySet (p q : ℕ) : IsOpen (admissibleResonantEccentricitySet p q)

The admissible eccentricity domain is open.

theorem LeanPool.PoincareThreeBody.admissibleResonantEccentricitySet_nonempty_iff {p q : ℕ} (hp : 0 < p) (hq : 0 < q) : (admissibleResonantEccentricitySet p q).Nonempty ↔ resonantFirstAction p q ^ 2 < 1

A positive resonance admits an interior eccentric ellipse exactly when its semimajor axis is strictly inside the unit primary orbit.

theorem LeanPool.PoincareThreeBody.isConnected_admissibleResonantEccentricitySet {p q : ℕ} (hnonempty : (admissibleResonantEccentricitySet p q).Nonempty) : IsConnected (admissibleResonantEccentricitySet p q)

A nonempty admissible eccentricity domain is connected.

theorem LeanPool.PoincareThreeBody.continuous_interiorDelaunayFrequency : Continuous fun (action : InteriorProgradeEllipticAction) => delaunayFrequency (↑action 0)

The Kepler frequency varies continuously on the full interior action subtype.

theorem LeanPool.PoincareThreeBody.IsJointlyAnalytic.continuous_interiorLeadingActionDifferential {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) : Continuous fun (action : InteriorProgradeEllipticAction) => leadingActionDifferential F ↑action

The represented leading differential varies continuously on the full interior action subtype.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.wedge_leadingActionDifferential_eq_zero_of_mem_poincareSet {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) (action : InteriorProgradeEllipticAction) (haction : action ∈ classicalPoincareSet) : wedge (delaunayFrequency (↑action 0)) (leadingActionDifferential F ↑action) = 0

Every member of the classical Poincaré set forces the leading differential and Kepler frequency to have zero wedge.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.wedge_leadingActionDifferential_eq_zero_of_densePoincareSet {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) (hdense : HasDenseClassicalPoincareSet) (action : InteriorProgradeEllipticAction) : wedge (delaunayFrequency (↑action 0)) (leadingActionDifferential F ↑action) = 0

Density of the classical Poincaré set propagates its resonant obstruction to every interior prograde elliptic action.

theorem LeanPool.PoincareThreeBody.hasDenseClassicalPoincareSet_of_nondegeneracy (hnondegenerate : ClassicalDisturbingNondegeneracy) : HasDenseClassicalPoincareSet

Nonvanishing at every interior rational resonance implies density of the classical Poincaré set. The proof uses density of rational Kepler frequencies along the fixed-eccentricity curve through each action.

theorem LeanPool.PoincareThreeBody.hasDenseClassicalPoincareSet_of_dense_resonant_eccentricities (hdense : HasDenseNondegenerateResonantEccentricities) : HasDenseClassicalPoincareSet

Density in eccentricity on each rational resonance is enough to make the full classical Poincaré set dense in the two-dimensional interior action region.

theorem LeanPool.PoincareThreeBody.hasDenseNondegenerateResonantEccentricities_of_analytic_separation (hseparation : HasAnalyticSeparatingResonantAverages) : HasDenseNondegenerateResonantEccentricities

Analyticity plus one separating value at each resonance makes the nondegenerate eccentricities dense. Thus the classical calculation need only prove a nonidentity statement, not pointwise nonvanishing at every eccentricity.

theorem LeanPool.PoincareThreeBody.hasDenseClassicalPoincareSet_of_analytic_separation (hseparation : HasAnalyticSeparatingResonantAverages) : HasDenseClassicalPoincareSet

The analytic nonidentity statement at each rational resonance supplies the full dense classical Poincaré set.

theorem LeanPool.PoincareThreeBody.hasDenseNondegenerateResonantEccentricities_of_nondegeneracy (hnondegenerate : ClassicalDisturbingNondegeneracy) : HasDenseNondegenerateResonantEccentricities

The original pointwise nondegeneracy condition implies the more flexible fiberwise density condition.