All missions

Repair facilities and the value of emergency repairs

A firm that maintains capital goods (aircraft, medical scanners, lithography machines) keeps spare parts and runs a repair shop. When a part fails, it is replaced from stock if possible. Otherwise a machine waits, and the firm pays a backorder cost. The firm must choose how many spares of each part type to hold, which failed part to repair next, and when to pay for an outside emergency repair. Özkan and van Houtum study this joint control problem in the heavy-traffic regime of a closed repairable-parts network (SSRN 3784144; published later in Operations Research). This mission works from the SSRN copy.

The limiting problem is solved exactly, and the answer is a decision rule: emergency repairs are worth using exactly when the least backorder saving per unit of repair time exceeds the least emergency cost per unit of repair time.

Setting

There are $n\ge1$ part types (SKUs), with repair rates $\mu_i>0$, limiting breakdown rates $\lambda_i>0$, costs $b_i,c_i,h_i>0$, a drift $\theta\le0$ and a variance $\Sigma>0$. Let $X$ be a Brownian motion with drift $0$ and variance $\Sigma$, started at $0$. An inventory vector $S\in\mathbb R^n_+$ is fixed.

The equivalent workload formulation (EWF) chooses a workload $W\ge0$, an idleness process $I$, an emergency repair process $E$, and an allocation $a(t)\in\mathcal A(W(t))$, where

$$\mathcal A(w)=\Big\{q\in\mathbb R^n_+:\sum_i q_i/\mu_i=w\Big\},$$

subject to

$$W(t)=X(t)+\theta t-\sum_i\frac{\lambda_i}{\mu_i}\int_0^t(a_i(s)-S_i)^+\,ds+I(t)-E(t).$$

The processes $I$ and $E$ start at $0$, are nondecreasing, càdlàg and adapted. Write $b_j\mu_j/\lambda_j=\min_i b_i\mu_i/\lambda_i$ and $c_k\mu_k=\min_i c_i\mu_i$. The objective is

$$\limsup_{t\to\infty}\ \sum_i h_iS_i+\frac1t\,\mathbf E\Big[\sum_i b_i\int_0^t(a_i(s)-S_i)^+\,ds+c_k\mu_kE(t)\Big].$$

The candidate solution comes from the Bellman system (13): find $(f,B,\gamma)$ with $f\in C^2$, $B>0$, $\gamma\ge0$ such that

$$\tfrac12\Sigma f''(w)+\theta f'(w)+\min_{q\in\mathcal A(w)}\sum_i\Big(b_i-\frac{\lambda_i}{\mu_i}f'(w)\Big)(q_i-S_i)^+=\gamma\quad\text{on }[0,B],$$

with $\ge\gamma$ for $w>B$, $0\le f'\le c_k\mu_k$ on $\mathbb R_+$, $f'(0)=0$ and $f'(B)=c_k\mu_k$.

