All missions

Motivation

Rental platforms, cloud computing, hotel and car-rental systems, and on-demand services all sell access to reusable resources: a unit that is rented comes back after a random rental duration and can be rented again. When such a platform displays a menu of products (an assortment) to each arriving customer, it faces an online decision problem: offering a product now earns a fee, but ties up a unit that a later, more valuable customer might have wanted. Feng, Niazadeh and Saberi study this problem in a Bayesian setting, where customer types are drawn from known distributions, and give an algorithm whose expected revenue is within a factor $1 - \min\{1/2, \varepsilon^*(c_{\min})\}$ of an LP upper bound on any online policy (arXiv:2512.06997; Operations Research, 2024). The factor tends to $1$ as the smallest inventory grows and never drops below $1/2$.

Earlier work on online assortment of reusable resources (Gong, Goyal, Iyengar, Simchi-Levi, Udwani and Wang, Management Science 2021; Goyal, Iyengar and Udwani, arXiv:2002.02430) studied the prior-free, adversarial setting, in which fees and rental-duration distributions are type-independent and identical across time. The Bayesian model here lets both depend on the customer type.

Setting

There are $n$ products; product $i$ has $c_i \ge 1$ identical units, and $c_{\min} = \min_i c_i$. Customers arrive at times $t = 1, \dots, T$. Customer $t$ has a type $z_t$, drawn independently from a known distribution $F_t$ on a finite set. A type $z$ fixes

• a choice model $\phi^z(S, i)$: the probability that a customer of type $z$ rents product $i$ when offered the assortment $S$ (with probability $1 - \sum_{i \in S}\phi^z(S,i)$ she rents nothing);
• fees $r^z_i \ge 0$;
• rental-duration distributions $g^z_i$ on $\{1, \dots, T\}$; write $\bar G^z_i(k) = \Pr[d > k]$.

Assortments come from a family $\mathcal S$ that is downward closed (Assumption 2), and choice models are weakly substitutable (Assumption 1): $\phi^z(\emptyset, i) = 0$, and adding a product to an assortment never increases the choice probability of another. A rented unit with duration $d$ is unavailable at times $t, \dots, t+d-1$; a product with no unit on hand cannot be offered.

The benchmark is the Bayesian expected LP Expected-LP$[\{F_t\}]$: with $y_{S,t,z}$ the probability of offering $S$ to type $z$ at time $t$, maximize $\sum_{t,z,S,i} F_t(z)\, r^z_i\, \phi^z(S,i)\, y_{S,t,z}$ subject to each product's inventory holding in expectation at every time, $\sum_{\tau \le t}\sum_{z,S} F_\tau(z)\, \bar G^z_i(t-\tau)\, \phi^z(S,i)\, y_{S,\tau,z} \le c_i$, and $\sum_S y_{S,t,z} \le 1$. Let $y^*$ be an optimal solution with $\sum_S y^*_{S,t,z} = 1$, and

$$\varepsilon^*(x) = \min_{\gamma \in [0,1]}\ 1 - (1-\gamma)\Big(1 - e^{-\gamma^2 x/(2-\gamma)}\Big).$$

All algorithms of the paper follow one template: at time $t$, sample $\hat S \sim y^*_{\cdot,t,z_t}$; for each $i \in \hat S$, discard $i$ if it has no unit on hand and otherwise according to a per-product discarding rule; then offer a random subset of the survivors drawn by sub-assortment sampling (Procedure 1). Algorithm 2 discards at random with probability $\gamma$. Algorithm 3 keeps $i$ only if its fee exceeds a threshold computed from an optimistic per-unit dynamic program $\mathcal V_{i,t}$ (equation (3)). Sim+Hybrid(i) chooses, product by product, between the two rules by comparing $\mathcal R_i = c_i\mathcal V_{i,1}/(\text{LP contribution of } i)$ with $1 - \varepsilon^*(c_i)$.

Formalization targets

Goal: Theorem 3

For every instance and every optimal normalized $y^*$,

$$\mathbb E\big[\mathrm{Rev}(\texttt{Sim+Hybrid(i)})\big] \ \ge\ \Big(1 - \min\Big\{\tfrac12, \varepsilon^*(c_{\min})\Big\}\Big)\, \mathrm{LP}(y^*).$$

Milestones

1. Proposition 3: sub-assortment sampling returns $\tilde S \subseteq S$ with $\mathbb E[\phi(\tilde S, i)] = p_i$ for every $i \in S$.
2. Lemma EC.2: the multiplicative Chernoff bound (already posed on the platform; referenced).
3. (EC.2): a randomly discarded product has no unit on hand with probability at most $\exp(-\gamma^2 c_i/(2-\gamma))$.
4. Per-product bound in the proof of Theorem 1: $\mathbb E[r^{z_t}_i I_{i,t}] \ge (1-\gamma)(1 - e^{-\gamma^2 c_i/(2-\gamma)})\sum_{z,S} F_t(z)\, r^z_i\, \phi^z(S,i)\, y_{S,t,z}$.
5. Theorem 1: Algorithm 2 with $\gamma = \gamma^*(c_{\min})$ is $(1 - \varepsilon^*(c_{\min}))$-competitive.
6. $\varepsilon^*(x)$ and its minimizers are $O(\sqrt{\log x / x})$.
7. Lemma EC.3: the per-unit revenue-to-go of Algorithm 3 from any inventory state is at least $\mathcal V_{i,t}$.
8. Part (ii) of the proof of Theorem 2: $c_i \mathcal V_{i,1} \ge \frac12$ (LP contribution of $i$).
9. Theorem 2: Algorithm 3 is $\frac12$-competitive.
10. $\varepsilon^*$ is continuous and nonincreasing, $\varepsilon^*(0) = 1$, $\varepsilon^*(\infty) = 0$.

Significance

The result gives a single polynomial-time policy that is simultaneously $\frac12$-competitive, which is optimal for small inventories (a two-period example on p. 17 shows no online policy does better against this LP), and asymptotically optimal as inventories grow. Its analysis is modular: each product is treated separately, which is what allows mixing two discarding rules in one algorithm. Sub-assortment sampling is of independent use whenever an assortment must be thinned without distorting the choice probabilities of the remaining products.

The paper's proofs are on paper only; the per-product decoupling, which the paper invokes in a few lines for Theorem 3, is exactly the kind of step a formal proof makes explicit. A complete development produces a reusable finite model of a Bayesian online rental process (types, simulated assortments, discarding, choices and durations), a verified sub-assortment sampler, and an LP-duality certificate for the optimistic DP. None of these results is formalized elsewhere.

Difficulty

