BanditRLwiki case · tabular-finite-horizon-rl-ucbvi

Tabular finite-horizon RL: UCBVI and minimax leading rates

UCBVI-BF has the near-minimax variance-aware leading rate; BanditRLlib currently compiles the known-reward Hoeffding UCBVI-CH terminal.

← Finite-horizon tabular reinforcement learning

Audited comparison

tabular-finite-horizon-rl-ucbvi Tabular finite-horizon RL: UCBVI and minimax leading ratesUCBVI-BF has the near-minimax variance-aware leading rate; BanditRLlib currently compiles the known-reward Hoeffding UCBVI-CH terminal. Near minimaxPartial local route

Open stable case page →Faithful restatement

UCBVIUCBVI-CHUCBVI-BFtabular MDPBernsteinminimax RL

MDP: Unknown episodic tabular transitions with S states, A actions, horizon H
Episodes: K episodes and total steps T=H K
Regret: High-probability cumulative episode pseudo-regret
Target scale: square root(H S A T), plus lower-order terms

Comparison judgment

Near minimax

The literature and local status must be read separately: UCBVI-CH compiles locally, while the variance-aware source-leading theorem does not.

Known gap. UCBVI-BF gives a high-probability upper bound whose leading large-T polynomial rate matches the expected-regret minimax lower scale up to logs and lower-order terms; these probability modes are not identical theorem contracts. A later modified MVP route addresses the full parameter range. The compiled local theorem is Hoeffding, not Bernstein/minimax.

Local Lean boundary

Partial local route

The canonical recurrent known-reward Hoeffding UCBVI-CH 20/250 high-probability terminal and failure-aware expected consumer compile. Bernstein/Freedman, stochastic rewards, and a minimax lower pair do not.

Upper bound

UCBVI high-probability regret upper bounds

Minimax Regret Bounds for Reinforcement Learning

Mohammad Azar, Ian Osband, and Rémi Munos · 2017 · Theorems 1–2

Upper bound guarantee. Formula renderer unavailable; readable fallback: The Hoeffding version has the explicit 20 and 250 bound; the Bernstein-Freedman version improves the leading horizon dependence to the near-minimax scale.\[R_K^{\mathrm{CH}}\le 20H^{3/2}L\sqrt{SAK}+250H^2S^2AL^2,\qquad R_K^{\mathrm{BF}}=\widetilde O\!\left(\sqrt{HSAT}\right).\]

Use the paper's confidence logarithm L, reward model, and horizon conditions.

Open primary source

Upper bound

Modified MVP full-range minimax regret bound

Settling the sample complexity of online reinforcement learning

Zihan Zhang and collaborators · 2024 · Modified MVP full-range result

Upper bound guarantee. Formula renderer unavailable; readable fallback: A modified MVP analysis supplies the closest full-range upper guarantee across all episode counts.\[R_K=\widetilde O\!\left(\min\{\sqrt{SAH^3K},HK\}\right).\]

This is a separate algorithmic route and must not be relabeled as UCBVI.

Open primary source

Lower bound

Tabular episodic minimax lower-bound comparison

Minimax Regret Bounds for Reinforcement Learning

Mohammad Azar, Ian Osband, and Rémi Munos · 2017 · Minimax lower-bound comparison

Lower bound guarantee. Formula renderer unavailable; readable fallback: Some tabular finite-horizon MDP forces expected regret at the square-root H S A T scale in the source regime.\[\inf_\pi\sup_M\mathbb E R_T(\pi,M)=\Omega\!\left(\sqrt{HSAT}\right).\]

Use the source's state, action, horizon, and total-time range.

Open primary source

Local Lean evidence

Exact declarations

Not yet proved here

Missing steps

Build the conditional variance and Freedman/Bernstein bonus layer.
Compile the law-of-total-variance and recurrent value/Q recursion needed by UCBVI-BF.
Treat stochastic rewards, realized sampled-return regret, and the MVP full-range route as distinct extensions.

formalization frontier

Can the recurrent generated UCBVI source be upgraded from Hoeffding bonuses to the exact Bernstein/Freedman source theorem?

The source-shaped UCBVI-CH endpoint compiles with the exact 20/250 surface; the minimax-leading UCBVI-BF route is absent.

Conditional variance
Freedman concentration
variance bonus summation
source-leading terminal
Named formalization leaf: UCBVI-BF-CONDITIONAL-VARIANCE
Named formalization leaf: UCBVI-BF-TOTAL-VARIANCE
Named formalization leaf: UCBVI-BF-TERMINAL

Improve this case

Corrections should preserve the comparison signature and cite a primary theorem, theorem number, source edition, and exact gap being closed. Lean contributions should target one named missing leaf without weakening the mathematical contract.

Propose a sourced update