Prove2Me

Theorem 37.14: Ω(n)\Omega(\sqrt n) lower bound for easy games

Proved
BanditAlgorithm.partial_monitoring_easy_sqrt_lower_bound

by Harry_Xu · Aug 13, 2026 · Mathlib c5ea003 (Lean v4.30.0)

bandit-algorithmslower-boundminimax-regretpartial-monitoring

Let G=(L,Φ)G=(L,\Phi) be a finite locally observable partial-monitoring game with a finite discrete signal alphabet and at least one pair of neighbouring actions. Then there are a game-dependent constant cG>0c_G>0 and a horizon NGN_G such that

cGn≤Rn∗(G)for every n≥NG.c_G\sqrt n \le R_n^*(G) \qquad \text{for every }n\ge N_G.

This is the lower half of the easy-game Θ(n)\Theta(\sqrt n) classification. It is obtained by testing two nearby stochastic environments on opposite sides of a neighbouring cell boundary.

Formalization Note The source says “for all large enough nn”; the existential threshold NGN_G makes that quantifier explicit.

Preamble
import Definitions.Def_PartialMonitoringGame
import Mathlib.Data.Real.Sqrt

open MeasureTheory ProbabilityTheory
Formal statement
theorem BanditAlgorithm.partial_monitoring_easy_sqrt_lower_bound
    {k d : ℕ} {𝕊 : Type*}
    [Fintype 𝕊] [MeasurableSpace 𝕊] [MeasurableSingletonClass 𝕊]
    (G : PartialMonitoringGame k d 𝕊)
    (h : LocallyObservable G ∧ HasNeighbouringActions G) :
    ∃ c : ℝ, 0 < c ∧ ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
      c * Real.sqrt n ≤ pmMinimaxRegret G n := by
  sorry
Source
Tor Lattimore and Csaba Szepesvári, Bandit Algorithms, Chapter 37, Section 37.4, Theorem 37.14 and proof sketch, printed p. 492 (PDF p. 500), https://tor-lattimore.com/downloads/book/book.pdf

View graph