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

BanditRLwiki case · contextual-finite-policy-exp4p

Finite-policy contextual bandits with Exp4.P

Exp4.P gives high-probability policy regret for a finite expert class; the exact matching lower source still needs theorem-level audit in this Wiki.

← Linear and contextual bandits

Audited comparison

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. Exp4.P has high-probability regret at most six times square root A T log N over delta under the source conditions.

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

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