Probability

Motivation

The precision matrix $X=\Sigma^{-1}$ of a Gaussian random vector $\xi\in\mathbb R^p$ encodes its conditional independence structure: $X_{ij}=0$ exactly when $\xi_i$ and $\xi_j$ are independent given the other coordinates. Estimating it is a basic step in Gaussian graphical models, portfolio selection and linear discriminant analysis. The textbook estimator, the inverse of the sample covariance matrix $\widehat\Sigma$, fails when the number $n$ of samples is smaller than the dimension $p$: then $\widehat\Sigma$ is singular and the maximum likelihood problem $\min_{X\succ0}\{-\log\det X+\langle\widehat\Sigma,X\rangle\}$ has no solution. Even for $n>p$ the inverse sample covariance is badly conditioned.

Nguyen, Kuhn and Mohajerin Esfahani (arXiv:1805.07194, Operations Research 2022) replace the nominal distribution $\mathcal N(0,\widehat\Sigma)$ in the likelihood by the worst case over all normal distributions within a type-2 Wasserstein distance $\rho$ of it, and show that the resulting robust problem has a closed-form solution. The solution keeps the eigenvectors of $\widehat\Sigma$ and maps its eigenvalues through an explicit nonlinear shrinkage, and it is invertible for every sample size. Shrinkage estimators of this kind had been proposed earlier for statistical reasons (Ledoit and Wolf, doi:10.1016/S0047-259X(03)00096-4); here the shrinkage follows from the robust model rather than being imposed.

Setting

Fix a dimension $p\ge1$. Write $\mathbb S^p_+$ and $\mathbb S^p_{++}$ for the positive semidefinite and positive definite symmetric $p\times p$ matrices, and $\langle A,B\rangle=\operatorname{Tr}[A^\top B]$ for the trace inner product. For distributions $\mathbb P_1,\mathbb P_2$ on $\mathbb R^p$ the type-2 Wasserstein distance is

$$\mathbb W(\mathbb P_1,\mathbb P_2)=\inf_\Pi\Big(\int\|\xi_1-\xi_2\|^2\,\Pi(d\xi_1,d\xi_2)\Big)^{1/2},$$

the infimum over couplings $\Pi$ with marginals $\mathbb P_1$, $\mathbb P_2$ (Definition 1.1).

Given a sample covariance matrix $\widehat\Sigma\in\mathbb S^p_+$ (possibly singular) and a radius $\rho>0$, the ambiguity set is

$$\mathcal P^0_\rho=\big\{\mathbb Q=\mathcal N(0,S):\ S\in\mathbb S^p_+,\ \mathbb W(\mathbb Q,\mathcal N(0,\widehat\Sigma))\le\rho\big\},$$

the centred normal distributions, degenerate ones included, within distance $\rho$ of the nominal one. The worst-case expectation is $g(\widehat\Sigma,X)=\sup_{\mathbb Q\in\mathcal P^0_\rho}\mathbb E^{\mathbb Q}[\langle\xi\xi^\top,X\rangle]$ (7), and the robust estimation problem (5) is

$$\mathcal J(\widehat\Sigma)=\inf_{X\in\mathcal X}\Big\{-\log\det X+g(\widehat\Sigma,X)\Big\},$$

where $\mathcal X\subseteq\mathbb S^p_{++}$ is the set of admissible precision matrices; without structural information $\mathcal X=\mathbb S^p_{++}$.

The paper reformulates (5) through the metric $\mathbb W_S(\Sigma_1,\Sigma_2)=\sqrt{\operatorname{Tr}[\Sigma_1]+\operatorname{Tr}[\Sigma_2]-2\operatorname{Tr}[\sqrt{\sqrt{\Sigma_2}\Sigma_1\sqrt{\Sigma_2}}]}$ on $\mathbb S^p_+$ (Definition 2.3), the scalar program (8)

$$\inf_{\gamma:\ \gamma I\succ X}\ \gamma\big(\rho^2-\operatorname{Tr}[\widehat\Sigma]\big)+\gamma^2\big\langle(\gamma I-X)^{-1},\widehat\Sigma\big\rangle,$$

and the joint convex program (6), which minimizes $-\log\det X$ plus the objective of (8) over $\gamma I\succ X\succ0$, $X\in\mathcal X$.

Formalization targets

Goal: Theorem 3.1 (p. 12)

Let $\rho>0$, $\mathcal X=\mathbb S^p_{++}$, and $\widehat\Sigma=\sum_{i=1}^p\lambda_iv_iv_i^\top$ with orthonormal $v_i$. Then the equation

$$\Big(\rho^2-\tfrac12\sum_{i=1}^p\lambda_i\Big)\gamma-p+\tfrac12\sum_{i=1}^p\sqrt{\lambda_i^2\gamma^2+4\lambda_i\gamma}=0\tag{16b}$$

has a unique positive solution $\gamma^\star$, and the unique minimizer of (5) is

$$X^\star=\sum_{i=1}^px^\star_iv_iv_i^\top,\qquad x^\star_i=\gamma^\star\Big[1-\tfrac12\Big(\sqrt{\lambda_i^2(\gamma^\star)^2+4\lambda_i\gamma^\star}-\lambda_i\gamma^\star\Big)\Big].\tag{16a}$$

Milestones

1. The worst case over $\mathcal P^0_\rho$ equals $\sup\{\langle S,X\rangle: S\in\mathbb S^p_+,\ \mathbb W_S(S,\widehat\Sigma)\le\rho\}$ (proof of Proposition 2.8, p. 8).
2. Lemma 2.7 (p. 7): partial infima of functions continuous in $\varepsilon$ are upper semicontinuous; under uniform calmness from below they are lower semicontinuous.
3. Proposition 2.8 (p. 7): for $\widehat\Sigma\succeq0$, $X\succ0$, $g(\widehat\Sigma,X)$ equals the value of (8), and $g$ is continuous on $\mathbb S^p_+\times\mathbb S^p_{++}$.
4. Theorem 2.6 (p. 7): for every $\mathcal X\subseteq\mathbb S^p_{++}$, $\mathcal J(\widehat\Sigma)$ equals the value of (6), and $\mathcal J$ is continuous on $\mathbb S^p_+$.
5. Equation (16b) has a unique root in $[0,\infty)$, and it is positive (p. 12).
6. Identity (17), $(\gamma^\star)^2x^\star_i\lambda_i=(\gamma^\star-x^\star_i)^2$ (p. 12), and $\rho^2(\gamma^\star)^2=\sum_ix^\star_i$ (p. 13).
7. For $\widehat\Sigma\succ0$, $(X^\star,\gamma^\star)$ is feasible and optimal in (6) (p. 12).

Significance

The result. Theorem 3.1 gives the robust estimator in closed form up to an eigendecomposition and a scalar root, so it costs no more than the sample covariance itself. It shows that the estimator commutes with $\widehat\Sigma$, is positive definite for every $\rho>0$ even when $\widehat\Sigma$ is singular, and depends on the data only through the eigenvalues; the paper's later sensitivity results (Proposition 3.5) and the numerical comparisons with Ledoit–Wolf shrinkage and the graphical lasso rest on this formula. Theorem 2.6 shows more generally, for sparsity-constrained $\mathcal X$, that the robust problem is a convex program although the ambiguity set is not convex.

Formalizing it. The results are proved on paper; none is machine-checked. The formalization exercises a measure-level definition of the robust problem, with the ambiguity set defined through the coupling Wasserstein distance, and connects it to matrix analysis: the Gelbrich formula for Gaussians, a semidefinite duality, continuity of optimal value functions, and a first-order optimality argument for a matrix-fractional objective. Each milestone is reusable for other Gaussian–Wasserstein robust models, of which the platform already has several (Kalman filtering, minimax mean-square-error estimation).

