BanditRLwiki case · finite-action-linear-contextual

Finite-action linear contextual minimax rates

SupLinUCB/VCL upper and lower theorems match the finite-action contextual rate up to iterated logarithms.

Audited comparison

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

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