The obvious argument fails at the first step: whether product $i$ is available at time $t$ depends on all earlier rentals, and the offer probabilities of different products are correlated through the shared assortment and through substitution, so rental indicators are neither independent nor product-separable. Two ingredients are needed. Sub-assortment sampling must make each product's selection probability exactly its LP target, whatever happened to the other products; only then can the rentals of product $i$ be coupled with an independent sequence for a concentration bound (EC.2). For small inventories, a concentration bound is too weak, and the analysis instead compares the true process with the optimistic DP by backward induction over inventory states (Lemma EC.3), then bounds the DP against the LP with an explicit dual solution (Part (ii)).

Formalization scope

Everything is finite: products are Fin n (the paper's product $i$ is index $i-1$), times are $1, \dots, T$, types range over one finite type space (the paper's $\mathcal Z_t$ as subsets), and durations lie in $\{1, \dots, T\}$. The online process is a product of explicit per-step kernels over finite sample paths; probabilities and expectations are finite sums, with no measure theory. Conventions committed to:

• $\phi^z(S,\cdot)$ is a sub-probability supported on $S$ for $S \in \mathcal S$; weak substitutability is required when $S \cup \{j\} \in \mathcal S$; $\mathcal S$ is nonempty and downward closed;
• $r \ge 0$, $c_i \ge 1$, $n \ge 1$;
• a unit rented at $\tau$ is out at $t$ iff its duration exceeds $t - \tau$, matching $\bar G(k) = \Pr[d > k]$ in the LP; $\mathcal V_{i,s} = 0$ for $s > T$;
• the competitive ratio is $\alpha \cdot \mathrm{LP}(y^*) \le \mathbb E[\mathrm{Rev}]$ for every optimal $y^*$ with $\sum_S y^*_{S,t,z} = 1$;
• Procedure 1 breaks ties among equal ratios by product index, and its recursive step uses the $j^*$ products of largest ratio;
• the page does not say which discarding probability a "large inventory" product uses; it is a minimizer $\gamma^*(c_i)$ of (1) at $x = c_i$;
• the page calls $\varepsilon^*$ "monotone increasing"; the formalized statement is nonincreasing, which is what the proof uses;
• running-time claims are not formalized.

The process is not allowed to rent a unit that is not on hand, the post-processing targets are $\phi^{z}(\hat S, i)$ (not $\phi^z(\bar S, i)$, which would make sub-assortment sampling the identity), and the path law uses the same $y^*$ as the benchmark; any formalization that drops one of these makes the goal a statement about a different process. Milestones 3, 4, 7 and 8 are stated for any feasible normalized $y$ and arbitrary rules for the other products, which is the generality Theorem 3's proof needs.

