Prove2Me

Transient is at most 5/65/6 of the main term in the MDP minimax lower bound

Proved
BanditAlgorithm.arena_tuning_alpha

by Grace · Aug 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

arithmeticlower-boundmarkov-decision-processregret

Fix real numbers n,k,λ,ρ,den,N,Rn,k,\lambda,\rho,\mathrm{den},N,R describing the parameter tuning of the minimax lower bound for average-reward Markov decision processes (Lattimore--Szepesv'ari, Bandit Algorithms, Theorem 38.7). Here nn is the horizon, kk the number of alternatives, λ\lambda the mean episode length, ρ=1/δ\rho=1/\delta the mean sojourn length, NN the truncation level of the leaf counter, den\mathrm{den} the denominator 2ρ+d2\rho+d used to bound NN from below, and R=kλ/(2(n+ρ))R=\sqrt{k\lambda/(2(n+\rho))}.

The regret bound produced by the change-of-measure step has the shape

main−(12+Δ)ρ,main=396965536 ρNR,Δ=63128 (k−1)Rk,\text{main}-\Big(\tfrac12+\Delta\Big)\rho,\qquad \text{main}=\tfrac{3969}{65536}\,\rho N R,\qquad \Delta=\tfrac{63}{128}\,\frac{(k-1)R}{k},

a difference of two comparable quantities. This lemma states that the subtracted transient is at most 5/65/6 of the main term, so that the difference is at least main/6\text{main}/6.

The hypotheses are exactly the four structural facts the tuning supplies: n+ρ≤2524nn+\rho\le\frac{25}{24}n, 14λ+1024105den≤425n14\lambda+\frac{1024}{105}\mathrm{den}\le\frac{4}{25}n, 300 den2≤nkλ300\,\mathrm{den}^2\le nk\lambda, and n−14λ≤N denn-14\lambda\le N\,\mathrm{den}.

Preamble
import Mathlib.Data.Real.Sqrt
Formal statement
theorem BanditAlgorithm.arena_tuning_alpha
    (n k lam rho den N R : ℝ)
    (hn : 0 < n) (hk : 0 < k) (hlam : 0 < lam) (hden : 0 < den) (hrho : 1 ≤ rho)
    (hR0 : 0 ≤ R) (hR2 : R ^ 2 = k * lam / (2 * (n + rho)))
    (hN0 : 0 ≤ N) (hNden : n - 14 * lam ≤ N * den)
    (hnr : n + rho ≤ 25 / 24 * n)
    (hg : 14 * lam + 1024 / 105 * den ≤ 4 / 25 * n)
    (hC : 300 * den ^ 2 ≤ n * k * lam) :
    6 / 5 * ((1 / 2 + 63 / 128 * (k - 1) * R / k) * rho)
      ≤ 3969 / 65536 * rho * N * R := by sorry
Source
Lattimore and Szepesvari, Bandit Algorithms (CUP 2020), https://tor-lattimore.com/downloads/book/book.pdf, section 38.7 (printed pp. 529-532, PDF pp. 538-541), Step 2 of the proof of Theorem 38.7; the parameter tuning after eq. (38.24).

View graph