The barrier policy reflects the workload at $0$ and at $B$ and allocates by $q^*$, which backorders only one SKU, $\kappa(w)\in\arg\min_i\{b_i\mu_i-\lambda_if'(w)\}$, above total inventory.

Formalization targets

Goal: Theorem 2

Suppose $b_j\mu_j/\lambda_j>c_k\mu_k$. Then (13) has a solution, and for each solution a barrier policy with upper barrier $B$ exists, and

$$\lim_{t\to\infty}\frac1t\,\mathbf E\Big[\sum_i b_i\int_0^t(a_i(s)-S_i)^+\,ds+c_k\mu_kE(t)\Big]=\gamma$$

under it, while every EWF-feasible solution with the same $S$ has objective at least $\sum_ih_iS_i+\gamma$.

Milestones

• The allocation problem: Lemma 1.
• The initial value problem for $f'$: Lemmas A.3.1, A.3.2, A.3.3, A.3.6, A.3.8, A.3.9.
• The Bellman system: Lemma 2 Part ii.
• The regulators: Lemmas A.4.3 and 4.
• The verification argument: (A.58), (A.45)–(A.47), (A.62), (A.63).

Significance

Theorem 2 identifies an explicit optimal policy and its cost for a singular ergodic control problem with a state-dependent drift. The cost is computed by a one-dimensional free-boundary problem, which is what makes the inventory optimization of the paper's §5 tractable.

The result is proved in the paper; no machine-checked proof of it is known to this mission. Formalizing it adds a verification theorem for ergodic singular control with jump controls, a reflected equation with discontinuous monotone drift, and a global analysis of a piecewise linear ODE. These are the recurring pieces of Brownian control problems in operations research. The only other instance on the platform is AtaBarjesteh23.Workload, for a different workload formulation, and its goals are still open.

The formalization also corrects the source. Printed Lemma 4 claims a regulator solution for every càdlàg input, and that is false when $q^*$ makes the drift jump (see Difficulty). The mission states the corrected lemma and the barrier policy almost surely.

Difficulty

The obvious existence argument for the barrier policy fails. The drift $\beta(w)=\sum_i(\lambda_i/\mu_i)(q_i^*(w)-S_i)^+$ jumps upward wherever $\kappa$ changes. The paper patches the regulator over the intervals between jumps. On a path that approaches a jump point $w_0$ from below with slope strictly between the two one-sided values of $\beta$, the workload can neither cross $w_0$ nor stay there. So no solution exists for that path, and existence holds only for almost every Brownian path, where the noise prevents this. Pathwise uniqueness is still true because $\beta$ is nondecreasing on $[0,B]$.

The second difficulty is the competitor class. Feasible solutions need not be Markov, work-conserving or continuous, and $E$ may jump. Expected workload may even grow linearly. Itô's formula alone therefore does not give the lower bound: the jumps of $E$ and $I$ and the growth of $\mathbf E[W(t)]$ need separate treatment.

Formalization scope

Time is indexed by $\mathbb R$, and only $t\ge0$ is constrained. The SKU set is Fin n with $n\ge1$. Costs are computed in $\mathbb R_{\ge0}\cup\{\infty\}$ with lower integrals, so an infinite expectation is $\infty$. The measures $d\ell$ and $du$ are Lebesgue–Stieltjes measures of the path extended by $0$ to negative times. Feasibility requires progressive measurability of the allocation and integrable paths, and it holds for every $\omega$. The filtration satisfies the usual conditions, as in the paper. The published definition AtaBarjesteh23.Workload.IsDriftBM is the Brownian motion.

The allocation $q^*$ is fixed: the fill of OA A.2 when no SKU is backordered, and the largest-$\lambda$ tie-break otherwise. That is the right-continuous choice named on OA p.26. Regulators are stated for $b\le B$, where $f'$ is strictly increasing.

A trivial reading is excluded in three ways. The goal asserts existence of the Bellman solution and of the barrier policy, so it is not conditional on either. The lower bound ranges over all feasible solutions. A path with non-integrable allocation is not feasible, so it cannot gain a junk drift of $0$.

The development needs an Itô formula for processes with finite-variation jump parts, a reflection map on $\mathbb D$, and global ODE comparison arguments. Each is reusable beyond this mission. Contributions to any of them are welcome, and so is a pathwise treatment of the regulator with monotone discontinuous drift.

Selected references

• E. Özkan, G.-J. van Houtum, Joint Inventory and Scheduling Control in a Repair Facility, SSRN 3784144 (2023). https://ssrn.com/abstract=3784144
• E. Özkan, G.-J. van Houtum, Joint Inventory and Scheduling Control in a Repair Facility, Operations Research (2023). https://doi.org/10.1287/opre.2023.2459
• J. M. Harrison, Brownian Models of Performance and Control, Cambridge University Press, 2013. https://doi.org/10.1017/CBO9781139087698
• W. Whitt, Stochastic-Process Limits, Springer, 2002. https://doi.org/10.1007/b97479
• A. Ju. Veretennikov, On strong solutions and explicit formulas for solutions of stochastic integral equations, Math. USSR-Sb. 39 (1981). https://doi.org/10.1070/SM1981v039n03ABEH001518

Motivation

A chance constrained program minimizes a cost while requiring a random constraint to hold with high probability. It models decisions under uncertainty in energy systems, finance, and process and water-quality engineering. Replacing the probability by an empirical frequency over $N$ samples gives the sample average approximation, whose constraint counts the violated samples. This counting function is a 0/1 loss: it is discontinuous, and the resulting problem is NP-hard. The usual remedies are mixed-integer reformulations, or smooth and convex surrogates that change the problem.

Zhou, Pan, Xiu and Li (arXiv:2210.11889v5) work on the 0/1 constraint directly. They compute the projection onto the constraint set, define a stationarity condition from it, and rewrite that condition as a system of equations. A semismooth Newton method, SNSCO, then solves the system. This mission formalizes the local analysis of SNSCO.

Setting

Let $f:\mathbb R^K\to\mathbb R$ and $G:\mathbb R^K\to\mathbb R^{M\times N}$ be continuously differentiable, let $\Omega\subseteq\mathbb R^K$ be nonempty, closed and convex, and let $s\ge 1$ be an integer. For a matrix $Z$, the quantity $\|Z\|_0^+$ counts the columns of $Z$ with a positive entry. The problem (SCO) is

$$\min_{x\in\Omega} f(x)\quad\text{subject to}\quad \|G(x)\|_0^+\le s.$$

With $G(x)=(g(x,\xi_1),\dots,g(x,\xi_N))$ and $s=\lceil\alpha N\rceil$ this is the sample average approximation.

Write $\mathcal S:=\{Z:\|Z\|_0^+\le s\}$. The set $\Pi_{\mathcal S}(Z)$ of nearest points of $\mathcal S$ has a closed form. It is described by a family $\mathbb T(Z;s)$ of column sets, which records the choices of $s$ columns of largest positive part. A point $x^*$ with multiplier $W^*$ is $\tau$-stationary if

$$x^*=\Pi_\Omega\bigl(x^*-\tau[\nabla f(x^*)+\textstyle\sum W^*_{mn}\nabla G_{mn}(x^*)]\bigr),\qquad Z^*\in\Pi_{\mathcal S}(Z^*+\tau W^*),$$

where $Z^*=G(x^*)$. Put $w=(x;\mathrm{vec}(W))$ and $\Lambda=G(x)+\tau W$. For an index set $\mathcal V$, the map $F(w;\mathcal V)$ collects a projected-gradient residual $\varphi(w;\mathcal V)$, the entries of $G(x)$ on $\mathcal V$, and the entries of $W$ off $\mathcal V$. Stationarity becomes $F(w^*;\mathcal V_*)=0$, where $\mathcal V_*$ is the set of zero entries of $Z^*$ in columns of zero maximum.

SNSCO does not know $\mathcal V_*$. At $w^\ell$ it selects $T_\ell\in\mathbb T(\Lambda^\ell;s)$ and $\mathcal V_\ell:=U_{T_\ell}=\{(m,n):n\in T_\ell,\ \Lambda^\ell_{mn}\ge0\}$, takes an element $H^\ell$ of the Clarke generalized Jacobian of $\varphi(\cdot;\mathcal V_\ell)$, and solves a Newton system with a regularization block $-\mu_\ell I$. A backtracking test on $\|G\|_0^+\le(\gamma+1)s$ fixes the step size.

Formalization targets

Goal: Theorem 5

Let $x^*$ be $\tau$-stationary with $0<\tau<\tau_*$, let Assumption 2 hold, and let $\gamma\ge|\Gamma_0^*|/s$. Then there is $\eta>0$ such that every run of SNSCO with $\|w^0-w^*\|<\eta$ takes full Newton steps and satisfies

$$w^\ell\to w^*,\qquad \|w^{\ell+1}-w^*\|=o(\|w^\ell-w^*\|).$$

Under strong semismoothness of $\varphi(\cdot;\mathcal V_*)$ and of $G_{mn}$, $(m,n)\in\mathcal V_*$, the bound improves to

$$\|w^{\ell+1}-w^*\|\le C\|w^\ell-w^*\|^2 .$$

Both clauses hold for every selection of $T_\ell$ and $H^\ell$, with $\eta$ and $C$ chosen before the run.

Milestones

In proof order: the sign of $Z^\downarrow_s$ (9); the closed form of $\Pi_{\mathcal S}$ (Proposition 1); column-wise complementarity (24); the fixed-point inclusion (Proposition 2); the stationary equations (Theorem 4); identification of the active set (Lemma 2); semismoothness of $F(\cdot;\mathcal V)$ (Lemma 3); uniform regularity of the Newton matrix (Lemma 4); and the superlinear and quadratic one-step estimates, (85) and the last display of p.22.

Significance

The theorem gives a local rate for an algorithm that attacks the 0/1 constraint itself, with no surrogate and no integer variables. The projection and the stationary equations are reusable for any problem with a column-counting constraint, including support vector machines and one-bit compressed sensing, which the paper notes as special cases.

The paper proves the result, and this mission adds the machine-checked proof. Two corrections are also recorded in the statements. The sentence of Theorem 5 omits $\tau<\tau_*$, without which it is false at $\tau=\tau_*$. Lemmas 3 and 4 hold only for those $\mathcal V\subseteq\mathcal V_*$ with $W^*_{\overline{\mathcal V}}=0$. As far as known, no result with a varying index set is formalized: the proved nonsmooth Newton theorems on the platform (Qi and Sun 1993 and Qi 1993) fix one system.

Difficulty

The standard Newton argument bounds $F(w^\ell)-F(w^*)-H^\ell(w^\ell-w^*)$ for one fixed map $F$. Here the map $F(\cdot;U_{T_\ell})$ changes with the iterate, so that argument does not apply directly. It needs $F(w^*;U_{T_\ell})=0$ for whichever set the iterate selects, although $U_{T_\ell}$ need not equal $\mathcal V_*$. This identification is where $\tau<\tau_*$ enters. Semismoothness is assumed only for $\varphi(\cdot;\mathcal V_*)$ and must transfer to each $\varphi(\cdot;\mathcal V)$, which involves a Clarke Jacobian of a composition with a non-surjective linear map. The chain rule available there is weaker than the usual inclusion.

Formalization scope

Points live in EuclideanSpace ℝ (Fin K) and matrices in Matrix (Fin M) (Fin N) ℝ, with [NeZero M] so that columns have a maximum. The variable $w$ lives in the Euclidean space on Fin K ⊕ (Fin M × Fin N), and $F$ and $\nabla F_\mu$ are written on that index type, so no block permutation appears. The Clarke Jacobian is the platform's NonsmoothNewton.Shared.clarkeJac. Semismoothness is the paper's (10)–(11), not Qi and Sun's limit form. $\Pi_\Omega$ is a function chosen by Classical.epsilon, and $\Pi_{\mathcal S}$ is a set. The hypothesis $\tau<\tau_*$ is BelowTauStar, with no division and with $\tau_*=+\infty$ when $\|Z^*\|_0^+<s$ or $W^*_{:\Gamma_0^*}=0$. A run has no stopping test, and it is a predicate on sequences, so every selection is covered.

The goal must not be restated for the one-step map, with Lemma 2's conclusion assumed, or for fixed $\mathcal V=\mathcal V_*$. A verification file shows that the run predicate and Assumption 2 are satisfiable on a concrete instance.

Needed infrastructure: the Clarke Jacobian of a Lipschitz map on Euclidean space (nonemptiness, local boundedness and closedness, partly available on the platform) and its behaviour under composition with a linear map. The results on $\Pi_{\mathcal S}$ are elementary and self-contained. Contributions of general lemmas on Clarke Jacobians are welcome.

Selected references

• S. Zhou, L. Pan, N. Xiu, G. Y. Li, A 0/1 Constrained Optimization Solving Sample Average Approximation for Chance Constrained Programming, arXiv:2210.11889v5, 2026. https://arxiv.org/abs/2210.11889v5
• L. Qi, J. Sun, A nonsmooth version of Newton's method, Mathematical Programming 58, 1993. https://doi.org/10.1007/BF01581275
• L. Qi, Convergence analysis of some algorithms for solving nonsmooth equations, Mathematics of Operations Research 18, 1993. https://doi.org/10.1287/moor.18.1.227
• F. H. Clarke, Optimization and Nonsmooth Analysis, SIAM Classics in Applied Mathematics 5, 1990. https://doi.org/10.1137/1.9781611971309

Why the mismatch between model and system matters

Optimal controllers are computed from a model, and the model is at best an approximation of the system that the controller will drive. The coefficients may be estimated from data, regularized for computation, or replaced by simpler functions. The question of robustness is whether the loss caused by this mismatch vanishes as the model improves. Kara and Yüksel answered it for discrete-time Markov decision processes under a condition they call continuous convergence in the control (SIAM J. Control Optim. 2020; average cost: arXiv:2003.05769). Pradhan and Yüksel treat the continuous-time counterpart for non-degenerate controlled diffusions, under several cost criteria (arXiv:2205.05894v2). This mission formalizes the discounted case, which the later sections of that paper use as their template.

Controlled diffusions and discounted optimality

Let $\mathbb U$ be a compact metric space of control actions and $\mathrm V=\mathcal P(\mathbb U)$ the space of probability measures on it. Given a drift $b:\mathbb R^d\times\mathbb U\to\mathbb R^d$ and a diffusion matrix $\sigma:\mathbb R^d\to\mathbb R^{d\times d}$, the state solves

$$\mathrm dX_t=b(X_t,U_t)\,\mathrm dt+\sigma(X_t)\,\mathrm dW_t,\qquad X_0=x,$$

where $W$ is a $d$-dimensional standard Wiener process, $U$ is a $\mathrm V$-valued process, and $b(x,\mathrm v)=\int_{\mathbb U}b(x,\zeta)\,\mathrm v(\mathrm d\zeta)$. The process $U$ is an admissible control if the increments of $W$ after time $s$ are independent of the completion of $\sigma(X_0,U_r,W_r:r\le s)$. A stationary Markov control is a Borel map $v:\mathbb R^d\to\mathrm V$, used as $U_t=v(X_t)$; these form the set $\mathfrak U_{\mathsf{sm}}$.

For a bounded running cost $c\ge0$ and $\alpha>0$, the discounted cost and the optimal value are

$$\mathcal J^U_\alpha(x,c)=\mathbb E^U_x\left[\int_0^\infty e^{-\alpha s}c(X_s,U_s)\,\mathrm ds\right],\qquad V_\alpha(x)=\inf_{U}\mathcal J^U_\alpha(x,c).$$

An approximating model $(b_n,\sigma_n,c_n)$ has its own optimal value $V^n_\alpha$. It converges to $(b,\sigma,c)$ if $\sigma_n\to\sigma$ almost everywhere and if, for almost every $x$, $\zeta_n\to\zeta$ implies $c_n(x,\zeta_n)\to c(x,\zeta)$ and $b_n(x,\zeta_n)\to b(x,\zeta)$. This last condition is continuous convergence in controls.

Formalization targets

Goal: robustness of optimal policies

Under assumptions (A1)–(A5), if $v^*_n\in\mathfrak U_{\mathsf{sm}}$ is optimal for the model $(b_n,\sigma_n,c_n)$ and $v^*$ for the true model, then for all $x\in\mathbb R^d$

$$\lim_{n\to\infty}\mathcal J^{v^*_n}_\alpha(x,c)=\mathcal J^{v^*}_\alpha(x,c).$$

The left side runs $v^*_n$ on the true dynamics with the true cost. The statement quantifies over every choice of optimal controls and every initial state, and the value is an infimum over all admissible controls.

Milestones

$$V^n_\alpha(x)\to V_\alpha(x)\quad\text{for all }x\qquad\text{(Theorem 3.3)}$$

The milestones also include: well-posedness of (2.1) under every admissible control, and well-posedness and the strong Feller property under $\mathfrak U_{\mathsf{sm}}$; compact metrizability of $\mathfrak U_{\mathsf{sm}}$; the characterization of $V_\alpha$ and of optimal controls by the HJB equation (Theorems 3.1 and 3.2); continuity of the cost in the policy (Remark 3.2); and optimality of limits of optimal controls.

What the result gives

The result. Theorem 3.3 alone says the optimal value is continuous in the model. Theorem 3.4 is stronger in content: it concerns the policy, which is what is actually deployed. A controller who solves an approximate problem suffers no asymptotic loss on the true system, without any quantitative knowledge of the error. The assumptions allow functional perturbations of the coefficients and uncountable action spaces.

The formalization. The theorems are proved in the paper, partly by citing Arapostathis, Borkar and Ghosh. A search of the platform found no formalization of them. A complete development would add the discounted HJB characterization for non-degenerate diffusions, the compact space of stationary Markov controls, and its topology. The published EthierKurtz SDE definitions supply the Brownian motion, the Itô integral and the strong solution predicate.

Where the difficulty lies

The obvious argument couples the two state processes through the same Wiener process and compares paths. It fails here: a stationary Markov control is merely measurable, so the closed-loop drift has no regularity in $x$, and neither it nor the convergence of $\sigma_n$ gives a stable pathwise estimate. Moreover, the optimal policies $v^*_n$ need not converge in any pointwise sense; they have limits only in a weak topology, in which products with gradients are delicate. The limit of $v^*_n$ must be identified as optimal for a model that none of the $v^*_n$ was designed for. Each of these steps also needs elliptic regularity that uniform ellipticity and uniform moduli of continuity have to supply.

Formalization scope

$\mathbb R^d$ is EthierKurtz.SDEState d; a $d\times d$ matrix is an element of EthierKurtz.SDEDiffusion d, so its norm is $\sqrt{\mathrm{Tr}(\sigma\sigma^{\mathsf T})}$. $\mathrm V$ is ProbabilityMeasure U. All models live on one probability space with one Brownian motion, whose completeness is not assumed; the filtrations join the null sets explicitly. An admissible control is jointly measurable. The value is a real sInf over admissible pairs, a nonempty set bounded below. The optimality predicate requires a solution from every $x$, so a policy with no solutions is not optimal.

Two hypotheses are corrected, and each correction is declared on the items that use it. Read literally, (A5)(iii) makes Theorem 3.3 false, and (A5)(ii) makes Theorems 3.3 and 3.4 false:

1. (A5)(iii) has constants uniform in $n$. The constants $C_R$ and $C_0$ of (A1)–(A3) are common to all models. Otherwise a vanishing $\sigma_n$ near a point yields a sticky limit diffusion.
2. (A5)(ii) has one null set. The exceptional set does not depend on the sequence $\zeta_n$. Otherwise bump functions in $\zeta$ moving with $x$ defeat both theorems.

Also, $c_n$ is real valued, not $\mathbb R^d$-valued as printed, and it need not be nonnegative.

Mathlib has no Itô integral, no Sobolev spaces and no $L^p$ elliptic theory. A proof needs Itô–Krylov-type calculus, interior $W^{2,p}$ estimates and compact Sobolev embeddings, and these are reusable well beyond this mission. No statement of the mission mentions a Sobolev space. Contributions are welcome at every milestone, and also on those substrate results.

Selected references

• S. Pradhan and S. Yüksel, Robustness of Stochastic Optimal Control to Approximate Diffusion Models Under Several Cost Evaluation Criteria, arXiv:2205.05894v2, 2023. https://arxiv.org/abs/2205.05894
• A. Arapostathis, V. S. Borkar and M. K. Ghosh, Ergodic Control of Diffusion Processes, Cambridge University Press, 2012. https://mathscinet.ams.org/mathscinet-getitem?mr=2884272
• A. D. Kara and S. Yüksel, Robustness to Incorrect System Models in Stochastic Control, SIAM J. Control Optim. 58 (2020), 1144–1182. https://doi.org/10.1137/18m1208058
• A. D. Kara, M. Raginsky and S. Yüksel, Robustness to Incorrect Models and Data-Driven Learning in Average-Cost Optimal Stochastic Control, arXiv:2003.05769, 2020. https://arxiv.org/abs/2003.05769
• S. Pradhan and S. Yüksel, Continuity of Cost in Borkar Control Topology and Implications on Discrete Space and Time Approximations for Controlled Diffusions Under Several Criteria, arXiv:2209.14982, 2022. https://arxiv.org/abs/2209.14982

Why polynomial voting rules

In a proof-of-stake blockchain, the participants who validate transactions are selected in proportion to the stakes they hold, and each round of validation pays a reward in new stakes. Roşu and Saleh (Manag. Sci. 2021) and Tang (arXiv:2206.02227) analysed this mechanism as a Pólya urn: the reward is issued in every round, so the total stake grows linearly in time. In the protocols of Bitcoin and Ethereum the volume of stakes grows sublinearly, and security arguments ask that no bidder keep a large probability of being selected.

Tang and Yao (arXiv:2206.10105) propose a family of rules that slows the issuance. A rule with parameter $\alpha\ge0$ scales each bidder's selection probability by $N_t^{-\alpha}$, where $N_t$ is the current total stake, and $\alpha=0$ is the Pólya urn. The question is what this does to the distribution of wealth among bidders and to the voting power of each bidder as time grows.

The Poly($\alpha$) model

There are $K$ bidders with initial stakes $n_{1,0},\dots,n_{K,0}$, and $N=\sum_k n_{k,0}\ge1$. Time is discrete. Write $n_{k,t}$ for the stakes of bidder $k$ at time $t$, $N_t=\sum_k n_{k,t}$ for the volume, $\pi_{k,t}=n_{k,t}/N_t$ for the bidder share, and

$$\theta_{k,t}=\frac{n_{k,t}}{N_t^{1+\alpha}}=\frac{\pi_{k,t}}{N_t^\alpha}$$

for the voting power. In each period a single stake is offered: given the past $\mathcal F_t$, bidder $k$ receives it with probability $\theta_{k,t}$, and nobody receives it with probability $1-N_t^{-\alpha}$. The Dirichlet distribution $\mathrm{Dir}(a_1,\dots,a_K)$ is the law on the simplex with density proportional to $\prod_k x_k^{a_k-1}$, and $d_W$ is the 1-Wasserstein distance.

Formalization targets

Goal: Theorem 6 (long-time behavior)

For every $K$, every initial stake vector and every real $\alpha\ge0$, the share process $(\pi_{k,t})$ is an $\mathcal F_t$-martingale, and almost surely

$$(\pi_{1,t},\dots,\pi_{K,t})\to(\pi_{1,\infty},\dots,\pi_{K,\infty})\overset d=\mathrm{Dir}(n_{1,0},\dots,n_{K,0}),$$ $$d_W\big(\pi_{k,t},\mathrm{Beta}(n_{k,0},N-n_{k,0})\big)=O\big(t^{-\frac1{1+\alpha}}\big).$$

The voting power $(\theta_{k,t})$ is an $\mathcal F_t$-supermartingale, for $\alpha>0$ it tends to $0$ almost surely, and

$$(1+\alpha)^{\frac\alpha{1+\alpha}}\,t^{\frac\alpha{1+\alpha}}\,\theta_{k,t}\overset d\longrightarrow\mathrm{Beta}(n_{k,0},N-n_{k,0}).$$

Milestones

The milestones follow the paper's argument, from the weakest ingredient to the goal: the time-changed urn representation (Proposition 1); divergence of $N_t$; the law of large numbers $N_t^{1+\alpha}/t\to1+\alpha$ in probability (Proposition 2 (ii)); the lower-tail large deviation bound (Theorem 3 (i)); the Beta marginals of a Dirichlet law; the one-step identity (2.18); the Dirichlet limit of the Pólya urn; the Goldstein–Reinert rate (2.19); the conditional law of the stakes given $N_t=s$; and the one-step identity for $\theta_{k,t}$.

Significance

Theorem 6 separates what the rule changes from what it preserves. The limit of the shares, and hence the level of decentralization, does not depend on $\alpha$; the speed of convergence and the decay of voting power do. The bound $t^{-1/(1+\alpha)}$ is stated in the paper to be sharp. The decay of $\theta_{k,t}$ is the security gain of the rule, since no bidder retains a non-vanishing chance of being selected.

The theorem is proved in the paper. No machine-checked proof of it is known. A formalization delivers more than this statement: the Pólya urn with its Dirichlet limit, in full generality of initial composition, is not on the platform or in Mathlib, and the Goldstein–Reinert bound is a nontrivial Stein's-method result. The published mission on the Roşu–Saleh model treats a different chain, with one tracked investor and deterministic rewards.

Difficulty

The first clause is a one-line computation, and the martingale convergence theorem gives the existence of the limit. The substance lies elsewhere.

Identifying the limit requires the embedding of the urn: the colour of each award is independent of the award times. A direct calculation with the one-step law does not give this, because the time change $L_t$ is random and the statement is one about laws of whole paths.

The rate (2.16) cannot be obtained from the martingale structure. It needs the conditional law given $N_t=s$, the urn rate (2.19), and a tail bound for $N_t$ at the scale $t^{1/(1+\alpha)}$, where the exponential tail must beat the polynomial rate.

Divergence of $N_t$ is not a Borel–Cantelli consequence of a deterministic lower bound on the award probability: for $\alpha>1$ the sum $\sum_t(N+t)^{-\alpha}$ converges. The argument has to use that each holding time is finite. Convergence (2.7) requires moment asymptotics for a Markov chain whose increments depend on its state.

Formalization scope

The chain is PolyVoting.Model μ K α n₀, a structure on a probability space. It carries a stake process n : ℕ → Ω → Fin K → ℕ, adapted to a filtration ℱ, with n 0 = n₀, and the joint conditional one-step law: Model holds for any filtration satisfying the law, the natural filtration among them. α is real and 0 ≤ α, with Real.rpow throughout, and 1 ≤ ∑ k, n₀ k. The Pólya urn is Model μ K 0 n₀, with no second definition. Derived quantities are M.total, M.share and M.power.

d_W is the published WassersteinDRO.Duality.wassersteinDistance 1 on ℝ, valued in ℝ≥0∞, and rates are compared in ℝ≥0∞, so an infinite distance cannot satisfy the bound. dirichletMeasure is the pushforward of a density on the first K - 1 coordinates. betaMeasure is Mathlib's.

Clauses naming a limit law are guarded exactly where the law would be undefined: every n₀ j ≥ 1 for Dir, and 1 ≤ n₀ k < N for Beta. The martingale, supermartingale and almost sure clauses are unguarded. A guard placed on them would narrow the theorem, and dropping a guard on a Beta clause would make it false rather than trivial, since Mathlib's betaMeasure a 0 is the zero measure.

A complete development needs a reusable theory of the Pólya urn (exchangeability or moments, the Dirichlet limit, the Stein bound), discrete-time random time change for Markov chains, and moment asymptotics. Those parts are useful beyond this mission, and contributions to any of them are welcome.

Selected references

• W. Tang and D. D. Yao, Polynomial Voting Rules, arXiv:2206.10105v5, 2024. https://arxiv.org/abs/2206.10105
• I. Roşu and F. Saleh, Evolution of shares in a proof-of-stake cryptocurrency, Manag. Sci. 67(2):661–672, 2021. https://doi.org/10.1287/mnsc.2020.3791
• W. Tang, Stability of shares in the Proof of Stake protocol – concentration and phase transitions, 2022. https://arxiv.org/abs/2206.02227
• L. Goldstein and G. Reinert, Stein's method for the beta distribution and the Pólya-Eggenberger urn, J. Appl. Probab. 50(4):1187–1205, 2013. https://doi.org/10.1239/jap/1389370107
• C. Villani, Optimal transport: old and new, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9

Motivation

Many selection problems ask for a team of $k$ items out of $n$ candidates whose individual performances are random and whose joint value is not additive: a team of contributors where only the best submission counts, a slate of content topics where a user clicks if at least one topic appeals, a portfolio of research projects where the strongest result dominates. The natural model is stochastic submodular maximization: choose $S$ with $|S|=k$ to maximize $u(S)=\mathbb E[g(M_S(X))]$, where $X_i$ is the random performance of item $i$ and $g$ is a monotone submodular value function of the performance vector (Asadpour and Nazerzadeh, Maximizing stochastic monotone submodular functions, Management Science 2016). The problem is NP-hard even for $g=\min$ (Goel, Guha and Munagala, PODS 2006, as cited on p.12 of arXiv:1605.07172v4).

Greedy and continuous-relaxation methods need to evaluate $u$ on many candidate sets, each evaluation being an expectation over a joint distribution. In practice a platform often wants something simpler: a test score $a_i$ per item, computed from that item's own distribution only, followed by picking the $k$ items with the highest scores. Sekar, Vojnovic and Yun (arXiv:1605.07172, Management Science 2021) ask which scores make this trivial algorithm a constant-factor approximation. Mean scores and quantile scores can fail badly (the paper's Example 1 and Propositions 1–2). The paper's answer is the replication test score: the expected value of a virtual team made of $k$ independent copies of item $i$.

