Validated quadrature certificates

These lemmas turn a finite trapezoidal sum and a certified second-derivative bound into a theorem about the exact interval integral. They form the narrow interface through which a verified finite computation can discharge a nonvanishing obligation in the Poincaré argument.

theorem LeanPool.PoincareThreeBody.intervalIntegral_ne_zero_of_trapezoidal_certificate {f : ℝ → ℝ} {a b errorBound : ℝ} {steps : ℕ} (hsmooth : ContDiffOn ℝ 2 f (Set.uIcc a b)) (hsecondDerivative : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.uIcc a b) x| ≤ errorBound) (hsteps : 0 < steps) (hcertificate : |b - a| ^ 3 * errorBound / (12 * ↑steps ^ 2) < |trapezoidal_integral f steps a b|) : ∫ (x : ℝ) in a..b, f x ≠ 0

If the absolute trapezoidal approximation exceeds its certified error bound, the exact integral is nonzero.

theorem LeanPool.PoincareThreeBody.intervalIntegral_pos_of_trapezoidal_certificate {f : ℝ → ℝ} {a b errorBound : ℝ} {steps : ℕ} (hsmooth : ContDiffOn ℝ 2 f (Set.uIcc a b)) (hsecondDerivative : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.uIcc a b) x| ≤ errorBound) (hsteps : 0 < steps) (hcertificate : |b - a| ^ 3 * errorBound / (12 * ↑steps ^ 2) < trapezoidal_integral f steps a b) : 0 < ∫ (x : ℝ) in a..b, f x

A positive trapezoidal approximation larger than its certified error bound forces the exact integral to be positive.