Strict descent in a duplicate-free Pareto-cell cover

Open

BanditAlgorithm.partial_monitoring_pareto_cover_strict_descent

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

banditsconvex-geometrypartial-monitoring

For every finite partial-monitoring game, one can select a nonempty, duplicate-free collection $S$ of Pareto-optimal actions whose cells cover the outcome simplex. Hence every finite outcome sequence has a hindsight-optimal action in $S$ . For every mixed outcome $\lambda$ , there is a root action in $S$ minimizing $\lambda$ -expected loss, and every other action $b\in S$ has a neighbouring action $c\in S$ with strictly smaller $\lambda$ -expected loss.

This is the strict-descent form of connectivity used to build the monotone in-tree in Lemma 37.21. Selecting one representative from each duplicate class handles duplicate actions; lower-dimensional cells do not enter $S$ .

Preamble

import Definitions.Def_PartialMonitoringGame

open scoped BigOperators

Formal statement

theorem BanditAlgorithm.partial_monitoring_pareto_cover_strict_descent
    {k d : ℕ} {𝕊 : Type*}
    (G : PartialMonitoringGame k d 𝕊) (hk : 2 ≤ k) (hd : 0 < d) :
    ∃ S : Finset (Fin k),
      S.Nonempty ∧
      (∀ (n : ℕ) (i : Fin n → Fin d), ∃ b ∈ S, ∀ a : Fin k,
        ∑ t, G.L b (i t) ≤ ∑ t, G.L a (i t)) ∧
      ∀ lam : Fin d → ℝ, lam ∈ stdSimplex ℝ (Fin d) →
        ∃ root ∈ S,
          (∀ b ∈ S,
            ∑ i : Fin d, G.L root i * lam i ≤
              ∑ i : Fin d, G.L b i * lam i) ∧
          ∀ b ∈ S, b ≠ root →
            ∃ c ∈ S, NeighbouringActions G b c ∧
              ∑ i : Fin d, G.L c i * lam i <
                ∑ i : Fin d, G.L b i * lam i := by
  sorry

Source

Tor Lattimore and Csaba Szepesvári, Bandit Algorithms, Cambridge University Press (2020), Lemma 37.7 p. 484, Exercise 37.10 p. 509, and Lemma 37.21 pp. 501–502. https://tor-lattimore.com/downloads/book/book.pdf

View graph