Difficulty

The obvious argument is to plug $X^\star$ into the first-order conditions of (6). This works only when $\widehat\Sigma\succ0$: for singular $\widehat\Sigma$, every zero eigenvalue gives $x^\star_i=\gamma^\star$, so $\gamma^\star I-X^\star$ is singular and $(X^\star,\gamma^\star)$ is not even feasible in (6). The singular case, which is the case of interest ($p>n$), therefore needs continuity of the optimal value $\mathcal J$ and of the worst-case expectation $g$ in $\widehat\Sigma$, which is the content of Theorem 2.6 and Proposition 2.8. Those in turn require the reduction from distributions to covariance matrices (the Gelbrich formula, which holds for degenerate normals and is an optimal-transport theorem in its own right), a Lagrangian duality with a Lyapunov-equation inner problem, and a priori eigenvalue bounds on near-optimal $X$ that vary continuously with $\widehat\Sigma$. Sufficiency of the first-order conditions also needs joint convexity of $\gamma^2\langle(\gamma I-X)^{-1},\widehat\Sigma\rangle$, which the paper cites.

Formalization scope

$\mathbb R^p$ is EuclideanSpace ℝ (Fin p) and matrices are Matrix (Fin p) (Fin p) ℝ with the entrywise topology. $\mathcal N(0,S)$ is Mathlib's multivariateGaussian 0 S, which allows singular $S$. The Wasserstein distance is the published coupling distance WassersteinDRO.Gelbrich.wassersteinDistance 2, valued in $[0,\infty]$; the radius enters through ENNReal.ofReal ρ. The square root is the published psdSqrt, and $\langle\cdot,\cdot\rangle$ the published WassMMSE.Sandwich.frob. The worst-case expectation, $\mathcal J$, and the values of (6) and (8) are suprema and infima in EReal. Every distribution in $\mathcal P^0_\rho$ is Gaussian, so the integrand $\langle\xi\xi^\top,X\rangle$ is integrable. Every matrix inverse sits under the constraint $\gamma I\succ X$ inside the infimum. "Unique minimizer" is stated as IsMinOn over all positive definite $X$ together with equality of every positive definite minimizer to $X^\star$. The eigendecomposition is an arbitrary orthonormal one, not a basis chosen by the library.

One hypothesis is added: $p\ge1$, because for $p=0$ (16b) has no positive solution. Definition 2.1 prints the normal density without the factor $\tfrac12$ in the exponent; the standard normal distribution is used.

The goal is stated for the measure-level problem (5). Stating it on the matrix program (6) would be a different and, for singular $\widehat\Sigma$, false theorem. Replacing $\mathcal P^0_\rho$ by the covariance ball or by all distributions, or computing suprema as real sSup (which returns $0$ on unbounded sets), would trivialize or change the statement.

The mission concerns the zero-mean problem (5) with $\mathcal X=\mathbb S^p_{++}$ for the goal; Theorem 2.6 is posed for general $\mathcal X\subseteq\mathbb S^p_{++}$. Out of scope: Theorem 2.10 (the unknown-mean problem (4)), Corollary 2.9, Lemma 3.3, Proposition 3.5, the algorithm of §4, the extremal distributions of §5 (Theorem 5.1) and the experiments of §6. The Gelbrich formula (Proposition 2.2) is not posed here; it is Open on the platform as WassKF.Reform.proposition_2_2. The Open theorem WassMMSE.Sandwich.proposition_A_4_i, a covariance-level duality behind Proposition 2.8, is included for reuse. Welcome contributions: the Gelbrich formula for possibly degenerate centred normals, second moments of multivariateGaussian, continuity of optimal value functions (Berge's maximum theorem), and convexity of the matrix-fractional function.

Selected references

• V. A. Nguyen, D. Kuhn, P. Mohajerin Esfahani, Distributionally Robust Inverse Covariance Estimation: The Wasserstein Shrinkage Estimator, Operations Research 70(1), 2022; read as arXiv:1805.07194v1, 2018. https://arxiv.org/abs/1805.07194
• C. R. Givens, R. M. Shortt, A class of Wasserstein metrics for probability distributions, Michigan Mathematical Journal 31(2), 1984. https://doi.org/10.1307/mmj/1029003026
• O. Ledoit, M. Wolf, A well-conditioned estimator for large-dimensional covariance matrices, Journal of Multivariate Analysis 88(2), 2004. https://doi.org/10.1016/S0047-259X(03)00096-4
• S. Boyd, L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://doi.org/10.1017/CBO9780511804441

Motivation

Misinformation campaigns target specific people in a social network and rely on the network to spread what they plant. Whether such a campaign can succeed depends on how people combine what they see themselves with what their neighbours believe. Mostagir, Ozdaglar and Siderius (SSRN 3474643; Management Science, 2022, doi:10.1287/mnsc.2021.4265) model a network in which a strategic principal injects slanted news into chosen agents. Some agents are Bayesian and know the truth; the rest are DeGroot agents who average their own news-based opinion with their neighbours' beliefs.

The paper asks when society as a whole can be manipulated. Every later result in it — which agents the principal targets, which networks resist manipulation, how the answer depends on the network's density — is a statement about the agents' long-run beliefs. Its Theorem 2 supplies those beliefs in closed form, and that closed form is the subject of this mission.

DeGroot updating (DeGroot, 1974) and its combination with personal Bayesian updates (Jadbabaie, Molavi, Sandroni and Tahbaz-Salehi, 2012) are standard models of non-Bayesian social learning. Stubborn agents in averaging dynamics were studied by Acemoglu, Como, Fagnani and Ozdaglar (2013). The present model adds a principal who corrupts the signals of targeted agents.

Setting

There are $n$ agents and a binary state $y\in\{S,R\}$ with prior $q=\mathbb P(y=S)\in(0,1)$. Agent $i$ has a signal quality $p_i\in[1/2,1)$. At each time $\tau=1,2,\dots$ agent $i$ receives a signal $s_{i,\tau}\in\{S,R\}$:

• Organic news equals the state with probability $p_i$: $\mathbb P(s_{i,\tau}=S\mid y=S)=\mathbb P(s_{i,\tau}=R\mid y=R)=p_i$.
• The principal fixes an influence state $\hat y$ and an influence strategy $\mathbf x=(x_1,\dots,x_n)\in\{0,1\}^n$. A targeted agent ($x_i=1$) receives the principal's message $\hat y$ with probability $\lambda^*/(\lambda+\lambda^*)$ and organic news with probability $\lambda/(\lambda+\lambda^*)$. Here $\lambda>0$ and $\lambda^*>0$ are the intensities of the organic and the principal's news. An untargeted agent receives only organic news.

Agent $i$'s signals are independent over time. Its personal experience is the posterior it would compute taking every signal at face value. With $z^S_{i,t},z^R_{i,t}$ the numbers of $S$ and $R$ signals among $s_{i,1},\dots,s_{i,t}$,

$$\mathrm{BU}_i(S\mid h_{i,t})=\frac{p_i^{z^S_{i,t}}(1-p_i)^{z^R_{i,t}}q}{p_i^{z^S_{i,t}}(1-p_i)^{z^R_{i,t}}q+p_i^{z^R_{i,t}}(1-p_i)^{z^S_{i,t}}(1-q)},$$

and $\mathrm{BU}_i(R\mid h_{i,t})=1-\mathrm{BU}_i(S\mid h_{i,t})$.

A set $B$ of agents is Bayesian. A Bayesian agent knows $y$ and always believes it. Each DeGroot agent $i\notin B$ has weights $\theta_i\ge0$ and $\alpha_{ij}\ge0$ with $\theta_i+\sum_j\alpha_{ij}=1$. For a state $y'$, its belief $\pi_{i,t}(y'\mid y)$ follows the DeGroot update

