BanditRLwiki case · stochastic-linear-oful

Stochastic linear bandits: OFUL versus dimension-dependent lower bounds

OFUL is near minimax up to logarithmic factors in dimension-dependent high-probability regret.

Audited comparison

stochastic-linear-oful Stochastic linear bandits: OFUL versus dimension-dependent lower boundsOFUL is near minimax up to logarithmic factors in dimension-dependent high-probability regret. Near minimaxPartial local route

Open stable case page →Exact source theorem

OFULlinear banditself normalizedelliptical potentialhigh probability

Reward model: Linear mean x_t dot theta-star with conditionally sub-Gaussian noise
Geometry: Bounded actions and parameter norm in dimension d
Regret: High-probability cumulative pseudo-regret
Target scale: d sqrt(T) up to logarithmic factors

Comparison judgment

Near minimax

The upper and lower dimension dependence agree at leading polynomial order. The local route is a finite-action scalar-ridge specialization, not the full paper theorem.

Known gap. Logarithmic factors, source normalization, decision-set generality, and constants separate the OFUL upper from the d sqrt(T) lower. The displayed upper is high probability, whereas the lower is an expected-regret minimax statement, so the comparison is only at leading polynomial scale.

Local Lean boundary

Partial local route

Elliptical potential, self-normalized ridge confidence, a measurable horizon-free finite-action policy, all-time confidence, and one-policy all-horizon regret compile. Full source geometry and the linear lower bound do not.

Upper bound

OFUL high-probability regret upper bound

Improved Algorithms for Linear Stochastic Bandits

Yasin Abbasi-Yadkori, Dávid Pál, and Csaba Szepesvári · 2011 · Theorem 13

Upper bound guarantee. Formula renderer unavailable; readable fallback: OFUL has a high-probability dimension times square root T regret bound up to logarithmic and regularization factors.\[R_T=\widetilde O\!\left(d\sqrt{T}\right)\quad\text{with probability at least }1-\delta.\]

Use the exact confidence radius, determinant term, action-set, and norm assumptions in Theorem 13.

Open primary source

Lower bound

Linear-bandit minimax expected-regret lower bound

Stochastic Linear Optimization under Bandit Feedback

Varsha Dani, Thomas Hayes, and Sham Kakade · 2008 · Theorem 3

Lower bound guarantee. Formula renderer unavailable; readable fallback: A constructed linear decision domain forces expected regret at least one tenth d square root T.\[\inf_\pi\sup_\theta\mathbb E R_T(\pi,\theta)\ge \frac1{10}d\sqrt{T}.\]

The lower theorem uses its explicit domain, dimension, and horizon range.

Open primary source

Local Lean evidence

Exact declarations

BanditRLProof.OFUL.telescopingCanonicalStandardHighProbabilityPseudoRegret_nonneg_and_allHorizon_tail_le_explicitBound_of_linearSubgaussianEnvironment_of_featureBound_le_regularization

Not yet proved here

Missing steps

Audit exact correspondence with OFUL Theorem 13 constants and normalization.
Generalize beyond the current finite-action scalar-ridge interface.
Formalize a compatible Gaussian linear hard family and d sqrt(T) lower terminal.

formalization frontier

Can the finite-action scalar route be lifted to the exact OFUL theorem and paired with a compatible linear minimax lower construction?

The local high-probability all-horizon consumer is strong but intentionally narrower than the source theorem.

General decision set
source radius identity
hard family
upper/lower comparison terminal
Named formalization leaf: OFUL-SOURCE-THEOREM-13-IDENTITY
Named formalization leaf: LINEAR-BANDIT-MINIMAX-LOWER

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