Operations Research

Motivation

Distributionally robust optimization chooses a decision against a range of plausible probability laws instead of a single fitted law. Here the decision is a linear rule evaluated through a loss function. The range of laws is specified by how much probability mass may be transported away from a baseline law. A conventional transport cost depends only on the displacement. Blanchet, Murthy and Zhang allow the cost of moving a point to depend on its starting location, so the uncertainty model can reflect local information. Their introduction gives a portfolio example: uncertainty about returns may differ across market conditions, and a state dependent cost can encode that difference. The paper develops a dual reformulation as the basis for its later convexity, optimizer, and algorithmic results.

The theorem in this mission is the first structural result of that development. It says that evaluating the worst-case loss does not require optimizing directly over all probability distributions. A dual objective built from the baseline law gives the same value, and its nonnegative scalar multiplier attains the best value. The earlier general transport duality theorem of Blanchet and Murthy is already formalized and proved on Prove2Me; the remaining target here is the state dependent Mahalanobis specialization and its explicit scalar form.

Setting

Let $X\in\mathbb R^d$ have a baseline law $P_0$, and let $B\subseteq\mathbb R^d$ be a convex set of decisions. A decision $\beta\in B$ incurs loss $\ell(\beta^{\mathsf T}X)$, where $\ell:\mathbb R\to\mathbb R$. The transport cost of moving $x$ to $x'$ is

