Finite certificates for the classical Poincaré set

This file is the interface between verified numerical computation and the classical density argument. A certificate records one rational resonance, two orientations, a finite trapezoidal sum, and a rigorous second-derivative error bound. The analytic quadrature theorem turns that finite data into membership in the exact Poincaré set. Consequently, it is enough to prove that the set of actions carrying such certificates is dense.

structure LeanPool.PoincareThreeBody.ClassicalPoincareCertificate (action : InteriorProgradeEllipticAction) : Type

Finite, checkable data proving that one interior action belongs to the classical Poincaré set. The second-derivative field is intended to be discharged by interval arithmetic, while the last inequality is a finite trapezoidal computation.

• p : ℕ

  Numerator of the certified rational resonance.

• q : ℕ

  Denominator of the certified rational resonance.

• hp : 0 < self.p
• hq : 0 < self.q
• firstAction_eq : ↑action 0 = resonantFirstAction self.p self.q
• phaseA : ℝ

  First resonant orientation used in the certified comparison.

• phaseB : ℝ

  Second resonant orientation used in the certified comparison.

• errorBound : ℝ

  Certified uniform bound on the absolute second derivative.

• steps : ℕ

  Number of subintervals in the certified trapezoidal sum.

• secondDerivative (time : ℝ) : |iteratedDerivWithin 2 (resonantDisturbingDifference self.p self.q (eccentricityFromActions ↑action) self.phaseA self.phaseB) (Set.uIcc 0 (resonantOrbitPeriod self.p)) time| ≤ self.errorBound
• steps_pos : 0 < self.steps
• trapezoidal_nonzero : |resonantOrbitPeriod self.p| ^ 3 * self.errorBound / (12 * ↑self.steps ^ 2) < |trapezoidal_integral (resonantDisturbingDifference self.p self.q (eccentricityFromActions ↑action) self.phaseA self.phaseB) self.steps 0 (resonantOrbitPeriod self.p)|

theorem LeanPool.PoincareThreeBody.ClassicalPoincareCertificate.mem_classicalPoincareSet {action : InteriorProgradeEllipticAction} (certificate : ClassicalPoincareCertificate action) : action ∈ classicalPoincareSet

Any action carrying a finite certificate belongs to the exact classical Poincaré set.

def LeanPool.PoincareThreeBody.certifiedClassicalPoincareSet : Set InteriorProgradeEllipticAction

The subset of interior actions whose Poincaré-set membership has been reduced to finite validated numerical data.

Equations

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

theorem LeanPool.PoincareThreeBody.certifiedClassicalPoincareSet_subset_classicalPoincareSet : certifiedClassicalPoincareSet ⊆ classicalPoincareSet

theorem LeanPool.PoincareThreeBody.hasDenseClassicalPoincareSet_of_dense_certified (hdense : Dense certifiedClassicalPoincareSet) : HasDenseClassicalPoincareSet

Density of finitely certified actions is sufficient for the exact classical Poincaré-set hypothesis used by the nonintegrability argument.