Entanglement is bounded by the configuration's deviation (Lem. 2 / 8)
ProvedMarkovEntanglement.rmab_entanglement_le_configuration_deviationConsider an -agent restless multi-armed bandit under an index policy with injective priority index and budget , and let be a stationary occupancy distribution of the induced chain. Let be a configuration (a point of the simplex) — in the application, the mean-field fixed point.
Then for every agent the measure of Markov entanglement of the joint chain, with respect to the occupancy-weighted agent-wise total variation distance, is bounded by the expected deviation of the system configuration from :
the expectation taken over the stationary occupancy measure.
This is where Proposition 1 is cashed in. Proposition 1 bounds the entanglement of a weakly-coupled system by the occupancy-weighted distance between the realised policy's per-agent marginal and any local policy; here the local policy chosen as witness is the mean-field limiting policy at , which activates an agent in state with the probability the index policy would allot at the configuration . Homogeneity of the agents makes the mismatch the same for every agent, so the supremum over may be replaced by an average, and the average collapses into a sum over local states weighted by the configuration. The remaining per-state estimate compares the fraction the index policy actually activates in state with the fraction it would activate at ; both are ratios of a budget residual to a state occupancy, and both numerator and denominator move by at most , which gives the stated bound.
With this lemma the asymptotic analysis reduces entirely to a question about the configuration process: how far does stray from the mean-field fixed point under the stationary distribution?
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.
import Mathlib import Definitions.Def_markov_entanglement_meanfield open scoped BigOperators open MarkovEntanglement
namespace MarkovEntanglement
variable {S : Type*} [Fintype S] [DecidableEq S]
/-- Lemma 2 / Lemma 8. For an index policy, the measure of Markov entanglement of any agent,
with respect to the occupancy-weighted agent-wise total variation distance, is bounded by the
expected deviation of the system configuration from the mean-field fixed point:
`Eᵢ(P^π_{1:N}) ≤ |S|² · E[‖m − m✦‖_∞]`,
the expectation taken over the stationary occupancy measure. This is where Proposition 1 is
cashed in: the local policy witnessing the bound is the mean-field limiting policy at `m✦`. -/
theorem rmab_entanglement_le_configuration_deviation
(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)
(N : ℕ) (hN : 0 < N)
(π : (Fin N → S) → (Fin N → Bool) → ℝ)
(hπ : IsIndexPolicy ν ⌊α * (N : ℝ)⌋₊ π)
(μ : Joint (StateAction (fun _ : Fin N => S) (fun _ : Fin N => Bool)) → ℝ)
(hμ : IsDist μ) (hexch : IsExchangeableDist μ)
(hstat : 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)) π)
≤ (Fintype.card S : ℝ) ^ 2 *
∑ p : Joint (StateAction (fun _ : Fin N => S) (fun _ : Fin N => Bool)),
μ p * supNorm (fun x => configuration (fun j => (p j).1) x - mstar x) := by
sorry
/-! ### M4 — Lemma 9, one-step concentration (Gast, Gaujal and Yan) -/
end MarkovEntanglementRead-back
What the Lean code literally says, in plain math · claude-opus-5
Fix a finite type with decidable equality (its cardinality is ), and write for the -element index type . The statement asserts: for every choice of the following data, satisfying all of the listed hypotheses, the displayed inequality holds.
Data and hypotheses.
- Two real matrices indexed by , each a transition matrix: and for every , and likewise for .
- A function that is injective.
- A real number with .
- A function that is a configuration: for all and . (No relation whatsoever is assumed between and , or the dynamics below; it is an arbitrary probability vector on .)
- A natural number with . Set , the natural-number floor (so whenever , e.g. when ).
- A function assigning to each joint state and each joint action (each a Boolean) a real number, subject to the three conditions of being an index policy for with budget :
- for all , and for every ;
- for all : if then is exactly -budgeted, i.e. (equality, not );
- for every joint state and every agent , the marginal probability that agent is activated,
equals $\mathrm{iap}_\nu^M(s, s_j)$, where for $x \in S$ one writes $c_s(x) := \#\{k \in [N] : s_k = x\}$ (the count of agents in state $x$), $h_s(x) := \sum_{y : \nu(x) < \nu(y)} c_s(y)$ (the number of agents in strictly higher-$\nu$ states), and
with $\dot-$ denoting **truncated natural-number subtraction** (so $M \dot- h_s(x) = 0$ when $h_s(x) \ge M$).
- A function on the joint state–action space — i.e. assigns a real number to each tuple where — such that:
- for all and ;
- is exchangeable: for every permutation of and every ;
- is stationary for the matrix on defined by
where $K(x,a,y) = P^1_{x y}$ if $a = \mathrm{true}$ and $K(x,a,y) = P^0_{x y}$ if $a = \mathrm{false}$; stationarity meaning $\sum_{p \in \Omega} \mu(p)\, T(p,q) = \mu(q)$ for every $q \in \Omega$. (Note the next action in $q$ is drawn by $\pi$ from the *next* state in $q$, and $T$ is not itself asserted to be a transition matrix.)
- A distinguished agent index .
Conclusion. With as above,
where is the state part of , the inner quantity is the empirical configuration (fraction of the agents whose state is , a real division by ), the supremum is the supremum over of (a maximum, since is finite and, as noted below, nonempty), and is the square of the real cast of the cardinality of . The left-hand side is the agent- entanglement, defined as the real infimum
Here the competitor ranges over all matrices indexed by the pair space (agent 's local coordinate is a state–action pair, not a state) whose entries are nonnegative with each row summing to ; is not required to arise from or in any way. The quantity is agent 's marginal one-step weight from the joint point to the local pair .
Degenerate and edge cases silently included. may be , in which case (since ), so every action profile carrying positive -mass activates exactly zero agents and is identically ; more generally is truncated at . cannot be empty: with an empty makes empty and , so the hypothesis that is a distribution is unsatisfiable there — the statement is vacuous for empty . The set whose infimum defines is nonempty and bounded below by , so the infimum is the ordinary real infimum. The hypotheses on and on (index policy, distribution, exchangeability, stationarity for ) are assumptions only; the statement makes no claim that such or exist for given , and if for some data no such or exists the assertion is vacuously true for that data. The hypotheses of injectivity of , of , and that is a configuration are assumed but the right-hand side depends on only through the displayed deviation; nothing forces to be a fixed point of any mean-field map, and nothing forces to be large — the bound is claimed for every .
Confirmed by the mission captain (proposal self-audit).