$$c(x,x')=(x-x')^{\mathsf T}A(x)(x-x'),$$

where $A(x)$ is positive definite at every $x$. Under Assumption 1, $c$ is lower semicontinuous, and the eigenvalues of $A(x)$ lie between fixed positive bounds $\rho_{\min}$ and $\rho_{\max}$ for $P_0$-almost every $x$. Since $A$ depends on the starting point, $c$ need not be symmetric. For two laws $P_0$ and $P$, $D_c(P_0,P)$ is the least expected cost among couplings whose first and second marginals are $P_0$ and $P$. The ambiguity set at radius $\delta>0$ consists of laws satisfying $D_c(P_0,P)\le\delta$. The paper writes the worst-case loss as an equivalent supremum over couplings with first marginal $P_0$ and cost at most $\delta$ (§2.1, p. 9).

For $x,\beta\in\mathbb R^d$, write $q_A(\beta,x)=\beta^{\mathsf T}A(x)^{-1}\beta$. The paper introduces a pointwise robust loss from

$$F(\gamma,\beta,\lambda;x)=\ell\bigl(\beta^{\mathsf T}x+\gamma\sqrt\delta\,q_A(\beta,x)\bigr)-\lambda\sqrt\delta\bigl(\gamma^2q_A(\beta,x)-1\bigr),$$

by setting $\ell_{\rm rob}(\beta,\lambda;x)=\sup_{\gamma\in\mathbb R}F(\gamma,\beta,\lambda;x)$ and $f_\delta(\beta,\lambda)=E_{P_0}[\ell_{\rm rob}(\beta,\lambda;X)]$. This expectation may be extended real. These are the objects of display (7) and Theorem 1 on p. 10.

Formalization targets

The goal is Theorem 1 of the paper. If $\ell$ is upper semicontinuous and the baseline loss is integrable, then for each $\beta\in B$,

$$\sup_{P:\,D_c(P_0,P)\le\delta}E_P[\ell(\beta^{\mathsf T}X)]=\inf_{\lambda\ge0}f_\delta(\beta,\lambda),$$

and a multiplier $\lambda^*(\beta)\ge0$ attains the infimum. The target retains the state dependence of $A$, the full range of $\beta$ in $B$, and the possible extended value of the worst-case loss. It asserts both the value identity and attainment; the latter is part of the printed theorem.

The milestone list follows the paper's proof on p. 32: the previously proved general strong duality theorem, the quadratic minimum under a linear constraint, and pointwise equality (25) between the transport envelope and $\ell_{\rm rob}$. The quadratic minimum is stated with attainment. The pointwise equality includes $\beta=0$ and records the change from the original transport multiplier to the scaled multiplier used in $F$.

Significance

The formula replaces a search over probability laws with a scalar outer optimization and an expectation under $P_0$. That representation is the paper's starting point for examining the shape of $f_\delta$, locating dual optimizers, describing worst-case laws, and designing iterative schemes. Without a faithful dual identity, those later claims would concern a function whose connection to the original distributional problem had not been established (Theorems 2–7).

The general Blanchet–Murthy strong duality theorem has a machine-checked proof on Prove2Me. This mission supplies the specialized model, the quadratic reduction, and the equality with the paper's $f_\delta$. Those declarations can then serve as a stable interface for the remaining missions in this series. The current goal and its new milestones are open Lean statements; the paper result itself is proved in the cited work.

Difficulty

The general duality theorem returns a dual problem whose envelope is a supremum over destination points in $\mathbb R^d$. The paper's formula instead uses one scalar $\gamma$, and its multiplier is scaled by $\sqrt\delta$. Showing that these describe the same value requires controlling a positive definite quadratic cost with a state dependent matrix at every starting point. At $\beta=0$, the hyperplane formula used in the nonzero case has a zero denominator, while equation (25) remains meaningful. Extended values also matter: the pointwise supremum can be infinite, and replacing it with a real-valued approximation could alter the theorem.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin d), laws are Borel probability measures, and matrices are real positive definite matrices. The local Setting definition fixes $c$, $q_A$, $F$, $\ell_{\rm rob}$, and $f_\delta$ using the paper's notation. The worst-case objective reuses the published coupling form ModelRiskOT.Duality.primalValue; its feasible plans already enforce the first marginal and cost budget. EReal carries the primal value, pointwise supremum, integral, and outer infimum. The extended integral is the published ModelRiskOT.Duality.extIntegral, with its documented convention for a difference of two infinite parts. The multiplier ranges over $\lambda\ge0$, and $\delta>0$ is explicit so its square root can be used in the rescaling.

The goal retains the paper's standing convexity of $B$, Assumption 1, and $\beta\in B$. It adds integrability of $x\mapsto\ell(\beta^{\mathsf T}x)$, required by the cited general duality theorem but omitted from the printed Theorem 1. This addition is disclosed so the statement's scope is clear. The goal equates the primal worst-case loss with the explicit infimum of $f_\delta$ and asserts attainment; an identity between two dual notations would leave the main claim unaddressed. Contributions to the positive definite quadratic minimization, the pointwise envelope equality, and their connection to the general duality theorem are in scope. The shared Setting layer is intended for reuse in the later convexity and worst-case-law missions.

Selected references

• J. Blanchet, K. Murthy and F. Zhang, Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes, Mathematics of Operations Research 47(2), 2022. arXiv:1810.02403v3
• J. Blanchet and K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Mathematics of Operations Research 44(2), 2019. arXiv:1604.01446v2

Motivation

Many noncooperative problems in communication networks, power markets and supply chains are stochastic Nash games. Each player minimizes an expected cost that depends on its own decision and on the decisions of its rivals, and the expectation can only be sampled, not evaluated. A natural distributed way to compute an equilibrium is the best-response scheme: each player repeatedly replies optimally to the rivals' current strategies. In a stochastic game an exact best response is itself an expectation-valued optimization problem, so a practical scheme replies inexactly, running a few stochastic gradient steps per reply. Lei, Shanbhag, Pang and Sen (arXiv:1704.04578v2; Mathematics of Operations Research, 2020) analyse three such inexact proximal best-response schemes: synchronous, randomized and asynchronous. For each they prove a linear rate of convergence and a bound on the total number of projected stochastic gradient steps.

This mission concerns the randomized scheme. In large games it is unrealistic for all players to update at every round; in the paper's model each player independently decides to update with probability $p_i$. This is the game-theoretic analogue of randomized block-coordinate descent (Nesterov 2012; Richtárik–Takáč 2014). A local Poisson clock per player is a special case (Remark 5 of the paper). The synchronous scheme, the paper's Theorem 1, and the asynchronous scheme are separate missions of this series.

Setting

There are $N \ge 1$ players. Player $i$ chooses $x_i$ in a compact convex set $X_i \subseteq \mathbb R^{n_i}$ and minimizes

$$f_i(x_i, x_{-i}) = \mathbb E\big[\psi_i(x_i, x_{-i}; \xi)\big],$$

where $\xi$ is a random vector and the oracle returns sampled gradients $\nabla_{x_i}\psi_i(x; \xi)$ with $\mathbb E\|\nabla_{x_i}\psi_i\|^2 \le M_i^2$ (Assumption 1). A Nash equilibrium $x^*$ is a profile in $X = \prod_i X_i$ from which no player can lower its cost by deviating alone.

For $\mu > 0$ the proximal best response to a profile $y$ is

$$\widehat x_i(y) = \operatorname*{argmin}_{x_i \in X_i}\Big[f_i(x_i, y_{-i}) + \tfrac{\mu}{2}\|x_i - y_i\|^2\Big].$$

The $N\times N$ matrix $\Gamma$ has entries $\gamma_{ii} = \mu/(\mu + \zeta_{i,\min})$ and $\gamma_{ij} = \zeta_{ij,\max}/(\mu + \zeta_{i,\min})$, built from the extreme curvatures $\zeta_{i,\min} = \inf_X \lambda_{\min}(\nabla^2_{x_i}f_i)$ and $\zeta_{ij,\max} = \sup_X\|\nabla^2_{x_ix_j}f_i\|$. Assumption 2 is $a = \|\Gamma\| < 1$ (spectral norm).

Algorithm 2. At major iteration $k$, each player $i$ flips an independent coin $\chi_{i,k} \in \{0,1\}$ with $\mathbb P(\chi_{i,k} = 1) = p_i > 0$, independent of the past information $\mathcal F_k$ (Assumption 3). If $\chi_{i,k} = 1$, the player replaces $x_{i,k}$ by an inexact proximal best response $x_{i,k+1} \in X_i$ with

$$\mathbb E\big[\|x_{i,k+1} - \widehat x_i(x_k)\|^2 \mid \mathcal F_k\big] \le \alpha_{i,k}^2;$$

otherwise $x_{i,k+1} = x_{i,k}$. The accuracy $\alpha_{i,k} = \eta^{\beta_{i,k}+1}$ is tied to the number of updates $\beta_{i,k} = \sum_{l<k}\chi_{i,l}$ the player has made so far. The reply is computed by $j_{i,k} = \lceil Q_i/\eta^{2(\beta_{i,k}+1)}\rceil$ projected stochastic gradient steps

$$z_{i,t+1} = \Pi_{X_i}\big[z_{i,t} - \gamma_t\big(\nabla_{x_i}\psi_i(z_{i,t}, x_{-i,k}; \xi^t_{i,k}) + \mu(z_{i,t} - x_{i,k})\big)\big],\qquad \gamma_t = \tfrac{1}{\mu(t+1)},$$

from $z_{i,1} = x_{i,k}$, where $Q_i = 2M_i^2/\mu^2 + 2D_{X_i}^2$ and $D_{X_i}$ is the diameter of $X_i$. The analysis uses the weighted norm $\|x\|_P^2 = \sum_i \|x_i\|^2/p_i$ and the constants $\tilde a^2 = 1 - p_{\min}(1 - a^2)$, $\tilde\eta^2 = 1 - p_{\min}(1 - \eta^2)$ and $\tilde\eta_0^{-2} = p_{\max}(\eta^{-2} - 1) + 1$.

Formalization targets

Goal: Theorem 2, (34)

Let $\tilde c = \max\{\tilde a, \tilde\eta\}$, $\tilde q \in (\tilde c, 1)$, $D = 1/(e\ln(\tilde q/\tilde c))$, $\tilde C = C(\sum_i N^{-1}p_i^{-1})^{1/2}$, $\tilde D = D\eta/\tilde\eta$ and $\tilde\epsilon = \epsilon/((Np_{\max})^{1/2}(\tilde C + \tilde D)) \in (0,1)$, where $\|x_{i,0} - x_i^*\| \le C$. After $K = \lceil\ln(1/\tilde\epsilon)/\ln(1/\tilde q)\rceil$ major iterations, $x_K$ is an $\epsilon$-NE$_2$, i.e. $\mathbb E\big(\sum_i\|x_{i,K} - x_i^*\|^2\big)^{1/2} \le \epsilon$, and for every player

$$\mathbb E\Big[\sum_{k=0}^{K-1} j_{i,k}\chi_{i,k}\Big] \le \frac{p_iQ_i}{\eta^2\tilde\eta_0^2\ln(1/\tilde\eta_0^2)}\Big(\frac1{\tilde\epsilon}\Big)^{\ln(1/\tilde\eta_0^2)/\ln(1/\tilde q)} + \Big\lceil\frac{\ln(1/\tilde\epsilon)}{\ln(1/\tilde q)}\Big\rceil.$$

Milestones

In the order the proof uses them:

1. the $\Gamma$-contraction (5);
2. its Euclidean form (9);
3. the fixed-point identity $\widehat x(x^*) = x^*$;
4. the one-step descent (A.3) and its contraction form (B.1) in $\|\cdot\|_P$;
5. the binomial moments (B.3) and (36) of $\eta^{\pm2\beta_{i,k}}$;
6. the elementary inequalities Lemma 2 ($zc^z \le Dq^z$) and (30) (a geometric sum bounded by an integral);
7. the linear rate, Lemma 5: $\mathbb E\|x_k - x^*\|_P \le \sqrt N(\tilde C + \tilde D)\tilde q^k$;
8. its transfer to the unweighted error, Remark 6;
9. the inner-loop bound, Lemma 6: $\mathbb E[\|z_{i,t} - \widehat x_i(y_k)\|^2 \mid \mathcal F_k] \le Q_i/(t+1)$.

Significance

Theorem 2 gives an explicit, non-asymptotic sample complexity for computing a Nash equilibrium of a stochastic game when only a random subset of players acts at each round. Its exponent $\ln(1/\tilde\eta_0^2)/\ln(1/\tilde q)$ quantifies the price of randomization: Remark 7 of the paper shows it reduces to the synchronous exponent exactly when every $p_i = 1$. Lemma 5 is the first linear-rate statement for inexact randomized best responses in this setting. The weighted-norm argument of App. A–B is the device that makes block-randomized fixed-point iterations contract.

The results are proved on paper. None of them has a machine-checked proof, and the platform holds no stochastic Nash game, proximal best-response map or randomized best-response scheme. A formal proof checks every constant of (34), including the interplay of the random inexactness $\eta^{\beta_{i,k}+1}$ with the random number of steps $j_{i,k}$. The paper does not prove (5): it adapts it from Facchinei–Pang 2009. A formal proof of (5) closes that gap.

Difficulty

The conditional-expectation bookkeeping is where a naive argument fails. The accuracy $\alpha_{i,k}$ and the step count $j_{i,k}$ are random, being functions of the past coins. The coin $\chi_{i,k}$ must be independent of both the past and the samples the player uses in round $k$. The descent step (A.4) multiplies the coin with the inexactness error, and its factorization uses exactly this joint independence. Bounding the expected work requires the moment generating identities (B.3) and (36) of a binomial count, with two different constants $\tilde\eta$ (through $p_{\min}$) and $\tilde\eta_0$ (through $p_{\max}$). Merging them gives a false bound. Lemma 6 is a stochastic approximation estimate conditional on $\mathcal F_k$, at a random, $\mathcal F_k$-measurable centre $\widehat x_i(x_k)$. Applying the unconditional $O(1/t)$ bound for strongly convex SGD pointwise is not enough. On the deterministic side, (5) needs a mean-value argument along a segment in the product space, using the mixed Hessian blocks.

Formalization scope

Players are Fin N and player $i$'s space is EuclideanSpace ℝ (Fin (n i)). Costs are functions of the whole profile. The Euclidean norm of the vector of block norms and the weighted norm $\|\cdot\|_P$ are written out explicitly, since Lean's norm on the product type is the sup norm. $\|\Gamma\|$ is the operator norm on Euclidean $\mathbb R^N$. $\zeta_{i,\min}$ is an infimum of Rayleigh quotients. The proximal best response is any map satisfying the argmin property on $X$. $\Pi_{X_i}$ is any map satisfying the published SpectralProjGrad.Shared.IsProjOnto. Randomness lives on a probability space with a filtration $(\mathcal F_k)$, and conditional expectations are Mathlib's condExp.

Statement repairs, all recorded in the items' Formalization Notes:

• Starting point. $x_0$ is deterministic, with $\|x_{i,0} - x_i^*\| \le C$. The proof's bound $\|x_0 - x^*\|_P \le C(\sum_i p_i^{-1})^{1/2}$ fails for a random start with only a first-moment bound.
• Regularity. $f_i$ is $C^2$ jointly in the profile on a neighbourhood of $X$, which the mixed blocks of (4) require.
• Independence. Assumption 3 is read as $\chi_{i,k}$ independent of $\mathcal F_k$ together with player $i$'s round-$k$ samples (or candidate), as step (A.4) needs.
• Sampling. Samples are drawn for every player at every round and used only when $\chi_{i,k} = 1$; in law this is the paper's scheme.
• Range of $\tilde\epsilon$. $\tilde\epsilon < 1$ is assumed.
• Integrability. Every expectation hypothesis carries an integrability condition.
• $D$. $D$ reads $1/\ln((q/c)^e)$ as $1/(e\ln(q/c))$.
• Excluded. Statement (35), the case $\eta = a$, is not formalized.

A formalization in which the coins are almost surely $1$ is the synchronous scheme, not this one. Coins and samples here are genuinely random with the stated laws and independence, and the expectation bounding the work is taken over both.

Reusable infrastructure includes the conditional $O(1/t)$ bound for projected SGD on strongly convex problems (Lemma 6), the binomial moment identities (B.3)/(36), and Lemma 2 and (30). Contributions of intermediate lemmas, such as (A.4)–(A.5), (B.2) and the measurability of the iterates, are welcome as separate theorems.

Selected references

• J. Lei, U. V. Shanbhag, J.-S. Pang, S. Sen, On Synchronous, Asynchronous, and Randomized Best-Response Schemes for Stochastic Nash Games, arXiv:1704.04578v2, 2018 (Mathematics of Operations Research, 2020). https://arxiv.org/abs/1704.04578v2
• F. Facchinei, J.-S. Pang, Nash equilibria: the variational approach, in Convex Optimization in Signal Processing and Communications, Cambridge University Press, 2009. https://doi.org/10.1017/CBO9780511804458.013
• Y. Nesterov, Efficiency of coordinate descent methods on huge-scale optimization problems, SIAM Journal on Optimization 22(2), 2012. https://doi.org/10.1137/100802001
• P. Richtárik, M. Takáč, Iteration complexity of randomized block-coordinate descent methods for minimizing a composite function, Mathematical Programming 144, 2014. https://doi.org/10.1007/s10107-012-0614-z
• H. Robbins, S. Monro, A stochastic approximation method, Annals of Mathematical Statistics 22, 1951. https://doi.org/10.1214/aoms/1177729586

Motivation

Many equilibrium problems in operations research have the form of a stochastic Nash game: each of $N$ players minimizes an expected cost that depends on the strategies of the others, and the expectation can only be sampled. The paper's introduction lists applications in generation-capacity and power markets and in communication networks (Abada, de Maere d'Aertrycke and Smeers, 2017; Başar, 2007). A natural way to compute an equilibrium is a best-response scheme: each player repeatedly re-optimizes against the current strategies of its rivals. In a large network the players cannot synchronize. They update at different times and see their rivals' strategies with delays.