Setting

Items are $N=\{1,\dots,n\}$, the cardinality is $0<k\le n$, and item $i$ has a nonnegative random performance $X_i\sim P_i$; the $X_i$ are independent and not necessarily identically distributed. A value function $g:\mathbb R_+^n\to\mathbb R_+$ is

• monotone if $x\le y$ componentwise implies $g(x)\le g(y)$;
• submodular if $g(x\vee y)+g(x\wedge y)\le g(x)+g(y)$ (eq. (3));
• symmetric if $g(x\circ\sigma)=g(x)$ for every permutation $\sigma$ of the coordinates.

For $S\subseteq N$, $M_S(x)$ keeps the coordinates in $S$ and sets the others to $0$; the utility is $u(S)=\mathbb E[g(M_S(X))]$ (eq. (4)). The replication test score of item $i$ is

$$a_i=\mathbb E\bigl[g(X_i^{(1)},\dots,X_i^{(k)},0,\dots,0)\bigr],$$

with $X_i^{(1)},\dots,X_i^{(k)}$ independent copies of $X_i$ (Definition 2).

Writing $g(z,x)$ for $g$ at $z\in\mathbb R_+^{n-1}$ extended by one coordinate $x$, and $g(z)=g(z,0)$, the function $g$ has extended diminishing returns (Definition 1) if every value $v$ of $g$ is taken at some $z$ such that $g(z,x)-g(z)\le g(y,x)-g(y)$ for all $x\ge0$ and all $y$ with $g(y)\le v$: a new item helps a group worth $v$ no more than it helps any group worth less. Sums of concave functions of the total, the maximum, CES functions, success probabilities and top-$r$ sums all have it (Appendix A).

