JAO Theorem 5, small-diameter regime $D < 12$ (footnote 11)

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

For any learning 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 $C\sqrt{DSAT}$ for a universal constant $C > 0$.

This is Theorem 5 of Jaksch, Ortner and Auer (2010), the matching lower bound for their $\tilde{O}(D S \sqrt{AT})$ UCRL2 upper bound, stated with the hypotheses of the original paper. Those hypotheses are not cosmetic: the construction places $k = \lfloor S/2 \rfloor$ copies of a two-state gadget with $A' = \lfloor (A-1)/2 \rfloor$ actions each, connected by $A'+1$ further actions per state inducing an $A'$-ary tree on the reward-$0$ states, so it simply does not exist unless $A$ is large enough to supply $2A'+1$ actions, and the final constant needs $kA' \ge 20$.

This is the small-diameter regime $D < 12$, i.e. $\delta = 4/D > 1/3$, which the main construction excludes. JAO handle it in footnote 11 (p. 1582) with a different instance. In this regime the hypothesis $D \ge 20\log_A S$ forces $A > 2S$ (a diameter below $12$ leaves room for very few states relative to actions), so there are plenty of spare actions: one uses $S-1$ of them to connect all states directly, producing an MDP of diameter $1$, and sets up an independent multi-armed bandit in each state with the remaining $A - S + 1$ actions, exactly one state carrying a better action. The bandit lower bound of Auer et al. (2002b) then gives regret $\Omega(\sqrt{SAT})$, which suffices because $D$ is bounded by $12$ in this regime, so $\sqrt{SAT}$ and $\sqrt{DSAT}$ agree up to a constant.

On the constant. The paper displays Theorem 5 with the explicit constant $0.015$ on $\sqrt{DSAT}$, but its own proof in Section 6 does not deliver that. The final line of Section 6 (p. 1586) reads

$$\mathbb{E}^*\!\left[\Delta(M', \mathfrak{A}, s, T)\right] > 0.015\sqrt{D'kA'T},$$

in terms of the gadget parameters $D' = D/4$, $k = \lfloor S/2 \rfloor$ and $A' = \lfloor (A-1)/2 \rfloor$, and the substitution $D'kA' \to DSA$ is never justified. It is in fact false: the composite MDP must fit in $S$ states and $A$ actions, which forces $2k \le S$ and $2A' + 1 \le A$, hence

$$D'kA' \;=\; \tfrac{D}{4}\,k\,A' \;\le\; \tfrac{DSA}{16},$$

so $0.015\sqrt{D'kA'T} \le 0.0039\sqrt{DSAT}$ under any rounding convention. Minimising $\tfrac14\cdot\tfrac{\lfloor S/2\rfloor}{S}\cdot\tfrac{\lfloor (A-1)/2\rfloor}{A}$ over $S, A \ge 10$ gives $1/22$ at $(S,A) = (11,10)$, so the largest constant the argument can yield on $\sqrt{DSAT}$ is $0.015/\sqrt{22} = 0.00320$.

The remaining arithmetic of Section 6 is correct: recomputing the bracket in the penultimate display at $kA' = 20$ (the minimum permitted by $S, A \ge 10$) gives $0.016660 > 0.015$, exactly as claimed. The error is the single unstated substitution at the end.

A second, smaller loss is that Section 6 proves the bound for the initial state $s_\circ$, while Theorem 5 asserts it for every initial state; transferring costs a further additive $O(D')$, of which the proof has already spent one copy ($D'/2$) of its bracket. For these reasons this node states a universal but unspecified constant $C > 0$ — the form in which the result is universally cited, and the form used by Lattimore and Szepesvari (Bandit Algorithms, Theorem 38.7). A witness $C = 0.0008$ is comfortably supported by Section 6.

Why this node was retired

The posted statement is

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

The source diameter parameter is natural/at least one, but the formal parameter is real and can be 1/2 although every MDP with two states has diameter≥1.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

Require D∈ℕ with D≥1, or add the explicit hypothesis 1≤D while retaining the source size and horizon conditions.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.

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

open MeasureTheory ProbabilityTheory

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