Lemma 9.3: $\mathbb P(\tilde\Delta \ge \Delta) \le 15k/(n\Delta^2)$

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

Lemma 9.3 of Lattimore--Szepesvári, specialized to $\delta = k/n$: the shortfall of the optimal arm's MOSS index below its true mean has a quadratic tail,

where $\tilde\Delta = \big(\mu^{*} - \min_{s \le n}(\hat\mu_{i^{*}\!,s} + \sqrt{(4/s)\log^{+}(n/(ks))})\big)^{+}$.

The source proves this with the peeling device: decompose over the geometric grid $s \in [2^j, 2^{j+1})$, apply the maximal subgaussian inequality (Theorem 9.2) on each block, and sum the resulting Gaussian tails using $(a+b)^2 \ge a^2 + b^2$ and a unimodal-summand integral comparison. It is the estimate that makes $\mathbb E[2n\tilde\Delta] \le 16\sqrt{kn}$ possible via the layer-cake formula.

Why this node was retired

The posted statement is

theorem BanditAlgorithm.moss_optimal_shortfall_tail_bound
    {k : ℕ} (hk : 0 < k)
    {ν : BanditAlgorithm.StochasticBandit k}
    (hν : BanditAlgorithm.IsSubgaussianBandit 1 ν)
    {n : ℕ} {π : BanditAlgorithm.BanditPolicy k}
    (hπ : BanditAlgorithm.IsMOSSPolicy n π) (hkn : k ≤ n)
    (iStar : Fin k)
    (hiStar : BanditAlgorithm.banditArmMean ν iStar =
      BanditAlgorithm.banditOptimalMean ν)
    (Δ : ℝ) (hΔ : 0 < Δ) :
    (BanditAlgorithm.banditMeasure ν π n).real
        {h | Δ ≤ BanditAlgorithm.mossOptimalShortfall ν iStar h} ≤
      15 * (k : ℝ) / ((n : ℝ) * Δ ^ 2) := by sorry

The sample-size empirical mean takes only the available finite-history rewards but divides by the requested sample size even when fewer samples exist.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

Define for each arm an infinite IID potential reward stream with that arm’s law, and use the first s rewards to define μ̂ᵢ,s for every s≥1. Couple realized pulls to prefixes of these streams before applying the shortfall/κ concentration bounds.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.