Explicit exponential decay of the even-index Zeilberger–Zudilin integrals
ProvedPiIrrationality.ZZEven.integral_boundcomplex-analysisnumber-theorypi
For every ,
where and , as in the definition file PiIrrationality_ZZEvenForms.
Zeilberger and Zudilin show for their integrals . At even index the true rate is . The rate is attained along a contour inside the disc that passes through the saddle points of . The statement is an explicit, slightly weaker form with a uniform constant.
Preamble
import Definitions.Def_PiIrrationality_ZZEvenForms import Mathlib.Analysis.SpecialFunctions.Exp
Formal statement
theorem PiIrrationality.ZZEven.integral_bound (n : ℕ) :
‖PiIrrationality.ZZEven.J n‖ ≤ 10 * Real.exp (-(7 * (n : ℝ))) := by
sorrySource
D. Zeilberger and W. Zudilin, The irrationality measure of π is at most 7.103205334137…, Moscow J. Combin. Number Theory 9 (2020), no. 4, 407–419, arXiv:1912.06345, Proposition 2 (limsup |I_n|^(1/n) = |N1| = 0.029458495928…); Y. Bai, The irrationality measure of π is at most 7.101862832357, arXiv:2609.11276 (v2, 11 Sep 2026), Section 4.2–4.3, Lemma 4.4 and Proposition 4.5.