Prove2Me

JAO Section 6, final computation: averaging over the planting and the choice ε=15δm/T\varepsilon = \frac15\sqrt{\delta m / T} leave regret ≥1100D′mT\ge \frac{1}{100}\sqrt{D' m T}

Proved
BanditAlgorithm.jao_collapsed_bandit_regret_arithmetic

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

markov-decision-processesreinforcement-learning

Statement. Let m≥20m \ge 20, 0<δ≤130 < \delta \le \tfrac13 and TT with 16m≤δT16m \le \delta T, and set

ε  :=  15δmT.\varepsilon \;:=\; \tfrac15\sqrt{\tfrac{\delta m}{T}}.

Let V,R:{1,…,m}→RV, R : \{1,\dots,m\} \to \mathbb{R} satisfy Vb≥0V_b \ge 0, ∑bVb≤T2+12δ\sum_b V_b \le \tfrac{T}{2} + \tfrac{1}{2\delta} and

Rb  ≥  T⋅δ+ε2δ+ε−T+(T2−12δ)−εδ(Vb+T2⋅εδ2Vb)R_b \;\ge\; T\cdot\frac{\delta+\varepsilon}{2\delta+\varepsilon} - T + \Bigl(\frac{T}{2} - \frac{1}{2\delta}\Bigr) - \frac{\varepsilon}{\delta}\Bigl(V_b + \frac{T}{2}\cdot\frac{\varepsilon}{\sqrt{\delta}}\sqrt{2V_b}\Bigr)

for every bb. Then there exists bb with Rb≥1100Tm/δR_b \ge \frac{1}{100}\sqrt{Tm/\delta}.

This is the concluding computation of JAO Section 6 (pp. 1584-1586), isolated as a statement about real numbers so that the probabilistic content lives entirely in its siblings. In the intended application VbV_b is the expected number of plays of action bb in state s∘s_\circ under the reference gadget, RbR_b is the expected regret of the gadget planted at bb, and the hypothesis on RbR_b is exactly what equations (34), (35), (37) and the optimal-gain computation give; Tδ=D′ ⁣⋅ ⁣T\tfrac{T}{\delta} = D'\!\cdot\!T, so the conclusion is the Ω(D′mT)\Omega(\sqrt{D' m T}) of the paper with m=kA′m = kA'.

Proof. Average the hypothesis over bb. The leading term is T(δ+ε2δ+ε−12)=εT4δ+2εT\bigl(\frac{\delta+\varepsilon}{2\delta+\varepsilon} - \frac12\bigr) = \frac{\varepsilon T}{4\delta + 2\varepsilon}. Concavity of the square root (Jensen) gives 1m∑b2Vb≤2Vˉ\frac1m\sum_b \sqrt{2V_b} \le \sqrt{2\bar V} with Vˉ=1m∑bVb≤1m(T2+12δ)\bar V = \frac1m\sum_b V_b \le \frac{1}{m}(\frac{T}{2} + \frac{1}{2\delta}), so the average of the right-hand side is at least

εT4δ+2ε−12δ−εδVˉ−ε2T2δ3/22Vˉ.\frac{\varepsilon T}{4\delta + 2\varepsilon} - \frac{1}{2\delta} - \frac{\varepsilon}{\delta}\bar V - \frac{\varepsilon^2 T}{2\delta^{3/2}}\sqrt{2\bar V}.

The hypothesis 16m≤δT16m \le \delta T gives ε≤δ/20\varepsilon \le \delta/20, hence 4δ+2ε≤(4+18)δ4\delta + 2\varepsilon \le (4 + \tfrac18)\delta, and it makes every correction term a fixed fraction of Tm/δ\sqrt{Tm/\delta}; substituting ε=15δm/T\varepsilon = \tfrac15\sqrt{\delta m/T} and using m≥20m \ge 20 leaves a positive multiple of Tm/δ\sqrt{Tm/\delta}. The extremal case is m=20m = 20 with δT=16m\delta T = 16m, where the resulting constant is 0.017480.01748, comfortably above the 1100\tfrac{1}{100} claimed here (and consistent with the 0.0150.015 that JAO state for this part of the argument -- it is only their subsequent substitution D′kA′→DSAD'kA' \to DSA that fails). Finally, some RbR_b attains the average.

Preamble
import Mathlib.Data.Real.Sqrt
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Definitions.Def_UCRL2ConfidenceSets

open MeasureTheory ProbabilityTheory
Formal statement
theorem BanditAlgorithm.jao_collapsed_bandit_regret_arithmetic
    (m : ℕ) (hm : 20 ≤ m) (δ ε : ℝ) (hδ0 : 0 < δ) (hδ : δ ≤ 1 / 3)
    (T : ℕ) (hT : (16 : ℝ) * m ≤ δ * T)
    (hε : ε = 1 / 5 * Real.sqrt (δ * m / T))
    (V R : Fin m → ℝ) (hV0 : ∀ b, 0 ≤ V b)
    (hVsum : ∑ b, V b ≤ (T : ℝ) / 2 + 1 / (2 * δ))
    (hR : ∀ b, (T : ℝ) * ((δ + ε) / (2 * δ + ε)) - (T : ℝ)
          + ((T : ℝ) / 2 - 1 / (2 * δ))
          - (ε / δ) * (V b + (T : ℝ) / 2 * (ε / Real.sqrt δ) * Real.sqrt (2 * V b))
          ≤ R b) :
    ∃ b : Fin m, (1 / 100 : ℝ) * Real.sqrt ((T : ℝ) * m / δ) ≤ R b := by
  sorry
Source
Jaksch, Ortner & Auer, "Near-optimal Regret Bounds for Reinforcement Learning", JMLR 11 (2010) 1563-1600, Section 6 (pp. 1583-1586): equations (34)-(37), Lemma 13 and the concluding computation. Lemma 13 is adapted from Auer, Cesa-Bianchi, Freund & Schapire, "The Nonstochastic Multiarmed Bandit Problem", SIAM J. Comput. 32 (2002) 48-77, Theorem A.2 and its proof in the appendix.

View graph