Lei, Shanbhag, Pang and Sen (arXiv:1704.04578v2; Mathematics of Operations Research, 2020) analyze inexact proximal best-response schemes in three regimes: synchronous, randomized and asynchronous. This mission formalizes the asynchronous one (§5 and Appendix C). It adapts the partially asynchronous iterations of Bertsekas and Tsitsiklis (1989) to stochastic games with inexact, sampled best responses, and it gives an explicit bound on the number of stochastic gradient steps each player needs.

Setting

Player $i$ chooses $x_i$ in a nonempty compact convex set $X_i \subseteq \mathbb R^{n_i}$. A profile is $x = (x_1,\dots,x_N) \in X = \prod_i X_i$. Player $i$'s cost is $f_i(x_i, x_{-i}) = \mathbb E[\psi_i(x_i, x_{-i};\xi)]$, which is convex and twice continuously differentiable in a neighbourhood of $X$. A sampling oracle returns $\nabla_{x_i}\psi_i(x;\xi)$, whose second moment is at most $M_i^2$ (Assumption 1). A Nash equilibrium $x^*$ is a profile in which each $x^*_i$ minimizes $f_i(\cdot, x^*_{-i})$ over $X_i$.

For $\mu > 0$, the proximal best response of player $i$ to a profile $y \in X$ is