A pair of set functions $(\underline v,\bar v)$ is a $(p,q)$-sketch of $u$ if $p\,\underline v\le u\le q\,\bar v$; scores are $(p,q)$-good if $(\min_{i\in S}a_i,\max_{i\in S}a_i)$ is a $(p,q)$-sketch.

Formalization targets

Goal: Theorem 1

For every top-$k$ set $S$ of the replication scores (any tie-breaking) and every $T$ with $|T|=k$,

$$u(S)\ge\frac{1-1/e}{5-1/e}\,u(T).$$

The constant is the paper's; no family of $g$ on growing dimension, no continuity and no relation between $n$ and $k$ beyond $k\le n$ is assumed.

Milestones

1. Lemma 1: $u$ is monotone submodular.
2. Lemma 2 and Corollary 1: $(p,q)$-good scores make top-$k$ selection a $p/(p+q)$-approximation,

$$u(S)\ge\frac{p}{p+q}\,u(T).$$

3. Lemma 4, lower half: inequality (18), $u(A\cup\{i\})\ge(1-\tfrac1k)u(A)+\tfrac1k a_i$, and its cascade $u(S)\ge(1-1/e)\min_{i\in S}a_i$ for $|S|=k$.
4. Lemma 4, upper half: the overlay bound (22)–(23), the chain (25)–(29), inequality (c) and the Markov step, giving $u(S)\le4\max_{i\in S}a_i$ for $0<|S|\le k$.
5. Lemma 4 itself: replication scores are $(1-1/e,4)$-good. Theorem 1 is Corollary 1 with $p=1-1/e$, $q=4$.

