Prove2Me

Theorem 37.13: Ω(n)\Omega(n) lower bound for hopeless games

Proved
BanditAlgorithm.partial_monitoring_hopeless_linear_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 partial-monitoring game with a finite discrete signal alphabet. Suppose that GG has neighbouring actions but is not globally observable. 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 n \le R_n^*(G) \qquad \text{for every }n\ge N_G.

This is the hopeless branch of the classification. Non-global observability gives two stochastic environments that induce identical feedback laws for every policy while favouring different neighbouring actions, forcing linear regret.

Formalization Note A neighbouring pair supplies the source theorem’s requirement of at least two non-dominated actions.

Preamble
import Definitions.Def_PartialMonitoringGame

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

View graph