JAO Theorem 5: MDP minimax regret lower bound $\mathbb{E}[\Delta] \ge 0.015\sqrt{DSAT}$

Open

BanditAlgorithm.mdp_regret_lower_bound_jao

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

banditslower-boundmarkov-decision-processreinforcement-learning

For any algorithm and any $S, A \ge 10$ , $D \ge 20\log_A S$ and $T \ge DSA$ , there is an MDP with $S$ states, $A$ actions and diameter at most $D$ on which, from every initial state, the expected regret after $T$ steps is at least $0.015\sqrt{DSAT}$ .

The proof splits on the size of the diameter. When $D \ge 12$ one has $\delta = 4/D \le 1/3$ and JAO's main construction applies: a two-state gadget replicated $\lceil S/2 \rceil$ times, the copies joined by an $A'$ -ary tree on the $s_\circ$ -states, which is then collapsed so that the analysis reduces to a bandit problem. When $D < 12$ the assumptions force $A > 2S$ and a different construction is used (JAO, footnote 11).

This is the original statement, with the explicit constant $0.015$ and the initial state universally quantified, as opposed to the Lattimore-Szepesvari restatement (Bandit Algorithms, Theorem 38.7) which asserts the bound for $S \ge 3$ , $A \ge 2$ with an unspecified universal constant. The hypothesis $S, A \ge 10$ is not cosmetic: JAO's construction uses a two-state gadget with $A' = \lceil (A-1)/2 \rceil$ actions together with $A'+1$ further actions per state to connect the copies, so at $A = 2$ the construction does not exist, and the final constant is obtained from $kA' \ge 20$ .

⚠ Not provable from the source as stated — see below. The constant $0.015$ on $\sqrt{DSAT}$ does not follow from JAO Section 6. The proof ends at $0.015\sqrt{D'kA'T}$ with $D' = D/4$ , $k = \lfloor S/2\rfloor$ , $A' = \lfloor (A-1)/2\rfloor$ ; since the composite MDP must fit in $S$ states and $A$ actions, $2k \le S$ and $2A'+1 \le A$ , hence $D'kA' \le DSA/16$ and the proven bound is at most $0.0039\sqrt{DSAT}$ . The exact supremum over $S, A \ge 10$ is $0.015/\sqrt{22} = 0.00320$ , attained at $(S,A) = (11,10)$ . The rest of Section 6 is correct: its bracket at $kA' = 20$ evaluates to $0.016660 > 0.015$ as claimed. The error is a single unstated substitution $D'kA' \to DSA$ in the final line.

This node is kept only as a record of the statement as published. Work instead on BanditAlgorithm.mdp_regret_lower_bound_jao_universal_constant, which carries the same hypotheses and the same $\sqrt{DSAT}$ scaling with a universal but unspecified constant. See mission comment afe04135 for the full computation.

Preamble

import Definitions.Def_FiniteMDPLearning
import Mathlib.Data.Real.Sqrt
import Mathlib.Analysis.SpecialFunctions.Log.Basic

open MeasureTheory ProbabilityTheory

Formal statement

theorem BanditAlgorithm.mdp_regret_lower_bound_jao :
    ∀ S A T : ℕ, ∀ D : ℝ, 10 ≤ S → 10 ≤ A →
      20 * (Real.log S / Real.log A) ≤ D → D * S * A ≤ (T : ℝ) →
        ∀ π : MDPPolicy S A,
          ∃ M : FiniteMDP S A,
            mdpDiameterENN M ≤ ENNReal.ofReal D ∧
            ∀ s : Fin S,
              0.015 * Real.sqrt (D * S * A * T) ≤
                ∫ h, mdpRegret M T h ∂(mdpMeasure M (mdpStateDirac s) π T) := by
  sorry

Source

Thomas Jaksch, Ronald Ortner, Peter Auer, "Near-optimal Regret Bounds for Reinforcement Learning", Journal of Machine Learning Research 11 (2010) 1563-1600, Theorem 5, p. 1567; proof in Section 6 "The Lower Bound", pp. 1582-1586. Formalised faithfully to the original: explicit constant 0.015, initial state universally quantified, hypotheses S,A >= 10 and D >= 20 log_A S.

View graph

JAO Theorem 5: MDP minimax regret lower bound E[Δ]≥0.015DSAT\mathbb{E}[\Delta] \ge 0.015\sqrt{DSAT}E[Δ]≥0.015DSAT​

JAO Theorem 5: MDP minimax regret lower bound $\mathbb{E}[\Delta] \ge 0.015\sqrt{DSAT}$