$$\pi_{i,t+1}=\theta_i\,\mathrm{BU}_i(y'\mid h_{i,t+1})+\sum_{j=1}^n\alpha_{ij}\,\pi_{j,t}.$$

The influence matrix $\mathbf W$ has zero rows for Bayesian agents and row $(\alpha_{ij})_j$ for DeGroot agents. The vector $\boldsymbol\theta=(\mathbf 1_B,\theta_{m+1},\dots,\theta_n)$ has entry $1$ on Bayesians. The unweighted graph $G^*$ has a link $i\to j$ when $i$ listens to $j$; for a DeGroot agent this means $\alpha_{ij}>0$.

Assumption 1 (pp. 10–11):

• (i) $p_i<(\lambda^*+\lambda)/(2\lambda)$ for every agent;
• (ii) $G^*$ is strongly connected;
• (iii) a DeGroot agent has $\theta_i>0$ exactly when $p_i>1/2$;
• (iv) some agent has $p_i>1/2$.

Formalization targets

Goal: Theorem 2 (p. 11)

Under Assumption 1, for every principal action $\mathbf x^*$, each DeGroot agent's personal experience converges almost surely to a constant $\mathrm{BU}_i(h_{i,\infty}(\mathbf x^*))(y'\mid y)$, and

$$\boldsymbol\pi_t(y'\mid y)\xrightarrow{\text{a.s.}}(\mathbf I-\mathbf W)^{-1}\big(\mathrm{BU}(\mathbf h_\infty(\mathbf x^*))(y'\mid y)\odot\boldsymbol\theta\big),$$

where the Bayesian entries of the vector $\mathrm{BU}(\mathbf h_\infty(\mathbf x^*))$ are the correct belief. The goal does not fix the constants: the paper computes them only later (display (2), p. 12).

Milestones

1. Lemma 3 (p. 45): the spectral radius of $\mathbf W$ is strictly less than $1$.
2. Proof of Theorem 2 (p. 47): $\mathbf I-\mathbf W$ and its DeGroot block $\mathbf I-\mathbf A_{DD}$ are invertible.
3. §3.2 (p. 11): $\mathrm{BU}_i(h_{i,t})$ converges almost surely to a constant.
4. Proof of Theorem 2 (p. 47): if $\mathbf u_t\to\mathbf u_\infty$ and $\boldsymbol\pi_{t+1}=\mathbf u_{t+1}+\mathbf W\boldsymbol\pi_t$, then $\boldsymbol\pi_t\to\boldsymbol\pi_\infty=(\mathbf I-\mathbf W)^{-1}\mathbf u_\infty$, the solution of $\boldsymbol\pi_\infty=\mathbf u_\infty+\mathbf W\boldsymbol\pi_\infty$.

Significance

Theorem 2 reduces the paper's manipulation question to linear algebra. A DeGroot agent ends up believing the wrong state exactly when the corresponding entry of $(\mathbf I-\mathbf W)^{-1}(\mathrm{BU}_\infty\odot\boldsymbol\theta)$ crosses a threshold. The principal's targeting problem then becomes a combinatorial problem over $\mathbf x^*$ in which the network enters only through $(\mathbf I-\mathbf W)^{-1}$. The paper's DeGroot centrality (Proposition 2) and its results on dense and sparse networks all start from this formula.

On formalization: the paper proves Theorem 2, but no machine-checked version exists. The mission's statements also record two places where the written argument needs repair. The text attributes the almost-sure convergence of $\mathrm{BU}_i$ to the martingale convergence theorem, but $\mathrm{BU}_i$ is a face-value posterior and not a martingale under the corrupted signal law. The proof's step from small increments of $\boldsymbol\pi_t$ to convergence of $\boldsymbol\pi_t$ is also not valid as written. Both claims are true under Assumption 1, and a complete development supplies correct arguments. The supporting results — spectral radius below one for a substochastic matrix with leakage reachable from every row, and convergence of linear recursions with convergent input — are reusable beyond this paper.

Difficulty

Two steps resist the obvious arguments.

First, $\mathrm{BU}_i(S\mid h_{i,t})$ is a function of the drift $z^S_{i,t}-z^R_{i,t}$ of a random walk. Its limit exists only if the walk is transient or $p_i=1/2$. For a targeted agent the walk's step law mixes the principal's message with organic news. For one boundary value of $p_i$ the step has mean zero, the walk is recurrent and $\mathrm{BU}_i$ oscillates forever. Assumption 1(i) excludes exactly that value. A proof must use it; a martingale argument does not apply.

Second, $\mathbf W$ is substochastic but not strictly so: a DeGroot row sums to $1-\theta_i$, which equals $1$ whenever $p_i=1/2$. A row-sum bound alone gives $\rho(\mathbf W)\le1$, not $<1$. Strict inequality needs every DeGroot agent to reach, in the weighted graph, an agent that leaks weight — a Bayesian or a DeGroot agent with $\theta_i>0$. This uses the interaction of Assumption 1 (ii), (iii) and (iv), with Bayesian agents' outgoing links playing no role in $\mathbf W$.

Formalization scope

Agents are Fin n and the Bayesian set is a Finset. Time is discrete, and the history at time $t$ is the signals at times $1,\dots,t$. The state space is a two-element inductive type. The signals are random variables on a probability space $(\Omega,P)$. Each agent's sequence is independent over time with the law above; signals of different agents may be dependent. This is deliberate: in the paper all targeted agents receive the same principal stream, so cross-agent independence would exclude the paper's own model. The principal's action is pure ($\mathbf x^*\in\{0,1\}^n$), as §3.2 allows without loss of generality. The DeGroot initial belief can be any value in $[0,1]$, and the conclusion holds for every such initial belief on one almost-sure event. "Spectral radius" is Mathlib's spectralRadius ℂ of the complexified matrix. $(\mathbf I-\mathbf W)^{-1}$ is Mathlib's matrix inverse; no invertibility hypothesis is added, because Assumption 1 implies it. In the graph $G^*$, a DeGroot agent's links are exactly its positive weights; Bayesian agents' links are free.

The personal experience is the explicit face-value posterior of the given signal process, and the conclusion of the goal includes its almost-sure convergence to the constants used in the limit. The goal therefore cannot be met by an abstract learning rule or a free limit vector.

A complete development needs:

• the strong law of large numbers (available in Mathlib) applied to the signal counts;
• a Perron–Frobenius-type spectral bound for substochastic matrices on a strongly connected graph;
• convergence of $\boldsymbol\pi_{t+1}=\mathbf u_{t+1}+\mathbf W\boldsymbol\pi_t$ when $\rho(\mathbf W)<1$.

Contributions of any of these, as standalone lemmas, are welcome.

Selected references

• M. Mostagir, A. Ozdaglar, J. Siderius, When Is Society Susceptible to Manipulation?, SSRN preprint 3474643 (version of 2020-06-08); Management Science 68(10), 2022. https://ssrn.com/abstract=3474643, https://doi.org/10.1287/mnsc.2021.4265
• M. H. DeGroot, Reaching a Consensus, Journal of the American Statistical Association 69(345), 1974. https://doi.org/10.1080/01621459.1974.10480137
• A. Jadbabaie, P. Molavi, A. Sandroni, A. Tahbaz-Salehi, Non-Bayesian Social Learning, Games and Economic Behavior 76(1), 2012. https://doi.org/10.1016/j.geb.2012.06.001
• D. Acemoglu, G. Como, F. Fagnani, A. Ozdaglar, Opinion Fluctuations and Disagreement in Social Networks, Mathematics of Operations Research 38(1), 2013. https://doi.org/10.1287/moor.1120.0570

