BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.Lean-verified build · exact declarations linked.

BanditRLwiki case · distributional-high-probability-regret

Distributional high-probability regret under an expected-regret constraint

A 2026 upper theorem matches the Chapter 17 logarithmic confidence tradeoff in order. Theorem 17.1, Corollaries 17.2–17.3, and the explicitly corrected adversarial terminal pass the full local repository gate. EQO+ remains a separate unformalized upper route.

← Distributional and high-probability lower bounds

Audited comparison

distributional-high-probability-regret Distributional high-probability regret under an expected-regret constraintA 2026 upper theorem matches the Chapter 17 logarithmic confidence tradeoff in order. Theorem 17.1, Corollaries 17.2–17.3, and the explicitly corrected adversarial terminal pass the full local repository gate. EQO+ remains a separate unformalized upper route. Minimax matchedPartial local route
Open stable case page →Exact source theorem
high probability lower bounddistributional regretEQO+Chapter 17tail tradeoff
Reward model
Finite stochastic sub-Gaussian or unit-Gaussian arms
Policy premise
Uniform expected regret of order B sqrt((A-1) T) for the lower theorem
Regret
Tail of random pseudo-regret
Target scale
sqrt(A T) log(1/delta), capped by T

Comparison judgment

Minimax matched

This literature frontier is closed by the 2026 EQO+ result. Chapter 17's stochastic endpoints compile, and corrected Theorem 17.4 passes focused compilation on 0 < δ ≤ 1/32 with c=1/160, C=64. Full local gates pass; this does not formalize EQO+.

Known gap. The upper and lower tradeoff match in confidence and square-root order, with constants, exact reward class, and the lower theorem's expected-regret premise remaining visible.

Local Lean boundary

Partial local route

BanditRLlib compiles the stochastic Chapter 17 endpoints, Claims 17.5–17.7, Eq. (17.8), same-policy shared-noise coupling, and deterministic matrix extraction. Approved corrections: Claim 17.6 uses T_i ≤ n/2; Theorem 17.4 uses 0 < δ ≤ 1/32, c=1/160, C=64 and a strict CDF tail. The full local repository gate passes; EQO+ is not formalized.

Upper bound

EQO+ distributional-regret upper bound

Unified Framework of Distributional Regret in Multi-Armed Bandits and Reinforcement Learning

Lee and Oh · 2026 · Theorem 4

Upper bound guarantee. EQO+ simultaneously controls expected regret at the minimax scale and the distributional tail with one logarithmic confidence factor.

Use the source's sub-Gaussian model and its displayed tuning c1 equals sigma square root T over A.

Open primary source

Lower bound

Chapter 17 distributional-regret lower bound

Bandit Algorithms

Tor Lattimore and Csaba Szepesvári · 2020 · Theorem 17.1

Lower bound guarantee. Any policy with the source's uniform expected-regret bound has a unit-Gaussian instance whose random pseudo-regret exceeds the displayed confidence-dependent threshold with probability at least delta.

Preserve the exact A, T, B, delta conditions and the same randomized nonanticipating policy.

Open primary source

Not yet proved here

Missing steps

  • Map and formalize the EQO+ algorithm and Theorem 4 as a separate upper route.

formalization frontier

Can the compiled corrected lower terminal be paired with a formalized EQO+ upper route?

Theorem 17.1, Corollaries 17.2–17.3, Eq. (17.8), corrected Claim 17.6, exact Claim 17.7, and corrected Theorem 17.4 pass the full local repository gate. Theorem 17.4 uses 0 < δ ≤ 1/32, c=1/160, C=64. No EQO+ algorithm theorem is claimed.

  • EQO+ source map and formalized upper terminal
  • Named formalization leaf: CH17-HISTORY-INFORMATION
  • Named formalization leaf: CH17-THEOREM-17-1
  • Named formalization leaf: CH17-COROLLARY-17-2
  • Named formalization leaf: CH17-COROLLARY-17-3
  • Named formalization leaf: EQOPLUS-UPPER

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