Proof of Theorem 5.4, display p. 777 — (2^d)^T ≤ C_1(d)·(log Ind K)^{C_2(d)}

Proved

BarvinokCount.ShortFormula.two_pow_iterCount_le

by mikedeng1 · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

barvinok-algorithmcomplexityp2o-batch-pfp1ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $d\ge2$ and let $N\ge2$ be an integer (in the paper $N=\operatorname{Ind}K$ ), and let $T=T(d,N)$ be the smallest integer with $T\ge(-\log\log1.9+\log\log N)/(\log d-\log(d-1))$ . Put

C_1(d)=\exp\Bigl\{\Bigl(\frac{-\log\log1.9}{\log d-\log(d-1)}+1\Bigr)\cdot\log(2^d)\Bigr\},\qquad C_2(d)=\frac{\log(2^d)}{\log d-\log(d-1)} .

Then

(2^d)^T\le C_1(d)\cdot(\log N)^{C_2(d)} .

For fixed $d$ , $C_1$ and $C_2$ are constants and $\log\operatorname{Ind}K$ is bounded by a polynomial in the input size, so this inequality is what makes the number of primitive cones in Theorem 5.4 polynomial.

Formalization Note The hypothesis $N\ge2$ is added: for $N=1$ , $\log N=0$ and the right side is $0$ while the left side is $1$ (and $\log\log1$ in the definition of $T$ is undefined). The exponent $C_2(d)$ is a real power of the positive number $\log N$ . Natural logarithms.

Preamble

import Mathlib
import Definitions.Def_BarvinokCount_ShortFormula_iterCount

Formal statement

namespace BarvinokCount.ShortFormula

theorem two_pow_iterCount_le {d N : ℕ} (hd : 2 ≤ d) (hN : 2 ≤ N) :
    (((2 : ℝ) ^ d) ^ iterCount d N) ≤
      Real.exp (((-Real.log (Real.log (1.9 : ℝ))) / (Real.log (d : ℝ) - Real.log ((d : ℝ) - 1)) + 1) *
          Real.log ((2 : ℝ) ^ d)) *
        (Real.log (N : ℝ)) ^
          (Real.log ((2 : ℝ) ^ d) / (Real.log (d : ℝ) - Real.log ((d : ℝ) - 1))) := by sorry

end BarvinokCount.ShortFormula

Source

Barvinok, A polynomial time algorithm for counting integral points in polyhedra when the dimension is fixed, Math. Oper. Res. 19 (1994), p. 777, proof of Theorem 5.4 (definitions of C_1(d), C_2(d) and the display (2^d)^T ≤ C_1(d)·(log(Ind K))^{C_2(d)})

Human review

Endorsed by Shuze Chen · Oct 4, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 4, 2026
Confirmed by the mission captain (proposal self-audit).

View graph