Motivation

On-demand ride-hailing platforms replaced street-hailing on the promise that matching a passenger to a car at the moment of the request shortens the wait. Feng, Kong and Wang (SSRN 2960991, later published in Manufacturing & Service Operations Management, doi:10.1287/msom.2020.0880) ask whether that is true in a stylized model and find that it need not be: when all traffic moves in one direction, the street-hailing ("no-call") mechanism never waits longer on average than the platform ("call") mechanism. The question matters to platform designers, to regulators weighing taxi against platform service, and to the queueing literature on spatial matching, where the cost of committing a car to a passenger before it arrives is a recurring theme.

The paper studies the exact systems by simulation and, for proofs, replaces each of them by a birth–death queue whose service rates depend on the number of passengers in the system. This mission formalizes the comparison theorem for those approximations (Theorem 4) together with the results its proof uses.

Setting

A circular road of perimeter $R > 0$ carries $k \ge 1$ taxis that move clockwise at constant speed $v > 0$. Passengers arrive as a Poisson process of rate $\lambda \ge 0$ at uniformly distributed points of the circle; each requests a ride of exponentially distributed length with mean $d > 0$, so a ride lasts $d/v$ on average. The paper writes $\mu = v/d$ for the ride completion rate.

• In the call mechanism a platform matches an arriving passenger at once to the nearest available taxi, or, if none is free, matches the next free taxi to its nearest waiting passenger.
• In the no-call mechanism a passenger is picked up by the first free taxi that passes by.

A state-dependent $M/M/k$ queue has arrival rate $\lambda$ and, when $n \ge 1$ customers are in the system, departure rate $\mu_n$. Its average waiting time (arrival to pick-up) is given in closed form (Appendix A, p. 34):

$$\mathcal W(\mu) = \frac{\sum_{i=1}^{\infty} \frac{i\lambda^{i-1}}{\mu_1\mu_2\cdots\mu_i}}{1 + \sum_{i=1}^{\infty} \frac{\lambda^{i}}{\mu_1\mu_2\cdots\mu_i}} - \frac dv ,$$

and $\mathcal W(\mu) < \infty$ means that both series converge (FiniteWait in Lean, avgWait for the value).

The one-direction call approximation is the queue with rates (1), p. 16:

$$\mu^{(1c)}_n = \frac{n}{\frac dv + \frac{R}{v(k-n+1)}}\ (n<k),\qquad \frac{k}{\frac dv + \frac{R}{2v}}\ (n=k),\qquad \frac{k}{\frac dv + \frac{R}{v(n-k+1)}}\ (n>k).$$

The no-call approximation is the queue with rates (3), p. 19:

$$\mu^{(nc)}_n = \frac{n}{\frac dv + \int_0^{R/v} \left(\frac{R-vt}{R}\right)^{k-n+1} e^{-\frac{(n-1)v^2t^2}{2Rd}}\,dt}\ (n\le k),\qquad \frac{k}{\frac dv + \int_0^{R/v} \left(\frac{R-vt}{R}\right)^{n-k} e^{-\frac{\lambda v t^2}{2R}}\,dt}\ (n>k).$$

Write $\mathcal W^{(1c)}(\lambda,d,v,k,R)$ and $\mathcal W^{(nc)}(\lambda,d,v,k,R)$ for the two waiting times (W1c, Wnc in Lean, with mu1c, muNC for the rates).

Formalization targets

Goal: Theorem 4 (p. 21)

For $d, v, R > 0$, $k \ge 1$ and $0 \le \lambda < kv/d$, both waiting times are finite and

$$\mathcal W^{(nc)}(\lambda,d,v,k,R) \le \mathcal W^{(1c)}(\lambda,d,v,k,R).$$

Milestones, in attack order

