BanditRLwiki case · stochastic-finite-arm-minimax

Finite-arm stochastic minimax expected regret

MOSS-type algorithms and Gaussian/Bernoulli hard families identify the square-root A times T minimax scale.

Audited comparison

stochastic-finite-arm-minimax Finite-arm stochastic minimax expected regretMOSS-type algorithms and Gaussian/Bernoulli hard families identify the square-root A times T minimax scale. Minimax matchedPartial local route

Open stable case page →Faithful restatement

MOSSminimaxexpected pseudo-regretbounded rewardsGaussian lower bound

Reward model: Independent stationary rewards; the literature upper uses rewards in [0,1]
Horizon: Any finite T; the cited MOSS-anytime result is horizon-free
Regret: Expected pseudo-regret
Target scale: Theta(sqrt(A T))

Comparison judgment

Minimax matched

The literature establishes the square-root minimax order. Local Lean now supplies the unit-Gaussian lower bound and fixed-horizon Algorithm 7 on unit-subgaussian laws with gaps in [0,1]. The cited anytime theorem remains a distinct formalization target.

Known gap. Universal constants and the exact hard-family reward class differ across the displayed source theorems.

Local Lean boundary

Partial local route

BanditRLlib compiles a unit-variance Gaussian lower bound with constant 1/54 and fixed-horizon MOSS on unit-subgaussian laws with gaps in [0,1]. The cited anytime MOSS theorem is not compiled.

Upper bound

Anytime MOSS regret

Anytime optimal algorithms in stochastic multi-armed bandits

Rémy Degenne and Vianney Perchet · 2016 · Theorem 3 with Lemma 3

Upper bound guarantee. Formula renderer unavailable; readable fallback: The anytime MOSS variant has expected regret at most 113 times square root A T plus the largest gap.\[\mathbb E R_T\le 113\sqrt{AT}+\Delta_{\max}.\]

Independent rewards supported in [0,1], with the source's anytime index and initialization.

Open primary source

Lower bound

Minimax stochastic-bandit lower bound

Anytime optimal algorithms in stochastic multi-armed bandits

Rémy Degenne and Vianney Perchet · 2016 · Lemma 3

Lower bound guarantee. Formula renderer unavailable; readable fallback: Every policy has a stochastic instance with expected regret at least one twentieth of square root A T under the source's parameter range.\[\inf_\pi\sup_\nu\mathbb E_\nu R_T(\pi)\ge \frac1{20}\sqrt{AT}.\]

Use the exact arm-count and horizon restrictions stated in the source.

Open primary source

Local Lean evidence

Exact declarations

BanditRLProof.LowerBounds.unitGaussianMinimaxExpectedPseudoRegret_ge_one_div_fiftyFour_sqrt

Not yet proved here

Missing steps

Define the anytime MOSS index and measurable generated history policy.
Prove the same-policy pull-count decomposition and bounded-reward confidence route.
Compile the matching square-root expected-regret upper terminal without conflating the Gaussian lower class with [0,1] rewards.

formalization frontier

Can the exact anytime MOSS source theorem be compiled on one generated bounded-reward trajectory?

The local Gaussian lower terminal and fixed-horizon MOSS near-minimax theorem compile; the distinct anytime variant remains unformalized.

Index measurability
armwise confidence
pull-count summation
expected-regret terminal
Named formalization leaf: MOSS-ANYTIME-GENERATED-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