Contributions welcome: lemmas on the process (normalization of the path law, the marginal law of one product's rentals), the Chernoff bound, and analytic facts about $\varepsilon^*$.

Selected references

• Y. Feng, R. Niazadeh, A. Saberi, Near-Optimal Bayesian Online Assortment of Reusable Resources, Operations Research (Technical Note), 2024; arXiv:2512.06997v1. https://arxiv.org/abs/2512.06997
• V. Goyal, G. Iyengar, R. Udwani, Online Allocation of Reusable Resources: Achieving Optimal Competitive Ratio, arXiv preprint, 2020. https://arxiv.org/abs/2002.02430
• V. Goyal, G. Iyengar, R. Udwani, Online Allocation of Reusable Resources via Algorithms Guided by Fluid Approximations, arXiv preprint, 2020 (an idea similar to sub-assortment sampling, found concurrently). https://arxiv.org/abs/2010.03983
• H. Chernoff, A Measure of Asymptotic Efficiency for Tests of a Hypothesis Based on the Sum of Observations, Annals of Mathematical Statistics, 1952. https://doi.org/10.1214/aoms/1177729330

Motivation

A qubit stored or transmitted in the presence of noise loses purity. If many copies of the same unknown pure state $\sigma = |\varphi\rangle\langle\varphi|$ have each passed through the same noisy channel, one may try to undo the noise collectively: feed the $N$ noisy copies into a quantum device and ask for $M$ output qubits that are as close as possible to $M$ perfect copies $\sigma^{\otimes M}$. The noise map itself is invertible as a linear map, but its inverse is not completely positive, so this purification problem is a genuine optimization over physical devices, closely related to optimal quantum cloning (Werner 1998, Keyl–Werner 1999).

Cirac, Ekert and Macchiavello (1999) found the optimal device for a single output qubit. Keyl and Werner (arXiv:quant-ph/9910124, 1999) solved the problem for an arbitrary number $M$ of outputs and two figures of merit, and computed the trade-off between output number and quality. For the figure of merit that tests all outputs jointly, the best fidelity is a function of the output rate $M/N$ alone in the limit, and that function is explicit. This mission formalizes that rate formula.

Setting

A qubit is $\mathbb C^2$ with basis $|0\rangle, |1\rangle$; $n$ qubits are $(\mathbb C^2)^{\otimes n}$, with basis indexed by words $x : \{0,\dots,n-1\} \to \{0,1\}$. Fix a noise parameter $\lambda$ with $0 < \lambda < 1$. The depolarizing channel acts on a one-qubit density matrix $\sigma$ by

$$R_*\sigma = \lambda\,\sigma + (1-\lambda)\,\tfrac{1}{2}\mathbb 1 .$$

A device from $N$ to $M$ qubits is a quantum channel $T_*$, i.e. a trace-preserving completely positive linear map from $2^N\times 2^N$ to $2^M\times 2^M$ complex matrices. Its all-qubit fidelity is the worst case over pure inputs:

$$F_{\mathrm{all}}(T) = \inf_{\|\varphi\|=1}\ \operatorname{tr}\Big(\sigma^{\otimes M}\, T_*\big((R_*\sigma)^{\otimes N}\big)\Big), \qquad \sigma = |\varphi\rangle\langle\varphi| .$$

The optimal all-qubit fidelity is $F^{\max}_{\mathrm{all}}(N,M) = \sup_T F_{\mathrm{all}}(T)$, the supremum over all channels from $N$ to $M$ qubits. Finally, the rate function is

$$\Phi(\mu) = \begin{cases} \dfrac{2\lambda^2}{2\lambda^2 + \mu(1-\lambda)} & \mu \le \lambda,\\[2mm] \dfrac{2\lambda^2}{\mu(1+\lambda)} & \mu \ge \lambda. \end{cases}$$

The proof works with the parametrization $\lambda = \tanh\beta$, $\beta > 0$, and with the decomposition of $(\mathbb C^2)^{\otimes N}$ into spin-$s$ blocks, $s \in I[N] = \{N/2, N/2-1, \dots\}\cap[0,\infty)$. Each block carries a weight $w_N(s)$ (eq. (14)), an explicit probability vector built from $\sinh$, $\cosh$ and binomial coefficients, and a state $\rho_s(\beta)$ on the symmetric subspace of $2s$ qubits.

Formalization targets

Goal: eq. (10)

For every sequence $N_k \to \infty$ and every sequence $M_k$ with $M_k/N_k \to \mu > 0$,

$$\lim_{k\to\infty} F^{\max}_{\mathrm{all}}(N_k, M_k) = \Phi(\mu).$$

Milestones

1. Multiplicities (p. 9). $\sinh\beta\,(2\cosh\beta)^N = \sum_{s\in I[N]}\sinh((2s+1)\beta)\dim\mathcal K_{N,s}$ with $\dim\mathcal K_{N,s} = \frac{2s+1}{N/2+s+1}\binom{N}{N/2-s}$, and $w_N$ is a probability vector.
2. Natural purifier block (p. 14). $\operatorname{tr}\rho_s(\beta) = 1$ and $\operatorname{tr}(\sigma^{\otimes 2s}\rho_s(\beta)) = \frac{1-e^{-2\beta}}{1-e^{-(4s+2)\beta}}$.
3. Proposition 4.2, corrected (p. 15). The fidelity of one block of the optimal purifier is the closed form $f_{\mathrm{all}}(M,\beta,s)$.
4. Theorem 5.1, all-qubit half (p. 15). $F^{\max}_{\mathrm{all}}(N,M) = \sum_{s} w_N(s)\,f_{\mathrm{all}}(M,\beta,s)$, and the supremum is attained.
5. Lemma 6.1, corrected (pp. 18–19). $\sum_s w_N(s) f_N(2s/N) \to f_\infty(\lambda)$ for uniformly bounded $f_N$ converging uniformly near $\lambda$.
6. Lemma 6.2, corrected (pp. 21–22). $\binom{K}{M}^{-1}\sum_{R=M}^{K}\binom{R}{M}z^{K-R} \to \frac{1}{1-(1-c)z}$ for $|z|<1$, $M/K \to c \in [0,1]$.

Significance

The result. Formula (10) says that $\Phi(\mu) < 1$ for every $\mu > 0$: in the all-qubit sense no purification procedure with a positive output rate approaches perfect fidelity, so optimal purification "works with zero rate". At the same time every fidelity level below one is achieved at a positive rate, and $\Phi$ gives the exact trade-off. This contrasts with the one-qubit figure of merit treated in the same paper, where the fidelity of each output tends to one at any rate. Theorem 5.1 reduces an optimization over all channels between exponentially large spaces to a sum of $\lfloor N/2\rfloor + 1$ explicit terms.

Formalizing it. The results are proved in the paper; none of them, to our knowledge, has a machine-checked proof. The paper's statement of Proposition 4.2 contains printing errors (swapped cases, a missing normalization factor, $f_{\mathrm{one}}$ for $f_{\mathrm{all}}$), and Lemmas 6.1 and 6.2 are stated with an incorrect domain and range; the milestones state the corrected versions, which were checked numerically against a semidefinite program for small $N, M$. A formal proof would certify the corrected formulas. Related platform items, not posed again here: uniqueness of the optimal cloner (Support21.P16.unique_optimal_cloner, open) and covariance averaging for cloners (Renew46.P45.symmetrization, open), both used in the optimality argument of Theorem 5.1.

Difficulty

The obvious route to the goal is to evaluate the fidelity of one good device. That gives only a lower bound: the goal is about the supremum over all channels, and the upper bound requires the optimality theorem (Theorem 5.1), whose proof needs a reduction to covariant, permutation-symmetric channels, the decomposition of tensor-power representations of $SU(2)$, and the optimality and uniqueness of the cloning maps on each spin block. The asymptotic part is also not a direct substitution: the weights $w_N(s)$ must be shown to concentrate at $2s/N = \lambda$, and on the side $\mu < \lambda$ the dominant blocks need the binomial-sum branch of $f_{\mathrm{all}}$, whose limit is Lemma 6.2. Near $\mu = \lambda$ the two branches meet, and the limit must be controlled uniformly in the block index.

Formalization scope

• Representation. $n$-qubit operators are complex matrices indexed by words Fin n → Fin 2; tensor powers are QAlgorithms.piKron; a pure state is QAlgorithms.pureDensity φ with ‖φ‖ = 1; a channel is a superoperator with a finite normalized Kraus family (QAlgorithms.IsChannel), which in finite dimension is exactly a CPTP map. The infimum and supremum are sInf/sSup on ℝ over sets that are nonempty and contained in $[0,1]$.
• Committed conventions. The noise is applied to each input copy before the tensor power, and the target is $\sigma^{\otimes M}$ for the same $\sigma$. The worst case is over all unit vectors in $\mathbb C^2$. The supremum is over all channels, not over covariant channels or the paper's purifiers. The goal assumes $0 < \lambda < 1$ and $\mu > 0$, and the limit is taken along every pair of sequences with $N_k \to \infty$, $M_k/N_k \to \mu$. Milestones are stated in $\beta > 0$ with $\lambda = \tanh\beta$. Spins are encoded by $k = N/2 - s \in \{0,\dots,\lfloor N/2\rfloor\}$, so $2s = N - 2k \in \mathbb N$; $\psi = (1,0)$ is basis vector $0$.
• Ruled out. Fixing the input state to $|0\rangle$ trivializes the problem (the channel that outputs $|0\cdots0\rangle$ has fidelity one); the infimum over all $\varphi$ is essential. Restricting the supremum to symmetric channels would make Theorem 5.1 a different statement.
• Infrastructure. A full development needs: Kraus-form channels and their compactness, the symmetric-subspace projector (boseProjector) and the optimal cloner (canonicalCloner), the $SU(2)$ decomposition of $(\mathbb C^2)^{\otimes N}$ with multiplicities, and concentration of the weights $w_N$. The binomial-sum limit (Lemma 6.2) and the weight concentration (Lemma 6.1) are reusable outside this mission. Contributions of any milestone, or of lemmas toward the $SU(2)$ decomposition, are welcome.

Selected references

• M. Keyl, R. F. Werner, The rate of optimal purification procedures, arXiv:quant-ph/9910124v1, 1999; Ann. Henri Poincaré 2 (2001) 1–26. https://arxiv.org/abs/quant-ph/9910124
• J. I. Cirac, A. K. Ekert, C. Macchiavello, Optimal purification of single qubits, Phys. Rev. Lett. 82 (1999) 4344. https://arxiv.org/abs/quant-ph/9812075
• R. F. Werner, Optimal cloning of pure states, Phys. Rev. A 58 (1998) 1827. https://arxiv.org/abs/quant-ph/9804001
• M. Keyl, R. F. Werner, Optimal cloning of pure states, testing single clones, J. Math. Phys. 40 (1999) 3283. https://arxiv.org/abs/quant-ph/9807010

Motivation

Retail inventory records are often wrong. A store's system may report units on the shelf that are not there (phantom inventory), so the replenishment system never reorders and the product silently stops selling. Audits fix such errors but are expensive, so a retailer wants to decide which store–SKU pairs to audit from sales data alone. The classical way, studying each pair's sales history over a long period, needs time-homogeneous data that rarely exists.

Farias, Li and Peng (arXiv:2006.13126v3, Manufacturing & Service Operations Management, 2024) instead use a single cross-sectional snapshot of sales across $n$ stores and $m$ SKUs. Expected demand is modelled as a low-rank matrix, anomalies corrupt a random subset of entries, and only some entries are observed. The paper proposes the entrywise (EW) algorithm and proves that its expected decision cost approaches that of an oracle knowing the model, at rate $\log^{1.5}(m)/\sqrt m$. A matching $\Omega(1/\sqrt m)$ lower bound (Proposition 1) is also proved. The paper evaluates the method on synthetic data and on real data from a consumer goods retailer.

Setting

An instance has an expected-demand matrix $M^*\in\mathbb R_+^{n\times m}$ with $2\le m\le n$, rank $r$ and SVD $M^*=U\Sigma V^\top$ with singular values $\sigma_1^*\ge\dots\ge\sigma_r^*>0$ and $\kappa=\sigma_1^*/\sigma_r^*$. It also has an anomaly model $\mathrm{Anom}(\alpha,M)$, which is a family of laws on $\mathbb N$ indexed by a parameter $\alpha\in\Gamma\subset\mathbb R^d$ and a mean level $M\ge0$. The remaining data are a true parameter $\alpha^*$, an anomaly probability $p_A^*$, an observation probability $p_O$, and costs $c^{(0)}_{ij}$ (flagging a normal entry) and $c^{(1)}_{ij}$ (missing an anomaly). Independently for every entry:

1. the entry is observed with probability $p_O$; the observed set is $\Omega$;
2. $B_{ij}\sim\mathrm{Bernoulli}(p_A^*)$ marks an anomaly;
3. sales are $X_{ij}\sim\mathrm{Poisson}(M^*_{ij})$ if $B_{ij}=0$ and $X_{ij}\sim\mathrm{Anom}(\alpha^*,M^*_{ij})$ if $B_{ij}=1$.

Assumptions (§2):

• $\|M^*\|_{\max}$ lies between a constant $c_M>0$ and $L$.
• Incoherence: $\|U\|_{2,\infty}\le\sqrt{\mu r/n}$ and $\|V\|_{2,\infty}\le\sqrt{\mu r/m}$.
• Sparsity: $\sqrt{p_O}\ge C\log^{1.5}(m)\mu r\kappa^2/\sqrt m$.
• $p_A^*\le1-c_A$.
• $\mathrm{Anom}(\alpha^*,M^*_{ij})$ has sub-exponential norm $\le L$.
• $\mathbb P(\mathrm{Anom}(\alpha,M)=k)$ is $K$-Lipschitz in $(\alpha,M)$.
• Mean decomposition: $\mathbb E\,\mathrm{Anom}(\alpha,M)=g(\alpha)M$ with $g$ valued in $[0,1]$ and $K$-Lipschitz.

The oracle $\pi^*$ knows $\theta^*=(\alpha^*,p_A^*)$ and $M^*$. It computes the posterior $f^*_{ij}=\mathbb P(B_{ij}=0\mid X_\Omega)=y^*_{ij}/(x^*_{ij}+y^*_{ij})$, where $x^*_{ij}=p_A^*\mathbb P_{\mathrm{Anom}(\alpha^*,M^*_{ij})}(X_{ij})$ and $y^*_{ij}=(1-p_A^*)\mathbb P_{\mathrm{Poisson}(M^*_{ij})}(X_{ij})$. It flags $(i,j)$ iff $c^{(1)}_{ij}/(c^{(0)}_{ij}+c^{(1)}_{ij})\ge f^*_{ij}$. The EW algorithm $\pi^{EW}$ runs four steps:

1. It computes $\hat M=\frac{nm}{|\Omega|}\mathrm{SVD}(X_\Omega)_r$, a rescaled best rank-$r$ approximation of the zero-filled observations.
2. It estimates $\hat\theta$ by matching $T$ empirical CDF values $|\{X_{ij}\le t,(i,j)\in\Omega\}|/|\Omega|$ to their model predictions $g_t(\theta,\hat M/e(\theta))$, where $e(\theta)=p_Ag(\alpha)+1-p_A$.
3. It forms plug-in estimates $\hat f_{ij}$ of $f^*_{ij}$.
4. It applies the oracle's threshold rule to $\hat f$.

The cost of decisions $A$ is

$$\mathrm{cost}^A(X_\Omega)=\frac1{|\Omega|}\sum_{(i,j)\in\Omega}\Big(c^{(0)}_{ij}\mathbf 1\{A_{ij}=1\}f^*_{ij}+c^{(1)}_{ij}\mathbf 1\{A_{ij}=0\}(1-f^*_{ij})\Big).$$

Formalization targets

Goal: Theorem 1 (p. 12)

$$\mathbb E_{X_\Omega}\Big(\mathrm{cost}^{\pi^{EW}}(X_\Omega)-\mathrm{cost}^{\pi^*}(X_\Omega)\Big)\le c_{\max}\,C_0\,(1+K+L+\kappa+\mu+r+p_O^{-1})^k\,\frac{\log^{1.5}(m)}{\sqrt m}.$$

The constants $C_0$ and $k$ and the sparsity constant depend only on $d$, $c_M$, $c_A$ and the regularity constant $C_{RC}$. The statement asserts the paper's rate with polynomial dependence on the model parameters. It does not fix the polynomial, so a sharper analysis still proves it.

Milestones, in the proof's order

• Lemma 8: $\|\mathrm{Poisson}(\lambda)\|_{\psi_1}\le4\lambda+1$.
• Lemma 14: a Bernstein bound for $\sum_{(i,j)\in\Omega}T_{ij}$.
• Theorem 2: the entrywise bound $\|\hat M-e(\theta^*)M^*\|_{\max}\le C\delta'$ with $\delta'=\kappa^4\mu rL\sqrt{\log m/(p_Om)}$.
• Lemmas 15 and 16: the model moments and the objective $h(\theta^*)$.
• Lemma 2: $\|F(\hat\theta)-F(\theta^*)\|\lesssim(K+L)\delta'$.
• Lemma 17: a quantitative inverse-function bound.
• Lemma 1: $\|\hat\theta-\theta^*\|\lesssim(K+L)\delta'$.
• Lemmas 18 and 19: plug-in likelihoods and the ratio perturbation bound.
• Lemma 3: $|f^*_{ij}-\hat f_{ij}|\le\min(C\delta/(x^*_{ij}+y^*_{ij}),1)$.
• Step 4 of the proof sketch: the excess cost is at most $\frac1{|\Omega|}\sum_\Omega|a_{ij}-b_{ij}|$.

Significance

Theorem 1 says that the value of cross-sectional data grows with the number of stores and SKUs. A retailer that can only see one snapshot does nearly as well as one that knows the demand matrix and the anomaly law exactly. With Proposition 1, the rate is optimal up to the logarithmic factor. Theorem 2 is, per the authors, the first entrywise guarantee for matrix completion under Poisson (more generally sub-exponential) noise, and it is reusable outside inventory problems.

The results are proved on paper: Theorem 1 by a proof sketch in §5.1 plus Appendix B, and Theorem 2 in Appendix A, which builds on a cited entrywise eigenvector perturbation theorem of Abbe et al. None of this is formalized. A machine-checked proof would also settle the constants and conventions that the paper leaves implicit. These include the dimension restriction in Lemma 17, the unspecified constant in Lemma 3, the form of the sparsity assumption used in the proof of Theorem 2, and the closed range of $p_A$ in $\Theta$.

Difficulty

The obvious argument plugs consistent estimates of $M^*$ and $\theta^*$ into the Bayes rule. It breaks at the first step: a Frobenius-norm bound for $\hat M$, which is what standard matrix completion gives, does not control any single $\hat f_{ij}$. An entrywise bound is needed, under heavy-tailed (sub-exponential, not sub-Gaussian) noise, and with the anomalies corrupting the mean by the unknown factor $e(\theta^*)$. The second step inverts the moment map $F$. Closeness of moments yields closeness of parameters only through a quantitative inverse-function argument, which needs the regularity conditions of Lemma 1. A third subtlety is that $f^*_{ij}$ is a ratio whose denominator $x^*_{ij}+y^*_{ij}$ can be tiny. The error bound of Lemma 3 therefore degrades on rare sales values, and Theorem 1 averages this over the law of $X$.

Formalization scope

One definitions module, InventoryAnomaly.EW.Model, holds the instance, the product sampling law over $\{$observed$\}\times\{$anomalous$\}\times\mathbb N$ per entry, the estimators, the costs and four predicates:

• Model: §2's assumptions;
• SparsityMax: the sparsity condition as read in the proof of Theorem 2, p. 41;
• Regular: Lemma 1's conditions;
• CostBound: costs in $[0,c_{\max}]$.

The sub-exponential norm is the published HighDimProb.Concentration.subexponentialNorm.

Conventions:

• Parameters. $\theta=(\alpha,p_A)\in\mathbb R^{d+1}$, and $T=d+1$ moments are matched.
• Parameter set. $\Theta=\Gamma\times[0,1-c_A]$.
• Clamped means. Laws are evaluated at the mean $\max(M,0)$.
• Cost. The cost is the closed form (5) with $f^*$ by Bayes' rule (8). $c^{(0)}$ is the false-positive cost (the display on p. 12 swaps the labels).
• Estimators. $\mathrm{SVD}_r$ is any exact best rank-$r$ approximation. $\hat\theta$ is any point of $\Theta$ with $h(\hat\theta)\le h(\theta^*)$, which every minimiser of (7) satisfies.
• Constants. "$O(\cdot)$" and "with probability $1-O(1/nm)$" are existential constants. They come after $d,c_M,c_A,C_{RC}$ and before the instance.
• Added conditions. $2\le m\le n$, $1\le r\le m$, finite anomaly means, and nonnegative costs. Lemma 17 is stated for square Jacobians. Lemma 3 has a constant $C$ in place of 2. Lemma 19's $\delta/(\hat x+\hat y)$ clause is stated when $\hat x+\hat y>0$. Each item's Formalization Note lists these.

The algorithm's selections are universally quantified together with their defining properties. Neither may be replaced by unconstrained functions. The cost of $\pi^*$ must use $f^*$, not $\hat f$. The goal must keep the explicit rate $\log^{1.5}(m)/\sqrt m$ and the full probability model, without assuming Theorem 2's event.

Not formalized: Proposition 1 (the lower bound), Appendix E (the TPR/FPR-constrained variant), the cited Lemmas 6–7, and the internal Lemmas 9–13 and Propositions 2–3 of Appendix A.

Useful infrastructure includes entrywise singular-subspace perturbation bounds, Bernstein's inequality for bounded independent sums, and Orlicz-norm bounds for Poisson variables. All three are reusable beyond this mission. Proofs of individual milestones are welcome, especially Lemmas 8, 14, 17 and 19 and Step 4, which are self-contained.

Selected references

• V. F. Farias, A. A. Li, T. Peng, Fixing Inventory Inaccuracies at Scale, Manufacturing & Service Operations Management, 2024; arXiv:2006.13126v3 (2022). https://arxiv.org/abs/2006.13126
• E. Abbe, J. Fan, K. Wang, Y. Zhong, Entrywise Eigenvector Analysis of Random Matrices with Low Expected Rank, Annals of Statistics 48(3), 2020. https://arxiv.org/abs/1709.09565
• A. D. McRae, M. A. Davenport, Low-rank matrix completion and denoising under Poisson noise, Information and Inference 10(2), 2021. https://arxiv.org/abs/1907.05325
• R. Vershynin, High-Dimensional Probability, Cambridge University Press, 2018. https://doi.org/10.1017/9781108231596

Motivation

A Gelfand–Tsetlin basis of a representation of the last group in a tower $G_1 \subset G_2 \subset \cdots \subset G_n$ is a basis adapted to every restriction at once: each basis vector spans a line that is cut out by the isotypic decompositions at all levels $k = 1, \dots, n$. When every restriction $G_k \downarrow G_{k-1}$ is multiplicity-free, these lines are canonical, and the basis vectors are indexed by paths in the branching graph. For the symmetric groups, Young's orthogonal form gives such a basis with completely explicit matrices for the simple transpositions (Young, 1932; see Headley, 1996, Theorem 2.1), and the Vershik–Okounkov approach (arXiv:math/0503040) builds the representation theory of $S_n$ around it.

The alternating groups $A_n$ also form a multiplicity-free tower, so their irreducible representations have Gelfand–Tsetlin bases too. Geetha and Prasad (arXiv:1606.04424) write these bases down explicitly inside Young's orthogonal form, so that the Gelfand–Tsetlin bases of $A_n$ and $S_n$ can be compared vector by vector. The branching rules of $A_n$ were known before (Ruff, Algebra Colloquium 2008, Theorem 6.1); the new ingredient is a sign normalisation of the associator that identifies the two halves $V_\lambda^{\pm}$ of a self-conjugate $V_\lambda$ consistently along the whole tower.

Setting

For a partition $\lambda$ of $n$, $V_\lambda$ is the complex vector space with basis $\{v_T\}$ indexed by the standard Young tableaux $T$ of shape $\lambda$. Tableaux are written inline row by row, e.g. $[1\,2\,4/3/5]$. The simple transposition $s_i = (i, i+1)$ acts by Young's formulas (2): if $i$ lies in row $j$, column $k$ of $T$ and $i+1$ in row $j'$, column $k'$, and $r = (k'-j') - (k-j)$, then $\rho_\lambda(s_i) v_T$ is $v_T$ (same row), $-v_T$ (same column), and otherwise $r^{-1} v_T + \sqrt{1-r^{-2}}\, v_{s_iT}$. For $\mu \in \lambda^{\downarrow}$ (one box fewer), $V_\mu$ embeds in $V_\lambda$ by $v_T \mapsto v_{T^\lambda}$, with $n$ written in the new box (4).

For self-conjugate $\lambda = \lambda'$, the associator $\varphi_\lambda$ is the operator

$$\varphi_\lambda(v_T) = i^{(n-d(\lambda))/2}\,\epsilon(w_T)\,v_{T'} \qquad (9),$$

where $T'$ is the transposed tableau, $d(\lambda)$ the number of diagonal boxes, and $\epsilon(w_T)$ the sign of the permutation carrying a fixed reference tableau $T_\lambda$ to $T$. The reference tableau is chosen through self-conjugate covers $(\mu, \lambda)$ ($\mu \in \lambda^\downarrow$, both self-conjugate): the smaller partition gets the row superstandard tableau, and the larger one the same tableau with $n$ added on the diagonal. $V_\lambda^{\pm}$ are the $\pm 1$ eigenspaces of $\varphi_\lambda$.

Labels $\alpha \in \tilde\Theta(n)$ are non-self-conjugate partitions $\lambda$, with $V_\alpha = V_\lambda$, and symbols $\lambda^{\pm}$ for self-conjugate $\lambda$, with $V_\alpha = V_\lambda^{\pm}$. Conjugate non-self-conjugate labels are equivalent, $\lambda \sim \lambda'$. A path $\underline\alpha = (\alpha^{(2)}, \dots, \alpha^{(n)}) \in \tilde{\mathcal S}(\alpha)$ has each $\alpha^{(i)}$ obtained from $\alpha^{(i+1)}$ by removing one box, with equal signs whenever both are self-conjugate. Definition 2 builds a vector $u_{\underline\alpha} \in V_\alpha$ recursively from $u_{(2)} = v_{[1\,2]}$ and $u_{(1^2)} = v_{[1/2]}$. At each step the previous vector $x$ is embedded by (4), and when the path passes from a non-self-conjugate shape to $\lambda^{\pm}$ it is replaced by $x \pm \varphi_\lambda(x)$.

Formalization targets

Goal: Theorem 4 (Main Theorem), p. 14

For $n \ge 2$ and $\alpha \in \tilde\Theta(n)$:

$$u_{\underline\alpha} \ne 0,\quad u_{\underline\alpha} \in V_\alpha \cap \bigcap_{k=2}^{n-1} \mathrm{Iso}_{A_k}\big(V_{\alpha^{(k)}}\big) \quad\text{for every } \underline\alpha \in \tilde{\mathcal S}(\alpha),$$

and for any set $R$ of paths ending at $\alpha$ containing one path from each equivalence class,

$$V_\alpha = \bigoplus_{\underline\alpha \in R} \mathbb C\, u_{\underline\alpha}.$$

Milestones

1. Lemma 1 (p. 4): the recursive characterisation of Gelfand–Tsetlin subspaces.
2. Lemma 2 (p. 6): every associator maps $v_T$ to a multiple of $v_{T'}$.
3. §3, (7)–(9) (pp. 7–9): for every partition, reference tableau $T_\lambda$ and scalar $c_{T_\lambda}$, the map $v_T \mapsto c_{T_\lambda}\epsilon(w_T)v_{T'}$ satisfies (5); the normalised self-conjugate $\varphi_\lambda$ of (9) also satisfies $\varphi_\lambda^2 = \mathrm{id}$.
4. Theorem 1 (1)–(2) (p. 9): $V_\lambda \cong V_{\lambda'}$ irreducible on $A_n$ for $\lambda \ne \lambda'$; $V_\lambda^\pm$ non-isomorphic irreducibles for $\lambda = \lambda'$.
5. Lemma 3 (p. 9): for self-conjugate $\mu \in \lambda^\downarrow$, the embedding (4) is $A_{n-1}$-equivariant and maps $V_\mu^{\pm}$ into $V_\lambda^{\pm}$.
6. Theorem 2 (p. 10): the branching table of $A_{n-1} \subset A_n$.
7. Theorem 3 (p. 12): each equivalence class of paths has $2^{r+1}$ elements.

Significance

The theorem gives closed-form Gelfand–Tsetlin bases for every irreducible representation of every alternating group. Each vector is a combination of Young's orthogonal basis vectors with Gaussian-integer coefficients; Example 2 of the paper shows one with four terms and coefficients $1, i, -1, i$. The matrices of $A_n$ in this basis then follow directly from Young's formulas. It also shows exactly how the two Gelfand–Tsetlin bases compare: on non-self-conjugate shapes they coincide, and on self-conjugate shapes the $A_n$-vectors are the $\pm$-symmetrisations $x \pm \varphi_\lambda(x)$ under the associator.

The result is proved in the paper; nothing about it is formalized. Lean's Mathlib has Young diagrams and the platform has standard tableaux, but there is no Young orthogonal form, no associator, no representation of $A_n$ built from partitions, and no Gelfand–Tsetlin basis for any group. A complete development would give the first machine-checked Gelfand–Tsetlin basis for $A_n$. Along the way it would give a machine-checked Young orthogonal form with its sign calculus, which is reusable for any later work on symmetric-group representations.

Difficulty

The Gelfand–Tsetlin property is a statement about isotypic components at every level. Checking it needs, at each level, the branching rule and an argument that the recursively built vector lands in the right isotypic component. For non-self-conjugate shapes this is inherited from $S_n$. The difficulty is the self-conjugate case. A path through two consecutive self-conjugate shapes $\mu^{\pm} \to \lambda^{\pm}$ keeps the sign only if $\varphi_\lambda$ restricts exactly to $\varphi_\mu$ on $V_\mu$, so the bare existence of an associator for each $\lambda$, unique up to scalar by Schur's lemma, is not enough. The sign of each $\varphi_\lambda$ has to be fixed coherently along self-conjugate covers, and this is what the choice of $T_\lambda$ and the factor $i^{(n-d(\lambda))/2}$ do. The basis half needs, in addition, the count of how many paths share a geodesic (Theorem 3) and the fact that distinct classes give distinct lines.

Formalization scope

• Tableaux. Standard tableaux are the published YoungTableau of QAlgorithms_Papers_Independent_Renew46_P26. Labels are $0, \dots, n-1$ (the paper's entry $i$ is label $i-1$) and boxes are 0-based (row, column).
• Spaces and operators. $V_\lambda$ is the space of finitely supported functions on standard tableaux of shape $\lambda$. Young's formulas (2), the embedding (4) and the associator (9) are explicit linear operators. That (2) defines a representation of $S_n$ is the cited [5, Theorem 2.1], not a result of the paper.
• Equivariance. "$A_k$-equivariant" means commuting with every product $\rho(s_i)\rho(s_j)$, $1 \le i, j \le k-1$. These products generate $A_k$, so this is equivalent to $A_k$-equivariance once (2) defines a representation.
• Isotypic subspaces. The $A_k$-isotypic subspace of type $W$ is the sum of the images of $W$ under all $A_k$-equivariant linear maps.
• Gelfand–Tsetlin vectors. A Gelfand–Tsetlin vector for a path is a nonzero vector of $V_\alpha$ lying in the isotypic subspace of type $V_{\alpha^{(k)}}$ at every level $k$.
• Standing hypothesis. The goal assumes $n \ge 2$, as the paper's paths start at $\tilde\Theta(2)$.

Ruled out. The Gelfand–Tsetlin predicate is defined intrinsically through isotypic components. It is never defined as membership in a span of the vectors that Definition 2 produces, and $u_{\underline\alpha}$ is never replaced by a formula that makes Theorem 4 hold by definition.

Not formalized. Corollary 1, the completeness clause of Theorem 1, the bijection clause of Theorem 3, Examples 1–3 and Remarks 1–4.

Solvers will need several pieces of infrastructure:

• that Young's formulas satisfy the Coxeter relations;
• the sign calculus $c_{s_iT} = -c_T$ for $\epsilon(w_T)$;
• multiplicity-freeness of $S_n \downarrow S_{n-1}$ in this model;
• the passage from generator-wise equivariance to isotypic decompositions.

The Coxeter relations and the sign calculus are reusable beyond this mission. Contributions proving any milestone, or proving that Young's operators define a representation, are welcome.

Selected references

• T. Geetha, A. Prasad, Comparison of Gelfand-Tsetlin bases for alternating and symmetric groups, arXiv:1606.04424v2, 2017 (published in Algebras and Representation Theory). https://arxiv.org/abs/1606.04424
• P. Headley, On Young's orthogonal form and the characters of the alternating group, Journal of Algebraic Combinatorics 5(2):127–134, 1996.
• A. M. Vershik, A. Yu. Okounkov, A new approach to the representation theory of the symmetric groups. II, Journal of Mathematical Sciences 131(2):5471–5494, 2005. https://arxiv.org/abs/math/0503040
• O. Ruff, Weight theory for alternating groups, Algebra Colloquium 15(3):391–404, 2008.
• A. Young, On quantitative substitutional analysis, Proceedings of the London Mathematical Society 2(1):196–230, 1932.
• A. Prasad, Representation Theory: A Combinatorial Viewpoint, Cambridge Studies in Advanced Mathematics 147, Cambridge University Press, 2015.

Motivation

Traffic models in transportation and network design come in two kinds. Nonatomic congestion games, with Wardrop equilibria, treat traffic as a continuum of infinitesimal users. Atomic games have finitely many players, each with a non-negligible effect on congestion. The Wardrop model is the one used in practice, and the usual justification is that it is the limit of atomic games as the number of players grows. Cominetti, Scarsini, Schröder and Stier-Moses (arXiv:2001.02797v7, forthcoming in Mathematics of Operations Research) make this precise in two regimes. In the first, the players' weights vanish. In the second, each player is present only with a small probability.

This mission is about the second regime, Bernoulli congestion games. Each of many potential users takes part only with a small probability, for example a commuter who may or may not travel on a given day. The limit is a Wardrop model for the mean flows, but with modified costs, and the flows themselves stay random: they are Poisson. This links Wardrop equilibria with Myerson's Poisson games (Myerson 1998).

Setting

A congestion structure consists of a finite set $\mathcal E$ of resources, each with a cost $c_e:\mathbb N^*\to\mathbb R_+$ that is nonnegative and weakly increasing on $\mathbb N^*=\{1,2,\dots\}$, and a finite set $\mathcal T$ of types. Each type $t$ has a nonempty family $\mathcal S_t\subseteq 2^{\mathcal E}$ of feasible strategies.

In the nonatomic game with demands $d=(d_t)_t$, a strategy flow $y=(y_{t,s})$ and a load vector $x=(x_e)$ are feasible, $(y,x)\in\mathcal F(d)$, when $d_t=\sum_{s\in\mathcal S_t}y_{t,s}$, $y_{t,s}\ge0$ and $x_e=\sum_t\sum_{s\in\mathcal S_t}y_{t,s}\mathbb 1_{\{e\in s\}}$. A feasible pair is a Wardrop equilibrium for costs $C_e$ when every used strategy is cheapest: $\hat y_{t,s}>0$ implies $\sum_{e\in s}C_e(\hat x_e)\le\sum_{e\in s'}C_e(\hat x_e)$ for all $s,s'\in\mathcal S_t$.

A Bernoulli congestion game $\Gamma_B$ has finitely many players $i$, each with a type $t_i$ and a participation probability $u_i\in(0,1]$. Player $i$ plays a mixed strategy $\sigma_i$ on $\mathcal S_{t_i}$ and is present ($U_i=1$) with probability $u_i$, independently of the other players. The random flows and loads are

$$Y_{t,s}=\sum_{i:t_i=t}U_i\mathbb 1_{\{S_i=s\}},\qquad X_e=\sum_iU_{i,e},\qquad U_{i,e}=U_i\mathbb 1_{\{e\in S_i\}},$$

with means $y_{t,s}=\sum_{i:t_i=t}u_i\sigma_i(s)$ and $x_e=\sum_iu_i\sigma_{i,e}$. A present player on resource $e$ pays $c_e(1+Z_{i,e})$, where $Z_{i,e}=\sum_{j\ne i}U_{j,e}$ is the load of the others. A profile $\hat\sigma$ is a Bayesian Nash equilibrium when every strategy in its support minimizes $\sum_{e\in s}\mathsf E_{\hat\sigma}[c_e(1+Z_{i,e})]$.

The limit game $\breve\Gamma^\infty$ is the nonatomic game with the same demands and the auxiliary costs

$$\breve c_e(x)=\mathsf E[c_e(1+X)],\qquad X\sim\mathrm{Poisson}(x).$$

Formalization targets

Goal: Theorem 2

Consider a sequence $\Gamma^n_B$ with $|\mathcal N^n|\to\infty$, $u^n=\max_iu^n_i\to0$ and $d^n_t=\sum_{i:t^n_i=t}u^n_i\to d_t$ (14). Assume condition (18): there are $\nu$ and $d_{\max}>\sum_td_t$ with $\mathsf E|\Delta^2c_e(1+V)|\le\nu$ for all $e$, where $V\sim\mathrm{Poisson}(d_{\max})$ and $\Delta^2c_e(k)=c_e(k+2)-2c_e(k+1)+c_e(k)$. For every sequence of Bayesian Nash equilibria $\hat\sigma^n$:

$$(\hat y^n,\hat x^n)\ \text{bounded},\qquad (\hat y,\hat x)=\lim_k(\hat y^{\varphi(k)},\hat x^{\varphi(k)})\ \Rightarrow\ (\hat y,\hat x)\in\mathsf{WE}(\breve\Gamma^\infty),$$

and along that subsequence $Y^n_{t,s}\to\mathrm{Poisson}(\hat y_{t,s})$ jointly and independently, and $X^n_e\to\mathrm{Poisson}(\hat x_e)$, in total variation.

Milestones

The milestones are the results the proof of Theorem 2 uses, in attack order:

• the Poisson–Poisson total-variation bound (46);
• the Barbour–Hall bound, Theorem 9(a);
• the limit theorem for arbitrary profiles, Proposition 1;
• the Poisson-moment facts, Propositions 5(a)–(b);
• the smoothness of Poisson mixtures, Proposition 6(b), and the derivative bound, Corollary 5(a);
• the Borisov–Ruzankin bound, Theorem 9(b);
• Lemma 1 in two parts: the regularity of $\breve c_e$, and the uniform approximation (21) of a player's expected cost by $\breve c_e(x_e)$, with a corrected constant (see Formalization scope).

Significance

Theorem 2 justifies a Wardrop description for large games with rare participation, and it says which Wardrop model. The costs are not $c_e$ but their Poisson averages $\breve c_e$, which account for the player's own presence and for the randomness of the others. The theorem also describes the fluctuations: flows are asymptotically independent Poisson variables, while loads are Poisson but correlated. The paper builds its approximation rates (§6) and its price-of-anarchy convergence results (§7) on the same Poisson calculus.

The result is proved in the paper. As far as is known, none of it is formalized. Mathlib has the Poisson distribution but no Poisson approximation of Bernoulli sums. The platform has nonatomic routing models and one-variable Chen–Stein bounds, but no Bernoulli players and no convergence-of-equilibria theorem. Formalizing the mission therefore produces:

• a checked Barbour–Hall bound and Poisson–Poisson total-variation bound;
• a calculus of Poisson mixtures (integrability transfer, smoothness, derivative bounds);
• the first machine-checked limit theorem from atomic equilibria to Wardrop equilibria.

Difficulty

The obvious approach is to say that Bayesian Nash equilibrium inequalities pass to the limit because the expected costs converge. That step fails without control on $c_e$: the costs are unbounded and evaluated at random loads, so convergence of the laws in total variation does not give convergence of $\mathsf E[c_e(1+Z_{i,e})]$. Condition (18) supplies the integrability, and the error must be bounded uniformly in the player and the profile. The Borisov–Ruzankin bound gives this, but at the Poisson parameter $z_{i,e}$ rather than at $d_{\max}$, so integrability has to be transferred between Poisson parameters. The other difficulties are independence of the limit flows, which is a joint statement on $\mathbb N^{\{(t,s)\}}$, and differentiating series in their Poisson parameter up to the end point $d_{\max}$.

Formalization scope

• Model. Players are Fin N, strategies are Finset E, and types and resources are finite types. Costs are c : E → ℕ → ℝ, nonnegative and monotone on $\{k\ge1\}$; $c_e(0)$ is never read. The page prints $c_e:\mathbb N_+\to\mathbb N_+$ and $\nu\in\mathbb N$, which are read as real-valued, the weaker hypothesis. Nonempty $\mathcal S_t$ is made explicit.
• Probability space. $\Omega=(\{0,1\}\times 2^{\mathcal E})^{\mathcal N}$ carries the product weights $\prod_i\mathsf P_i(\omega_i)\sigma_i(s_i)$. Expectations are finite sums, and the laws of flows, loads and the flow vector are image measures. Laws are therefore computed from $u$ and $\sigma$, never passed in as free measures.
• Total variation. Total variation is the published MarkovChainCLT.tvDist, the supremum over events (15). Poisson laws are Mathlib's poissonMeasure.
• Accumulation points are limits along a strictly increasing $\varphi$.
• Independence. "The $Y_{t,s}$ are independent" is formalized as total-variation convergence of the joint law of $(Y^n_{t,s})$ to the product of Poisson laws. On a countable space this is equivalent to the joint convergence in distribution that the paper proves.
• Junk values. Every expectation that is a series carries summability: in (18), Propositions 5–6, Corollary 5 and Theorem 9(b). Without it, a cost such as $c_e(k)=k!$ would satisfy (18) through Lean's value $0$ for a divergent tsum, and Theorem 2 would become false. Derivatives are taken within $[0,d_{\max}]$. Lemma 1 and Theorem 9 assume $u<1$ and $p<1$, so that $(1-u)^{-2}$ is not Lean's $1/0=0$.
• Correction to Lemma 1 (21). As printed, (21) is false. Take one resource with $c_e(j)=403(j-2)^+$, $\nu=1$, $d_{\max}=6$ and 300 players with $u_i=1/100$. Then $|\mathsf E[c_e(1+Z_{i,e})]-\breve c_e(3)|=4.1311>\Lambda(1/100)=4.0552$. The mission states (21) with $\tilde\Lambda(u)=\frac{\nu d_{\max}e^{d_{\max}}}{2}\frac{ue^u}{(1-u)^2}+u\zeta$, which is what the paper's proof gives once Proposition 5(a) transfers (18) to the parameter $z_{i,e}$. It adds the counterexample as a separate item. Theorem 2 needs only $\tilde\Lambda(u)\to0$ and is unaffected.
• Not trivializable. The goal cannot hold vacuously: the hypotheses are met by one resource, one type, $n+1$ players with $u_i=1/(n+1)$ and linear costs, for which every profile is an equilibrium (checked in Lean).
• Contributions. Contributions toward any milestone are welcome. The Poisson-approximation and Poisson-mixture results (Theorem 9, (46), Propositions 5–6, Corollary 5) do not depend on the game and can be reused elsewhere.
• Out of scope. Weighted games (Theorem 1), Poisson games (Theorems 3–4), rates (§6) and price of anarchy (§7) are not part of this mission.

Selected references

• R. Cominetti, M. Scarsini, M. Schröder, N. Stier-Moses, Approximation and Convergence of Large Atomic Congestion Games, Mathematics of Operations Research (forthcoming), arXiv:2001.02797v7, 2022. https://arxiv.org/abs/2001.02797
• A. D. Barbour, P. Hall, On the rate of Poisson convergence, Math. Proc. Cambridge Philos. Soc. 95(3), 1984. https://doi.org/10.1017/S0305004100061806
• I. S. Borisov, P. S. Ruzankin, Poisson approximation for expectations of unbounded functions of independent random variables, Annals of Probability 30(4), 2002. https://doi.org/10.1214/aop/1039548369
• J. A. Adell, A. Lekuona, Sharp estimates in signed Poisson approximation of Poisson mixtures, Bernoulli 11(1), 2005. https://doi.org/10.3150/bj/1110228242
• R. B. Myerson, Population uncertainty and Poisson games, International Journal of Game Theory 27, 1998. https://doi.org/10.1007/s001820050079
• J. G. Wardrop, Some theoretical aspects of road traffic research, Proceedings of the Institution of Civil Engineers, Part II, 1, 325–378, 1952 (no DOI given in the paper).