One-step concentration of the configuration (Lem. 9, Gast et al. 2024)

Proved

MarkovEntanglement.rmab_one_step_concentration

by tianyipeng · Aug 28, 2026 · Mathlib c5ea003 (Lean v4.30.0)

Consider one step of the $N$ -agent restless-bandit chain under an index policy, started from an arbitrary joint state $s$ , and let $\varphi$ be the explicit mean-field map of the configuration, taken at the exact activation fraction $\lfloor \alpha N \rfloor / N$ of the $N$ -agent system. Writing $\epsilon[1] = m[1] - \varphi(m[0])$ for the one-step deviation of the configuration from its mean-field image,

\mathbb{E}\big[\|\epsilon[1]\|_1 \;\big|\; m[0]\big] \;\le\; \sqrt{\frac{|S|}{N}}.

The mechanism is the usual $1/\sqrt{N}$ of an average of $N$ indicators. Conditionally on the current joint state, the index policy activates a deterministic number of agents in each local state — only which agents is random, and the agents in a state are exchangeable — so the next local states are an independent family: for each local state $x$ , a fixed number of draws from $P_1(x, \cdot)$ and a fixed number from $P_0(x,\cdot)$ . The next configuration is their average, its mean is exactly $\varphi(m[0])$ by definition of the mean-field map, and each coordinate has variance at most $1/N$ times its mean. Bounding each $\mathbb{E}|\epsilon_x|$ by the standard deviation and then summing over $x$ with Cauchy–Schwarz produces $\sqrt{|S|/N}$ .

This is the input that fixes the rate in Theorem 7: everything downstream amplifies it by constants that do not depend on $N$ .

Preamble

import Mathlib
import Definitions.Def_markov_entanglement_meanfield

open scoped BigOperators
open MarkovEntanglement

Formal statement

namespace MarkovEntanglement

variable {S : Type*} [Fintype S] [DecidableEq S]

/-- Lemma 9 (One-step Concentration; Lemma 1 of Gast, Gaujal and Yan 2024).  Starting from any
joint state, the configuration after one step deviates from its mean-field image by at most
`√(|S| / N)` in expected `ℓ¹` norm:

`E[‖m[1] − φ(m[0])‖₁ ∣ m[0]] ≤ √(|S| / N)`.

The expectation is over one step of the `N`-agent chain, the mean-field map is the explicit
one at the exact activation fraction `⌊αN⌋ / N` of the `N`-agent system, and the rate is the
usual `1/√N` of an average of `N` conditionally independent indicators. -/
theorem rmab_one_step_concentration
    (P0 P1 : Matrix S S ℝ) (hP0 : IsTransitionMatrix P0) (hP1 : IsTransitionMatrix P1)
    (ν : S → ℝ) (α : ℝ) (N : ℕ) (hN : 0 < N)
    (π : (Fin N → S) → (Fin N → Bool) → ℝ)
    (hπ : IsIndexPolicy ν ⌊α * (N : ℝ)⌋₊ π)
    (s : Fin N → S) :
    ∑ s' : Fin N → S, rmabStep P0 P1 π s s' *
        l1Norm (fun x => configuration s' x
          - meanFieldMap P0 P1 ν ((⌊α * (N : ℝ)⌋₊ : ℝ) / (N : ℝ)) (configuration s) x)
      ≤ Real.sqrt ((Fintype.card S : ℝ) / (N : ℝ)) := by
  sorry

/-! ### M5 — Lemma 10, multi-step concentration (Gast, Gaujal and Yan) -/

end MarkovEntanglement

Source

Nicolas Gast, Bruno Gaujal and Chen Yan, 'Reoptimization nearly solves weakly coupled Markov decision processes' (2024), Lemma 1; cited as Lemma 9 in Chen and Peng, arXiv:2506.02385v3, Appendix I, p. 43

Read-back

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

$\newcommand{\Fin}{\mathrm{Fin}}$ For every type $S$ carrying a finiteness structure and decidable equality (both implicit, so $S$ ranges over all finite types, the empty one included), for all matrices $P_0,P_1 \in \mathbb{R}^{S\times S}$ , every function $\nu : S \to \mathbb{R}$ , every real number $\alpha$ , every natural number $N$ , every function $\pi : S^{\{0,\dots,N-1\}} \to \{\mathrm{false},\mathrm{true}\}^{\{0,\dots,N-1\}} \to \mathbb{R}$ , and every tuple $s = (s_0,\dots,s_{N-1}) \in S^N$ , the statement asserts the displayed inequality below under the following hypotheses. Write $M := \lfloor \alpha N \rfloor_{\mathbb{N}}$ for the natural-number floor of the real number $\alpha \cdot N$ — this is the greatest natural number $\le \alpha N$ , and it is $0$ whenever $\alpha N < 0$ ; nothing in the statement constrains $\alpha$ to lie in $[0,1]$ , so $M$ may be $0$ or may exceed $N$ . For a tuple $u \in S^N$ and $x \in S$ put $n_u(x) := \#\{i : u_i = x\}$ (a natural number) and $c_u(x) := n_u(x)/N$ (a real quotient; $N \neq 0$ is guaranteed by hypothesis (c) below). The hypotheses are:

(a) $P_0$ has all entries $\ge 0$ and each of its rows sums to $1$ : $\sum_{j \in S} P_0(i,j) = 1$ for every $i$ .
(b) $P_1$ likewise has all entries $\ge 0$ and every row summing to $1$ .
(c) $0 < N$ .
(d) $\pi$ $π$ is an index policy for the priority function $\nu$ $ν$ at budget $M$ $M$ , meaning all three of:
- $\pi(u,a) \ge 0$ for all $u \in S^N$ and all action profiles $a \in \{\mathrm{false},\mathrm{true}\}^N$ , and $\sum_{a \in \{\mathrm{false},\mathrm{true}\}^N} \pi(u,a) = 1$ for every $u$ ;
- for all $u$ and $a$ , if $\pi(u,a) \neq 0$ then $a$ is exactly budgeted: $\#\{i : a_i = \mathrm{true}\} = M$ ;
- for every $u \in S^N$ and every index $i$ , the marginal probability that agent $i$ is activated, $\sum_{a \in \{\mathrm{false},\mathrm{true}\}^N} [\,a_i = \mathrm{true}\,]\,\pi(u,a)$ , equals $q_\nu^M(u, u_i)$ , where for $x \in S$

q_\nu^M(u,x) := \begin{cases} 0 & \text{if } n_u(x) = 0,\\[4pt] \dfrac{\min\!\big(n_u(x),\; M \dot- h_\nu(u,x)\big)}{n_u(x)} & \text{otherwise,}\end{cases} \qquad h_\nu(u,x) := \sum_{y \,:\, \nu(x) < \nu(y)} n_u(y),

with $\dot-$ denoting **truncated natural-number subtraction** (so $M \dot- h_\nu(u,x) = 0$ whenever $h_\nu(u,x) \ge M$), the numerator being cast to $\mathbb{R}$ after the truncated subtraction and the minimum, and the comparison $\nu(x) < \nu(y)$ being strict (ties in $\nu$ contribute nothing to $h_\nu$; $\nu$ is not assumed injective).

Under these hypotheses the conclusion is the single inequality

\sum_{s' \in S^N} \left(\sum_{a \in \{\mathrm{false},\mathrm{true}\}^N} \pi(s,a)\prod_{j=0}^{N-1} K_{a_j}\!\left(s_j, s'_j\right)\right)\cdot\left(\sum_{x \in S}\Big|\,c_{s'}(x) \;-\; \Phi\big(c_s\big)(x)\,\Big|\right) \;\le\; \sqrt{\frac{|S|}{N}},

where $K_{\mathrm{true}} := P_1$ and $K_{\mathrm{false}} := P_0$ ; the outer sum runs over all $|S|^N$ tuples $s'$ ; $|S|$ is the cardinality of $S$ ; $\sqrt{\cdot}$ is the total real square root; and $\Phi$ is the mean-field map at activation fraction $\alpha' := M/N = \lfloor \alpha N\rfloor_{\mathbb{N}}/N$ (a nonnegative real, not $\alpha$ itself), defined for an arbitrary $m : S \to \mathbb{R}$ by

\Phi(m)(y) := \sum_{x \in S}\Big[\big(m(x) - f(m,x)\big)\,P_0(x,y) \;+\; f(m,x)\,P_1(x,y)\Big],\qquad f(m,x) := \min\!\Big(m(x),\; \max\big(0,\; \alpha' - \textstyle\sum_{y \,:\, \nu(x)<\nu(y)} m(y)\big)\Big).

Note that $\Phi$ is applied only to the particular argument $c_s$ , the empirical configuration of the given starting tuple $s$ ; the left-hand side is a single weighted average of $\ell^1$ distances taken over one step from that fixed $s$ , not a supremum over starting tuples, not an iterate, and not a statement about any stationary or limiting object. The quantities in the bracketed weight are exactly the sum over joint action profiles of $\pi(s,a)$ times the product over the $N$ agents of the corresponding one-agent transition probability; the statement does not separately assume this weight is nonnegative or sums to $1$ over $s'$ — that is left to follow, or not, from (a), (b), (d). Degenerate instances silently included: $|S| = 1$ ; $S$ empty, in which case for $N \ge 1$ there is no tuple $s$ at all and the claim is vacuous for that $S$ ; $M = 0$ (which forces $\pi(u,a) = 0$ unless $a$ is all- $\mathrm{false}$ , and makes $q_\nu^M \equiv 0$ and $f \equiv 0$ ); $M > N$ , in which case no action profile can satisfy $\#\{i : a_i = \mathrm{true}\} = M$ , so the second and first clauses of (d) are jointly unsatisfiable and hypothesis (d) is impossible to meet for such $\alpha, N$ ; and $\alpha < 0$ , which collapses to the $M = 0$ case. The inequality is non-strict ( $\le$ ), and both the truncated $M \dot- h_\nu(u,x)$ in the discrete activation probability and the $\max(0,\cdot)$ in the continuum $f(m,x)$ floor their arguments at zero.

Human review

Endorsed by Shuze Chen · Aug 30, 2026
Endorsed by tianyipeng · Aug 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph