Prove2Me
Navigate
MissionsFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Index policies are asymptotically separable (Thm. 7)

Proved
MarkovEntanglement.rmab_index_policy_entanglement_le_sqrt

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

Consider an NNN-agent restless multi-armed bandit: homogeneous agents sharing a local state space SSS and a pair of local kernels P0,P1P_0, P_1P0​,P1​, each agent choosing between idle and activate, and a budget that activates the fraction α\alphaα of the agents at every step. Fix an injective priority index ν\nuν and let π\piπ be the index policy it induces for the budget ⌊αN⌋\lfloor \alpha N \rfloor⌊αN⌋. Assume the two standard technical conditions, both stated for the explicit mean-field map of the configuration process at activation fraction α\alphaα — properties of the limit model, quantified before the constant and before NNN:

  1. Uniform global attractor property (UGAP): the map admits a fixed point m∗m^\astm∗ that attracts every initial configuration, uniformly in the initial point.
  2. Mean-field non-degeneracy: at m∗m^\astm∗ the budget runs out strictly inside some state, 0<α−∑νy>νxmy∗<mx∗0 < \alpha - \sum_{\nu_y > \nu_x} m^\ast_y < m^\ast_x0<α−∑νy​>νx​​my∗​<mx∗​, so the limiting policy genuinely randomises there.

Then there is a constant CCC, independent of NNN, such that for every stationary occupancy distribution μ1:Nπ\mu^\pi_{1:N}μ1:Nπ​ of the induced chain and every agent iii, the measure of Markov entanglement of the joint chain, with respect to the occupancy-weighted agent-wise total variation distance, satisfies

Ei(P1:Nπ)  ≤  CN.\mathcal{E}_i(P^\pi_{1:N}) \;\le\; \frac{C}{\sqrt{N}}.Ei​(P1:Nπ​)≤N​C​.

Index policies are therefore asymptotically separable: their joint transition matrix approaches the separable ones as the system grows, at rate 1/N1/\sqrt{N}1/N​.

The proof assembles the preceding milestones. Lemma 8 reduces the entanglement to the expected deviation E[∥m−m∗∥∞]\mathbb{E}[\|m - m^\ast\|_\infty]E[∥m−m∗∥∞​] of the configuration from the mean-field fixed point under the stationary distribution. Lemma 9 gives the per-step fluctuation of the configuration, of order 1/N1/\sqrt{N}1/N​. Lemma 10 propagates it over a horizon, and Lemma 11 supplies both a uniform horizon at which every trajectory has entered a neighbourhood of m∗m^\astm∗ and the contraction that stops the propagated error from compounding. What comes out is a stationary deviation of order 1/N1/\sqrt{N}1/N​ with a constant built from the local kernels, the priority index, the activation fraction and the contraction rate — none of which involve NNN.

Combined with the general decomposition bound of the companion mission, this yields Corollary 1: the value decomposition error of an index policy is sublinear in NNN.

The stationary distribution is assumed exchangeable — invariant under permuting the agents. The source's proof exchanges agent indices and asserts the stationary distribution is unchanged, which is exactly exchangeability; it holds automatically for the unique stationary distribution of an ergodic symmetric chain, but a reducible chain also has non-exchangeable stationary distributions concentrated on asymmetric closed classes, for which the agent-averaging step (and with it the stated bound) is not available. The hypothesis records precisely the consequence of ergodicity the argument uses.

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]

/-- Theorem 7 (Chen and Peng, Section 7.1, p. 24).  For an index policy satisfying the uniform
global attractor property and non-degeneracy there is a constant `C`, independent of `N`, with

`Eᵢ(P^π_{1:N}) ≤ C / √N`

for every agent `i`: the measure of Markov entanglement of the `N`-agent chain vanishes as the
system grows, so index policies are asymptotically separable.  The two technical conditions
are stated for the explicit mean-field map at the activation fraction `α` — properties of the
limit model, quantified before `C` and before `N`.  This is Lemma 8 combined with the `1/√N`
concentration of the configuration around the mean-field fixed point. -/
theorem rmab_index_policy_entanglement_le_sqrt
    (P0 P1 : Matrix S S ℝ) (hP0 : IsTransitionMatrix P0) (hP1 : IsTransitionMatrix P1)
    (ν : S → ℝ) (hν : Function.Injective ν) (α : ℝ) (hα : 0 < α) (hα1 : α < 1)
    (mstar : S → ℝ) (hmstar : IsConfiguration mstar)
    (hUGAP : IsUniformGlobalAttractor (meanFieldMap P0 P1 ν α) mstar)
    (hnd : IsNonDegenerateMeanField ν α mstar) :
    ∃ C : ℝ, 0 ≤ C ∧
      ∀ (N : ℕ), 0 < N →
        ∀ (π : (Fin N → S) → (Fin N → Bool) → ℝ),
          IsIndexPolicy ν ⌊α * (N : ℝ)⌋₊ π →
          ∀ (μ : Joint (StateAction (fun _ : Fin N => S) (fun _ : Fin N => Bool)) → ℝ),
            IsDist μ →
            IsExchangeableDist μ →
            IsStationary (inducedTransition
              (fun s a s' => ∏ j, rmabKernel P0 P1 (s j) (a j) (s' j)) π) μ →
            ∀ i : Fin N,
              entanglementN i μ (inducedTransition
                  (fun s a s' => ∏ j, rmabKernel P0 P1 (s j) (a j) (s' j)) π)
                ≤ C / Real.sqrt (N : ℝ) := by
  sorry

end MarkovEntanglement
Source
Shuze Chen and Tianyi Peng, 'Multi-agent Markov Entanglement', arXiv:2506.02385v3, Section 7.1, p. 24, Theorem 7
Read-back

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

Fix a finite type SSS with decidable equality (the per‑agent state space). The statement asserts, for every choice of the following data:

  • two matrices P0,P1∈RS×SP_0, P_1 \in \mathbb{R}^{S\times S}P0​,P1​∈RS×S, each assumed to be a transition matrix, i.e. Pk(x,y)≥0P_k(x,y)\ge 0Pk​(x,y)≥0 for all x,yx,yx,y and ∑yPk(x,y)=1\sum_{y} P_k(x,y)=1∑y​Pk​(x,y)=1 for every xxx (for k=0,1k=0,1k=0,1);
  • a function ν:S→R\nu : S \to \mathbb{R}ν:S→R (a priority index) assumed injective, so distinct states get distinct priorities;
  • a real number α\alphaα with 0<α0 < \alpha0<α and α<1\alpha < 1α<1;
  • a function m⋆:S→Rm^\star : S \to \mathbb{R}m⋆:S→R assumed to be a configuration, i.e. m⋆(x)≥0m^\star(x)\ge 0m⋆(x)≥0 for all xxx and ∑xm⋆(x)=1\sum_{x} m^\star(x) = 1∑x​m⋆(x)=1;

subject to two further hypotheses spelled out below, the following conclusion.

Hypothesis (uniform global attractor). Write, for a vector m:S→Rm : S\to\mathbb{R}m:S→R and x∈Sx\in Sx∈S,

Hν(m,x)  =  ∑ y : ν(x)<ν(y) m(y),Aν,α(m,x)  =  min⁡ ⁣(m(x),  max⁡(0,  α−Hν(m,x))),H_\nu(m,x) \;=\; \sum_{\,y \,:\, \nu(x)<\nu(y)\,} m(y),\qquad A_{\nu,\alpha}(m,x)\;=\;\min\!\big(m(x),\;\max(0,\;\alpha - H_\nu(m,x))\big),Hν​(m,x)=y:ν(x)<ν(y)∑​m(y),Aν,α​(m,x)=min(m(x),max(0,α−Hν​(m,x))),

and let φ\varphiφ be the map sending m:S→Rm : S\to\mathbb{R}m:S→R to the vector

φ(m)(y)  =  ∑x∈S[(m(x)−Aν,α(m,x)) P0(x,y)  +  Aν,α(m,x) P1(x,y)].\varphi(m)(y)\;=\;\sum_{x\in S}\Big[\big(m(x)-A_{\nu,\alpha}(m,x)\big)\,P_0(x,y)\;+\;A_{\nu,\alpha}(m,x)\,P_1(x,y)\Big].φ(m)(y)=x∈S∑​[(m(x)−Aν,α​(m,x))P0​(x,y)+Aν,α​(m,x)P1​(x,y)].

(This φ\varphiφ is defined on all of S→RS\to\mathbb{R}S→R, not just on the simplex, and does not involve NNN.) Let φt\varphi^tφt denote ttt‑fold iteration, with φ0(m)=m\varphi^0(m)=mφ0(m)=m, and let ∥v∥∞=sup⁡x∈S∣v(x)∣\lVert v\rVert_\infty = \sup_{x\in S}|v(x)|∥v∥∞​=supx∈S​∣v(x)∣. The hypothesis is the conjunction of:

  1. φ(m⋆)=m⋆\varphi(m^\star) = m^\starφ(m⋆)=m⋆ (as functions on SSS), and
  2. for every ε>0\varepsilon>0ε>0 there exists T∈NT\in\mathbb{N}T∈N such that for every t≥Tt\ge Tt≥T and every configuration mmm (i.e. every mmm with m(x)≥0m(x)\ge0m(x)≥0 for all xxx and ∑xm(x)=1\sum_x m(x)=1∑x​m(x)=1),   ∥φt(m)−m⋆∥∞<ε\;\lVert \varphi^t(m)-m^\star\rVert_\infty < \varepsilon∥φt(m)−m⋆∥∞​<ε.

Hypothesis (mean‑field non‑degeneracy). There exists a state x∈Sx\in Sx∈S with

0<m⋆(x),0<α−Hν(m⋆,x),α−Hν(m⋆,x)<m⋆(x).0 < m^\star(x),\qquad 0 < \alpha - H_\nu(m^\star,x),\qquad \alpha - H_\nu(m^\star,x) < m^\star(x).0<m⋆(x),0<α−Hν​(m⋆,x),α−Hν​(m⋆,x)<m⋆(x).

Conclusion. There exists a real number CCC with C≥0C \ge 0C≥0 such that for every natural number NNN with N>0N>0N>0, every function

π:(Fin N→S)  →  (Fin N→Bool)  →  R\pi : (\mathrm{Fin}\,N \to S) \;\to\; (\mathrm{Fin}\,N \to \mathrm{Bool}) \;\to\; \mathbb{R}π:(FinN→S)→(FinN→Bool)→R

satisfying the index‑policy property at budget M:=⌊αN⌋M := \lfloor \alpha N\rfloorM:=⌊αN⌋ (natural‑number floor of αN\alpha NαN; since 0<α<10<\alpha<10<α<1 and N≥1N\ge1N≥1 this lies in {0,1,…,N−1}\{0,1,\dots,N-1\}{0,1,…,N−1} and may be 000), and every function μ\muμ on Fin N→(S×Bool)\mathrm{Fin}\,N \to (S\times\mathrm{Bool})FinN→(S×Bool) satisfying three further properties, and every index i∈Fin Ni \in \mathrm{Fin}\,Ni∈FinN, the quantity EiE_iEi​ defined below satisfies

Ei  ≤  CN.E_i \;\le\; \frac{C}{\sqrt{N}}.Ei​≤N​C​.

The constant CCC is chosen before NNN, π\piπ, μ\muμ and iii, so it is uniform in all of them (it may depend on SSS, P0P_0P0​, P1P_1P1​, ν\nuν, α\alphaα, m⋆m^\starm⋆).

Unfolding the four properties and the quantity:

  • π\piπ is an index policy at budget MMM: (a) π(s,a)≥0\pi(s,a)\ge 0π(s,a)≥0 for all s∈SNs\in S^{N}s∈SN, a∈BoolNa\in\mathrm{Bool}^{N}a∈BoolN, and ∑a∈BoolNπ(s,a)=1\sum_{a\in\mathrm{Bool}^N}\pi(s,a)=1∑a∈BoolN​π(s,a)=1 for every sss; (b) for all s,as,as,a, if π(s,a)≠0\pi(s,a)\neq 0π(s,a)=0 then #{j:aj=true}=M\#\{j : a_j = \text{true}\} = M#{j:aj​=true}=M exactly; and (c) for every sss and every iii,
∑a∈BoolN1[ai=true]  π(s,a)  =  ρν,M(s,si),\sum_{a\in\mathrm{Bool}^N}\mathbf{1}[a_i=\text{true}]\;\pi(s,a)\;=\;\rho_{\nu,M}(s,s_i),a∈BoolN∑​1[ai​=true]π(s,a)=ρν,M​(s,si​),

where, with c(s,x)=#{j:sj=x}c(s,x)=\#\{j : s_j = x\}c(s,x)=#{j:sj​=x} and h(s,x)=∑y:ν(x)<ν(y)c(s,y)h(s,x)=\sum_{y:\nu(x)<\nu(y)} c(s,y)h(s,x)=∑y:ν(x)<ν(y)​c(s,y),

ρν,M(s,x)  =  {0if c(s,x)=0,min⁡(c(s,x),  M−˙h(s,x))c(s,x)otherwise,\rho_{\nu,M}(s,x)\;=\;\begin{cases}0 & \text{if } c(s,x)=0,\\[2pt] \dfrac{\min\big(c(s,x),\; M \dot- h(s,x)\big)}{c(s,x)} & \text{otherwise,}\end{cases}ρν,M​(s,x)=⎩⎨⎧​0c(s,x)min(c(s,x),M−˙​h(s,x))​​if c(s,x)=0,otherwise,​

and M−˙h(s,x)M \dot- h(s,x)M−˙​h(s,x) is truncated natural subtraction, equal to 000 whenever h(s,x)≥Mh(s,x)\ge Mh(s,x)≥M.

  • μ\muμ is a distribution: μ(p)≥0\mu(p)\ge 0μ(p)≥0 for every p∈(S×Bool)Np \in (S\times\mathrm{Bool})^{N}p∈(S×Bool)N and ∑pμ(p)=1\sum_{p}\mu(p)=1∑p​μ(p)=1. (Strict positivity is not required.)

  • μ\muμ is exchangeable: for every permutation σ\sigmaσ of Fin N\mathrm{Fin}\,NFinN and every p:Fin N→S×Boolp:\mathrm{Fin}\,N\to S\times\mathrm{Bool}p:FinN→S×Bool,   μ(p∘σ)=μ(p)\;\mu(p\circ\sigma)=\mu(p)μ(p∘σ)=μ(p).

  • μ\muμ is stationary for the induced chain. The induced chain is the matrix P\mathcal{P}P on the state‑action product space (S×Bool)N(S\times\mathrm{Bool})^{N}(S×Bool)N given by

P((s,a),(s′,a′))  =  (∏j=1NK(sj,aj,sj′))⋅π(s′,a′),K(x,b,y)={P1(x,y)b=trueP0(x,y)b=false,\mathcal{P}\big((s,a),(s',a')\big)\;=\;\Big(\prod_{j=1}^{N} K\big(s_j, a_j, s'_j\big)\Big)\cdot \pi(s',a'),\qquad K(x,b,y)=\begin{cases}P_1(x,y)&b=\text{true}\\ P_0(x,y)&b=\text{false,}\end{cases}P((s,a),(s′,a′))=(j=1∏N​K(sj​,aj​,sj′​))⋅π(s′,a′),K(x,b,y)={P1​(x,y)P0​(x,y)​b=trueb=false,​

where a point ppp of (S×Bool)N(S\times\mathrm{Bool})^N(S×Bool)N is read as the pair (s,a)(s,a)(s,a) with sj=(pj)1s_j=(p_j)_1sj​=(pj​)1​, aj=(pj)2a_j=(p_j)_2aj​=(pj​)2​; note the policy factor is evaluated at the destination pair (s′,a′)(s',a')(s′,a′), not the source. Stationarity is: for every qqq,   ∑pμ(p) P(p,q)=μ(q)\;\sum_{p}\mu(p)\,\mathcal{P}(p,q)=\mu(q)∑p​μ(p)P(p,q)=μ(q).

  • The bounded quantity EiE_iEi​ is the "agent‑iii entanglement" of μ\muμ and P\mathcal{P}P: the infimum (in R\mathbb{R}R) of the set
{ r∈R  :  ∃ Π∈R(S×Bool)×(S×Bool) a transition matrix, r=∑pμ(p)⋅12 ⁣ ⁣∑t∈S×Bool ⁣∣Pi(p,t)−Π(pi,t)∣},\Big\{\, r \in\mathbb{R} \;:\; \exists\, \Pi \in \mathbb{R}^{(S\times\mathrm{Bool})\times(S\times\mathrm{Bool})} \text{ a transition matrix, } r = \sum_{p}\mu(p)\cdot\tfrac12\!\!\sum_{t\in S\times\mathrm{Bool}}\!\big| \mathcal{P}_i(p,t) - \Pi(p_i,t)\big| \Big\},{r∈R:∃Π∈R(S×Bool)×(S×Bool) a transition matrix, r=p∑​μ(p)⋅21​t∈S×Bool∑​​Pi​(p,t)−Π(pi​,t)​},

where Pi(p,t)=∑q1[qi=t] P(p,q)\mathcal{P}_i(p,t)=\sum_{q}\mathbf{1}[q_i=t]\,\mathcal{P}(p,q)Pi​(p,t)=∑q​1[qi​=t]P(p,q) is the marginal one‑step law of coordinate iii from ppp, and "Π\PiΠ a transition matrix" means Π(u,v)≥0\Pi(u,v)\ge0Π(u,v)≥0 and ∑vΠ(u,v)=1\sum_v \Pi(u,v)=1∑v​Π(u,v)=1 for all uuu. In words: the smallest μ\muμ‑averaged total‑variation distance between agent iii's true marginal transition law and any single Markov kernel on S×BoolS\times\mathrm{Bool}S×Bool depending only on agent iii's own state‑action pair.

Degenerate cases the quantifiers silently include. If SSS is empty the configuration hypothesis ∑xm⋆(x)=1\sum_x m^\star(x)=1∑x​m⋆(x)=1 and the non‑degeneracy hypothesis (which asserts the existence of a state) cannot hold, so the hypotheses force SSS nonempty. For a given NNN the inner statement is vacuous if no π\piπ meets the index‑policy conditions at budget ⌊αN⌋\lfloor\alpha N\rfloor⌊αN⌋, or if no μ\muμ is simultaneously a distribution, exchangeable and stationary for P\mathcal{P}P; in particular the case M=0M=0M=0 (all ⌊αN⌋=0\lfloor\alpha N\rfloor = 0⌊αN⌋=0, e.g. N=1N=1N=1) is included, where the budget condition forces π\piπ to be supported on the all‑false action profile. The bound is stated with ≤\le≤, not <<<, and asserts only C≥0C\ge0C≥0, not C>0C>0C>0. The infimum defining EiE_iEi​ is the real infimum of the displayed set, taken over transition matrices on the full pair space S×BoolS\times\mathrm{Bool}S×Bool (not on SSS alone). Finally, N\sqrt{N}N​ is the real square root of NNN, positive since N>0N>0N>0, so the right‑hand side is an ordinary quotient.

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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactJoin Slack© 2026 Prove2Me