1. Theorem 1(1) (p. 16). For $\lambda \ge 0$: $\mathcal W^{(1c)} < \infty$ if and only if $\lambda < kv/d$.
2. Rate comparison (proof of Theorem 4, p. 38). For every state $n \ge 1$: $0 < \mu^{(1c)}_n \le \mu^{(nc)}_n$.
3. Coordinatewise monotonicity (proof of Theorem 4, pp. 38–39). In any state-dependent $M/M/k$ queue with positive rates, $\lambda > 0$ and finite waiting time, raising a single rate $\mu_m$ strictly lowers $\mathcal W$ (the paper's $\partial \mathcal W/\partial\mu_m < 0$).
4. Comparison principle (proof of Theorem 4, p. 38). If $0 < \mu_n \le \mu'_n$ for every $n \ge 1$ and $\mathcal W(\mu) < \infty$, then $\mathcal W(\mu') < \infty$ and $\mathcal W(\mu') \le \mathcal W(\mu)$.

Milestones 3 and 4 are statements about every state-dependent $M/M/k$ queue, not only about the two approximations.

Significance

Theorem 4 is the paper's analytical support for its simulation finding (Figure 11(a)) that, with one-directional traffic, the on-demand mechanism's early commitment costs more than it gains: a no-call taxi can pick up a passenger who appeared on its path after the call mechanism would already have dispatched it elsewhere. The paper contrasts this with the two-direction system, where the call mechanism wins at very low and very high load (Theorem 5), so Theorem 4 isolates the effect of the road geometry.

The comparison principle (milestone 4) is used again, without restatement, in the proofs of Theorem 1(4) and Theorem 5. It is a general fact about birth–death queues: the average sojourn time is monotone in the service rates. A formal statement and proof of it is reusable for any model approximated by a state-dependent $M/M/k$ queue.

Status: the results are proved in the paper (Appendix A). They have not been formalized; no machine-checked proof of any of them is known.

Difficulty

The rate comparison is elementary but casewise: the three branches of (1) meet the two branches of (3), the state $n = k$ falls in different branches of each, and for $n < k$ the call en-route time is not the no-call integral with the exponential removed, so no single identity covers all states.

The central difficulty is the passage from one coordinate to all coordinates. The paper shows that $\mathcal W$ decreases when one rate $\mu_m$ increases, and concludes that it decreases when all rates increase at once. With infinitely many rates this is not a finite chain of one-coordinate changes, so the coordinatewise statement alone does not give the comparison principle; a limit argument, or a direct argument on all coordinates, is needed, together with the transfer of summability from $\mu$ to $\mu'$.

Theorem 1(1) requires a convergence test for series whose ratios $\lambda/\mu^{(1c)}_n$ tend to $\lambda d/(kv)$, and the converse needs the strict bound $\mu^{(1c)}_n < kv/d$ in every state.

Formalization scope

• Parameters are real numbers lam d v R : ℝ (λ is lam) and k : ℕ. The standing assumptions $d, v, R > 0$, $k \ge 1$, $\lambda \ge 0$ are implicit in the paper and explicit hypotheses of every theorem. The constant $\mu = v/d$ is written v / d; the name μ is reserved for rate sequences.
• Rates are functions ℕ → ℝ used for $n \ge 1$; products run over Finset.Icc 1 i, both series start at $i = 1$, and the "$1 +$" is the $i = 0$ term. Lean's $0^0 = 1$ gives $\mathcal W = 1/\mu_1 - d/v$ at $\lambda = 0$, the paper's value.
• In (1) the factors $k-n+1$, $n-k+1$ are real; in (3) the exponents are natural numbers used only inside their branches. The integrals are Mathlib interval integrals over $[0, R/v]$.
• "For any $\lambda$" in Theorem 4 is posed on $0 \le \lambda < kv/d$. Outside it both waiting times are infinite and the inequality has no content. The paper's printed strict inequalities ($\mu^{(nc)}_n > \mu^{(1c)}_n$, $\mathcal W^{(nc)} < \mathcal W^{(1c)}$) fail in degenerate cases ($n = k = 1$; $\lambda = 0$, $k = 1$) and are stated as "$\le$".
• $\mathcal W^{(1c)}$ and $\mathcal W^{(nc)}$ are the closed-form waiting times of the $M/M/k$ approximations, not of the simulated ride-hailing systems; Theorem 4 is a statement about the approximations.
• Trivializing formalizations are ruled out: muNC is defined from (3) as printed, not through mu1c and not with its integrals replaced by bounds; no theorem compares waiting times without asserting or assuming FiniteWait (Lean's tsum of a divergent series is $0$); the index base and the "$1 +$" follow the paper; and the goal holds for every $\lambda$ in the stability region, not a single value.
• Needed infrastructure: Mathlib's tsum, Summable, Finset.prod, intervalIntegral, Real.exp. Useful contributions beyond the milestones: a general ratio-test lemma for products of rates with a limit, and the comparison principle for birth–death waiting times, both reusable outside this paper.

Selected references

• G. Feng, G. Kong, Z. Wang, We Are on the Way: Analysis of On-Demand Ride-Hailing Systems, SSRN working paper 2960991, version of 2020-04-16. https://ssrn.com/abstract=2960991
• G. Feng, G. Kong, Z. Wang, We Are on the Way: Analysis of On-Demand Ride-Hailing Systems, Manufacturing & Service Operations Management, 2021. https://doi.org/10.1287/msom.2020.0880

Motivation

A firm can sell utility tokens before it has produced the good those tokens will buy. The sale supplies cash for production, but the firm can keep some or all of that cash instead. Speculators anticipate both the later value of a token and this diversion incentive when deciding whether to buy. Gan, Tsoukalas and Netessine study the resulting financing and production decisions in a three-period model of an initial coin offering (ICO). Their utility-token analysis identifies a value-to-cost threshold below which the ICO cannot raise cash and, above it, a unique equilibrium design under the paper's demand condition. Gan, Tsoukalas and Netessine, SSRN author version, §§2–3 and Appendix B.1.

The question matters to operations and finance because the funds obtained before production change the firm's later incentive to produce. Selling more tokens supplies a larger budget but leaves the firm with fewer tokens to sell after demand is realized. The model makes that tension quantitative through the ICO cap, production quantity and market token price. Gan, Tsoukalas and Netessine, pp. 7–14.

Setting

The firm initially has no wealth and owns $m>0$ utility tokens, redeemable for its future product. It chooses an ICO price $\tau\ge0$ and a cap $n\in[0,m]$ on tokens sold to speculators. There are $z\ge m$ potential speculators. Each wants at most one token and arrives simultaneously. If $s$ tokens sell, the firm may produce $Q$ units at unit cost $c>0$, subject to $0\le Q\le\tau s/c$. Customer demand $D$ has probability law $\mu$ and cumulative distribution function $F$; customers value each unit at $v>c$. Token counts and quantities are represented by real numbers, as in the paper's continuous optimization. Gan, Tsoukalas and Netessine, §2, pp. 7–10.

The market-clearing price of a token after demand is realized is $(v/m)\min\{Q,D\}$. Write $S(Q)=\mathbb E_\mu[\min\{D,Q\}]$ for expected sales. Conditional on $s$ sales, the firm maximizes $(m-s)(v/m)S(Q)-cQ$ over the production budget. A production rule $Q(\tau,s)$ selects a maximizer at every feasible history; it is determined by this optimization problem rather than prescribed by a closed formula. At the ICO stage a speculator's expected utility is

$$u_\tau(s)=\frac{s}{z}\left(\frac vm S(Q(\tau,s))-\tau\right).$$

The participation rule sells all $n$ offered tokens when $u_\tau(n)\ge0$, and otherwise sells none. The firm's expected terminal wealth is ICO receipts less production cost plus the market value of its unsold tokens. An equilibrium consists of production optimality after every feasible history and a pair $(\tau,n)$ maximizing this wealth over all $\tau\ge0$ and $0\le n\le m$. The market-clearing and participation rules are the model's interpretations of Lemma 1 and Lemma 2(i). Gan, Tsoukalas and Netessine, (1)–(3), (10), pp. 8–10, 12, 34.

Formalization targets

Proposition 1 identifies the optimal production quantity in two regimes. Proposition 2 identifies when a cap can support positive sales at a positive ICO price. Lemma 2 and Propositions 12–13 supply the participation and optimal-cap statements recorded as milestones. The main target is Proposition 3, including every part of its conclusion. Gan, Tsoukalas and Netessine, pp. 11–14, 34–35.

If $v\le2c$, no feasible ICO design raises cash. If $v>2c$, the equilibrium ICO price $\tau^*$ and cap $n^*$ exist and are unique. With

$$Q^*=F^{-1}\!\left(1-\frac{m}{m-n^*}\frac cv\right),$$

the cap is the unique point in $(mc/v,m/2)$ satisfying

$$\frac{vn^*}{cm}S(Q^*)=Q^*.$$

The remaining conclusions are $\tau^*=(v/m)S(Q^*)$, all $n^*$ tokens sell, market-period token price equals $(v/m)\min\{Q^*,D\}$ with expectation $\tau^*$, and the full ICO proceeds are used for production: $cQ^*=\tau^*n^*$. Gan, Tsoukalas and Netessine, Proposition 3, pp. 13–14.

Significance

The result gives a precise failure threshold for a utility-token ICO and ties the successful design to demand, production cost and the amount of tokens retained by the firm. In particular, its cap is below half of the total token supply, and at the optimum the production budget binds. These are statements about the model's incentive problem, with the demand condition required for its uniqueness result. Gan, Tsoukalas and Netessine, discussion after Proposition 3, p. 14.

The paper proves these results mathematically. This mission records their Lean statements as open goals; it does not yet supply machine-checked proofs. Completing the formalization would also develop reusable facts about expected truncated demand, inverse distribution functions, and optimization under a cash budget. The equity-token comparison, extensions and numerical experiments remain separate from this target. Gan, Tsoukalas and Netessine, §§4, 6 and Appendix C.

Difficulty

The firm controls the ICO price and cap before the production decision, while speculator participation responds to the production rule. Raising the cap increases possible receipts but can lower the firm's incentive to produce and therefore the resale value speculators expect. A production optimum for fixed sales does not by itself identify which sales level will occur. The firm's wealth also changes regime when the production budget ceases to bind, so a single smooth optimization statement does not cover the entire feasible set. The uniqueness claim depends on the demand-density condition stated before Proposition 12. Gan, Tsoukalas and Netessine, §§3.1–3.4 and Appendix B.1.

Formalization scope

Demand is one probability measure $\mu$ on $\mathbb R$: $F$ is its cumulative distribution function and $S(Q)$ is the integral of $\min(D,Q)$ against that same measure. The inverse expression is the infimum of nonnegative $x$ with $F(x)\ge y$. The paper's $F^{-1}(0)=0$ is represented by $F(x)=0$ for $x\le0$ and $F(x)>0$ for $x>0$. Because the proofs and the Appendix B.1 condition use a density and its derivative, the formal setting requires a positive differentiable density wherever $x>0$ and $F(x)<1$. The paper's informal $z\gg m$ is represented by $m\le z$. These choices are explicit added assumptions or readings of the source's conventions. Gan, Tsoukalas and Netessine, pp. 8–9, 34, 37–38, 46–48.

The Appendix B.1 condition on $f'/f^2$ is applied at interior quantiles $0<y<1-2c/v$, avoiding the support boundary where the paper does not define the derivative. Lemma 2(ii)–(iii) is stated at $\tau>0$, because at zero price its printed conclusions fail. The positive boundary price in Proposition 12 is considered on the open viable-cap interval; its printed upper endpoint has no positive solution. Its “unique solution” is the unique positive solution, since zero also solves the first displayed equation. The participation equality there is evaluated at full sales $s=n$: evaluated after abstention at $s=0$, it would hold automatically. These boundary readings follow the paper's own adjacent analysis. Gan, Tsoukalas and Netessine, pp. 12–13, 34–35, 45–47.

The production rule is quantified over every rule that truly optimizes the budgeted production subgame. Expected sales is the integral against $\mu$, never a free function unrelated to $F$. The equilibrium optimizes over all feasible prices and caps; the narrow interval for $n^*$ is a conclusion. The work needed includes measure-theoretic sales identities, quantile behavior, and the firm's regime-dependent optimization. Contributions establishing these facts or proving the named milestones fit this mission. The model here is the base utility-token, simultaneous-arrival model; equity tokens, sequential arrival, the §6 extensions and numerics are outside its scope.

Selected references

• J. R. Gan, G. Tsoukalas and S. Netessine, Initial Coin Offerings, Speculation, and Asset Tokenization, SSRN author version 3361121, June 29, 2020; published in Management Science (2020). SSRN author version, DOI.

Motivation

Sellers sometimes offer a customer a choice among individual products and a product whose final item is revealed only after purchase. Airlines, for example, can sell a fixed itinerary alongside a discounted option that leaves one feature unspecified. The seller must decide whether this opaque product earns enough to justify limiting how much individual item prices can differ. Elmachtoub and Hamilton study this question for unit-demand customers who know their own values for the possible items. Their 2021 paper identifies two conditions under which the best menu of opaque products earns at least as much as the best separate item prices.

The comparison matters because the opaque menu uses less item-specific pricing information. The seller gives every item one price and gives opaque products of equal size the same price. The theorem says that this constrained format can still match discriminatory pricing when the valuation law is symmetric and either customers assess opaque products pessimistically or valuations have only two levels. The paper also supplies counterexamples outside those conditions; the symmetry and customer-type hypotheses are substantive.

Setting

There are $N\ge2$ items. A customer has a nonnegative valuation vector $v=(v_1,\ldots,v_N)$, sampled from a probability law $F$. A menu option has a price and a valuation. Its utility is valuation minus price. The customer buys one option of greatest utility when that utility is nonnegative. If several options have greatest utility, the customer buys one with the highest price. Remaining ties at the same price do not affect revenue. A customer may also buy nothing, yielding zero revenue.

In discriminatory pricing (DP), the seller assigns a nonnegative price $p_i$ to each item and offers only the individual items. Write $R_{\mathrm{DP}}(p_1,\ldots,p_N)$ for expected revenue and $R_{\mathrm{DP}}$ for its optimum over item-price vectors.

In opaque selling (OPQ), the seller offers the items at a common price $p$ and also offers every set $S$ of at least two items. A set of size $k$ costs $p^k$, independent of which items it contains. A pessimistic customer values $S$ at $\min_{i\in S}v_i$; a risk-neutral customer values it at $|S|^{-1}\sum_{i\in S}v_i$. Both value a singleton at its item value. A customer is pessimistic with probability $\alpha$ and risk-neutral with probability $1-\alpha$, independently of the valuation vector. The expected revenue of a price menu is $R_{\mathrm{OPQ}}^\alpha(p,p^2,\ldots,p^N)$; its optimum is $R_{\mathrm{OPQ}}^\alpha$.

A law $F$ is exchangeable if permuting the coordinates of $v$ leaves its joint distribution unchanged. Coordinates may be correlated, and they need not be independent. A law is two-valued when there are real numbers $a<b$ such that almost every valuation vector has every coordinate in $\{a,b\}$. This says the same pair applies to the entire vector, rather than allowing a different pair at each coordinate.

Formalization targets

Theorem 1: revenue dominance

For exchangeable $F$, nonnegative valuations, and $0\le\alpha\le1$, the target is

$$\bigl(\alpha=1\ \text{or}\ F\text{ is two-valued}\bigr) \quad\Longrightarrow\quad R_{\mathrm{OPQ}}^\alpha\ge R_{\mathrm{DP}}.$$

The first case covers any exchangeable law, including discrete laws with ties, when all customers are pessimistic. The second covers every mix of customer types when the valuations take two common values. Neither case requires independent item values. This mission retains both cases in one goal because that is Theorem 1 as stated in the paper.

The milestones trace the two cases. They identify the equal probabilities of valuation-order events, the value of the best opaque subset at a fixed size, the pessimistic dominance case, the three candidate DP price vectors under two values, the conditional revenue identity printed as display (1), the opaque price ladder's revenue for both customer types, and the two-valued dominance case. Each milestone is attached to a passage in the proof of Theorem 1.

Significance

The theorem gives a comparison of optimal revenues, not just a comparison of one chosen menu with one chosen price vector. For a seller with exchangeable valuations, it guarantees that size-based opaque prices can recover at least the revenue available from item-specific prices in either named regime. Outside those regimes, the paper's counterexamples prevent extending that guarantee merely by relaxing the hypotheses.

The result is proved in the cited paper; the goal here is a machine-checked version of its statement and proof. A formal development would establish the choice rule for finite menus, expectations for discrete and continuous valuation laws, permutation symmetry, finite order statistics, and the behavior of size-based menus at utility and price ties. These components are reusable in later formalizations of unit-demand pricing and opaque-product models. The present mission starts with unproved Lean theorem statements; compiling those statements does not certify the paper's argument.

Difficulty

One tempting argument treats the opaque menu as discriminatory pricing with the valuation order known to the seller. That comparison overlooks a restriction: the same price must be attached to each product size, so a price that is useful for the highest-valued item need not be useful for every realized ordering. The paper explicitly notes that the apparent information advantage alone would also suggest dominance in settings where dominance fails.

Ties create another obstacle. The probability formulas displayed for DP and OPQ in the selling-model section use inequalities that can count a tied purchase more than once. The paper sets aside ties for exposition in that section, yet the two-valued case necessarily has them. A faithful proof has to use the stated customer choice rule and the highest-price tie-break, rather than treating those displayed sums as definitions for discrete laws. The two-valued case also requires tracking how revenue changes with the number of high valuations, without assuming independent coordinates.

Formalization scope

Items are represented by Fin N and valuation profiles by functions Fin N → ℝ; the paper's item indices start at one, while Lean's start at zero. The probability law is a measure on profiles with a probability-measure instance and almost-sure nonnegative coordinates. Exchangeability means invariance of this law under every coordinate permutation. Two-valued support is an almost-sure condition on the whole profile. No independence or density assumption is included.

The menu contains every nonempty item set. Singletons stand for the ordinary items at their common price; sets of equal larger size share an opaque price. All seller prices are nonnegative. Revenue is the highest price among options with maximal nonnegative utility, with zero when no option qualifies. This directly represents the rule on page 8, including discrete laws. The pessimistic valuation is a finite minimum and the risk-neutral valuation a finite average. Customer type is mixed independently of the valuation law, so the OPQ expectation is the $\alpha$-weighted sum of the two type-specific expectations.

Expected revenues and optimal revenues use extended nonnegative reals $[0,\infty]$. The optima are suprema over nonnegative prices; existence of a maximizing price vector is not assumed. This avoids default values for an unbounded real supremum and records possible infinite revenue. Prices for unused cardinalities are nonnegative but have no effect on the menu. The order statistic sorts the coordinates with multiplicity; it is not defined through the subset identity it is meant to satisfy.

The goal is not implied by a degenerate model: the revenue function charges the highest price among utility maximizers and sells only at nonnegative utility; the optimal revenues range over nonnegative prices; exchangeability is invariance under every coordinate permutation. Contributions toward the finite-menu choice lemmas, permutation-invariant integration, order-statistic identity, two-valued DP structure, and the two cases are within scope.

Selected references

• A. N. Elmachtoub and M. L. Hamilton, The Power of Opaque Products in Pricing, Management Science, 2021, doi:10.1287/mnsc.2020.3750. This mission uses the author's 54-page manuscript, pinned locally by SHA-256 ccd5b53ae01d607eca3b7df8549f418f52245b99bb2dfa050b6f5c4878a3cffe; its printed and PDF page numbers agree.

Motivation

Stress testing and data-driven decision making often combine two samples: observations $X_1,\dots,X_n$ of the quantity of interest and additional scenarios $Y_1,\dots,Y_m$ (stress scenarios supplied by a regulator, or unlabeled data). Blanchet and Kang (arXiv:1605.01340v4, 2020; later in Operations Research, 2021) propose to measure how far the empirical distribution of the observations is from the set of distributions that live on the merged sample and satisfy a hypothesis about a parameter, such as "the mean is $\theta$". The distance is an optimal-transport (Wasserstein) cost, and the resulting statistic is the sample out-of-sample (SOS) profile function.

The construction is the transport analogue of empirical likelihood (Owen 1988), whose central result is a Wilks-type theorem (Wilks 1938): $-2\log$ of the likelihood ratio at the true mean is asymptotically $\chi^2$. Empirical likelihood can only reweight the observed points. The SOS function can also move mass to out-of-sample scenarios, which is what makes it usable for stress testing. Confidence regions require the asymptotic law of the statistic at the true parameter. That law is the subject of this mission: the paper's main theorem for means, Theorem 1 (pp. 15–16).

Setting

Let $l\ge1$. Observations $X_1,X_2,\dots$ and scenarios $Y_1,Y_2,\dots$ are random vectors in $\mathbb R^l$, all mutually independent, with Lebesgue densities $f_X$ and $f_Y$. A ratio $\kappa\in[0,\infty)$ fixes the number of scenarios $m=\lfloor\kappa n\rfloor$ used with $n$ observations. The standing assumptions A1)–A4) (p. 14) are: the samples are i.i.d. with these densities; $\mathbb E\|X_1\|_2^2+\mathbb E\|Y_1\|_2^2<\infty$; $f_X,f_Y>0$ everywhere; and, if $l\ge2$, $f_X,f_Y$ are differentiable with bounded gradients.

