BanditRLwiki setting

Linear and contextual bandits

Linear realizability, self-normalized confidence, finite policy classes, and dimension-dependent lower bounds.

Comparison signature

Problem class. Linear stochastic or adversarial contextual bandits
Feedback. Selected-action reward or loss
Objective. Cumulative pseudo-regret or policy regret
Parameters. Dimension d, actions A, policies N, rounds T, confidence delta

Matching rule. A rate is called matched only when the upper and lower theorem contracts agree on the fields above; every remaining mismatch is named in the case.

3 cases

contextual-finite-policy-exp4p Finite-policy contextual bandits with Exp4.PExp4.P gives high-probability policy regret for a finite expert class; the exact matching lower source still needs theorem-level audit in this Wiki. Source audit pendingPlanned

Open stable case page →Primary reference pending

Exp4.Pcontextual banditfinite policy classhigh probabilitysource audit pending

Context model: Adversarial contexts and rewards
Policy class: N finite experts mapping contexts to A actions
Regret: High-probability regret to the best policy
Target scale: sqrt(A T log(N/delta))

Comparison judgment

Source audit pending

This is a source-audit queue item, not a claim that the lower bound is unknown in the literature.

Known gap. The upper theorem is indexed exactly; a compatible primary lower theorem, assumptions, and constants have not yet been frozen here.

Local Lean boundary

Planned

No finite-policy contextual Exp4.P terminal is mapped to a local Lean declaration.

Upper bound

Exp4.P high-probability policy-regret upper bound

Contextual Bandit Algorithms with Supervised Learning Guarantees

Alina Beygelzimer, John Langford, Lihong Li, Lev Reyzin, and Robert Schapire · 2010 · Theorem 2

Upper bound guarantee. Formula renderer unavailable; readable fallback: Exp4.P has high-probability regret at most six times square root A T log N over delta under the source conditions.\[R_T\le 6\sqrt{AT\log(N/\delta)}\quad\text{with probability at least }1-\delta.\]

Includes the source's uniform expert and log(N/delta) at most A T conditions.

Open primary source

Lower bound

No source theorem claimed

The source audit has not registered a compatible theorem for this side of the comparison.

Local Lean evidence

Exact declarations

No local declaration is claimed for this target.

Not yet proved here

Missing steps

Define measurable context-to-action experts and the expert-mixture sampler.
Formalize the importance-weighted estimator and Exp4.P variance bonus.
Audit and freeze the exact compatible lower theorem before assigning near-minimax status.

formalization frontier

Which exact contextual lower theorem matches the displayed Exp4.P contract, and how should its policy class be represented in Lean?

The Exp4.P upper theorem is frozen; the lower-source audit and all local formalization remain pending.

Exact lower source
expert measurability
mixture action law
high-probability terminal
Named formalization leaf: EXP4P-LOWER-SOURCE-AUDIT
Named formalization leaf: EXP4P-CONTEXT-POLICY-INTERFACE

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

finite-action-linear-contextual Finite-action linear contextual minimax ratesSupLinUCB/VCL upper and lower theorems match the finite-action contextual rate up to iterated logarithms. Near minimaxPlanned

Open stable case page →Exact source theorem

linear contextualSupLinUCBVCLfinite actionsnear minimax

Context model: d-dimensional realizable contexts with n available actions per round
Reward model: Stochastic linear reward
Regret: Expected cumulative regret
Target scale: square root(d T log T log n), up to iterated logarithms

Comparison judgment

Near minimax

The source gives both sides under an explicit parameter fence. Do not treat the local OFUL scaffold as a proof of this contextual finite-action result.

Known gap. The upper differs from the lower by iterated logarithms; Theorem 2 also requires n at most 2^(d/2) and T at least d (log_2 n)^(1+epsilon).

Local Lean boundary

Planned

No time-varying finite-action contextual theorem is claimed locally. Existing OFUL declarations are reusable proof infrastructure only.

Upper bound

Finite-action linear contextual upper bound

Nearly Minimax-Optimal Regret for Linearly Parameterized Bandits

Lihong Li, Wei Wang, and Zhihua Zhou · 2019 · Theorem 1

Upper bound guarantee. Formula renderer unavailable; readable fallback: The minimax regret is at most square root d T log T log n times iterated-logarithmic factors.\[R^*(T;n,d)\le \operatorname{poly}(\log\log(nT))\,O\!\left(\sqrt{dT\log T\log n}\right).\]

Finite action sets and the source's realizability, action-count, dimension, and horizon conditions.

Open primary source

Lower bound

Finite-action linear contextual lower bound

Nearly Minimax-Optimal Regret for Linearly Parameterized Bandits

Lihong Li, Wei Wang, and Zhihua Zhou · 2019 · Theorem 2

Lower bound guarantee. Formula renderer unavailable; readable fallback: Under the theorem's action-count and horizon fence, every algorithm has regret at the displayed finite-action contextual scale.\[R^*(T;n,d)=\Omega_\varepsilon\!\left(\sqrt{dT\log n\,\log(T/d)}\right).\]

For every small epsilon greater than zero, n is at most 2^(d/2) and T is at least d (log_2 n)^(1+epsilon), together with the source's remaining conditions.

Open primary source

Local Lean evidence

Exact declarations

No local declaration is claimed for this target.

Not yet proved here

Missing steps

Represent time-varying action sets and contexts measurably.
Formalize the VCL layer partition and contextual lower construction.
Retain the action-count and horizon fence in the final comparison theorem.

formalization frontier

Can the exact Theorems 1–2 parameter fence and VCL construction be represented in one contextual Lean history law?

The primary upper/lower comparison is audited; all local contextual algorithm and lower-construction work remains planned.

Contextual history law
VCL layers
parameter fence
lower construction
Named formalization leaf: VCL-CONTEXTUAL-HISTORY-LAW
Named formalization leaf: VCL-LAYER-PARTITION
Named formalization leaf: VCL-LOWER-CONSTRUCTION