Ranked descent from a duplicate-free hindsight cover

Open

BanditAlgorithm.partial_monitoring_duplicate_free_pareto_cover_ranked_descent_from_hindsight

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. Assume that every finite outcome sequence has a hindsight-optimal action in $S$ . Then, for every mixed outcome $\\lambda$ in the probability simplex, there is a root and a natural-number rank such that every non-root $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 a terminating, non-increasing in-tree toward a $\\lambda$ -optimal region, including boundary mixtures where several actions tie. The hindsight-cover assumption ensures that no Pareto region needed by the geometric argument was omitted.

Formalization Note Duplicate-freeness is expressed extensionally by equality of all loss coordinates implying equality of actions; decreasing natural-number ranks encode acyclicity.

Preamble

import Definitions.Def_PartialMonitoringGame

open scoped BigOperators

Formal statement

theorem BanditAlgorithm.partial_monitoring_duplicate_free_pareto_cover_ranked_descent_from_hindsight
    {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)
    (hbest : ∀ (n : ℕ) (out : Fin n → Fin d), ∃ b ∈ S, ∀ a : Fin k,
      ∑ t, G.L b (out t) ≤ ∑ t, G.L a (out t)) :
    ∀ 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