The merged sample is $\mathcal Z_{n+m}=(Z_1,\dots,Z_{n+m})=(X_1,\dots,X_n,Y_1,\dots,Y_m)$. For $\theta\in\mathbb R^l$ the SOS function (Definition 1, in the linear-programming form (21)) is

$$R_n^W(\theta)=\min\Big\{\sum_{i=1}^n\sum_{j=1}^{n+m}\pi(i,j)\|X_i-Z_j\|_2^2:\ \pi\ge0,\ \sum_j\pi(i,j)=\tfrac1n\ \forall i,\ \sum_j\Big(\sum_i\pi(i,j)\Big)Z_j=\theta\Big\}.$$

It is the least squared transport cost from the empirical measure $\mu_n$ of the $X_i$ to a probability measure supported on $\mathcal Z_{n+m}$ with mean $\theta$. The statistic of interest is $R_n^W(\theta_*)$ at the true mean $\theta_*=\mathbb E X_1$. Write $\mathrm{Var}(X)=\mathbb E[(X_1-\theta_*)(X_1-\theta_*)^{\mathsf T}]$ and $\tilde Z\sim N(0,\mathrm{Var}(X))$.

The limits involve a mixed exponential variable. With the rate $\Lambda(x,\lambda)=[f_X(x+\lambda/2)+\kappa f_Y(x+\lambda/2)]\,\pi^{l/2}/\Gamma(l/2+1)$, the variable $\tau(\lambda)$ satisfies $\mathbb P[\tau(\lambda)>t]=\mathbb E[\exp(-\Lambda(X_1,\lambda)t)]$. From $\tau(0)$ one defines $\tilde g(x)=\mathbb P(\tau(0)\le\|x\|_2^2)$, $\tilde\eta(x)=\mathbb E[\max(1-\tau(0)/\|x\|_2^2,0)]$, the solution $\rho(z)>0$ of $1/\rho=\tilde g(\rho z)$, and $c_0=\mathbb E[\Lambda(X_1,0)]$.

