No neighbouring cells implies a universally optimal action

Proved

BanditAlgorithm.partial_monitoring_no_neighbours_has_universally_optimal_action

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

banditsconvex-geometrypartial-monitoring

Let $G$ be a finite partial-monitoring game with at least one action and at least one outcome. If the cell decomposition of the outcome simplex has no pair of neighbouring Pareto-optimal actions, then some action $a$ is optimal for every outcome individually:

\exists a\;\forall b,i,\qquad L_{a i} \le L_{b i}.

Equivalently, the cell of $a$ is the whole outcome simplex. This is the finite-polyhedral geometric core of the trivial class in the partial-monitoring classification theorem.

Formalization Note Nonemptiness of the finite action and outcome sets is explicit because the source treats these as nonempty by convention.

Preamble

import Definitions.Def_PartialMonitoringGame

open MeasureTheory ProbabilityTheory

Formal statement

theorem BanditAlgorithm.partial_monitoring_no_neighbours_has_universally_optimal_action
    {k d : ℕ} {𝕊 : Type*}
    (G : PartialMonitoringGame k d 𝕊)
    (hk : 0 < k) (hd : 0 < d)
    (h : ¬ HasNeighbouringActions G) :
    ∃ a : Fin k, ∀ b : Fin k, ∀ i : Fin d, G.L a i ≤ G.L b i := by
  sorry

Source

Lattimore and Szepesvári, Bandit Algorithms (2020), Section 37.8, Theorem 37.22, printed p. 503 (PDF p. 511); https://tor-lattimore.com/downloads/book/book.pdf

View graph