$$\hat x_i(y) = \operatorname*{argmin}_{x_i \in X_i}\Big[f_i(x_i, y_{-i}) + \tfrac{\mu}{2}\|x_i - y_i\|^2\Big].$$

The curvature constants $\zeta_{i,\min} = \inf_{x\in X}\lambda_{\min}(\nabla^2_{x_i}f_i(x))$ and $\zeta_{ij,\max} = \sup_{x\in X}\|\nabla^2_{x_ix_j}f_i(x)\|$ define the matrix $\Gamma$ with $\gamma_{ii} = \mu/(\mu+\zeta_{i,\min})$ and $\gamma_{ij} = \zeta_{ij,\max}/(\mu+\zeta_{i,\min})$. Assumption 5 (strict diagonal dominance) asks $\zeta_{i,\min} > \sum_{j\ne i}\zeta_{ij,\max}$. It makes $a_\infty = \|\Gamma\|_\infty$, the maximum absolute row sum, smaller than one.

The asynchronous scheme (Algorithm 3) runs on a deterministic schedule. At time $k$ the players in $I_k$ update. Player $i \in I_k$ sees the outdated profile $y^i_k = (x_{1,k-\tau_{i1}(k)},\dots,x_{N,k-\tau_{iN}(k)})$ and computes $x_{i,k+1} \in X_i$ with