Formalization targets

Goal: Theorem 1 (pp. 15–16)

As $n\to\infty$,

$$l=1:\quad nR_n^W(\theta_*)\Rightarrow\sigma^2\chi_1^2=\text{law of }\|\tilde Z\|_2^2,\qquad \sigma^2=\mathrm{Var}(X);$$ $$l=2:\quad nR_n^W(\theta_*)\Rightarrow\rho(\tilde Z)\big(2-\tilde\eta(\rho(\tilde Z)\tilde Z)\,\rho(\tilde Z)\big)\|\tilde Z\|_2^2;$$ $$l\ge3:\quad n^{1/2+3/(2l+2)}R_n^W(\theta_*)\Rightarrow\frac{2l+2}{l+2}\cdot\frac{\|\tilde Z\|_2^{1+1/(l+1)}}{c_0^{1/(l+1)}} .$$

The goal is the paper's theorem in all three regimes. The $l=2$ case is stated with $\tilde\eta(\rho\tilde Z)$, a correction of the printed $\tilde\eta(\tilde Z)$ (see Formalization scope).

Milestones (in attack order)

1. (21)–(22), pp. 35–36: LP duality, $R_n^W(0)=\max_{\lambda,\gamma\ge0}\{-\lambda^{\mathsf T}\bar X_n-\frac1n\sum_i\gamma_i\}$ subject to $-\lambda^{\mathsf T}X_i-\gamma_i\le\inf_j\{-\lambda^{\mathsf T}Z_j+\|X_i-Z_j\|_2^2\}$.
2. §7.2.1, p. 38: the closest-point bound, $\inf_a\{-\lambda^{\mathsf T}a+\|x-a\|_2^2\}=-\lambda^{\mathsf T}x-\|\lambda\|_2^2/4$, attained at $x+\lambda/2$.
3. (27), p. 41: $R_n^W(0)=\max_\lambda\{-2\lambda^{\mathsf T}\bar X_n-\frac1n\sum_i\max(\|\lambda\|_2^2-D_i(\lambda),0)\}$, with $D_i(\lambda)$ the squared distance from $X_i+\lambda$ to the nearest other point of $\mathcal Z_{n+m}$.
4. Lemma 1, p. 40 (two bounds): $\limsup_n\mathbb E\sup_{t\le T}|n^{-1/2}\sum_i(\cdot-\mathbb E\,\cdot)|<\infty$ for $I(T_i(n,\lambda)\le t)$ and for $\max(t^2-T_i(n,\lambda)^\alpha,0)$, where $T_i(n,\lambda)$ is the first-arrival time of the counting process of other sample points near $X_i+\lambda/2$.
5. Lemma 2, p. 41 (first clause): $\mathbb P[T_i(n,\lambda)\le t]-\mathbb P[\tau(\lambda)\le t]=O(t^{1+1/l}/n^{1/l})$.
6. (31), p. 45: $1/\rho=\tilde g(\rho z)$ has a unique solution for $z\ne0$ ($l=2$).
7. §7.2.5, p. 45: $\max_\zeta\{-2\zeta^{\mathsf T}z-\|\zeta\|_2^2\tilde\eta(\zeta)\}=\rho(z)(2-\tilde\eta(\rho(z)z)\rho(z))\|z\|_2^2$, attained at $-\rho(z)z$.
8. §7.2.6, pp. 47–48: $\max_\zeta\{-2\zeta^{\mathsf T}z-\frac{2C}{l+2}\|\zeta\|_2^{l+2}\}=\frac{2l+2}{l+2}\|z\|_2^{1+1/(l+1)}/C^{1/(l+1)}$.

