Lemma 8.2 exponential-sum bound

Proved

BanditAlgorithm.bandit_ucb_index_exponential_sum_bound

by MKPynnic · Jul 19, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analysisbanditsconcentration

For $n\in\mathbb{N}$ , $\varepsilon>0$ , and $a>0$ , split the Lemma 8.2 index-count sum at $u=2a/\varepsilon^2$ . Bound each pre-cutoff term by $1$ and each post-cutoff term by $\exp(-[t(\varepsilon-\sqrt{2a/t})]^2/(2t))$ . The resulting finite sum is at most $1+\frac{2}{\varepsilon^2}(a+\sqrt{\pi a}+1)$ . This is the deterministic sum-to-integral and Gaussian-calculus stage of the source proof.

Preamble

import Mathlib.Probability.Moments.SubGaussian
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

open MeasureTheory ProbabilityTheory Real

Formal statement

namespace BanditAlgorithm

theorem bandit_ucb_index_exponential_sum_bound
    {n : ℕ} {ε a : ℝ} (hε : 0 < ε) (ha : 0 < a) :
    (∑ t ∈ Finset.Icc 1 n,
      if 2 * a / ε ^ 2 < (t : ℝ) then
        Real.exp (-((t : ℝ) * (ε - Real.sqrt (2 * a / t))) ^ 2 /
          ((2 : ℝ) * (t : ℝ) * (1 : ℝ)))
      else 1) ≤
      1 + 2 / ε ^ 2 * (a + Real.sqrt (Real.pi * a) + 1) := by
  sorry

end BanditAlgorithm

Source

Lattimore and Szepesvari, Bandit Algorithms (CUP 2020), Lemma 8.2 proof, printed pp. 118-119 / PDF pp. 127-128: cutoff u = 2a ε^-2, Corollary 5.5 exponential sum, comparison with the displayed improper integral, and substitution s = ε sqrt(t) - sqrt(2a).

View graph