Significance

The theorem shows that for a broad class of symmetric value functions a score computed from one item's distribution in isolation, without any joint evaluation, gives a constant-factor guarantee. Replication scores can be estimated by showing $k$ copies of an item to users and averaging, so the guarantee covers algorithms that a platform can run without knowing $g$ or the $P_i$. The sketch framework of Lemma 2 and Corollary 1 is independent of the stochastic setting and applies to any submodular set function with a minorant and majorant of this form. The paper's welfare-maximization result (Theorem 2) extends the same approach and is not part of this mission.

The result is proved in the paper; no machine-checked proof of it or of the sketch lemma exists on the platform. Formalizing it also repairs the printed argument. The printed proof evaluates $g$ on up to $n-1+k$ coordinates (footnote 6 concedes the abuse) and assumes $g$ continuous with an attained maximum, which neither the theorem nor the examples of §2.3 (step success probabilities) provide. Lemma 2 is false as printed when $n<2k$ or when $u$ is not monotone, and Definition 3's "for all $S\subseteq N$" makes Lemma 4 false at sizes other than $k$. The mission states the corrected lemmas, with counterexamples recorded in the items.

Difficulty

The obvious proof of the upper bound adds the $n-1$ "fictitious" items of a vector $z$ with $g(z)\approx c\,a_k$ to $S$ and bounds each marginal by a replica marginal. With $g$ defined on exactly $n$ coordinates, $S^*\cup S$ does not fit, so (22)–(23) must be replaced by an inequality that stays inside $n$ coordinates; symmetry of $g$ is what makes this possible. The choice of $z$ uses extended diminishing returns at a value $v\le 2a_k$ that must be attained on $k-1$ coordinates; without continuity such a $v$ need not equal $\min\{2a_k,g^{\max}_{k-1}\}$, and $g^{\max}_{k-1}$ need not be attained (for $g(x)=1-e^{-\sum x_i}$ it is not). The lower bound (18) at $j>1$ likewise compares $j-1$ items plus $k$ replicas, up to $2k-1$ coordinates. The measure-theoretic side (product measures, conditioning on $g(Y_i)\le g(z)$, Fubini over replicas) is routine but must be carried out with the integrability that the replication scores alone provide.