$$\mathbb E\big[\|x_{i,k+1} - \hat x_i(y^i_k)\|^2 \mid \mathcal F_k\big] \le \alpha_{i,k}^2 .$$

The other players keep their strategies. Assumption 4 requires every player to update at least once in every $B_1$ consecutive times, and every delay to be at most $B_2$. The accuracy is $\alpha_{i,k} = \eta^{\beta_{i,k}}$, where $\beta_{i,k}$ counts player $i$'s updates so far. The inexact response is computed by $j_{i,k} = \lceil Q_i/\eta^{2(k+1)}\rceil$ projected stochastic gradient steps (43), with step size $1/(\mu(t+1))$ and $Q_i = 2M_i^2/\mu^2 + 2D_{X_i}^2$. Write $n_0 = \lceil B_2/B_1\rceil$, $\rho = (\max\{a_\infty,\eta\})^{1/(n_0+1)}$ and $c = \rho^{1/B_1}$.

Formalization targets

Goal: Theorem 3, (45)

Let $q \in (c,1)$, $D \ge 1/(e\ln(q/c))$, $\epsilon > 0$, and

$$\hat\epsilon = \frac{\epsilon}{C+D}\,\rho^{\frac{B_1-1}{B_1}} < 1,$$

where $\mathbb E\|x_{i,0}-x^*_i\|^2 \le C^2$. After $K = \lceil \ln(1/\hat\epsilon)/\ln(1/q)\rceil$ major iterations, $\max_i \mathbb E\|x_{i,K}-x^*_i\| \le \epsilon$, and player $i$ has taken at most

$$\ell^{(1)}_i(\eta) = \frac{Q_i}{\eta^4\ln(1/\eta^2)}\Big(\frac1{\hat\epsilon}\Big)^{\frac{\ln(1/\eta^2)}{\ln(1/q)}} + \Big\lceil\frac{\ln(1/\hat\epsilon)}{\ln(1/q)}\Big\rceil$$

projected gradient steps.

Milestones

In the order the proof uses them:

• the $\Gamma$-contraction (5) of the proximal best response;
• the fixed-point identity $x^*_i = \hat x_i(x^*)$;
• $a_\infty < 1$ under Assumption 5;
• its expected $\infty$-norm form (40), $\mathbb E\|\hat x_i(y)-x^*_i\| \le a_\infty\max_j\mathbb E\|y_j-x^*_j\|$;
• the one-step recursion (C.2) and the delay step (C.3) of Appendix C;
• Lemma 2, $zc^z \le Dq^z$;
• Lemma 7, the rate

$$\max_i\mathbb E\|x_{i,k}-x^*_i\| \le (C+k)\rho^{\lfloor k/B_1\rfloor},\qquad \max_i\mathbb E\|x_{i,k}-x^*_i\| \le \rho^{-\frac{B_1-1}{B_1}}(C+D)q^k;$$

• Lemma 8, the $Q_i/(t+1)$ mean-square error of the inner stochastic approximation loop;
• the summation bound (30).

Significance

Theorem 3 makes the cost of asynchrony explicit. Bounded delays and a bounded update window enter only through the rate per window, $\max\{a_\infty,\eta\}^{1/(n_0+1)}$. The overall effort stays polynomial in $1/\epsilon$, and the paper's Table 1 summarizes the exponent as $2B_1(1+\lceil B_2/B_1\rceil)+\delta$ for a suitable choice of $q$. The result connects classical partially asynchronous fixed-point theory with the sample-complexity analysis of stochastic approximation. Lemma 7 holds for any inexact solver that achieves the accuracy (38), not only for the stochastic gradient loop, so it applies to other subproblem solvers as well.

The paper proves these results by hand. As far as is known, no part of them has been machine-checked: there is no formal treatment of stochastic Nash games, of proximal best-response maps, or of asynchronous iterations with delays in Mathlib or on this platform. A formalization would check the induction over windows in Appendix C, whose index bookkeeping has several printed slips. It would also make precise which properties of the delays the argument needs.

