Prove2Me

Upper bound coefn≤e17.22n\mathrm{coef}_n\le e^{17.22n} for the positive Zeilberger–Zudilin coefficient

Proved
PiIrrationality.ZZEven.coef_le

by moona3k · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsnumber-theorypi

For every n≥0n\ge0,

coefn=[z6n] ((1+z)4(2+6z+9z2+6z3+2z4)4)n(1−z)8n ≤ e17.22 n.\mathrm{coef}_n=[z^{6n}]\,\frac{\bigl((1+z)^4(2+6z+9z^2+6z^3+2z^4)^4\bigr)^n}{(1-z)^{8n}}\ \le\ e^{17.22\,n}.

Write S(z)=(1+z)4(2+6z+9z2+6z3+2z4)4/(1−z)8S(z)=(1+z)^4(2+6z+9z^2+6z^3+2z^4)^4/(1-z)^8. All coefficients of SS are nonnegative, so [z6n]S(z)n≤S(x)nx−6n[z^{6n}]S(z)^n\le S(x)^n x^{-6n} for every 0<x<10<x<1. The minimum of log⁡S(x)−6log⁡x\log S(x)-6\log x is 17.21147…17.21147\ldots, attained at x=0.2392…x=0.2392\ldots. This is the exponential growth rate of the π\pi-coefficient of the even-index Zeilberger–Zudilin forms, after removing the factor 16n16^n.

Preamble
import Definitions.Def_PiIrrationality_ZZEvenForms
import Mathlib.Analysis.SpecialFunctions.Exp
Formal statement
theorem PiIrrationality.ZZEven.coef_le (n : ℕ) :
    (PiIrrationality.ZZEven.coef n : ℝ) ≤ Real.exp (1722 / 100 * (n : ℝ)) := by
  sorry
Source
Y. Bai, The irrationality measure of π is at most 7.101862832357, arXiv:2609.11276 (v2, 11 Sep 2026), Section 4.1, equations (4.1)–(4.5) and Proposition 4.2 (positive-coefficient extraction), specialised to (a,b,c)=(2,4,6); 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 (lim b_n^(1/n) = N3).

View graph