Formalization scope

Items are Fin (m + 1) with $n=m+1$; performances are ℝ≥0; the laws $P_i$ are probability measures on ℝ≥0 and independence is Measure.pi P. The padding element $\varphi$ is $0$. Expectations are Bochner integrals, so $g$ is assumed measurable and the $k$-fold replica $g(X_i^{(1)},\dots,X_i^{(k)},0,\dots,0)$ integrable for each $i$; the integrability of every $u(S)$ is derived, not assumed. Extended diminishing returns is stated with the value $v$ attained on $\mathbb R_+^{n-1}$, which the printed definition implies. A top-$k$ set is any $S$ with $|S|=k$ and $a_j\le a_i$ for $i\in S$, $j\notin S$, so no tie-breaking rule is fixed. $(p,q)$-good scores require the lower sketch bound at $|S|=k$ and the upper one at $0<|S|\le k$.

The statement is not trivialized by an empty instance: the hypotheses hold for $g=\sum_i x_i$ and $g=\max_i x_i$ at every $n$, and at $n=3$, $k=2$, $g=\max$ with $P_1=P_2=\delta_1$, $P_3=0.8\,\delta_0+0.2\,\delta_2$ the top-2 set has utility $1$ while another pair has $1.2$.

The development needs product measures over replicas, conditioning by independence, and a monotone-submodular calculus for set functions; the sketch lemma and the overlay inequality are reusable for other test-score results. Proofs of any milestone, alternative arguments for the upper bound, and better constants are welcome.

