Algorithmic Game Theory

Motivation

Mean-field games were introduced by Lasry and Lions (2007) and by Huang, Malhamé and Caines (2006) as limits of stochastic differential games with many symmetric players, each interacting with the others only through the empirical distribution of their states. The limit replaces a game of $N$ coupled players by one representative player facing a deterministic flow of distributions that it must reproduce. That flow is the equilibrium condition. The limit object is easier to solve. Whether it says anything about the finite game it came from is a separate question: a mean-field equilibrium is useful only if the strategies it produces are nearly optimal for each of $N$ actual players.

Carmona and Delarue (SIAM J. Control Optim. 51, 2013) solve the mean-field game through the stochastic maximum principle. For drifts that are affine and costs that are convex, the equilibrium is the solution of a forward–backward SDE of McKean–Vlasov type. Its existence is the subject of the first mission of this series. This mission formalizes §4 of the paper. The strategies read off from that solution are an approximate Nash equilibrium of the $N$-player game, with an explicit rate in $N$.

Setting

The state space is $\mathbb R^d$ and the control space is $\mathbb R^k$, both with the Euclidean norm. Each player $i$ has a private state $U^i_t$, driven by its own $m$-dimensional Brownian motion $W^i$, the motions being independent. The dynamics are

$$dU^i_t = b(t, U^i_t, \bar\nu^N_t, \beta^i_t)\,dt + \sigma\,dW^i_t,\qquad U^i_0 = x_0,\qquad \bar\nu^N_t = \frac1N\sum_{j=1}^N\delta_{U^j_t},$$

where $b(t,x,\mu,\alpha) = b_0(t,\mu) + b_1(t)x + b_2(t)\alpha$ is affine and $\sigma$ is a constant matrix. Player $i$ chooses a strategy $\beta^i$, a process that is progressively measurable for the filtration of $(W^1,\dots,W^N)$ and satisfies $\mathbb E\int_0^T|\beta^i_t|^2dt<\infty$. It pays

$$\bar J^{N,i}(\beta^1,\dots,\beta^N) = \mathbb E\Big[g(U^i_T,\bar\nu^N_T) + \int_0^T f(t,U^i_t,\bar\nu^N_t,\beta^i_t)\,dt\Big].$$

The costs $f$, $g$ satisfy the paper's assumptions (A.1)–(A.7): joint convexity in $(x,\alpha)$ with strong convexity in $\alpha$, $C^{1,1}$ regularity, local Lipschitz continuity in the measure argument for the 2-Wasserstein distance $W_2$, and growth conditions.

On the mean-field side, let $(X_t,Y_t,Z_t)$ solve the McKean–Vlasov FBSDE (3.1), let $\mu_t = \mathbb P_{X_t}$, and let $u$ be the FBSDE value function. This is a function that is Lipschitz in $x$ with linear growth and satisfies $Y_t = u(t,X_t)$. Let $\hat\alpha(t,x,\mu,y)$ minimize the Hamiltonian $\langle b,y\rangle + f$ over $\alpha$, and let $J$ be the mean-field cost (4.1). The candidate strategies are

$$\bar\alpha^{N,i}_t = \hat\alpha\big(t, X^i_t, \mu_t, u(t,X^i_t)\big),$$

where $(X^1,\dots,X^N)$ solves the particle system (4.2): the dynamics above, with each player using this feedback against the frozen flow $\mu$. Each player needs only its own state.

Formalization targets

Goal: Theorem 4.2

There exist $c>0$ and positive numbers $(\epsilon_N)_{N\ge1}$ with $\epsilon_N\le cN^{-1/(d+4)}$ such that, for every $N\ge1$, every player $i$ and every admissible deviation $\beta^i$,

$$\bar J^{N,i}(\bar\alpha^{N,1},\dots,\beta^i,\dots,\bar\alpha^{N,N})\ \ge\ \bar J^{N,i}(\bar\alpha^{N,1},\dots,\bar\alpha^{N,N}) - \epsilon_N.$$

The constant and the sequence come before $N$, the player and the deviation.

Milestones

The milestones follow the proof, in attack order:

• Lemma 4.1 (Horowitz–Karandikar): $\mathbb E[W_2^2(\bar\mu^N,\mu)]\le CN^{-2/(d+4)}$ for i.i.d. samples from $\mu\in\mathcal P_{d+5}$.
• Well-posedness of (4.2).
• The moment bound (4.4).
• The transport inequality (4.13).
• Propagation of chaos (4.11) and its consequence (4.12) for the empirical measure.
• The equilibrium cost estimate (4.14): $\bar J^{N,i}(\bar\alpha) = J + O(N^{-1/(d+4)})$.
• For a deviation of bounded energy $\mathbb E\int|\beta^1|^2\le A$: (4.17), (4.20) and the lower bound (4.23), $\bar J^{N,1}\ge J - c_AN^{-1/(d+4)}$.
• The coercivity (4.25) for deviations of large energy.

Companion: Corollary 4.3

Large deviations are unprofitable for every player (4.27). A bounded deviation of one player keeps every player's cost above $J-\epsilon_N$ (4.28).

Significance

The theorem justifies the mean-field game as a model of large finite games. Solving one McKean–Vlasov FBSDE produces distributed closed-loop strategies. No player can improve its cost by more than $O(N^{-1/(d+4)})$ by deviating, even with a strategy that uses all players' noises. The rate gives a quantitative meaning to "large $N$". The milestones (4.11)–(4.12) are a quantitative propagation-of-chaos result for the particle system driven by the decoupling field. Such results are used on their own in the numerics and statistics of interacting particle systems.

The result is proved in the paper. No part of it has been machine-checked, as far as the platform's records show. The work that remains is to formalize the known proof. That needs Wasserstein estimates for empirical measures (Lemma 4.1, cited by the paper without proof), Gronwall arguments for SDE systems, and the optimality of the mean-field control (Theorem 2.2, the first mission's milestone, used here through $J\le J(\beta^1)$). Sharper rates are known in low dimension (Fournier and Guillin, 2015). They would be welcome as variants, but they are not the target.

Difficulty

The obvious argument compares the deviating player's cost with the mean-field cost of the same strategy. It fails in two places. The deviation changes the empirical measure that every other player sees, so the other players' states are no longer independent copies of $X$. It must be shown that one player of bounded energy moves the population's empirical measure by only $O(N^{-1/(d+4)})$ in $W_2$ ((4.17)–(4.20)). The second problem is that the deviation $\beta^1$ is adapted to the filtration of all $N$ Brownian motions, larger than the one in which the mean-field control problem is posed. The comparison $J\le J(\beta^1)$ must survive this enlargement. Finally, nothing bounds the energy of a deviation a priori. Deviations of large energy have to be excluded separately by a coercivity estimate ((4.25)), and only then can the rate be obtained uniformly.

Formalization scope

The data live on EuclideanSpace ℝ (Fin n), so every norm, $M_2$ and $W_2$ is Euclidean. Matrix norms are operator norms. $W_2$ is the published WassersteinDRO.Duality.wassersteinDistance 2, valued in $[0,\infty]$. Measures carry Mathlib's σ-algebra on Measure, which on probability measures on $\mathbb R^d$ coincides with the paper's Borel σ-field of weak convergence. The SDEs and BSDEs are the published Itô-process predicates of Peng (Peng1990.SMP.SolvesSDE, SolvesBSDE). Solutions also have almost surely continuous paths on $[0,T]$. The game filtration is generated by $(W^1,\dots,W^N)$ and augmented by the null sets. Players are indexed by Fin N, so the paper's player $1$ is index $0$.

The mean-field solution and the game live on two probability spaces. Only $\mu_t=\mathbb P_{X_t}$, $J$ and $u$ pass between them. The value function $u$ enters through its properties (3.3), the identity $Y_t=u(t,X_t)$ and joint measurability, as in Lemma 3.5. $\hat\alpha$ is the chosen minimizer of the Hamiltonian, with default $0$; by Lemma 2.1 the default is never used on $[0,T]\times\mathcal P_2$. The assumptions also contain a standing convention the page does not write: $f$ and $g$ are Borel measurable. Without it the expected costs would not be expectations of measurable integrands. Moments and expected energies are lower Lebesgue integrals in $[0,\infty]$. Costs are real expectations, finite under (A.5) for admissible strategies.

The statements exclude the trivializing readings:

• the flow is the law of the mean-field state, not an arbitrary flow;
• distances are Euclidean, not sup-norm;
• the empirical measure is used only for $N\ge1$;
• $W_2^2$ is never converted to a real number where it could be infinite;
• the constants $c$, $(\epsilon_N)$, $c_A$, $N_0$ sit exactly where the page's quantifiers put them;
• in a deviation the other players keep their processes $\bar\alpha^{N,j}$, while the empirical measure follows the new states.

