Finite certificates for nonconstant resonant averages

To prove that a Poincaré disturbing average is nonconstant, it is enough to compare its values at two phases. This file reduces that comparison to a finite trapezoidal sum plus a certified global bound on the second time derivative of the integrand difference.

noncomputable def LeanPool.PoincareThreeBody.resonantDisturbingDifference (p q : ℕ) (eccentricity phaseA phaseB time : ℝ) : ℝ

Difference between the disturbing functions at two orientation phases.

Equations

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

theorem LeanPool.PoincareThreeBody.contDiffOn_resonantDisturbingDifference {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity phaseA phaseB start finish : ℝ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) : ContDiffOn ℝ 2 (resonantDisturbingDifference p q eccentricity phaseA phaseB) (Set.uIcc start finish)

theorem LeanPool.PoincareThreeBody.resonantDisturbingAverage_ne_of_trapezoidal_certificate {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity phaseA phaseB errorBound : ℝ} {steps : ℕ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) (hsecondDerivative : ∀ (time : ℝ), |iteratedDerivWithin 2 (resonantDisturbingDifference p q eccentricity phaseA phaseB) (Set.uIcc 0 (resonantOrbitPeriod p)) time| ≤ errorBound) (hsteps : 0 < steps) (hcertificate : |resonantOrbitPeriod p| ^ 3 * errorBound / (12 * ↑steps ^ 2) < |trapezoidal_integral (resonantDisturbingDifference p q eccentricity phaseA phaseB) steps 0 (resonantOrbitPeriod p)|) : resonantDisturbingAverage p q eccentricity phaseA ≠ resonantDisturbingAverage p q eccentricity phaseB

A finite trapezoidal certificate for the phase difference proves that the exact Poincaré averages at those phases are distinct.

theorem LeanPool.PoincareThreeBody.exists_deriv_resonantDisturbingAverage_ne_zero_of_trapezoidal_certificate {p q : ℕ} (hp : 0 < p) (hq : 0 < q) {eccentricity phaseA phaseB errorBound : ℝ} {steps : ℕ} (heccentricity : 0 ≤ eccentricity) (heccentricityOne : eccentricity < 1) (hapoapsis : resonantFirstAction p q ^ 2 * (1 + eccentricity) < 1) (hsecondDerivative : ∀ (time : ℝ), |iteratedDerivWithin 2 (resonantDisturbingDifference p q eccentricity phaseA phaseB) (Set.uIcc 0 (resonantOrbitPeriod p)) time| ≤ errorBound) (hsteps : 0 < steps) (hcertificate : |resonantOrbitPeriod p| ^ 3 * errorBound / (12 * ↑steps ^ 2) < |trapezoidal_integral (resonantDisturbingDifference p q eccentricity phaseA phaseB) steps 0 (resonantOrbitPeriod p)|) : ∃ (orientation : ℝ), deriv (resonantDisturbingAverage p q eccentricity) orientation ≠ 0

The same finite certificate produces an orientation with a nonzero derivative of the exact Poincaré average.