Selected references

• S. Sekar, M. Vojnovic, S.-Y. Yun, A Test Score Based Approach to Stochastic Submodular Optimization, Management Science, 2021; arXiv:1605.07172v4 (2019). https://arxiv.org/abs/1605.07172
• A. Asadpour, H. Nazerzadeh, Maximizing Stochastic Monotone Submodular Functions, Management Science 62(8), 2016. https://doi.org/10.1287/mnsc.2015.2254
• A. Goel, S. Guha, K. Munagala, Asking the Right Questions: Model-Driven Optimization Using Probes, PODS 2006, pp. 203–212.
• G. L. Nemhauser, L. A. Wolsey, M. L. Fisher, An Analysis of Approximations for Maximizing Submodular Set Functions—I, Mathematical Programming 14, 1978. https://doi.org/10.1007/BF01588971

Motivation

Many control problems are posed on networks of agents that each see only a local state and take a local action: traffic signals at intersections, wireless transmitters sharing a channel, nodes of an epidemic or a power grid. Treated as one Markov decision process, such a system has a state space whose size is exponential in the number of agents $n$, so tabular reinforcement learning, and even storing a single Q-function, is out of reach. Qu, Wierman and Li (arXiv:1912.02906; Operations Research, 2022) exploit the network structure: if the next local state depends only on the neighbours' states, then the influence of far-away agents on an agent's Q-function decays with graph distance, and each agent can learn with tables indexed only by its κ-hop neighbourhood. Their algorithm, Scalable Actor Critic (SAC), comes with a non-asymptotic guarantee: it finds an approximate stationary point of the global objective with an error that decays exponentially in $\kappa$.

Setting

There are $n$ agents $\mathcal N=\{1,\dots,n\}$ on an undirected graph $G$. For $\kappa\ge0$ the κ-hop neighbourhood $N_i^\kappa$ is the set of agents at graph distance at most $\kappa$ from $i$, $N_i=N_i^1$, and $f(\kappa)=\max_i|N_i^\kappa|$. Agent $i$ has finite local state and action sets $\mathcal S_i$, $\mathcal A_i$; global states and actions are tuples $s\in\mathcal S=\prod_i\mathcal S_i$, $a\in\mathcal A=\prod_i\mathcal A_i$. Transitions factorize,

$$P(s(t+1)\mid s(t),a(t))=\prod_{i=1}^nP\big(s_i(t+1)\mid s_{N_i}(t),a_i(t)\big),$$

agent $i$ earns $r_i(s_i,a_i)$, the global reward is $r=\frac1n\sum_ir_i$, $s(0)\sim\pi_0$ and $\gamma\in(0,1)$ is the discount factor.

A localized policy gives agent $i$ a parameter $\theta_i\in\mathbb R^{d_i}$ and a law $\zeta_i^{\theta_i}(\cdot\mid s_i)$ on $\mathcal A_i$; agents act independently, $\zeta^\theta(a\mid s)=\prod_i\zeta_i^{\theta_i}(a_i\mid s_i)$. The objective is $J(\theta)=\mathbb E_{s\sim\pi_0}\mathbb E[\sum_{t\ge0}\gamma^tr(s(t),a(t))\mid s(0)=s]$, and $Q_i^\theta(s,a)$ is the discounted sum of agent $i$'s rewards started from $(s,a)$.