The goal does not mention the decoupled copies or Lemma 4.1.

A complete development needs:

• Wasserstein estimates for empirical measures, which are reusable well beyond this mission;
• existence, uniqueness and moment bounds for Lipschitz SDE systems with measure-dependent drift;
• the stochastic-maximum-principle comparison of the first mission.

Contributions on any of these are welcome. Well-posedness of the deviated system (4.5) is used but is not stated on the page; a proof of it is also welcome.

Selected references

• R. Carmona and F. Delarue, Probabilistic analysis of mean-field games, SIAM J. Control Optim. 51(4):2705–2734, 2013. https://doi.org/10.1137/120883499
• J.-M. Lasry and P.-L. Lions, Mean field games, Japanese Journal of Mathematics 2:229–260, 2007. https://doi.org/10.1007/s11537-007-0657-8
• M. Huang, R. P. Malhamé and P. E. Caines, Large population stochastic dynamic games: closed-loop McKean–Vlasov systems and the Nash certainty equivalence principle, Communications in Information and Systems 6(3):221–252, 2006. https://doi.org/10.4310/CIS.2006.v6.n3.a5
• J. Horowitz and R. L. Karandikar, Mean rates of convergence of empirical measures in the Wasserstein metric, J. Comput. Appl. Math. 55(3):261–273, 1994. https://doi.org/10.1016/0377-0427(94)90033-7
• A.-S. Sznitman, Topics in propagation of chaos, École d'Été de Probabilités de Saint-Flour XIX, Lecture Notes in Math. 1464, Springer, 1991. https://doi.org/10.1007/BFb0085169
• N. Fournier and A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probab. Theory Related Fields 162:707–738, 2015. https://doi.org/10.1007/s00440-014-0583-7

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

Many equilibrium problems in operations research, such as networked Cournot competition, power markets and communication networks, are stochastic Nash games: each player minimizes an expected cost $f_i(x_i,x_{-i})=\mathbb E[\psi_i(x_i,x_{-i};\xi)]$ that depends on the rivals' strategies and on a random vector $\xi$ whose law is accessible only through samples. Best-response schemes, in which every player in turn solves its own optimization problem given the others' latest strategies, are the natural distributed method for such games. In the stochastic setting no player can compute an exact best response, because evaluating $f_i$ requires the expectation itself. Lei, Shanbhag, Pang and Sen (arXiv:1704.04578v2; Mathematics of Operations Research, 2020) analyze inexact proximal best-response schemes in which each best response is approximated by a finite number of stochastic gradient steps, and they ask how many sampled gradients each player needs to reach an approximate equilibrium.

The deterministic theory of proximal best responses, including the contraction matrix $\Gamma$ used here, is due to Facchinei and Pang (Nash equilibria: the variational approach, 2009, §12.6; reference [19] of the paper). The present mission covers the paper's first scheme, the synchronous one, in which all players update simultaneously.

Setting

There are $N$ players. Player $i$ chooses $x_i$ from a closed, compact, convex, nonempty set $X_i\subseteq\mathbb R^{n_i}$; a profile is $x=(x_1,\dots,x_N)\in X=\prod_iX_i$, and $(z,y_{-i})$ is the profile $y$ with its $i$-th block replaced by $z$. A Nash equilibrium is a profile $x^*\in X$ such that every $x^*_i$ minimizes $f_i(\cdot,x^*_{-i})$ over $X_i$.

Assumption 1 asks that each $f_i$ be convex in $x_i$ and twice continuously differentiable near $X$, that the sampled gradients $\nabla_{x_i}\psi_i(x;\xi)$ be unbiased for $\nabla_{x_i}f_i(x)$, and that $\mathbb E\|\nabla_{x_i}\psi_i(x;\xi)\|^2\le M_i^2$. For $\mu>0$ the proximal best response is

$$\hat x_i(y)=\operatorname*{argmin}_{x_i\in X_i}\Big[f_i(x_i,y_{-i})+\tfrac\mu2\|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})$, where $\zeta_{i,\min}$ is the least eigenvalue of $\nabla^2_{x_i}f_i$ over $X$ and $\zeta_{ij,\max}$ the largest spectral norm of the mixed block $\nabla^2_{x_ix_j}f_i$ over $X$. Assumption 2 is $a:=\|\Gamma\|<1$ (spectral norm).

