Prove2Me

Quadratic upper bound for the Algorithm 26 stability function

Proved
BanditAlgorithm.pmPsi_le_quadratic

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

bandit-algorithmsinequalitiesonline-learning

Let q be a probability distribution on a finite action set and let z be a real vector with z_b at least -1 in every coordinate. For the exponential-weights stability function

Ψq(z)=∑bqb(e−zb+zb−1),\Psi_q(z)=\sum_b q_b\bigl(e^{-z_b}+z_b-1\bigr),

one has the quadratic bound

Ψq(z)≤∑bqbzb2.\Psi_q(z)\leq\sum_b q_b z_b^2.

This is the pointwise stability estimate used in both the global- and local-observability analyses of Algorithm 26.

Preamble
import Definitions.Def_PartialMonitoringAlgorithm26

open scoped BigOperators
Formal statement
namespace BanditAlgorithm

/-! Lattimore--Szepesvári, equation (37.15), printed p. 497. -/

theorem pmPsi_le_quadratic {k : ℕ} (q z : Fin k → ℝ)
    (hq : q ∈ stdSimplex ℝ (Fin k)) (hz : ∀ b, -1 ≤ z b) :
    pmPsi q z ≤ ∑ b : Fin k, q b * (z b) ^ 2 := by
  sorry

end BanditAlgorithm
Source
Tor Lattimore and Csaba Szepesvári, Bandit Algorithms, Chapter 37, equation (37.15), printed p. 497, https://tor-lattimore.com/downloads/book/book.pdf

View graph