The $(c,\rho)$-exponential decay property holds when, for every policy $\theta$ and agent $i$, $|Q_i^\theta(z)-Q_i^\theta(z')|\le c\rho^{\kappa+1}$ whenever $z=(s,a)$ and $z'$ agree on $N_i^\kappa$. Then a truncated Q-function, a weighted average of $Q_i^\theta$ over the coordinates outside $N_i^\kappa$, is a table on $\mathcal Z_{N_i^\kappa}=\mathcal S_{N_i^\kappa}\times\mathcal A_{N_i^\kappa}$ within $c\rho^{\kappa+1}$ of $Q_i^\theta$.

SAC (Algorithm 1) repeats, for $m=0,1,\dots$: draw an episode $z(0),\dots,z(T)$ under $\theta(m)$; each agent runs temporal-difference learning with step $\alpha_t=h/(t+t_0)$ on its local pairs $z_{N_i^\kappa}(t)$, producing a table $\hat Q^T_i$; then each agent forms $\hat g_i(m)=\sum_{t=0}^T\gamma^t\frac1n\sum_{j\in N_i^\kappa}\hat Q^T_j(z_{N_j^\kappa}(t))\nabla_{\theta_i}\log\zeta_i^{\theta_i(m)}(a_i(t)\mid s_i(t))$ and steps $\theta_i(m+1)=\theta_i(m)+\eta_m\hat g_i(m)$ with $\eta_m=\eta/\sqrt{m+1}$.

Formalization targets

Goal: Theorem 4

Under bounded rewards $0\le r_i\le\bar r$ and $|\mathcal S_i|\le S$, $|\mathcal A_i|\le A$ (Assumption 1), exponential decay with $\rho\le\gamma$ (Assumption 2), sufficient local exploration with parameters $\tau,\sigma$ (Assumption 3), and $\|\nabla_{\theta_i}\log\zeta_i\|\le L_i$, $L=\sqrt{\sum_iL_i^2}$, with $\nabla J$ $L'$-Lipschitz (Assumption 4), and for step sizes and an episode length $T$ satisfying explicit conditions, with probability at least $1-\delta$,

$$\frac{\sum_{m=0}^{M-1}\eta_m\|\nabla J(\theta(m))\|^2}{\sum_{m=0}^{M-1}\eta_m}\le\frac{\frac{2\bar r}{\eta(1-\gamma)}+\frac{8\bar r^2L^2}{(1-\gamma)^4}\sqrt{\log M\log\frac4\delta}+\frac{96\bar r^2L'L^2}{(1-\gamma)^4}\eta\log M}{\sqrt{M+1}}+\frac{12L^2c\bar r}{(1-\gamma)^5}\rho^{\kappa+1}.$$

The constants are those of the paper; the statement is the paper's Theorem 4 at full strength.

Milestones

The milestones follow the paper's proof, from foundations to the components of the main bound:

1. Lemma 1, the policy gradient theorem $\nabla J(\theta)=\frac{1}{1-\gamma}\mathbb E_{s\sim\pi^\theta,a\sim\zeta^\theta}[Q^\theta(s,a)\nabla\log\zeta^\theta(a\mid s)]$.
2. Lemma 3, accuracy of truncated Q-functions ($c\rho^{\kappa+1}$) and of the truncated policy gradient ($\frac{cL_i}{1-\gamma}\rho^{\kappa+1}$).
3. Lemma 17, the projected Bellman operator $g_d=\Pi_dT_D\Phi$: a $\gamma$-contraction in $\|\cdot\|_\infty$ whose fixed point is within $\frac{c\rho^{\kappa+1}}{1-\gamma}$ of $Q_i^\theta$.
4. Lemma 9 and Lemma 12, real-analysis bounds on the step-size products of the critic recursion.
5. Lemma 18, an Azuma–Hoeffding bound for martingale differences whose conditional mean vanishes $\tau$ steps back: $|\sum_{k=0}^tX_k|\le\sqrt{2\tau\sum_k\bar X_k^2\log(2\tau/\delta)}$.
6. Theorem 5, the critic bound $\sup_{(s,a)}|Q_i^\theta(s,a)-\hat Q^T_i(s_{N_i^\kappa},a_{N_i^\kappa})|\le\frac{C_a}{\sqrt{T+t_0}}+\frac{C_a'}{T+t_0}+\frac{2c\rho^{\kappa+1}}{(1-\gamma)^2}$ with probability $1-\delta$.
7. Lemmas 13–16, the bounds on the three error terms $e^1=\hat g-g$ (critic error), $e^2=g-h$ (sampling noise, a martingale difference) and $e^3=h-\nabla J$ (truncation), and the almost-sure norm bounds $\bar rL/(1-\gamma)^2$.

Significance

Theorem 4 is a finite-sample guarantee for a model-free multi-agent algorithm whose memory per agent depends on the size of the largest κ-hop neighbourhood, not on $n$. The bias term $O(\rho^{\kappa+1})$ quantifies how much communication radius buys: each additional hop shrinks the guaranteed gap to stationarity by a factor $\rho\le\gamma$. The truncation idea (Lemma 3) and the exponential decay property have since been used in a line of work on networked and mean-field reinforcement learning.

The result is proved in the paper; none of it is formalized. A complete formalization would give machine-checked versions of the policy gradient theorem for product policies, of a shifted Azuma–Hoeffding inequality, and of a finite-time analysis of tabular TD learning with state aggregation, each of which is reusable. Related platform items exist in other conventions: the discounted policy gradient theorem from a start state, SampleComplexityRL.PolicyGrad.discounted_policy_gradient, and the open RandomHorizonPG.Asymp.policy_gradient_theorem; the Hoeffding–Azuma inequality ModernOnlineLearning.OnlineToBatch.theorem_3_9 (the case $\tau=1$ of Lemma 18).

Difficulty

The critic is the hard part. The TD iterate on local pairs is not a stochastic approximation of a fixed operator: the sampling distribution of $z_{N_i^\kappa}(t)$ changes with $t$, consecutive samples are dependent, and the truncated table has no exact fixed point equal to $Q_i^\theta$. The usual argument for TD learning, a fixed contraction plus martingale-difference noise, fails at both ends: the operator moves with the sampling distribution, and the noise has zero conditional mean only given the information $\tau$ steps back. On the actor side, the critic error must be controlled simultaneously for all agents and all outer iterations, while the policy of each iteration depends on all earlier episodes.

Formalization scope

The setting is finite: agents are Fin n, local state and action sets are finite types, and parameters are $\theta_i\in\mathbb R^{d_i}$, with $\theta$ in PiLp 2 so that $\|\theta\|$ is the Euclidean norm of the whole tuple and $\nabla J$ is Mathlib's gradient. The local kernel of agent $i$ is typed on the restricted tuple $s_{N_i}$, so locality is part of the model. $Q_i^\theta$, $Q^\theta$ and $J$ are built from the published finite-MDP layer FoundationsML.ReinforcementLearning (QFunction, PolicyValue, OccupationDist) applied to the global MDP. Policies are assumed positive and differentiable in their parameters, which Assumption 4 presupposes. Assumption 3's "probability at time $\tau$ given $z(1)$" is the $(\tau-1)$-step law of the state-action chain.

Probabilities are explicit finite sums: the law of a run of SAC over $M$ outer iterations is the product of the episode probabilities, episode $m$ drawn under the policy $\theta(m)$ that the algorithm computed from the earlier episodes. The critic tables are functions on the local pairs $\mathcal Z_{N_i^\kappa}$, updated exactly as in (14), and the actor uses each neighbour's own table at its own local pair.

No hypothesis is vacuous: the assumptions hold together, for instance, for one agent with one state, two actions, a constant policy with zero-dimensional parameter, $\tau=2$, $\sigma=\frac12$, and $c,\rho>0$ with $\rho\le\gamma$. Contributions of any milestone are welcome; Lemmas 9, 12 and 18 are self-contained and need none of the model.

Selected references

• G. Qu, A. Wierman, N. Li, Scalable Reinforcement Learning for Multi-Agent Networked Systems, arXiv:1912.02906v3; Operations Research 70(6), 2022. https://arxiv.org/abs/1912.02906 · https://doi.org/10.1287/opre.2021.2226
• R. S. Sutton, D. McAllester, S. Singh, Y. Mansour, Policy gradient methods for reinforcement learning with function approximation, NeurIPS 2000. https://proceedings.neurips.cc/paper/1999/hash/464d828b85b0bed98e80ade0a5c43b0f-Abstract.html
• R. Srikant, L. Ying, Finite-time error bounds for linear stochastic approximation and TD learning, COLT 2019. https://arxiv.org/abs/1902.00923
• G. Qu, Y. Lin, A. Wierman, N. Li, Scalable multi-agent reinforcement learning for networked systems with average reward, NeurIPS 2020. https://arxiv.org/abs/2006.06626