Algorithm 1 starts from a deterministic $x_0\in X$. At major iteration $k$ every player computes $x_{i,k+1}\in X_i$ with $\mathbb E[\|x_{i,k+1}-\hat x_i(x_k)\|^2\mid\mathcal F_k]\le\alpha_{i,k}^2$, by running $j_{i,k}$ projected stochastic gradient steps

$$z_{i,t+1}=\Pi_{X_i}\Big[z_{i,t}-\tfrac{1}{\mu(t+1)}\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 z_{i,1}=x_{i,k},$$

and setting $x_{i,k+1}=z_{i,j_{i,k}}$. A random profile $x$ is an $\epsilon$-NE$_2$ if $\mathbb E\big[(\sum_i\|x_i-x^*_i\|^2)^{1/2}\big]\le\epsilon$.

Formalization targets

Goal: Theorem 1(a)

With $\alpha_{i,k}=\eta^{k+1}$, $\eta\in(0,1)$, $\|x_{i,0}-x^*_i\|\le C$, $c=\max\{a,\eta\}$, $q\in(c,1)$, $D=1/\ln((q/c)^e)$, $Q_i=2M_i^2/\mu^2+2D_{X_i}^2$ and $j_{i,k}=\lceil Q_i/\eta^{2(k+1)}\rceil$, the iterate $x_K$ after $K=\lceil\ln(\sqrt N(C+D)/\epsilon)/\ln(1/q)\rceil$ major iterations is an $\epsilon$-NE$_2$, and player $i$ uses at most

$$\ell_i(\eta)=\frac{Q_i}{\eta^4\ln(1/\eta^2)}\left(\frac{\sqrt N(C+D)}{\epsilon}\right)^{\frac{\ln(1/\eta^2)}{\ln(1/q)}}+\left\lceil\frac{\ln(\sqrt N(C+D)/\epsilon)}{\ln(1/q)}\right\rceil$$

projected stochastic gradient steps. The goal fixes the paper's explicit expression, not its $O(\cdot)$ summary.

Milestones

1. (5): $\|\hat x_i(y')-\hat x_i(y)\|\le\sum_j\gamma_{ij}\|y'_j-y_j\|$ for $y,y'\in X$.
2. (9): the same in the Euclidean norm of block distances, with factor $a$.
3. A Nash equilibrium is a fixed point: $\hat x(x^*)=x^*$.
4. Lemma 2: $zc^z\le Dq^z$ for $z\ge0$, $0<c<q<1$, $D\ge1/(e\ln(q/c))$.
5. (20): $u_{k+1}\le au_k+\sqrt N\max_i\alpha_{i,k}$, where $u_k$ is the mean Euclidean norm of block errors.
6. Proposition 4: $u_k\le\sqrt N(C+D)q^k$.
7. Lemma 3: $\mathbb E[\|z_{i,t}-\hat x_i(x_k)\|^2\mid\mathcal F_k]\le Q_i/(t+1)$.
8. (30): $\sum_{k=1}^K\beta^k\le\int_1^{K+1}\beta^xdx\le\beta^{K+1}/\ln\beta$ for $\beta>1$.

Significance

Theorem 1(a) shows that the synchronous inexact scheme keeps the linear rate of the exact best-response iteration, with factor arbitrarily close to $\max\{\|\Gamma\|,\eta\}$, and turns it into a sample complexity explicit in $\epsilon$, in the number of players and in the game's constants. Choosing $\eta=\|\Gamma\|$ gives a bound of order $(\sqrt N/\epsilon)^{2+\delta}$ for any $\delta>0$ (Theorem 1(b)), close to the $O(1/\epsilon^2)$ of a single stochastic convex program; the dependence on $N$ is mild, which matters for games with many players. The same building blocks (the contraction (5), Lemma 2, Lemma 3 and (30)) are reused by the randomized and asynchronous schemes of the same paper.

The result is proved in the paper; it has not been machine-checked. A formalization adds a verified proof of the complexity bound together with fully explicit hypotheses: several conditions that the paper leaves implicit or states imprecisely (listed under Formalization scope) are made exact, and the Lean statement records which version of each is used.

Difficulty

The arithmetic of Theorem 1(a) from Proposition 4, Lemma 3 and (30) is routine. The weight lies elsewhere. The contraction (5) is quoted from Facchinei–Pang and not proved in the paper; it needs the variational optimality conditions of the two proximal problems and a mean-value argument along a segment of $X$ for the partial gradient, which mixes the Hessian blocks $\nabla^2_{x_i}f_i$ and $\nabla^2_{x_ix_j}f_i$. Lemma 3 is a conditional-expectation argument about a stochastic approximation recursion: the iterate $z_{i,t}$ must be shown measurable for the nested $\sigma$-fields generated by the samples, and the conditional unbiasedness and moment hypotheses must be combined with the tower property and the projection's nonexpansiveness. Proposition 4 then needs conditional Jensen to pass from (8) to the Euclidean norm of block errors.

Formalization scope

Players are Fin N, player $i$'s space is EuclideanSpace ℝ (Fin (n i)), profiles are dependent functions, and $(z,y_{-i})$ is Function.update y i z. The Euclidean norm of the vector of block distances is written out (blockDist), since Mathlib's norm on profiles is the sup norm; $\|\Gamma\|$ is the operator norm of Matrix.toEuclideanCLM Γ. $\zeta_{i,\min}$ and $\zeta_{ij,\max}$ are the infimum and supremum of Rayleigh-type quotients of the second derivative over $X$ and unit vectors. The proximal BR is any map minimizing the proximal objective on $X$ (unique there), and $\Pi_{X_i}$ is any map satisfying the published SpectralProjGrad.Shared.IsProjOnto. The $\sigma$-fields $\mathcal F_k$ and $\sigma\{\mathcal F_k,\xi^{[t-1]}_{i,k}\}$ are generated by the samples. Every expectation carries an integrability hypothesis.

Statement repairs, each recorded in the item's Formalization Note:

• the initial point is deterministic, as Algorithm 1 states, so $\mathbb E\|x_{i,0}-x^*_i\|\le C$ reads $\|x_{i,0}-x^*_i\|\le C$ (the proof's $u_0\le\sqrt NC$ needs this);
• Assumption 1(b) is twice continuous differentiability in the whole profile, which (4) needs for the mixed blocks, and convexity on an open set containing $X_i$;
• in Lemma 3, $\psi_i$ is read as $\nabla_{x_i}\psi_i$, and the second hypothesis is the bound $\mathbb E[\|\nabla_{x_i}\psi_i\|^2\mid\cdot]\le M_i^2$ that the proof uses (the printed equality would force zero sampling noise);
• $0<\epsilon<\sqrt N(C+D)$, without which the ceiling in (27) can be non-positive;
• $D=1/(e\ln(q/c))$, the reading of $\ln((q/c)^e)$ confirmed by Lemma 2's proof.

The goal is not trivialized by deterministic gradients: the sampled gradients are random, constrained only by conditional unbiasedness and a conditional second-moment bound, the proximal BR is tied to $f_i$ by its argmin property, $x^*$ must be a Nash equilibrium, and the norms are Euclidean. A deterministic instance ($N=1$, $f_1(x)=\|x\|^2$ on a ball, exact gradients) satisfies every hypothesis jointly.

Needed infrastructure: optimality conditions for constrained strongly convex minimization, the mean-value inequality for partial gradients of $C^2$ functions on convex sets, conditional expectation of vector-valued functions with the tower property and conditional Jensen, and the nonexpansiveness of Euclidean projection. The contraction (5) and Lemma 3 are reusable beyond this mission. Proofs of any milestone 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; published in 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 (reference [19] of arXiv:1704.04578v2).
• B. T. Polyak, Introduction to Optimization, Optimization Software, 1987 (reference [38] of the paper).

Motivation

The secretary problem asks how well an online decision maker can do when items arrive one at a time in random order and each must be accepted or rejected on the spot. With a single selection, the classical rule (observe a $1/e$ fraction, then take the first item better than everything seen) selects the best item with probability about $1/e$, and no rule does better. Many allocation problems are not single-choice: a seller with $k$ identical goods facing bidders who arrive over time, an advertiser with a budget of $k$ impressions, an employer with $k$ openings. Each asks the multiple-choice secretary problem: how much of the best achievable total can an online rule collect when $k$ selections are allowed?

Kleinberg's 2005 SODA paper answered this for the sum objective. It gave a recursive algorithm whose expected total is at least $(1 - 5/\sqrt k)$ times the sum of the $k$ largest values, so the ratio tends to $1$ as $k$ grows, and stated a matching $1 - \Omega(\sqrt{1/k})$ upper bound for every algorithm, whose proof the extended abstract omits. The motivating application was online auctions: the algorithm becomes a strategyproof mechanism for selling $k$ identical items to bidders who arrive and depart over time, extending the single-item online auction of Hajiaghayi, Kleinberg and Parkes (EC 2004).

Timeline. Dynkin (1963) and the classical literature settle $k = 1$ with ratio $1/e$. Hajiaghayi, Kleinberg and Parkes (2004) turn the single-item rule into an online auction. Kleinberg (2005) proves $1 - O(1/\sqrt k)$ for $k$ selections, with the explicit constant $5$. Babaioff, Immorlica, Kempe and Kleinberg (2008) survey the resulting family of generalized secretary problems and their use in online auctions.

Setting

Let $S$ be a finite set of $n$ distinct non-negative real numbers. The elements of $S$ are revealed in a uniformly random order: each of the $n!$ orders has probability $1/n!$. After each arrival the algorithm decides, irrevocably and using only the values seen so far, whether to select it. At most $k \ge 1$ elements may be selected. Write $T$ for the set of the $k$ largest elements of $S$ (all of $S$ if $k > n$) and

$$v = \sum_{x \in T} x$$

for their sum, the best total any rule could collect knowing $S$ in advance.

Kleinberg's algorithm $\mathcal A_k$ is defined by recursion on $k$:

1. If $k = 1$, use the classical rule: observe the first $\lfloor n/e \rfloor$ arrivals, then select the first later arrival that exceeds all earlier ones, if there is one.
2. If $k \ge 2$, draw $m$ from the binomial distribution $B(n, 1/2)$. Apply $\mathcal A_\ell$, with $\ell = \lfloor k/2 \rfloor$, to the first $m$ arrivals. Let $y_1 > y_2 > \dots > y_m$ be those $m$ values in decreasing order. After the $m$-th arrival, select every arrival exceeding $y_\ell$, until $k$ elements have been selected in total or the sequence ends.

The expected value of the algorithm is taken over the random order and over every binomial draw at every level of the recursion.

Formalization targets

Goal: Theorem 2.1

$$\mathbb E\Big[\sum_{x \text{ selected by } \mathcal A_k} x\Big] \;\ge\; \Big(1 - \frac{5}{\sqrt k}\Big)\, v \qquad \text{for every } S \subset \mathbb R_{\ge 0} \text{ finite and every } k \ge 1.$$

The statement is uniform in $n$ and $k$; it says nothing beyond the explicit constant $5$ printed in the paper.

Milestones: the claims of the proof sketch

The paper proves the theorem by induction on $k$. Its sketch introduces $Y$, the set of the first $m$ arrivals, $Z = S \setminus Y$, the modified value of a set (the sum of its elements lying in $T$), and $q$, the number of elements of $Z$ exceeding $y_\ell$. The milestones are its stated claims, in order:

1. $Y$ is uniformly distributed on the $2^n$ subsets of $S$.
2. $|Y \cap T|$ has the distribution $B(k, 1/2)$.
3. Conditional on $|Y \cap T| = r$, the expected modified value of $Y$ is $(r/k)v$.
4. The displayed bound $\sum_{r=1}^{k}\Pr(|Y\cap T| = r)\,\frac{\min(r,\ell)}{k}\,v \ge \big(1 - \frac{1}{2\sqrt k}\big)\frac v2$ with $\ell = k/2$.
5. The top $\ell = k/2$ elements of $Y$ have expected modified value at least $\big(1 - \frac{1}{2\sqrt k}\big)\frac v2$.
6. $\mathbb E\,|q - \ell| \le \sqrt k$.
7. The elements the algorithm selects from $Z$ have expected modified value at least $\big(\frac12 - \sqrt{1/k}\big)v$.
8. The closing computation $\big(1 - \frac{5}{\sqrt{k/2}}\big)\big(1 - \frac{1}{2\sqrt k}\big)\frac12 + \frac12 - \sqrt{\frac1k} > 1 - \frac{5}{\sqrt k}$.

Significance

The result. Theorem 2.1 shows that random arrival order costs only a $1 - O(1/\sqrt k)$ factor when many items are sold, against the constant $1/e$ for a single item. With the paper's matching upper bound, it pins down the optimal rate for the $k$-choice problem. It is the base of the paper's strategyproof online auction for $k$ identical goods and a standard reference point for the later literature on secretary problems with combinatorial constraints and on online allocation in the random-order model.

Formalizing it. The paper is a two-page extended abstract, and the theorem's proof is a sketch: several steps are described as "easy", a stochastic-domination argument is stated without detail, and the behaviour of the algorithm when fewer than $\ell$ elements have been observed is not specified. A machine-checked proof would supply the complete argument for the explicit constant. The result is proved on paper only in this sketch; no machine-checked proof of it is known.

Difficulty

The obvious argument fixes $m = n/2$ and treats the threshold $y_\ell$ as if it split the remaining elements exactly. Both steps fail. With a fixed $m$, the first $m$ arrivals are not a uniform subset of $S$ and $|Y \cap T|$ is hypergeometric, so the clean binomial computations of the sketch are not available; the binomial choice of $m$ is what makes $Y$ uniform. And the number $q$ of later elements beyond $y_\ell$ fluctuates by order $\sqrt k$: the second phase may run out of budget before reaching all of $T \cap Z$, or accept elements outside $T$. Controlling this fluctuation, while the cap of $k$ also counts the first phase's selections, is the central step. The induction must then combine a recursive guarantee on a random, random-sized prefix with this estimate.

Formalization scope

The Lean development fixes these conventions.

• $S$ is a Finset ℝ with all elements non-negative; distinctness is automatic. The arrival at time $t$ (0-based) under the order $\pi \in \mathrm{Perm}(\mathrm{Fin}\, n)$ is the $\pi(t)$-th smallest element of $S$, and expectations over the order use the published uniform average SecretaryWD.DiscUpper.uniformAvg.
• The algorithm is a PMF over sets of selected positions, defined by well-founded recursion on $k$. The base case is the published SecretaryWD.DiscUpper.classicalSecretary. $B(n, 1/2)$ is Mathlib's PMF.binomial (1/2). At $k = 0$ the algorithm selects nothing, for totality only; all statements assume $k \ge 1$.
• When the first phase has seen fewer than $\ell$ arrivals ($m < \ell$), $y_\ell$ is taken to be $-\infty$: every later arrival is selected until the cap. The page does not specify this case; under the reading "select nothing", the theorem fails when $n$ is much smaller than $k$.
• The cap of $k$ counts the selections of both phases. A cap applied to the second phase alone would let the algorithm select up to $k + \ell$ elements and is excluded.
• The goal mentions only the algorithm, the order, $S$, $k$ and $v$. It does not mention $Y$, $Z$, $q$ or the modified value, which appear only in milestones, so the goal cannot be discharged by assuming any part of the sketch.
• Three milestone hypotheses are added and disclosed: $k \le n$ for milestones 2, 3, 5 and 6 (for $n < k$ the law of $|Y \cap T|$ is $B(n, 1/2)$, and milestone 6 fails); $k$ even for milestone 5 (the sketch writes $\ell = k/2$; for odd $k$ with $\ell = \lfloor k/2\rfloor$ the bound fails at $k = 3$). Milestone 4 uses the real number $\ell = k/2$, as printed; with $\lfloor k/2\rfloor$ it fails for odd $k$.

A complete development needs: the uniform-subset law of a binomially sized random prefix; conditional expectations over random subsets; tail and absolute-deviation bounds for sums of geometric variables and a stochastic-domination argument; and a careful treatment of the recursion through PMF.bind. The first and third are reusable beyond this mission, for other random-order and sample-based algorithms. Proofs of any milestone, of auxiliary lemmas about the random prefix, and of the goal by a route different from the sketch are all welcome.

Selected references

• R. Kleinberg, A multiple-choice secretary algorithm with applications to online auctions, Proceedings of the 16th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2005.
• M. T. Hajiaghayi, R. Kleinberg, D. C. Parkes, Adaptive limited-supply online auctions, Proceedings of the 5th ACM Conference on Electronic Commerce (EC), 2004, pp. 71–80. https://doi.org/10.1145/988772.988784
• E. B. Dynkin, The optimum choice of the instant for stopping a Markov process, Soviet Mathematics Doklady 4, 1963.
• T. S. Ferguson, Who solved the secretary problem?, Statistical Science 4(3), 1989. https://doi.org/10.1214/ss/1177012493
• M. Babaioff, N. Immorlica, D. Kempe, R. Kleinberg, Online auctions and generalized secretary problems, ACM SIGecom Exchanges, 2008. https://doi.org/10.1145/1399589.1399596