Difficulty

The obvious argument does not carry over from the synchronous case. There, one step of the scheme contracts the whole error vector by $a$ in one norm. Here a step updates only some players, and each of them uses information up to $B_2$ steps old. No single step contracts anything. The proof has to show that every window of $B_1$ steps contracts the worst-case expected error by a factor $\rho$, with the delays absorbed into the root $1/(n_0+1)$. This requires a nested induction with case distinctions on the window position (Appendix C). The analysis also mixes three layers: a deterministic contraction of the exact best response; conditional expectations, Jensen's inequality and adaptedness for the inexact responses; and an $O(1/t)$ stochastic-approximation bound for the inner loop, which in turn needs strong convexity, the first-order optimality conditions and nonexpansiveness of the projection.

Formalization scope

Players are indexed by Fin N. Player $i$'s space is EuclideanSpace ℝ (Fin (n i)), and costs are functions of the whole profile: $f_i(z, y_{-i})$ is f i (Function.update y i z). The projection $\Pi_{X_i}$ is any map satisfying the published predicate SpectralProjGrad.Shared.IsProjOnto. The proximal best response is a map constrained by an argmin predicate on $X$. $\zeta_{i,\min}$ and $\zeta_{ij,\max}$ are Rayleigh-quotient infima and suprema of second Fréchet derivatives, and $\|\Gamma\|_\infty$ is the maximum absolute row sum. The probability space carries a filtration $(\mathcal F_k)$ to which the iterates are adapted. The inner-loop $\sigma$-algebras $\sigma\{\mathcal F_k,\xi^{[t-1]}_{i,k}\}$ are parameters satisfying the inclusions the proof uses. Conditional expectations are Mathlib's condExp.

Statement repairs and implicit hypotheses, each recorded in the item it affects:

• Deterministic delays. Assumption 4(c) allows random delays, but step (C.5) of the proof bounds an expectation at a random past time by the maximum over past times. That step is valid only when the delays do not depend on the iterates. The delays here are deterministic functions $\tau_{ij}(k) \le k$ with $\tau_{ii}(k) = 0$.
• Oracle second moment. Lemma 8 prints $\psi_i$ for $\nabla_{x_i}\psi_i$, and its hypothesis $\mathbb E[\|\nabla_{x_i}\psi_i\|^2\mid\cdot] = \|\nabla_{x_i}f_i\|^2$ forces zero noise. The bound $\le M_i^2$ that the proof uses replaces it.
• Regularity. Joint $C^2$ regularity of $f_i$ is assumed, which the mixed Hessian blocks in $\Gamma$ need, and $X_i$ is nonempty.
• Constants. Theorem 3 assumes $C \ge 0$ and $\hat\epsilon < 1$. Its "$D \ge /\ln((q/c)^e)$" is read as $D \ge 1/(e\ln(q/c))$, as in Lemma 7.
• Step count. Theorem 3 counts the steps over player $i$'s update times; the proof's bound is for the larger sum over all times.

The special case $B_1 = 1$, $B_2 = 0$ of Theorem 3, Corollary 3 (cyclic updates) and Theorem 4 are not stated.

The goal cannot be met trivially. The schedule is a parameter, not "every player at every step". The sampled gradients may be genuinely random, since the second-moment hypothesis is an inequality. $\hat x$ is tied to $f_i$ by its argmin property, and $x^*$ is a Nash equilibrium. Each expectation in a conclusion is of a bounded measurable quantity, so it cannot vanish by non-integrability.

The development needs the following:

• the contraction (5), which the paper only cites from Facchinei and Pang (2009, §12.6.1) and which uses the mean-value theorem along segments in $X$;
• strong-convexity optimality conditions on convex sets;
• nonexpansiveness of Euclidean projections;
• conditional Jensen and tower arguments;
• an integer-index induction over windows.

The projection and strong-convexity lemmas, and (5) itself, are reusable for the synchronous and randomized missions of this series. Proofs of individual milestones, or of general Mathlib-level facts such as the first-order optimality condition over a convex set, are welcome.

Selected references

• J. Lei, U. V. Shanbhag, J.-S. Pang, S. Sen, On Synchronous, Asynchronous, and Randomized Best-Response Schemes for Stochastic Nash Games, arXiv:1704.04578v2, 2018; Mathematics of Operations Research, 2020, https://doi.org/10.1287/moor.2018.0986. https://arxiv.org/abs/1704.04578v2
• D. P. Bertsekas, J. N. Tsitsiklis, Parallel and Distributed Computation: Numerical Methods, Prentice Hall, 1989 (reference [9] of the paper).
• F. Facchinei, J.-S. Pang, Nash equilibria: the variational approach, in Convex Optimization in Signal Processing and Communications, Cambridge University Press, 2009 (reference [19] of the paper).
• I. Abada, G. de Maere d'Aertrycke, Y. Smeers, On the multiplicity of solutions in generation capacity investment models with incomplete markets, Mathematical Programming 165(1):5–69, 2017 (reference [1] of the paper).

Motivation

