An online algorithm with vanishing swap regret

Proved

AGT.no_swap_regret_algorithm

by Shuze Chen · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

correlated-equilibriumgame-theoryonline-learningregret

There is an online algorithm whose swap regret against every adversary is at most $2N\sqrt{T\ln N}$ — the mission goal, Corollary 4.16 of Algorithmic Game Theory in explicit form. For every number of actions $N = n+1$ and every known horizon $T$ there exists an online algorithm $H$ , playing a genuine probability distribution after every history, whose swap regret is uniformly small: against every $[0,1]$ -valued loss sequence and every modification rule $F$ ,

L^T_H \;\le\; L^T_{H,F} + 2N\sqrt{T\,\ln N}.

Per round, the swap regret vanishes at rate $2N\sqrt{\ln N/T}$ ; combined with Theorem 4.12, if every player of a finite game runs such an algorithm, the empirical joint play is a $2N\sqrt{\ln N/T}$ -correlated equilibrium — the chapter's punchline, and the algorithmic foundation of correlated equilibrium.

A note on the constant and the quantifiers. The book states the bound as $O(N\sqrt{T\log N})$ ; the constant $2$ is the one its own route produces — Polynomial Weights tuned at $\eta = \min\{\sqrt{\ln N/T}, 1/2\}$ has external regret $\le 2\sqrt{T\ln N}$ (in the small-horizon regime $T < 4\ln N$ this follows from the trivial bound $L \le T \le 2\sqrt{T\ln N}$ rather than from the potential argument), and the reduction of Theorem 4.15 multiplies it by $N$ . The algorithm is quantified before the loss sequence and the rule $F$ : one $H$ must serve every adversary, so no witness can be chosen with hindsight. $H$ may depend on $T$ (the book's known-horizon convention; guess-and-double removes this at a constant-factor cost and is out of scope).

Preamble

import Definitions.Def_agt_regret
import Mathlib.Analysis.SpecialFunctions.Sqrt
import Mathlib.Analysis.SpecialFunctions.Log.Basic

Formal statement

namespace AGT

/-- **Corollary 4.16 of *Algorithmic Game Theory* (explicit form)**, the
capstone of Chapter 4: there is an online algorithm with vanishing swap
regret.  For every number of actions `n + 1` and every known horizon `T`
there is an online algorithm `H` playing genuine distributions such that
against every `[0,1]`-valued loss sequence and every modification rule `F`,
`L_H ≤ L_{H,F} + 2 (n+1) √(T ln(n+1))`.

The explicit constant is the one the chapter's own route produces: the
Polynomial Weights bound (Theorem 4.6) tuned at `η = min{√(ln N / T), 1/2}`
gives external regret `2√(T ln N)`, and the external-to-swap reduction
(Theorem 4.15) multiplies it by `N`.  Combined with Theorem 4.12, an `H` of
this quality for every player drives the empirical joint play into an
`ε`-correlated equilibrium at rate `ε = 2N√(ln N / T)`. -/
theorem no_swap_regret_algorithm {n : ℕ} (T : ℕ) :
    ∃ H : OnlineAlgorithm (n + 1), (∀ h, IsLottery (H h)) ∧
      ∀ ℓ : ℕ → Fin (n + 1) → ℝ, (∀ t i, ℓ t i ∈ Set.Icc (0 : ℝ) 1) →
        ∀ F : Fin (n + 1) → Fin (n + 1),
          algLoss H ℓ T ≤ swapLoss H ℓ F T +
            2 * (n + 1) * Real.sqrt (T * Real.log (n + 1)) := by
  sorry

end AGT

Source

N. Nisan, T. Roughgarden, E. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press 2007, https://doi.org/10.1017/CBO9780511800481, Section 4.5, Corollary 4.16, p. 94 (explicit constant)

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Read-back: `no_swap_regret_algorithm`

Setting. Fix a natural number $n \ge 0$ (implicit) and a natural number $T \ge 0$ (the time horizon, given as an explicit argument). Throughout, the action set is $\{0, 1, \dots, n\}$ , i.e. it has exactly $n+1$ elements (so it is never empty). An online algorithm on $n+1$ actions is, by the custom definition being used, simply a function $H$ that maps every finite list of loss vectors in $\mathbb{R}^{n+1}$ (a "history") to a single vector in $\mathbb{R}^{n+1}$ ; nothing in the type forces the output to be a probability distribution — that is imposed separately below. The algorithm is deterministic as a function of the history.

What the theorem asserts. For every $n$ and every $T$ , there exists an online algorithm $H$ (which may depend on both $n$ and $T$ , since both are fixed before the existential) satisfying both of the following.

$H$ always outputs a lottery. For every finite list $h$ of loss vectors — including the empty list, and including lists of arbitrary length and with arbitrary real entries, whether or not they could ever arise as an actual history — the output $H(h) \in \mathbb{R}^{n+1}$ satisfies the custom lottery predicate:

H(h)_i \ge 0 \text{ for every action } i, \qquad \sum_{i=0}^{n} H(h)_i = 1.

A uniform swap-regret bound at horizon $T$ . For every loss sequence $\ell : \mathbb{N} \to \mathbb{R}^{n+1}$ such that $\ell_t(i) \in [0,1]$ (the closed interval, endpoints included) for all times $t \in \mathbb{N}$ and all actions $i$ , and for every function $F : \{0,\dots,n\} \to \{0,\dots,n\}$ (an arbitrary "swap" map, not required to be injective or surjective), the following inequality holds:

L_H(T) \;\le\; L_H^F(T) \;+\; 2\,(n+1)\,\sqrt{\,T \cdot \ln(n+1)\,}.

Unfolding the two loss quantities. Write $p_t := H\big([\ell_0, \ell_1, \dots, \ell_{t-1}]\big)$ for the vector the algorithm outputs at time $t$ when fed the list of the first $t$ loss vectors in order (at $t = 0$ this is the empty list). Then, by the custom definitions:

the algorithm's (expected) cumulative loss is

L_H(T) \;=\; \sum_{t=0}^{T-1} \sum_{i=0}^{n} p_t(i)\, \ell_t(i),

and the swapped loss under $F$ is

L_H^F(T) \;=\; \sum_{t=0}^{T-1} \sum_{i=0}^{n} p_t(i)\, \ell_t\big(F(i)\big),

i.e. the same play distributions $p_t$ , but each action $i$ 's loss replaced by the loss of the swapped action $F(i)$ . Both sums run over the $T$ time steps $t = 0, 1, \dots, T-1$ .

Quantifier order, precisely. The single algorithm $H$ is chosen after $n$ and $T$ are fixed, but before $\ell$ and $F$ : one and the same $H$ must satisfy the lottery condition for all histories and the regret inequality uniformly over all $[0,1]$ -valued loss sequences $\ell$ and all swap functions $F$ , with the same additive slack $2(n+1)\sqrt{T \ln(n+1)}$ . The inequality is non-strict ( $\le$ ), and it is asserted only at the single horizon $T$ named in the statement, not for all horizons.

The bound expression. The additive term is exactly $2 \cdot (n+1) \cdot \sqrt{T \cdot \ln(n+1)}$ , where $n+1$ and $T$ are the natural numbers cast to reals, $\ln$ is the natural logarithm, and $\sqrt{\cdot}$ is the real square root (Lean's total square root, which returns $0$ on negative inputs; here the argument $T\ln(n+1)$ is nonnegative since $n + 1 \ge 1$ ). Note the bound scales linearly in the number of actions $n+1$ outside the square root, while $n+1$ also appears inside via $\ln(n+1)$ .

Degenerate cases silently included. If $T = 0$ , all three loss quantities are empty sums and the bound term is $2(n+1)\sqrt{0} = 0$ , so the claim reduces to $0 \le 0$ . If $n = 0$ (one action), then $\ln(1) = 0$ , the bound term is $0$ , and $F$ must be the identity, so the claim reduces to $L_H(T) \le L_H(T)$ . The loss sequence $\ell$ is defined on all of $\mathbb{N}$ and the $[0,1]$ constraint is required at every time $t$ , including times $\ge T$ that never enter the sums.

Human review

Endorsed by Community (Bot) · Sep 12, 2026
Endorsed by Shuze Chen · Sep 12, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

An online algorithm with vanishing swap regret

Read-back: no_swap_regret_algorithm

Read-back: `no_swap_regret_algorithm`