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 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}$.

This is the small-diameter regime $D < 12$, which JAO treat separately in footnote 11 (p. 1582) because their main construction assumes $\delta = 4/D \le 1/3$. In this regime the hypotheses force $A > 2S$: from $D \ge 20\log_A S$ and $D < 12$ one gets $\log_A S < 3/5$, hence $S < A^{3/5}$ and so $A > S^{5/3} > 2S$ for $S \ge 10$.

With that many actions a different and simpler construction works. Use $S-1$ of the actions to connect all states to each other, producing an MDP of diameter $1$, and with the remaining $A - S + 1$ actions set up an independent bandit problem in each state, exactly one state having a better action, as in the lower bound of Auer et al. (2002b). This yields regret $\Omega(\sqrt{SAT})$, which suffices here precisely because $D$ is bounded by a constant, so $\sqrt{DSAT}$ and $\sqrt{SAT}$ agree up to a constant factor.

This case is absent from the Lattimore-Szepesvari account of the result.

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.

Why this node was retired

The posted statement is

theorem BanditAlgorithm.mdp_regret_lower_bound_jao_small_diameter :
    ∀ 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,
              0.015 * 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 Definitions.Def_FiniteMDPLearning
import Mathlib.Data.Real.Sqrt
import Mathlib.Analysis.SpecialFunctions.Log.Basic

open MeasureTheory ProbabilityTheory

theorem BanditAlgorithm.mdp_regret_lower_bound_jao_small_diameter :
    ∀ 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,
              0.015 * Real.sqrt (D * S * A * T) ≤
                ∫ h, mdpRegret M T h ∂(mdpMeasure M (mdpStateDirac s) π T) := by
  sorry