The lost-sales inventory model with a positive lead time is one of the basic models of inventory theory. A retailer reviews stock once per period, places an order that arrives $L$ periods later, and loses (rather than backlogs) any demand that cannot be met from stock on hand. Lost sales are the norm in retail, where a customer facing an empty shelf buys elsewhere. The optimal policy is the solution of a dynamic program whose state is the on-hand inventory together with the whole pipeline of $L$ outstanding orders. The state dimension therefore grows with the lead time, and computing the optimal policy is intractable beyond small $L$: for a lead time of four and geometric demand the dynamic program already has 228,581 states (Zipkin 2008a, Operations Research 56(5), 1256–1263).

Heuristics (base-stock, myopic, cost-balancing) have been studied at length. Reiman (2004) analyzed an open-loop policy that orders one unit at fixed intervals in a continuous-review lost-sales model with Poisson demand. Zipkin (2008a) observed numerically that ordering the same constant amount every period performs well already at lead time four. Huh, Janakiraman, Muckstadt and Rusmevichientong (2009) proved that order-up-to policies are asymptotically optimal as the lost-sales penalty grows. Goldberg, Katz-Rogozhnikov, Lu, Sharma and Squillante proved that a constant-order policy is asymptotically optimal as the lead time grows, with an explicit threshold. This mission formalizes that result, Theorem 1 of their paper.

Setting

Fix a holding cost $h>0$ per unit left over at the end of a period, a lost-demand penalty $c>0$ per unit of unmet demand, a lead time $L\ge1$, and a horizon $T>L$. Demands $D_1,D_2,\dots$ are i.i.d. with a law $\mathcal D$ on $[0,\infty)$ that has a finite third moment and is not deterministic. At the start of period $t$ the system holds inventory $I_t$ and a pipeline $\mathbf x_t=(x_{1,t},\dots,x_{L,t})$ of outstanding orders. First $x_{1,t}$ arrives; then an order is placed and joins the end of the pipeline; then $D_t$ is realized, and

$$I_{t+1}=(I_t+x_{1,t}-D_t)^+,\qquad C_t=hI_{t+1}+c\,(I_t+x_{1,t}-D_t)^-.$$

The system starts empty. A policy chooses each order from the information available before the period's demand, possibly with randomization. Problem (1) is

$$\mathrm{OPT}(L,T)=\inf_{\pi}\sum_{t=L+1}^{T+L}\mathbb E[C^\pi_t].$$

For $r\ge0$ let $I^r_\infty=\sup_{k\ge0}\big(kr-\sum_{i=1}^kD_i\big)$, the steady-state waiting time of a GI/D/1 queue. For $r<\mathbb E[D]$ the constant-order policy $\pi_r$ orders the random amount $I^r_\infty+r$ (drawn independently of the demands) in the first period and $r$ in every later period. The best constant is $z=\arg\min_{v\ge0}(h\mathbb E[I^v_\infty]-cv)$ (the smallest minimizer). With $Q$ the $c/(c+h)$ quantile of $\mathcal D$, $g=h\mathbb E[(Q-D)^+]+c\mathbb E[(D-Q)^+]$, $\sigma$ the standard deviation and $\zeta$ the skewness of $D$, set $m=\lceil(26(3\zeta+c(h\sigma)^{-1}\mathbb E[D]+1))^2\rceil$ and

$$y(\epsilon)=\max\Big(2^{14}h(Q+2^{3/2}\mathbb E[D])(\mathbb E^2[D]+\mathbb E[D^2])^3\sigma^{-6}m^3g^{-1}\epsilon^{-1},\ \big(12c\,\mathbb E[D]\,g^{-1}((2ch^{-1})^{1/2}+3)\big)^2\epsilon^{-2}\Big).$$

Formalization targets

Goal: Theorem 1

For all $\epsilon\in(0,1)$, $L\ge y(\epsilon)$ and $T\ge(1+3\epsilon^{-1})L$,

$$\mathbb E\Big[\sum_{t=L+1}^{T+L}C^{\pi_z}_t\Big]\ \le\ (1+\epsilon)\,\mathrm{OPT}(L,T).$$

Milestones

The milestones follow the paper's argument in its order:

• the cost of $L$ consecutive periods from a given state (Lemma 3) and under $\pi_r$ (Lemma 4);
• a bounded optimal policy (Lemma 5) and the existence of a most favourable state $(\mathbf x^*,\mathcal I^*)$ (§5);
• lower bounds on the optimal cost over $L$ periods (Lemmas 6, 7);
• random-walk estimates ((26) and Lemma 9) and the per-window gap of $\pi_{r^*}$, $r^*=L^{-1}\sum_ix^*_i$ (Theorem 8);
• an explicit Lipschitz CLT rate (Theorem 11), the separation $\mathbb E[D]-r^*\ge\frac12\sigma m^{-1/2}$ (Lemma 10), and the resulting explicit gap (Corollary 12);
• the newsvendor bound $\mathbb E[C^\pi_t]\ge g$ (§3.1) and the stationary cost of $\pi_r$, (25).

Significance

The theorem says that the policy which ignores the state entirely, ordering the same amount every period after a single randomized first order, loses at most a factor $1+\epsilon$ against the optimal policy once the lead time exceeds an explicit threshold. The threshold depends only on $h$, $c$ and the demand law. Optimal policies are out of computational reach precisely when $L$ is large, so this is the first guarantee of near-optimality whose computation does not grow with the lead time. The paper's Corollary 2 (the ratio tends to $1$ as $L\to\infty$) follows directly.

