Ranked descent for a duplicate-free Pareto-cell cover

Open

BanditAlgorithm.partial_monitoring_duplicate_free_pareto_cover_ranked_descent

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

banditsconvex-geometrygraph-theorypartial-monitoring

Let $S$ be a nonempty, duplicate-free collection of Pareto-optimal actions in a finite partial-monitoring game with at least one outcome. Then, for every mixed outcome $\\lambda$ in the probability simplex, there is a root action and a natural-number rank such that every non-root action $b\\in S$ has a neighbouring successor $c\\in S$ satisfying

\\langle L_c,\\lambda\\rangle\\leq\\langle L_b,\\lambda\\rangle \\quad\\text{and}\\quad \\operatorname{rank}(c)<\\operatorname{rank}(b).

Thus the Pareto-cell adjacency graph admits an acyclic in-tree oriented toward a $\\lambda$ -optimal root, including boundary mixtures where several actions tie. This is the geometric connectivity and monotone-tree component used by partial-monitoring estimators.

Formalization Note Duplicate-freeness is expressed extensionally by equality of all loss coordinates implying equality of actions; the decreasing rank makes termination explicit.

Preamble

import Definitions.Def_PartialMonitoringGame

open scoped BigOperators

Formal statement

theorem BanditAlgorithm.partial_monitoring_duplicate_free_pareto_cover_ranked_descent
    {k d : ℕ} {𝕊 : Type*}
    (G : PartialMonitoringGame k d 𝕊) (hd : 0 < d)
    (S : Finset (Fin k)) (hSne : S.Nonempty)
    (hpareto : ∀ a ∈ S, ParetoOptimalAction G a)
    (hunique : ∀ a ∈ S, ∀ b ∈ S,
      (∀ i, G.L a i = G.L b i) → a = b) :
    ∀ lam : Fin d → ℝ, lam ∈ stdSimplex ℝ (Fin d) →
      ∃ root ∈ S, ∃ rank : Fin k → ℕ,
        ∀ 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 ∧
            rank c < rank b := 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, especially the finite-subsequence boundary argument. https://tor-lattimore.com/downloads/book/book.pdf

View graph