Significance

Theorem 1 calibrates the SOS method. Its quantiles define the radius of a confidence region for the mean, and through the paper's Theorems 2–3 for estimating equations and for stochastic programs whose uncertainty set must cover out-of-sample scenarios. Unlike empirical likelihood, the limit depends on the dimension and on the densities $f_X,f_Y$: more dispersed scenarios give smaller distances and smaller quantiles (§4.1.1). The theorem also shows that the scaling itself changes with $l$, from $n$ for $l\le2$ to $n^{1/2+3/(2l+2)}$ for $l\ge3$.

The result is proved in the paper; nothing here is an open problem. As far as we know, none of it has been formalized. A formal development adds:

• a checked version of a proof that is informal in places: it passes $o_p(1)$ terms through maxima over unbounded dual variables;
• the correction of the $l=2$ limit;
• reusable pieces: a duality theorem for finite transport problems with a mean constraint, a binomial-to-Poisson estimate for nearest-neighbour counts, and empirical-process bounds for dependent nearest-neighbour statistics.

Difficulty

The obvious approach is a Wilks-type expansion: take the dual of the LP, find the dual multiplier $\lambda_n\approx c\,\bar X_n$ by a quadratic approximation, and read off a $\chi^2$ limit. This works only for $l=1$. In higher dimensions the transport may only move mass to sample points, and the constraint for observation $i$ is controlled by the distance from $X_i+\lambda/2$ to the nearest other sample point. That distance is of order $n^{-1/l}$, so it competes with $\|\lambda\|^2$ at a dimension-dependent scale. The quadratic approximation therefore fails: the dual objective becomes, after rescaling, an average of $\max(\|\zeta\|^2-T_i^{2/l},0)$ over $n$ dependent first-arrival times, which share the same merged sample.

Three steps carry the weight. (a) The dependent array $T_i(n,\lambda)$ needs a uniform $n^{-1/2}$ empirical-process bound (Lemma 1); i.i.d. tools such as the Dvoretzky–Kiefer–Wolfowitz inequality do not apply. (b) A quantitative Poisson approximation (Lemma 2) needs the bounded density gradients. (c) The random concave objective must converge to a deterministic one uniformly enough that its maximiser converges (argmax continuity). Step (c) also needs a multivariate central limit theorem for $\sqrt n\bar X_n$, which Mathlib does not yet provide.

Formalization scope

Representation. Points live in EuclideanSpace ℝ (Fin l). The samples are infinite sequences on a probability space $(\Omega,\mathbb P)$, jointly independent (iIndepFun over $\mathbb N\sqcup\mathbb N$), with laws volume.withDensity. The $n$-th statistic uses the first $n$ observations and the first $\lfloor\kappa n\rfloor$ scenarios; $m=[\kappa n]$ is read as the floor, and $\kappa=0$ is allowed. The SOS function is a real infimum over couplings $\pi:\{1..n\}\times J\to\mathbb R$ of indexed families. Convergence in distribution is Mathlib's TendstoInDistribution, with limit the image of multivariateGaussian 0 Var(X) under an explicit map $\varphi_l$. The goal is a conjunction of three clauses, $l=1$, $l=2$, $l\ge3$.

Conventions and disclosed readings.

• The $l=2$ limit uses $\tilde\eta(\rho(\tilde Z)\tilde Z)$. Theorem 1 prints $\tilde\eta(\tilde Z)$, but the derivation on p. 45 evaluates $G(\zeta,n)=\|\zeta\|^2\tilde\eta(\zeta)+o(1)$ at $\zeta^*_n=-\rho Z_n$, and the two laws differ for every $\tilde Z\ne0$. Milestone 7 isolates this computation.
• When $\theta_*$ is outside the convex hull of the merged sample, the LP is infeasible; $R_n^W$ is then $0$ by convention, where the paper has $+\infty$. The event has probability tending to zero, and no feasibility hypothesis is added to the goal.
• $\rho(0):=0$ (the equation has no solution at $0$, which is a null event for $\tilde Z$), and $\tilde\eta(0)=1$ is never used.
• In (27), after $\lambda\leftarrow2\lambda$, the nearest-point distance is centred at $X_i+\lambda$; the page keeps the symbol $T_i(n,\lambda)$.
• "$Z_j\ne X_i$" in the counting process is a condition on values.
• Lemma 1's $\overline{\lim}$ is a $\limsup$ of a lower Lebesgue integral.
• Lemma 2 is posed at fixed $t$, with the constant allowed to depend on $t$. Its second clause ($O(1/n^l)$) is not posed: it is not supported by the estimate (26) its proof cites. For $l=1$ Lemma 2 adds the density regularity that A4) requires only for $l\ge2$.
• In §7.2.6 the sign of $G$ is read as $+$, and the scaling $n^{1/2+5/(4l+2)}$ printed on p. 48 is read as $n^{1/2+3/(2l+2)}$ (Theorem 1).

Ruled out. The following are not acceptable formalizations: a feasibility hypothesis on every sample; a limit law left as a parameter or quantified existentially; $\rho$, $\tilde g$ or $\tilde\eta$ given by closed forms rather than from the law of $\tau(0)$ and the fixed-point property; the printed $\tilde\eta(\tilde Z)$ presented as proved; Lemma 2 with a constant uniform in $t$; Lemma 1 with a Bochner integral, which would be a default $0$ for a non-integrable supremum.

Infrastructure. A full proof needs: finite LP strong duality (Farkas), absent as a packaged theorem; binomial/Poisson estimates for small-ball counts; a pathwise Burkholder–Davis–Gundy inequality (Beiglböck and Siorpaes 2015) or another route to Lemma 1; dominated-convergence differentiation of $\mathbb E\max(\|\zeta\|^2-\tau,0)$; a multivariate CLT; and argmax-continuity for random concave functions. The LP duality and the multivariate CLT are reusable well beyond this mission. Contributions to any milestone are welcome; milestones 1, 2, 6, 7 and 8 are deterministic and independent of the probabilistic core.

Selected references

• J. Blanchet, Y. Kang, Sample Out-of-Sample Inference Based on Wasserstein Distance, arXiv:1605.01340v4, 2020; Operations Research, 2021. https://arxiv.org/abs/1605.01340
• J. Blanchet, Y. Kang, K. Murthy, Robust Wasserstein Profile Inference and Applications to Machine Learning, Journal of Applied Probability 56(3), 2019. https://arxiv.org/abs/1610.05627
• A. B. Owen, Empirical likelihood ratio confidence intervals for a single functional, Biometrika 75(2), 1988. https://doi.org/10.1093/biomet/75.2.237
• S. S. Wilks, The large-sample distribution of the likelihood ratio for testing composite hypotheses, Annals of Mathematical Statistics 9(1), 1938. https://doi.org/10.1214/aoms/1177732360
• M. Beiglböck, P. Siorpaes, Pathwise versions of the Burkholder–Davis–Gundy inequality, Bernoulli 21(1), 2015. https://arxiv.org/abs/1305.6188