The result is proved in the paper (up to the correction below); this platform holds no formalization of it or of its lemmas. A formalization would produce reusable statements about suprema of random walks with negative drift (Lemma 9, (26)), a quantitative central limit theorem for Lipschitz test functions (Theorem 11), and the finite-horizon lost-sales problem built on the published model of this platform.

Difficulty

The obvious comparison fails. An optimal policy may vary its orders arbitrarily over time, so its pipeline need not look like a constant stream. Comparing it period by period with $\pi_r$ gives nothing, because the inventory of $\pi_r$ is driven by an unbounded random-walk supremum.

The paper instead bounds the optimal cost over any $L$ consecutive periods by the cost from the most favourable state. It then has to show that the average $r^*$ of that state's pipeline stays bounded away from $\mathbb E[D]$ uniformly in $L$. This last step is the crux. The components of $\mathbf x^*$ may vary considerably over the window, and a qualitative central limit theorem is not enough: the argument needs an explicit rate (Theorem 11) with constants that survive summation over $L$ windows. On the probabilistic side, the expectations of random indices $i^r_k$ at which random walks attain their maxima are not adapted to the demand filtration. They are controlled only through the distributional identity of Lemma 9 and the geometric tail (26).

Formalization scope

The model is the published CappedBaseStock_Model. Its parameter record supplies $L\ge1$, $h>0$ and the penalty $c>0$ (field p; the record is called prm). Its demand law supplies a probability law on $[0,\infty)$ with finite positive mean. The finite third moment and non-determinism are explicit hypotheses. $Q$ and $g$ are the published newsvendorLevel and backorderCost. The conventions:

• Time is zero-based: Lean period $t$ is the paper's period $t+1$, and a window starting at Lean $t_0$ is the paper's $\tau=t_0+1$. Pipeline slot $i$ is $x_{i+1}$.
• Costs, OPT and expectations of nonnegative quantities are lower integrals in $[0,\infty]$, and $I^r_\infty$ is valued in $[0,\infty]$. Real expectations appear only for integrable quantities.
• OPT is the infimum over the model's admissible policies: measurable functions of past demands and a private uniform seed. This class contains the paper's policy class, so OPT is at most the paper's and the goal is at least as strong as the page.
• "Conditional on $\mathbf x^\pi_\tau=\mathbf x$, $I^\pi_\tau=\mathcal I$" is rendered by running the system from that state. Lemma 3 states that this integrates back to the policy's cost.
• Lemmas 6–7, Theorem 8 and Corollary 12 are stated for every policy that almost surely never orders more than $Q$, which includes the paper's optimal $\bar\pi$; their proofs use only that bound.
• $\pi_r$ draws its first order as the quantile function of $I^r_\infty$ at the policy's uniform seed.
• The ratio of Theorem 1 is stated multiplicatively. A ratio would read $0$ at $\mathrm{OPT}=0$, whereas $\mathrm{OPT}(L,T)\ge Tg>0$.

A correction. As printed, the second term of $y(\epsilon)$ (p. 5) and of Corollary 12 (p. 14) lack a factor $\mathbb E[D]$. The proof of Corollary 12 establishes $\mathcal I^*\le(\lceil(2ch^{-1}L)^{1/2}\rceil+2)\mathbb E[D]$, and the printed bounds are not invariant under rescaling the demand. Both are stated here with the factor restored, and each item's note says so.

Neither a long-run average cost nor a restricted comparator (stationary, Markov, or bounded-order) may replace the finite-horizon OPT. The demand law may not be specialized, and $\pi_r$ may not order $r$ in its first period: each change makes the goal a different, easier theorem.

A complete development needs Lindley-type recursions and the stationarity of the GI/D/1 waiting time, Chernoff and moment bounds for random-walk maxima, a Stein-method CLT rate, and the existence of optimal policies for a finite-horizon problem with a continuous state. The random-walk and CLT parts are independent of inventory theory and reusable. Proofs of any milestone are welcome, as are alternative proofs of the goal.

Selected references

• D. A. Goldberg, D. A. Katz-Rogozhnikov, Y. Lu, M. Sharma, M. S. Squillante, Asymptotic Optimality of Constant-Order Policies for Lost Sales Inventory Models with Large Lead Times, Mathematics of Operations Research, 2016; preprint arXiv:1211.4063v2 (cited version). https://arxiv.org/abs/1211.4063
• P. Zipkin, Old and New Methods for Lost-Sales Inventory Systems, Operations Research 56(5), 1256–1263, 2008.
• P. Zipkin, On the Structure of Lost-Sales Inventory Models, Operations Research 56(4), 937–944, 2008.
• W. T. Huh, G. Janakiraman, J. A. Muckstadt, P. Rusmevichientong, Asymptotic Optimality of Order-Up-To Policies in Lost Sales Inventory Systems, Management Science 55(3), 404–420, 2009.
• M. Reiman, A New and Simple Policy for a Continuous Review Lost-Sales Inventory Model, unpublished manuscript, 2004.
• L. H. Y. Chen, Q.-M. Shao, Stein's Method for Normal Approximation, in An Introduction to Stein's Method, 1–59, 2005.
• S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003.