The mean-field limit of a restless bandit
Definitionmarkov_entanglement_meanfieldmarkov_entanglement_rmab characterises the mean-field map only through the configurations that an actual -agent system can occupy — the points of the simplex whose coordinates are multiples of . That is enough to state the asymptotic theorems, but not to reason about as a map on the simplex: the stability analysis of Gast, Gaujal and Yan differentiates , iterates it and takes its spectral radius, all of which need defined everywhere.
This layer supplies the missing continuum objects.
The mean-field map on the whole simplex. Under an index policy with priority and activation fraction , the mass sitting in a local state splits into an activated part and an idle part. The activated part is whatever is left of the budget after every strictly higher-priority state has been served, capped by the mass actually in and floored at zero:
and each part then moves by its own kernel:
No appears, which is exactly the point: it is the fixed activation fraction that makes the map independent of the system size. The companion theorem meanFieldMap_isMeanFieldMap checks that this formula agrees with the -agent characterisation whenever , so the two descriptions are the same map.
The priority regions. The configuration lies in the priority region of the state when is the state the budget runs out in, . These regions cover the simplex, and is affine on each of them — the content of Lemma 7.
The limiting local policy. The activated mass in as a fraction of the mass in is the probability with which the mean-field limiting policy activates an agent in state . This is the local policy that the index policy converges to, and the one the local chains in the value decomposition are built from.
The finite-horizon law of the process. One step of the -agent joint state chain draws the joint action from the policy and then moves the agents independently through their own kernels; iterating gives the law after steps. The concentration lemmas are statements about this law, expressed as finite sums rather than measure-theoretically.
Distributions, norms, non-degeneracy and stability. A plain distribution predicate (nonnegative, summing to one): the stationary occupancy of an index policy vanishes on every non-budgeted action profile, so the strictly positive predicate of the two-agent development is unsatisfiable here — every -weighted quantity downstream is stated with products rather than divisions, so nothing needs positivity. The norm on configurations, in which the one-step concentration bound is stated (the bounds reuse supNorm from the previous layer). The continuum form of non-degeneracy: the budget runs out strictly inside some state at , placing the fixed point in the interior of its priority region — the per- form cannot hold at every simultaneously (at the budget floors to zero). And stability on the tangent space: the affine piece at the fixed point is determined by the dynamics only up to the rank-one gauge , which moves the spectrum but acts trivially on zero-sum vectors, so the well-posed notion is geometric contraction of 's powers on the differences .
import Definitions.Def_markov_entanglement_rmab
open scoped BigOperators
namespace MarkovEntanglement
/-! ## The mean-field limit of a restless bandit
`Def_markov_entanglement_rmab` characterises the mean-field map `φ` only through the
configurations that an actual `N`-agent system can occupy — the points of the simplex whose
coordinates are multiples of `1/N`. That is enough to *state* the asymptotic theorems, but
not to reason about `φ` as a map on the simplex: the stability analysis of Gast et al.
differentiates `φ`, iterates it and takes its spectral radius, all of which need `φ` defined
everywhere.
This layer supplies the missing continuum objects. It gives an explicit formula for the
mean-field map on the whole simplex, and `meanFieldMap_isMeanFieldMap` checks that the
formula agrees with the characterisation of the previous layer on every configuration a real
system can occupy — so the two descriptions are the same map, and the asymptotic theorems may
be proved about the explicit one.
It also supplies the finite-horizon law of the configuration process, which the concentration
lemmas are statements about, and the two norms those lemmas use. -/
variable {S : Type*} [Fintype S] [DecidableEq S]
/-- The fraction of agents sitting in states of strictly higher priority than `x`. This is
the continuum counterpart of `higherPriorityCount`. -/
noncomputable def higherPriorityMass (ν : S → ℝ) (m : S → ℝ) (x : S) : ℝ :=
∑ y ∈ Finset.univ.filter fun y => ν x < ν y, m y
/-- The fraction of the whole population that an index policy activates out of state `x`:
whatever is left of the budget `α` after every strictly higher-priority state has been served,
capped by the mass actually sitting in `x` and floored at zero. This is the continuum
counterpart of `activateCount / N`. -/
noncomputable def activateFraction (ν : S → ℝ) (α : ℝ) (m : S → ℝ) (x : S) : ℝ :=
min (m x) (max 0 (α - higherPriorityMass ν m x))
/-- The **mean-field transition map** on the whole simplex: the mass in each state splits into
the part that is activated and the part that is not, each moving by its own kernel. Note that
`N` does not occur — it is the fixed activation *fraction* `α` that makes this possible. -/
noncomputable def meanFieldMap (P0 P1 : Matrix S S ℝ) (ν : S → ℝ) (α : ℝ)
(m : S → ℝ) : S → ℝ := fun y =>
∑ x, ((m x - activateFraction ν α m x) * P0 x y + activateFraction ν α m x * P1 x y)
/-- The **priority region** of the state `x`: the configurations at which `x` is the marginal
state, the one the budget runs out in. These `|S|` regions cover the simplex, and the
mean-field map is affine on each of them. -/
def IsPriorityRegion (ν : S → ℝ) (α : ℝ) (m : S → ℝ) (x : S) : Prop :=
higherPriorityMass ν m x ≤ α ∧ α < higherPriorityMass ν m x + m x
/-- The probability that the **mean-field limiting policy** at the configuration `m` activates
an agent sitting in state `x`: the activated mass in `x` as a fraction of the mass in `x`.
This is the local policy that the index policy converges to, and the one the local chains in
the decomposition are built from. -/
noncomputable def meanFieldActivationProb (ν : S → ℝ) (α : ℝ) (m : S → ℝ) (x : S) : ℝ :=
if m x = 0 then 0 else activateFraction ν α m x / m x
/-- The mean-field limiting policy as a local policy on `S × Bool`. -/
noncomputable def meanFieldLocalPolicy (ν : S → ℝ) (α : ℝ) (m : S → ℝ)
(x : S) (a : Bool) : ℝ :=
if a then meanFieldActivationProb ν α m x else 1 - meanFieldActivationProb ν α m x
/-- One step of the `N`-agent joint state chain under a policy: the agents draw their actions
jointly from `π` and then move independently through their own kernels. -/
noncomputable def rmabStep {N : ℕ} (P0 P1 : Matrix S S ℝ)
(π : (Fin N → S) → (Fin N → Bool) → ℝ) (s s' : Fin N → S) : ℝ :=
∑ a : Fin N → Bool, π s a * ∏ j, rmabKernel P0 P1 (s j) (a j) (s' j)
/-- The law of the joint state after `t` steps from a fixed start. -/
noncomputable def rmabLaw {N : ℕ} (P0 P1 : Matrix S S ℝ)
(π : (Fin N → S) → (Fin N → Bool) → ℝ) (s0 : Fin N → S) : ℕ → (Fin N → S) → ℝ
| 0, s => if s = s0 then 1 else 0
| (t + 1), s' => ∑ s, rmabLaw P0 P1 π s0 t s * rmabStep P0 P1 π s s'
/-- The `ℓ¹` norm on configurations, the one the one-step concentration bound is stated in.
The `ℓ∞` bounds reuse `supNorm` from the previous layer, so that they speak the same language
as the uniform global attractor property. -/
noncomputable def l1Norm (v : S → ℝ) : ℝ := ∑ x, |v x|
/-- A plain distribution: nonnegative weights summing to one. The stationary occupancy of an
index policy vanishes on every non-budgeted action profile, so the strictly positive
`IsPositiveDist` of the two-agent development is unsatisfiable for the chains this theory is
about, and the asymptotic statements use this weaker form. Every `μ`-weighted quantity
downstream (`muNorm`, `muAgentTVDistN`, `entanglementN`, `IsLocalTransitionN`) is already
stated with products rather than divisions, so nothing needs the weights to be positive. -/
def IsDist {ι : Type*} [Fintype ι] (μ : ι → ℝ) : Prop :=
(∀ p, 0 ≤ μ p) ∧ ∑ p, μ p = 1
/-- A distribution over joint objects of `N` homogeneous agents is **exchangeable** when it
is invariant under permuting the agents. The agents of a restless bandit are homogeneous and
the induced chain is symmetric, so its ergodic stationary distribution is exchangeable — and
exchangeability is the exact consequence the asymptotic arguments use: it is what lets a
per-agent quantity be replaced by its average over the agents, turning agent-indexed sums
into configuration-weighted ones. A reducible chain also has non-exchangeable stationary
distributions concentrated on asymmetric closed classes, which is why the asymptotic
statements carry this as a hypothesis rather than deriving it. -/
def IsExchangeableDist {N : ℕ} {X : Type*} [Fintype X] (μ : (Fin N → X) → ℝ) : Prop :=
∀ σ : Equiv.Perm (Fin N), ∀ p : Fin N → X, μ (p ∘ σ) = μ p
/-- **Non-degeneracy in the mean-field limit** (the continuum form of Assumption 2): at
`m✦` some state is served only fractionally — the budget runs out strictly inside it, so the
limiting policy genuinely randomises there. The strict inequalities place `m✦` in the
interior of its priority region, which is what makes the mean-field map genuinely affine in a
neighbourhood of the fixed point. The per-`N` form `IsNonDegenerate` of the previous layer
cannot hold at every `N` simultaneously (at `N = 1` the budget floors to `0`), so the
asymptotic statements use this `N`-free form. -/
def IsNonDegenerateMeanField (ν : S → ℝ) (α : ℝ) (mstar : S → ℝ) : Prop :=
∃ x : S, 0 < mstar x ∧ 0 < α - higherPriorityMass ν mstar x ∧
α - higherPriorityMass ν mstar x < mstar x
/-- A matrix is **stable on the tangent space** of the simplex when its powers contract
zero-sum row vectors geometrically. The affine piece `K` of the mean-field map at the fixed
point is determined by the dynamics only up to the rank-one gauge `K ↦ K + 𝟙 cᵀ` (a constant
row shift, absorbed by the affine offset `b`), and that gauge moves the spectrum; what is
well defined — and what the stability analysis actually uses — is the action of `K` on the
differences `m − m✦`, which sum to zero. Geometric decay of the powers on that subspace is
the finite-dimensional meaning of "the spectral radius of the linearised dynamics is `< 1`". -/
def IsStableOnTangent (K : Matrix S S ℝ) : Prop :=
∃ C ρ : ℝ, 0 ≤ C ∧ 0 ≤ ρ ∧ ρ < 1 ∧
∀ v : S → ℝ, (∑ x, v x) = 0 → ∀ t : ℕ,
supNorm (Matrix.vecMul v (K ^ t)) ≤ C * ρ ^ t * supNorm v
end MarkovEntanglementRead-back
What the Lean code literally says, in plain math · claude-opus-5
higherPriorityMass — For an arbitrary finite type (no further structure assumed) this defines a real number from three inputs: a "priority" function , a "mass" function , and a point . Its value is
i.e. the sum of over exactly those whose priority is strictly greater than the priority of . Ties () are excluded, and in particular itself never contributes. Nothing requires to be nonnegative, to sum to , or to be a distribution of any kind, and nothing requires to be injective; may take negative values and the sum may be negative. If no has strictly larger priority the sum is over the empty set and the value is ; if is empty the function has no arguments to be applied to.
activateFraction — For a finite type , priorities , a real scalar , a mass function and a point , this is the real number
where is the total mass carried by states of strictly higher priority than . So one takes the "budget left over after all strictly higher-priority states are served", , truncates it below at , and then caps it at . There is no hypothesis that , that , or that : if the outer minimum returns itself, so the value is then negative rather than lying in ; if the value is .
meanFieldMap — Given a finite type , two arbitrary real square matrices indexed by (no stochasticity, nonnegativity, or row-sum hypothesis is imposed on either), priorities , a real scalar , and a mass function , this produces a new function whose value at is
where is the clamped leftover-budget quantity described above. That is, at each source state the mass is split into an "active" part pushed through and a "passive" remainder pushed through , and the contributions are summed over all . Nothing constrains to be a probability vector, so the passive remainder and the output need not be nonnegative. If is empty, the result is the empty function and every such sum is .
IsPriorityRegion — This is a proposition (not a number) about a finite type , priorities , a real scalar , a mass function , and a point . It asserts the conjunction of two inequalities:
where is the mass of strictly-higher-priority states. Equivalently, lies in the half-open interval — closed on the left with a non-strict , open on the right with a strict . Note that the two conditions can only both hold if ; for the interval is empty and the proposition is unsatisfiable for that . No hypotheses are placed on , , or .
meanFieldActivationProb — For a finite type , priorities , a real scalar , a mass function , and a point , this is the real number defined by cases: it equals when , and otherwise equals the ratio
The branch is a stipulated value, chosen to avoid division by zero rather than derived. Despite the name, nothing forces this quantity into : it is a ratio of two unconstrained reals, and when the numerator equals , making the value exactly . No hypothesis states that is nonnegative or a distribution, or that .
meanFieldLocalPolicy — For a finite type , priorities , a real , a mass function , a state and a Boolean , this is the real number
where is the quantity of the previous declaration: if , and otherwise, with . By construction the two values sum to for every , but there is no hypothesis making either of them nonnegative or at most ; the action set is the two-element Boolean type.
rmabStep — Fix a natural number (which may be ), a finite type with decidable equality, and two arbitrary real matrices (no row-stochasticity or nonnegativity assumed). Given an arbitrary real-valued function of a joint state (a function ) and a joint action — with no hypothesis that is nonnegative, normalized, or budget-respecting — and given joint states , this defines
The sum ranges over all Boolean tuples and the product over all coordinates, so the per-arm transitions are taken to be conditionally independent given the action. In the degenerate case there is exactly one (empty) action tuple and the empty product is , so the value reduces to for the unique empty state tuples.
rmabLaw — Fix , a finite type with decidable equality, arbitrary real matrices , an arbitrary real-valued function on (joint state, joint action) pairs with no assumption that it is a probability distribution, and an initial joint state . This defines, by recursion on a time index , a real-valued function on joint states:
where with and . So is the point mass (as an indicator function) at and each subsequent time step is left-multiplication of the current row vector by the one-step matrix. Since no positivity or normalization hypotheses are present on , , or , the values are arbitrary reals and need not be nonnegative or sum to . The sums range over the full finite set of joint states; when this set is a single point.
l1Norm — For a finite type and an arbitrary function , this is the real number , the sum of absolute values of the coordinates over all of . If is empty the value is . No normalization or sign hypothesis is placed on .
IsDist — For an arbitrary finite type and an arbitrary function , this is the proposition asserting both of:
That is, is pointwise nonnegative and its total mass over the whole index type is exactly . Note that when is empty the sum is , so the proposition is unsatisfiable in that case. The index type here is a fresh type variable independent of the ambient .
IsExchangeableDist — For a natural number , an arbitrary finite type , and an arbitrary function defined on tuples , this is the proposition
quantifying over all permutations of the index set and all tuples ; is the tuple whose -th entry is . This asserts only permutation-invariance of the function ; despite the name, nothing here requires to be nonnegative or to sum to , so any constant function — including the zero function — satisfies it. When there is a single tuple and a single permutation and the condition holds trivially.
IsNonDegenerateMeanField — For a finite type , priorities , a real scalar , and a function , this is the proposition that there exists a state satisfying all three of:
where is the total -mass of the states with strictly higher priority than . Equivalently: some state carries strictly positive mass and the residual budget at that state lies strictly between and — both endpoints excluded. Existence, not uniqueness, is asserted; no hypothesis says is a distribution, is nonnegative, or is a fixed point of anything, and no hypothesis constrains . If is empty the proposition is false.
IsStableOnTangent — For a finite type and an arbitrary real square matrix indexed by (with no stochasticity, nonnegativity, or symmetry hypothesis), this is the proposition that there exist real numbers and such that
and such that for every vector whose coordinates sum to zero, , and for every natural number (including ),
where denotes the row-vector-times-matrix product, i.e. the function , with the -th matrix power ( being the identity matrix), and where denotes the supremum over the finite index type (for empty this supremum is by the convention for the supremum of an empty set of reals). The bound is a non-strict , the decay rate satisfies a strict but is allowed to be , and is . Because the case is included, the condition at reads for all zero-sum . The zero vector always satisfies the zero-sum hypothesis; if is empty, or more generally if the only zero-sum vector considered is , the universally quantified condition is satisfiable trivially.
Confirmed by the mission captain (proposal self-audit).