Optimization

Motivation

Maximizing a homogeneous polynomial $p$ over the unit sphere, $p_{\max}=\max_{x\in S^{d-1}}p(x)$, covers the largest stable set of a graph (degree three), the $2\to4$ norm of a matrix (degree four) and the best separable state problem of quantum information. For quadratic $p$ it is an eigenvalue problem; for degree at least three it is NP-hard. The sum-of-squares hierarchy of Parrilo and Lasserre replaces "$\gamma-p\ge0$ on the sphere" by "$\gamma-p$ is a sum of squares of polynomials of degree at most $\ell$ on the sphere", giving upper bounds $p_\ell\ge p_{\max}$ that are computable by a semidefinite program of size $d^{O(\ell)}$ and decrease to $p_{\max}$. How fast they converge decides how large $\ell$ has to be for a given accuracy. Fang–Fawzi, §1–1.1

Timeline:

• 1995. Reznick shows, for $p_{\min}=0$, that $p_\ell/p_{\max}\to1$ at rate $d/\ell$ for $\ell$ large enough. Rez95
• 2012. Doherty and Wehner study the same hierarchy on the hypersphere and obtain the same rate. DW12
• 2019. De Klerk and Laurent prove a rate $O(1/\ell^2)$ for a hierarchy of lower bounds on $p_{\max}$, and ask whether the upper bounds $p_\ell$ converge at the same rate. dKL19
• 2019. Fang and Fawzi answer this: for $\ell\ge C_nd$ the error is $O((d/\ell)^2)$, and the statement holds for symmetric matrix-valued polynomials with constants that do not depend on the matrix size. Fang–Fawzi, Theorems 1–2

Setting

Write $x=(x_1,\dots,x_d)$, $\|x\|^2=\sum_ix_i^2$, and $S^{d-1}=\{x\in\mathbb R^d:\|x\|^2=1\}$. A $k\times k$ matrix polynomial $F$ has a real polynomial in each entry, and $F(x)$ is the real matrix of values. $A\succeq0$ means that the symmetric matrix $A$ is positive semidefinite. A matrix polynomial $G$ is $\ell$-sos on $S^{d-1}$ if there are finitely many $k\times k$ matrix polynomials $U_j$, each entry of total degree at most $\ell$, with

$$G(x)=\sum_jU_j(x)U_j(x)^{\mathsf T}\qquad\text{for all }x\in S^{d-1}.$$

For a scalar polynomial $p$, $p_\ell$ is the least $\gamma$ such that $\gamma-p$ (a $1\times1$ matrix) is $\ell$-sos on $S^{d-1}$, and $p_{\min}$ is the minimum of $p$ on $S^{d-1}$. The level value is $+\infty$ when no such $\gamma$ exists.

The milestones use three further objects. A harmonic decomposition of a homogeneous $f$ of degree $2n$ is $f=\sum_{k=0}^n\|x\|^{2(n-k)}f_{2k}$ with $f_{2k}$ homogeneous of degree $2k$ and $\Delta f_{2k}=0$. $B_{2n}$ is the least constant with $\max_{S^{d-1}}|f_{2k}|\le B_{2n}\max_{S^{d-1}}|f|$ for all such $f$ in all dimensions. The Gegenbauer coefficients $\lambda_i(\phi)$ of a univariate polynomial $\phi$ are its coefficients against the orthogonal polynomials $C_i$ for the weight $(1-t^2)^{(d-3)/2}$ on $[-1,1]$, equation (9). For $q$ of degree at most $\ell$, the kernel error is

$$\rho_{2n}(d,\ell)=\min_{\deg q\le\ell,\ \lambda_0(q^2)=1}\ \sum_{k=1}^n\big|\lambda_{2k}(q^2)^{-1}-1\big|.$$

Formalization targets

Goal: Theorem 2 (p. 3)

For every $n$ there are constants $C_n,C'_n$ depending only on $n$ such that, for all $d,k,\ell$ and every $k\times k$ matrix polynomial $F$, homogeneous of degree $2n$ with $n\le d$, symmetric at every $x$, with $0\preceq F(x)\preceq I$ on $S^{d-1}$:

$$\ell\ge C_nd\ \Longrightarrow\ F+C'_n\Big(\frac d\ell\Big)^2I\ \text{is }\ell\text{-sos on }S^{d-1}.$$

The goal fixes only the shape $(d/\ell)^2$ and the regime $\ell\ge C_nd$, and leaves the constants open.

Milestones

They follow the paper's proof, in attack order:

1. Harmonic projection: Lemma 16 (Reznick's bound on $\Delta^kf$), Proposition 5 ($B_{2n}$ is independent of $d$, with $B_2\le2$, $B_4\le9$), the explicit value (34), and Proposition 17 (matrices, spectral norm).
2. Kernels: the Funk–Hecke formula (8), Remark 1, and the first part of Theorem 6: $F+\frac{B_{2n}}2\sum_k|\lambda_{2k}^{-1}-1|\,I$ is $\ell$-sos for every admissible $q$.
3. The kernel error: $C_i'(1)/C_i(1)=i(i+d-2)/(d-1)$, Proposition 18 (tangent line at $1$), Proposition 8 (spectra of Toeplitz matrices of linear functions), the value of $h'(1)$ and the eigenvalue comparison from the proof of Proposition 7, Proposition 9 ($\rho\le\tilde\rho/(1-\tilde\rho)$), and the second part of Theorem 6:

$$\rho_{2n}(d,\ell)\le C_n\Big(\frac d\ell\Big)^2\qquad(\ell\ge C'_nd).$$

4. Corollary: Theorem 1, $1\le\frac{p_\ell-p_{\min}}{p_{\max}-p_{\min}}\le1+(C_nd/\ell)^2$ for $\ell\ge C_nd$.

Significance

Theorem 2 says how the level must grow with the dimension: $\ell=\Theta(d/\sqrt\varepsilon)$ suffices for relative error $\varepsilon$, where Reznick's analysis needs $\ell=\Theta(d/\varepsilon)$. Theorem 10 of the paper shows that, for $n=1$, the kernel error of this technique really is of order $(d/\ell)^2$. Independence of the matrix size gives certificates for polynomials that are bihomogeneous of degree $(2n,2)$ on $S^{k-1}\times S^{d-1}$. The paper's Theorem 15 uses this, together with the DPS duality of the companion mission, to bound the convergence of the DPS hierarchy for separability. Fang–Fawzi, pp. 3, 10, 14

The theorem is proved in the 2019 preprint and was published in Mathematical Programming in 2021. No machine-checked proof of it or of its ingredients is known. Proving it formally takes reusable infrastructure: degree-bounded matrix SOS on the sphere, harmonic decomposition of homogeneous polynomials, Gegenbauer polynomials with their coefficients and the Funk–Hecke formula, and spectra of Jacobi matrices of orthogonal polynomials. The milestones also correct the printed text, as listed under Formalization scope.

Difficulty

Positive semidefiniteness of $F+\delta I$ at each point of the sphere does not give a factorization with factors of prescribed degree, and Reznick's kernel $\langle x,y\rangle^{2\ell}$ only reaches error $d/\ell$. Two estimates must be uniform at once. First, harmonic projection of a degree-$2n$ form must be bounded in sup norm independently of $d$; the $L^2$ bound is easy, and the sup-norm bound is the content of Proposition 5. Second, the kernel error $\rho_{2n}(d,\ell)$ must be bounded throughout the regime $\ell\ge C_nd$, which comes down to the location of the largest zero of a Gegenbauer polynomial. The printed bounds on that zero and on $\lambda_{\max}$ in Proposition 7 are false in small dimensions, so the paper's explicit constants cannot be relied on.

Formalization scope

• Objects. $\mathbb R^d$ is Fin d → ℝ (0-based coordinates), and $S^{d-1}$ is the equation $\sum_ix_i^2=1$, not the sup-norm sphere. Matrix polynomials are matrices over MvPolynomial (Fin d) ℝ, evaluated entrywise, and homogeneity is entrywise.
• $\ell$-sos. A finite family of $k\times k$ factors, every entry of total degree at most $\ell$, with equality on the sphere only. Without the degree bound the level disappears; with equality on all of $\mathbb R^d$ Theorem 2 becomes false. Neither change is a faithful reading.
• Constants. In the goal the constants are chosen before $d$, $k$, $\ell$ and $F$. No assumption $d\ge2$ is added: the cases $d=0,1$ are true and elementary.
• Standing assumption $d\ge2$. Every milestone that uses the Gegenbauer objects assumes it, as §2–3 do: the weight $(1-t^2)^{(d-3)/2}$, $\omega_{d-1}/\omega_d$ and the divisions by $d-1$ need it. Gegenbauer polynomials are normalized by $C_i(1)$ and defined by their three-term recurrence. $\sigma$ is the normalized surface measure built from Mathlib's Measure.toSphere.
• $B_{2n}$. It is not defined (it would be a real infimum). Statements quantify over every constant $B$ with the defining property, and $B_{2n}$ is one of them.
• $\rho_{2n}$. It takes values in $[0,\infty]$, with $|\lambda^{-1}-1|=\infty$ at $\lambda=0$ and $\infty$ on an empty feasible set. Its sum runs over $k=1,\dots,n$, following (12), (13) and (16); (10) prints $2n$, a slip. Its minimum is over $\deg q\le\ell$, as in (13). The first part of Theorem 6 is posed per polynomial $q$, which is what (12) proves and implies the printed form.
• Other conventions. Proposition 17's spectral norm is written as $\max_{\|y\|=1}|y^{\mathsf T}Ay|$, and homogeneity of $F$ is explicit there. Theorem 1 is stated cross-multiplied, so that it is meaningful when $p$ is constant on the sphere. Its level value is extended real to record infeasibility; the theorem asserts a finite attained value and a degree-bounded SOS certificate.
• Not posed. Proposition 7 ($\lambda_{\max}(\mathcal T[h])\ge1-\frac{7n}{12}\frac{d^2}{\ell^2}$) fails, for example, at $d=2$, $n=1$, $\ell=10$. The zero bound it quotes and the explicit constants at the end of p. 9 are not posed either; the true first inequality of its proof is.

Proofs of any milestone are welcome. So are reusable developments of Gegenbauer polynomials, spherical harmonics, the Funk–Hecke formula, Jacobi matrices, and Carathéodory-type finite quadratures that turn an integral of squares into a finite sum of squares.

Selected references

• K. Fang, H. Fawzi, The sum-of-squares hierarchy on the sphere, and applications in quantum information theory, arXiv preprint, 2019. https://arxiv.org/abs/1908.05155v1
• B. Reznick, Uniform denominators in Hilbert's seventeenth problem, Mathematische Zeitschrift 220(1), 75–97, 1995. https://doi.org/10.1007/BF02572604
• A. C. Doherty, S. Wehner, Convergence of SDP hierarchies for polynomial optimization on the hypersphere, arXiv preprint, 2012. https://arxiv.org/abs/1210.5048
• E. de Klerk, M. Laurent, Convergence analysis of a Lasserre hierarchy of upper bounds for polynomial minimization on the sphere, arXiv preprint, 2019. https://arxiv.org/abs/1904.08828
• J. B. Lasserre, Global optimization with polynomials and the problem of moments, SIAM Journal on Optimization 11(3), 796–817, 2001. https://doi.org/10.1137/S1052623400366802

Motivation

Deciding whether a bipartite quantum state is entangled is a basic computational problem of quantum information theory, and it is NP-hard in general (Gurvits 2003). The most widely used family of tests is the DPS hierarchy of Doherty, Parrilo and Spedalieri (DPS 2002, DPS 2004): a sequence of semidefinite programs, indexed by an integer level $\ell\ge1$, whose feasible sets shrink to the set of separable states. On the dual side, a matrix $M$ that is nonnegative on separable states is an entanglement witness, and certifying such witnesses is the problem of certifying nonnegativity of a biquadratic Hermitian form, a classical question in real algebraic geometry.

That the DPS hierarchy is, dually, a sum-of-squares hierarchy for these forms has been used repeatedly in the literature, but, as Fang and Fawzi note (arXiv:1908.05155v1, p. 4), without a formal and complete proof. Their Theorem 12 gives one. They then combine it with their sum-of-squares convergence rate on the sphere (Theorem 2 of the same paper) to recover the $O(d_B^2/\ell^2)$ convergence rate of Navascués, Owari and Plenio 2009 for the DPS hierarchy.

Timeline:

• 2002–2004: Doherty, Parrilo, Spedalieri introduce the hierarchy and prove completeness.
• 2009: Navascués, Owari, Plenio prove $h_{\mathrm{DPS}_\ell}\le(1+O(d_B^2/\ell^2))h_{\mathrm{Sep}}$ by a quantum argument.
• 2019: Fang and Fawzi prove the duality (Theorem 12) and recover the 2009 rate from sums of squares (Theorem 15).

Setting

Let $\mathcal H_A=\mathbb C^{d_A}$ and $\mathcal H_B=\mathbb C^{d_B}$. A matrix $M$ on $\mathcal H_A\otimes\mathcal H_B$ has entries $M_{ij,kl}$ (row $(i,j)$, column $(k,l)$); $\mathrm{Herm}(d_Ad_B)$ is the space of Hermitian ones.

• The separable cone $\mathcal{SEP}$ is the set of finite conic combinations $\sum_ip_i(x_ix_i^\dagger)\otimes(y_iy_i^\dagger)$, $p_i\ge0$.
• Fix $\ell\ge1$ and $\ell$ copies $B_1,\dots,B_\ell$ of $\mathcal H_B$. The DPS cone $\mathcal{DPS}_\ell$ is the set of positive semidefinite $\rho$ on $\mathcal H_A\otimes\mathcal H_B$ that have a positive semidefinite extension $\rho_{AB[\ell]}$ on $\mathcal H_A\otimes\mathcal H_B^{\otimes\ell}$ with three properties: tracing out $B_2,\dots,B_\ell$ returns $\rho$; $(I\otimes\Pi_\ell)\rho_{AB[\ell]}(I\otimes\Pi_\ell)=\rho_{AB[\ell]}$, where $\Pi_\ell=\frac1{\ell!}\sum_{\sigma\in\mathfrak S_\ell}P_\sigma$ projects onto the symmetric subspace of $\mathcal H_B^{\otimes\ell}$; and every partial transpose $\rho_{AB[\ell]}^{\mathsf T_{B[s]}}$ on $B_1,\dots,B_s$, $s=1,\dots,\ell$, is positive semidefinite.
• The EXT cone $\mathcal{EXT}_\ell$ is the same without the partial-transpose conditions.
• For a set $K$, the dual cone is $K^*=\{M\in\mathrm{Herm}(d_Ad_B):\mathrm{Tr}[M\rho]\ge0\ \forall\rho\in K\}$.
• To $M$ is attached the Hermitian polynomial $p_M(x,\bar x,y,\bar y)=\sum_{ijkl}M_{ij,kl}x_i\bar x_ky_j\bar y_l$.
• A real-valued polynomial in $(x,\bar x,y,\bar y)$ is rsos if it is a finite sum of squares of Hermitian polynomials, equivalently of real polynomials in the real and imaginary parts of $x,y$; it is csos if it is a finite sum $\sum_i|q_i(x,y)|^2$ with $q_i$ holomorphic polynomials.

Formalization targets

Goal: Theorem 12

$$\mathcal{SEP}^*=\{M: p_M\ge0\},\qquad \mathcal{DPS}_\ell^*=\{M:\|y\|^{2(\ell-1)}p_M\ \text{is rsos}\},\qquad \mathcal{EXT}_\ell^*=\{M:\|y\|^{2(\ell-1)}p_M\ \text{is csos}\},$$

for all $d_A,d_B$ and all $\ell\ge1$, with $M$ ranging over $\mathrm{Herm}(d_Ad_B)$.

Milestones

1. Theorem 12 (i), the first equality.
2. The identity (37): $(x\otimes\bar y^{\otimes s}\otimes y^{\otimes\ell-s})^\dagger W(\cdot)=(x\otimes y^{\otimes\ell})^\dagger W^{\mathsf T_{B[s]}}(x\otimes y^{\otimes\ell})$.
3. Lemma 19: $\|y\|^{2(\ell-1)}p_M$ is rsos iff it is $\sum_{s=0}^\ell(x\otimes\bar y^{\otimes s}\otimes y^{\otimes\ell-s})^\dagger W_s(x\otimes\bar y^{\otimes s}\otimes y^{\otimes\ell-s})$ with $W_s\succeq0$.
4. (39): $(x\otimes y^{\otimes\ell})^\dagger(Y-\Pi_\ell Y\Pi_\ell)(x\otimes y^{\otimes\ell})=0$.
5. The dual SDP description: $\mathcal{DPS}_\ell^*=\{M: M\otimes I_{B[2:\ell]}=(Y-\Pi_\ell Y\Pi_\ell)+\sum_{s=0}^\ell W_s^{\mathsf T_{B[s]}},\ Y\in\mathrm{Herm},\ W_s\succeq0\}$.
6. Lemma 20: $\|y\|^{2(\ell-1)}p_M$ is csos iff it is $(x\otimes y^{\otimes\ell})^\dagger W(x\otimes y^{\otimes\ell})$ with $W\succeq0$.
7. Theorem 15: there are absolute $C,C'>0$ with $h_{\mathrm{Sep}}(M)\le h_{\mathrm{DPS}_\ell}(M)\le(1+Cd_B^2/\ell^2)h_{\mathrm{Sep}}(M)$ for $\ell\ge C'd_B$, whenever $(x\otimes y)^\dagger M(x\otimes y)\ge0$.

Significance

Theorem 12 makes the DPS hierarchy and the sum-of-squares hierarchy for biquadratic forms interchangeable. A convergence bound for one is a convergence bound for the other: the paper uses this to derive the DPS rate (Theorem 15) from a rate for sums of squares on the sphere, and conversely quantum de Finetti arguments give sum-of-squares bounds. Part (iii) separates the two notions of Hermitian sum of squares: dropping the partial transposes corresponds exactly to passing from real to complex sums of squares. This explains, for example, why $(z+\bar z)^2$ (rsos but not csos) behaves differently in the two hierarchies.

The results are proved on paper; none is formalized. The mission produces a machine-checked statement and proof of the duality, together with the matrix-analytic infrastructure behind it: partial traces and partial transposes on $\mathcal H_A\otimes\mathcal H_B^{\otimes\ell}$, the symmetric projector, conic duality for semidefinite cones, and the passage between Gram matrices and sums of squares. Theorem 15 additionally depends on the sphere rate of the companion mission (Theorem 6 there) and on the unproved Lemma 13 and display (26) of the paper.

Difficulty

The inclusion of each sum-of-squares cone in the corresponding dual cone is a direct computation. The reverse inclusions are harder: a certificate involving arbitrary Hermitian polynomials must yield positive semidefinite matrices indexed by the prescribed tensor products, even though its square terms can mix different patterns of complex conjugation. Likewise, weak semidefinite duality alone does not show that every element of $\mathcal{DPS}_\ell^*$ has the displayed finite certificate; limits of certificates may require a separate closedness argument. The symmetric-subspace condition adds another constraint because an extension must be supported on that subspace, not merely invariant under permutations.

Formalization scope

• Indices: $\mathcal H_A\otimes\mathcal H_B$ is Fin dA × Fin dB (Mathlib's Kronecker convention); $\mathcal H_A\otimes\mathcal H_B^{\otimes\ell}$ is Fin dA × (Fin ℓ → Fin dB).
• The level is written $\ell=m+1$ with $m\in\mathbb N$, so $\ell\ge1$ is built in and $\|y\|^{2(\ell-1)}=\|y\|^{2m}$; $B_1,\dots,B_\ell$ are coordinates $0,\dots,m$.
• Matrices are complex; positive semidefiniteness is Mathlib's Matrix.PosSemidef (which includes Hermitian). Dual cones are subsets of $\mathrm{Herm}(d_Ad_B)$ with the pairing $\operatorname{Re}\mathrm{Tr}[M\rho]$.
• $p_M$ is (25) literally; "$p_M\ge0$" is $\operatorname{Re}p_M\ge0$.
• rsos is a finite sum of squares of real polynomials (MvPolynomial over $\mathbb R$) in the real and imaginary parts of $(x,y)$; csos is a finite sum of $|q_i|^2$ with $q_i$ complex polynomials in $(x,y)$ only. Swapping the two, or allowing complex $g_i$ in rsos, would change parts (ii) and (iii).
• Condition (21) is stated literally with the explicit projector; "commutes with all permutations" would be weaker and is not used.
• In Theorem 15, $h_{\mathrm{Sep}}$ and $h_{\mathrm{DPS}_\ell}$ are real suprema over trace-one elements, $d_A,d_B\ge1$ is assumed so the sets are nonempty, and $C,C'$ are quantified before all dimensions.

No trivializing reading is available: the cones are defined by their page conditions, the dual cones keep the Hermitian constraint, and no degree bound or extra hypothesis is placed on the sums of squares. Welcome contributions include a general library for partial traces and transposes of multipartite matrices, the spanning property of $\{y^{\otimes\ell}\}$ in the symmetric subspace, and Gram-matrix characterizations of sums of squares of polynomials; all are reusable well beyond this mission.

Selected references

• K. Fang, H. Fawzi, The sum-of-squares hierarchy on the sphere, and applications in quantum information theory, arXiv preprint, 2019. https://arxiv.org/abs/1908.05155v1
• A. C. Doherty, P. A. Parrilo, F. M. Spedalieri, Distinguishing separable and entangled states, Physical Review Letters 88, 187904, 2002. https://arxiv.org/abs/quant-ph/0112007
• A. C. Doherty, P. A. Parrilo, F. M. Spedalieri, Complete family of separability criteria, Physical Review A 69, 022308, 2004. https://arxiv.org/abs/quant-ph/0308032
• M. Navascués, M. Owari, M. B. Plenio, Power of symmetric extensions for entanglement detection, Physical Review A 80, 052306, 2009. https://arxiv.org/abs/0906.2731
• L. Gurvits, Classical deterministic complexity of Edmonds' problem and quantum entanglement, STOC 2003. https://doi.org/10.1145/780542.780545

Motivation

A decision maker who must choose $x$ to minimize an expected cost $\mathbb E_F[c(x;\xi)]$ rarely knows the distribution $F$ of the uncertain parameter $\xi$; what is available is a sample $\xi^1,\dots,\xi^N$. Sample average approximation (SAA) replaces $F$ by the empirical distribution. Data-driven distributionally robust optimization (DRO) instead minimizes the worst case of the expected cost over a set $\mathcal F_N$ of distributions built from the data, which protects against the error of the empirical distribution at small $N$. Many such sets have been proposed: moment sets (Delage and Ye, 2010), $\phi$-divergence balls (Ben-Tal et al., 2013), Wasserstein balls (Mohajerin Esfahani and Kuhn, 2018).

Bertsimas, Gupta and Kallus (arXiv:1408.4445v3; Mathematical Programming, 2018, doi:10.1007/s10107-017-1174-z) observe that each such set can be read as the confidence region of a statistical goodness-of-fit (GoF) test, and call the resulting method Robust SAA. A basic question for any such method is whether, as $N\to\infty$, its objective, optimal value and optimal solutions converge to those of the full-information problem. The paper answers it for all data-driven DROs at once, with a single property of the test.

Setting

The support $\Xi\subseteq\mathbb R^d$ of $\xi$ is closed, and $\mathcal P(\Xi)$ is the set of Borel probability distributions on $\Xi$ with the topology of weak convergence. The data $\xi^1,\xi^2,\dots$ are i.i.d. from an unknown $F\in\mathcal P(\Xi)$. A data-driven uncertainty set (DUS) map assigns to each sample $(\xi^1,\dots,\xi^N)$ a set $\mathcal F_N\subseteq\mathcal P(\Xi)$; it is the confidence region of the test that rejects a hypothesis $F_0$ exactly when $F_0\notin\mathcal F_N$. Decisions lie in a closed set $X\subseteq\mathbb R^{d_x}$, the cost is $c(x;\xi)$, and the robust objective is the worst-case expectation

$$\mathcal C(x;\mathcal F_N)=\sup_{F_0\in\mathcal F_N}\mathbb E_{F_0}[c(x;\xi)] .$$

A test is uniformly consistent (Definition 3) if, for every data-generating $F$, almost surely every sequence $F_N$ that does not converge weakly to $F$ lies outside $\mathcal F_N$ for infinitely many $N$. The admissible instances are those satisfying three assumptions: (1) $c(\cdot;\xi)$ is equicontinuous in $x$ uniformly over $\xi$; (2) $X$ is bounded, or $c$ is coercive in $x$ uniformly over a set $D$ of positive $F$-probability and bounded below off $D$; (3) $\Xi$ is bounded, or there is a growth function $\phi\ge0$ with $c(x;\xi)=O(\phi(\xi))$ whose expectation the DUS tracks: $\sup_{F_0\in\mathcal F_N}|\mathbb E_{F_0}\phi-\frac1N\sum_i\phi(\xi^i)|\to0$ almost surely. The convergence conditions are (18) $\mathcal C(x;\mathcal F_N)\to\mathbb E_F[c(x;\xi)]$ uniformly on compact subsets of $X$; (19) convergence of optimal values; and (20) every sequence of robust minimizers has a limit point, and all its limit points are true minimizers.

Formalization targets

Goal: Theorem 2

For a DUS map with nonempty sets,

$$\mathcal F_N\ \text{is uniformly consistent}\iff\Big[\forall F,X,c\ \text{satisfying Assumptions 1–3}:\ (18),(19),(20)\ \text{hold a.s.}\Big].$$

The statement carries no rates and no constants; it is a characterization, so it does not depend on any particular test.

Milestones

1. Proposition 8: under uniform consistency and Assumptions 1 and 3, almost surely $\mathbb E_{F_N}[c(x;\xi)]\to\mathbb E_F[c(x;\xi)]$ for every $x\in X$ and every sequence $F_N\in\mathcal F_N$.
2. Proposition 9: deterministically, convergence of $\mathcal C(x_N;\mathcal F_N)$ along every convergent $x_N\to x$ implies (18).
3. Theorem 2, "only if" side: uniform consistency implies (18)–(20) a.s. for every admissible instance.
4. Theorem 2, "if" side: if the test is not uniformly consistent, some admissible instance fails (18)–(20) with positive probability.
5. Theorem 3: if $\mathcal F_N$ always contains the empirical distribution and the test is $c$-consistent (Definition 5, consistency with respect to the expected costs only), then (18)–(20) hold a.s.
6. Proposition 4 (first sentence): a uniformly consistent test is consistent in the classical sense, $\mathbb P(F_0\notin\mathcal F_N)\to1$ for each $F_0\neq F$.

Significance

The result. Theorem 2 reduces the asymptotic analysis of a data-driven DRO to a property of a statistical test, which can be checked once per test rather than once per optimization model. The paper uses it to classify DUSs: the $\chi^2$ and G-tests on a finite support and the Kolmogorov–Smirnov, Kuiper, Cramér–von Mises, Watson and Anderson–Darling tests on the line are uniformly consistent (Theorems 4–5, separate missions of this series), while the test of marginals is not even consistent and so cannot give convergence for every cost. The necessity direction makes the property sharp: a weaker test always admits a well-behaved cost on which the DRO fails to converge. Theorem 3 explains the remaining cases where a DRO converges for one given cost.

Formalizing it. The result is proved in the paper (§10.5), but its proof leans on several standard facts used without detail: the portmanteau theorem, uniform integrability arguments from Billingsley's Convergence of Probability Measures, the Lévy continuity theorem with the Cramér–Wold device, and coercivity arguments carried over from the paper's Theorem 1. A machine-checked version would fix exactly which regularity of the cost these steps need; three such conditions are stated explicitly here (see the scope section). No part of the result is formalized elsewhere to our knowledge; the platform has no notion of a data-driven uncertainty set or of uniform consistency.

Difficulty

Uniform consistency is a statement about weak convergence, while (18)–(20) are statements about expectations of an unbounded, $x$-dependent cost under the members of $\mathcal F_N$. Weak convergence controls expectations only of bounded continuous functions, so the "only if" side must recover convergence of $\mathbb E_{F_N}[c(x;\xi)]$ from Assumption 3, which requires uniform integrability, and then upgrade pointwise convergence to uniform convergence on compacts and to convergence of minimizers when $X$ is unbounded. The tempting route through a single limiting minimization problem fails: the sets $\mathcal F_N$ change with the sample, the worst case is a supremum over infinitely many distributions, and the minimizers of $\mathcal C(\cdot;\mathcal F_N)$ could escape to infinity unless coercivity on $D$ transfers to every member of $\mathcal F_N$. The "if" side needs, from the mere failure of uniform consistency, a single admissible cost whose worst-case objective detects every failure of weak convergence.

Formalization scope

Points are EuclideanSpace ℝ (Fin d), distributions are ProbabilityMeasure ↥Ξ (whose topology is weak convergence), and the data live on the canonical product space $\Xi^{\mathbb N}$ with the product law, 0-indexed. "Almost surely" is ∀ᵐ, and in Definition 3 one null set serves every sequence $F_N$. An expectation over a member of $\mathcal F_N$ is $+\infty$ when the integrand is not integrable, never Lean's default $0$. Minima in (19)–(20) are infima in the extended reals, so the empty and unattained cases need no special treatment; (20) applies to sequences that are minimizers for all large $N$.

Four hypotheses are added to the page, each used by the paper's own proof: every $\mathcal F_N$ is nonempty (otherwise the worst case is $-\infty$ and uniform consistency is vacuous); $c(x;\cdot)$ is continuous on $\Xi$; the set $D$ of Assumption 2b is open; the growth function $\phi$ of Assumption 3b is continuous, with $\mathbb E_F\phi<\infty$ as fixed on p. 10 of the paper. Theorem 3 additionally assumes Assumption 2, which its proof uses. Proposition 4 assumes the rejection events are measurable. A formalization in which the worst case uses the raw Bochner integral, the supremum ranges over a possibly empty set, or (20) requires minimizers at $N=0$ would make the statements false or vacuous, and is ruled out.

A full development needs weak convergence and the portmanteau theorem (in Mathlib), uniform integrability and its relation to convergence of means under weak convergence, the strong law of large numbers for the growth function and the empirical measure, the Lévy continuity theorem in several dimensions (in Mathlib, via characteristic functions), and a countable convergence-determining class of bounded continuous functions. The uniform-integrability step and the path characterization of local uniform convergence (Proposition 9) are reusable beyond this mission. Contributions to any milestone are welcome; Proposition 9 is self-contained and deterministic.

Selected references

• D. Bertsimas, V. Gupta, N. Kallus, Robust Sample Average Approximation, arXiv:1408.4445v3, 2016; Mathematical Programming 171 (2018). https://arxiv.org/abs/1408.4445v3, https://doi.org/10.1007/s10107-017-1174-z
• P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999. https://doi.org/10.1002/9780470316962
• E. Delage, Y. Ye, Distributionally Robust Optimization Under Moment Uncertainty with Application to Data-Driven Problems, Operations Research 58(3), 2010. https://doi.org/10.1287/opre.1090.0741
• A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2), 2013. https://doi.org/10.1287/mnsc.1120.1641
• P. Mohajerin Esfahani, D. Kuhn, Data-Driven Distributionally Robust Optimization Using the Wasserstein Metric, Mathematical Programming 171, 2018. https://doi.org/10.1007/s10107-017-1172-1

Motivation

The newsvendor problem is the basic single-period inventory decision: a retailer orders $q\ge0$ units at unit cost $c$ before a random demand $\tilde d$ is observed, sells at unit price $p>c$, and loses unsold units. When the demand law is known, the optimal order is a quantile of that law. In practice the law is rarely known, and a distributionally robust newsvendor instead hedges against the worst law in an ambiguity set of laws consistent with partial information.

Scarf (1958; reference [42] of arXiv:1806.05379) solved the case where only the mean and the variance of demand are known, and observed that for a range of small profit margins the robust newsvendor orders nothing. Demand data in retail and spare-parts settings are often heavy tailed: Pareto fits with exponent close to $1$ have been reported, so a finite mean is plausible while a finite variance is not. Das, Dhara and Natarajan (arXiv:1806.05379) therefore replace the variance by an $\alpha$-th moment for an arbitrary real $\alpha>1$. This mission formalizes their result that the zero-order phenomenon survives for every such $\alpha$.

Setting

Write the critical ratio as $\eta=1-c/p\in[0,1)$. A demand law is a probability measure $F$ on $[0,\infty)$. Fix a real $\alpha>1$ and two moments $m_1,m_\alpha$ with

$$m_\alpha>m_1^\alpha>0 .$$

The ambiguity set is

$$\mathcal F_{1,\alpha}=\Big\{F:\ \int_0^\infty w\,dF(w)=m_1,\ \int_0^\infty w^\alpha\,dF(w)=m_\alpha\Big\},$$

the laws on $[0,\infty)$ with mean $m_1$ and $\alpha$-th moment $m_\alpha$. The worst-case expected shortage is

$$\Pi_{1,\alpha}(q)=\sup_{F\in\mathcal F_{1,\alpha}}\mathbb E_F[\tilde d-q]^+ ,$$

and the robust newsvendor problem (3.2) is

$$\min_{q\ge0}\ \big((1-\eta)q+\Pi_{1,\alpha}(q)\big).$$

An optimal order quantity is a minimizer $q^*\ge0$ of this objective. Two thresholds appear:

$$\eta_0=1-\Big(\frac{m_1^\alpha}{m_\alpha}\Big)^{1/(\alpha-1)},\qquad q_0=\frac{\alpha-1}{\alpha}\Big(\frac{m_\alpha}{m_1}\Big)^{1/(\alpha-1)} .$$

In Lean these are ambiguitySet, worstCase, robustCost, eta0, q0 and IsOptimalOrder in the namespace HeavyTailNV.ZeroOrder.

Formalization targets

Goal: Proposition 3.2 (p. 13)

$\eta_0\in(0,1)$, and

• for every $\eta\in[0,\eta_0)$ the set of optimal order quantities is exactly $\{0\}$;
• for every $\eta\in(\eta_0,1)$ an optimal order quantity exists, and every optimal order quantity $q^*$ satisfies $q^*>0$ and

$$q^*\ge q_0 ;$$

• for $\eta=\eta_0$ every $q\in[0,q_0]$ is optimal.

Milestones

1. Proposition 3.1 (p. 12): for $0\le q\le q_0$,

$$\Pi_{1,\alpha}(q)=m_1-q\Big(\frac{m_1^\alpha}{m_\alpha}\Big)^{1/(\alpha-1)},$$

and the two-point law with mass $(m_1^\alpha/m_\alpha)^{1/(\alpha-1)}$ at $(m_\alpha/m_1)^{1/(\alpha-1)}$ and the rest at $0$ lies in $\mathcal F_{1,\alpha}$ and attains the supremum. 2. Properties of $\Pi$ (§2.1, p. 6): $\Pi_{1,\alpha}$ is non-increasing and convex, $\Pi_{1,\alpha}(q)+q=m_1$ for $q\le0$, and $\Pi_{1,\alpha}(q)\to0$ as $q\to\infty$. 3. Display (3.10) (p. 14): for $\eta\in[0,1)$ and $0\le q\le q_0$,

$$(1-\eta)q+\Pi_{1,\alpha}(q)=m_1-q(\eta-\eta_0).$$

Significance

Proposition 3.2 shows that for every finite moment order $\alpha>1$, however high, there is a nonempty interval $[0,\eta_0)$ of critical ratios in which the robust newsvendor orders nothing, and it gives the threshold $\eta_0$ and the minimum positive order $q_0$ in closed form. For $\alpha=2$ it recovers Scarf's zero-order region. The worst-case law associated with $\Pi_{1,\alpha}$ therefore carries a positive mass at zero demand, which is the low-service-level counterpart of the paper's heavy-tail result for high critical ratios (the companion mission of this series).

The results are proved in the paper: the proof of Proposition 3.1 follows the statement on pp. 12–13 and the proof of Proposition 3.2 is on p. 14. None of them has a machine-checked proof. Formalizing them requires a usable treatment of moment-constrained suprema over probability measures on $[0,\infty)$, of the stop-loss transform $q\mapsto\mathbb E[\tilde d-q]^+$, and of minimizers of convex functions on a half-line. These pieces recur across robust inventory and pricing models.

Difficulty

The closed form of Proposition 3.1 is the central step. The lower bound is a computation with a two-point law. The matching upper bound has to hold against every law in $\mathcal F_{1,\alpha}$, including laws with unbounded support and non-integer $\alpha$. The paper obtains it from a dual certificate for the moment problem (3.3)–(3.4), and weak duality for this semi-infinite problem is not available off the shelf. The closed form also holds only on $[0,q_0]$. To conclude anything about minimizers on all of $[0,\infty)$, where no closed form is known for general $\alpha$ (the dual leads to equations $aw^\alpha+bw+c=0$, p. 11), one needs convexity of $\Pi_{1,\alpha}$ on the whole line. Inspecting the objective on $[0,q_0]$ alone does not determine the global minimizers.

Formalization scope

• Demand laws are Measure ℝ with IsProbabilityMeasure F and F (Set.Iio 0) = 0. Moments are Bochner integrals, and the set requires Integrable (fun w => w) F and Integrable (fun w => w ^ α) F (real rpow), so that the moment equalities are genuine.
• $\Pi_{1,\alpha}$ is a real sSup. Under the standing hypotheses $\alpha>1$, $m_1>0$, $m_\alpha>m_1^\alpha$ the set is nonempty (it contains the two-point law of Proposition 3.1) and the expectations are bounded above by $m_1+|q|$, so the value is not Lean's default for an empty or unbounded set. Every statement carries these standing hypotheses of (3.1); no other hypothesis is added except the range $\eta\in[0,1)$ in (3.10), which is the paper's standing range of the critical ratio.
• Optimality is minimization over $q\in[0,\infty)$, as in (3.2), not over $\mathbb R$. Over $\mathbb R$ the objective equals $m_1-\eta q$ for $q\le0$, and part (a) would fail at $\eta=0$.
• Trivializing readings are ruled out. Part (a) asserts that $\{0\}$ is the whole set of minimizers, not only that $0$ is a minimizer. Part (b) asserts that a minimizer exists, so its lower bound is not vacuous. Dropping the support constraint, the normalization, or the integrability clauses would change the problem or let junk integrals satisfy the moment constraints.
• The unit cost and price never appear; everything is stated in $\eta$.
• The ambiguity set, worst-case value and objective come from the shared HeavyTailNV.Tail.Model. This mission defines the thresholds, optimality predicate and two-point law in HeavyTailNV.ZeroOrder.Model. Contributions to the general moment-problem duality used by Proposition 3.1 are welcome and reusable well beyond this mission.

Selected references

• B. Das, A. Dhara and K. Natarajan, On the heavy-tail behavior of the distributionally robust newsvendor, Operations Research 69(4), 2021; preprint arXiv:1806.05379v2, 2019. https://arxiv.org/abs/1806.05379
• H. Scarf, A min–max solution of an inventory problem, in K. Arrow, S. Karlin and H. Scarf (eds.), Studies in the Mathematical Theory of Inventory and Production, pp. 201–209, Stanford University Press, 1958 (no DOI; reference [42] of https://arxiv.org/abs/1806.05379).

Motivation

A newsvendor chooses an order quantity before seeing demand. Unsold units have no salvage value, while demand above the order quantity cannot be filled. If the demand law is unknown but a few moments are known, the decision maker may minimize cost against the worst distribution consistent with those moments. Das, Dhara and Natarajan study this distributionally robust problem when the known moments are the first and an arbitrary real moment of order $\alpha>1$ Das, Dhara and Natarajan, 2019. The high-demand tail matters especially when the cost ratio favors large orders. The mission asks what tail behavior is implicitly selected by the robust objective, even though each admissible distribution has a finite $\alpha$th moment.

The two-moment case $\alpha=2$ goes back to Scarf's newsvendor bound. The paper extends the model to noninteger $\alpha$ and gives lower and upper shortage bounds before proving its tail result. Its preprint is the pinned source for every statement here; the proof of each numbered result follows that result in the paper Das, Dhara and Natarajan, 2019, §§1, 3–4.

Setting

Let $q\ge0$ be the order quantity and let $\tilde d\ge0$ be random demand. The expected shortage under a demand law $F$ is $\mathbb E_F[(\tilde d-q)^+]$, where $x^+=\max(x,0)$. Fix $\alpha>1$, a positive mean $m_1$, and a moment $m_\alpha>m_1^\alpha$. The moment ambiguity set $\mathcal F_{1,\alpha}$ contains all probability laws supported on $[0,\infty)$ whose first moment is $m_1$ and whose finite $\alpha$th moment is $m_\alpha$. Its worst-case expected shortage is

$$\Pi_{1,\alpha}(q)=\sup_{F\in\mathcal F_{1,\alpha}}\mathbb E_F[(\tilde d-q)^+].$$

For a critical ratio $\eta\in[0,1)$, the robust newsvendor minimizes $(1-\eta)q+\Pi_{1,\alpha}(q)$ over $q\ge0$. This mission centers on $\Pi_{1,\alpha}$; the optimal-order threshold is treated in the companion mission. The ambiguity set and objective are the paper's (3.1)–(3.3) Das, Dhara and Natarajan, 2019, pp. 10–11.

A positive function $u$ is regularly varying with index $\rho$ if $u(tx)/u(x)\to t^\rho$ as $x\to\infty$ for every $t>0$. The notation is $u\in RV_\rho$. For a probability law $F$, its survival tail is $\bar F(x)=P_F(\tilde d>x)$; $\bar F\in RV_{-\alpha}$ means a tail parameter $\alpha$ Das, Dhara and Natarajan, 2019, §4.1, p. 26.

Formalization targets

Worst-case shortage

The first target is Theorem 4.3(a):

$$\Pi_{1,\alpha}\in RV_{-(\alpha-1)}.$$

It covers every $\alpha>1$, including $\alpha=2$. Scarf's piecewise formula (1.3), Proposition 3.3, and both parts of Proposition 3.4 supply the paper's cited bounds. Each upper bound retains its strict quantity threshold and its printed denominator Das, Dhara and Natarajan, 2019, pp. 3, 15, 19, 28.

One representative demand law

The full goal, Theorem 4.3, also states that a nonnegative probability law $F^*$ exists outside $\mathcal F_{1,\alpha}$ with

$$\mathbb E_{F^*}[(\tilde d^*-q)^+]=\Pi_{1,\alpha}(q)\quad(q\ge0), \qquad \bar F^*\in RV_{-\alpha}.$$

Every moment of $F^*$ of order $0\le a<\alpha$ is finite, while every moment of order $a\ge\alpha$ is infinite. The milestone list includes the properties of $\Pi_{1,\alpha}$ stated in §2.1 (non-increasing, convex, $\Pi_{1,\alpha}(q)+q=m_1$ for $q\le0$, $\Pi_{1,\alpha}(q)\to0$), the single-law representation (2.1) and the two stated Karamata results used to characterize the tail Das, Dhara and Natarajan, 2019, pp. 6, 27–30.

High critical ratios

A companion milestone is Proposition 4.1. For $\eta\in(0,1)$ let $q^*_\eta$ be a robust optimal order quantity and $C^*_\eta$ the optimal robust cost. Then $q^*_\eta$ is optimal for the standard newsvendor with demand law $F^*$, and

$$q^*_\eta\sim\frac{\alpha-1}{\alpha}\,\frac{1}{1-\eta}\,C^*_\eta,\qquad \eta\to1$$

Das, Dhara and Natarajan, 2019, p. 30, (4.9). It is a consequence of the goal, not a step toward it.

Significance

The theorem connects a decision made against an entire moment class to a single effective law. That law matches the robust expected shortage for every admissible order quantity but has an infinite $\alpha$th moment, so it does not belong to the class being optimized over. This distinction explains why large robust orders behave as though demand were heavy tailed. The paper also uses the result to relate the robust optimal order quantity to the optimal cost at high service levels in Proposition 4.1 Das, Dhara and Natarajan, 2019, pp. 30–31.

The mathematical theorem was proved in the cited paper. This mission asks for a Lean proof of its exact statement and reusable formal results for moment-constrained probability laws, stop-loss transforms, and regular variation. No machine-checked proof of these particular statements is part of the present draft. The cited bounds and analytic results are posed as separate milestones so their hypotheses and constants remain inspectable.

Difficulty

Pointwise optimization over demand laws does not automatically give one law that attains the worst-case shortage for every $q$. For a fixed $q$, an extremal law may depend on $q$, as Scarf's formula illustrates Das, Dhara and Natarajan, 2019, p. 3. The theorem asks for a single $F^*$ and then a precise tail index and a sharp moment cutoff. A generic upper bound on shortages would establish neither the representative law nor its infinite $\alpha$th moment. The regimes $1<\alpha<2$, $\alpha=2$, and $\alpha>2$ have different cited upper-bound statements, yet the final theorem has no regime restriction.

Formalization scope

Lean represents a demand law by a Borel measure on $\mathbb R$ with probability mass one and zero mass below zero. Membership in $\mathcal F_{1,\alpha}$ requires both real moments to be integrable; this makes the moment equalities genuine rather than default values of a nonintegrable Bochner integral. Under $m_1>0$ and $m_\alpha>m_1^\alpha$, the paper's two-point law (3.6) makes the ambiguity set nonempty. Its shortage values are bounded above by $m_1+|q|$, so the real supremum defining $\Pi_{1,\alpha}$ is finite and meaningful. The strict thresholds in Propositions 3.3–3.4 keep their power denominators positive Das, Dhara and Natarajan, 2019, pp. 12, 15, 19.

Regular variation includes eventual positivity, excluding a zero-over-zero ratio from passing as a tail law. Infinite moments of $F^*$ are lower Lebesgue integrals in extended nonnegative reals. The existence of $F^*$ is asserted rather than built into a definition. Theorem 4.2(b)'s displayed limit has a negative sign in the preprint, although its nonnegative numerator and denominator require the positive value $\alpha$; the formal statement uses the corrected sign. Its regularly varying tail integral is eventually positive, which ensures genuine finite tail integrals for large lower limits. Theorem 4.1 explicitly requires local integrability. Two encodings would trivialize the goal and are excluded: defining $F^*$ inside the statement (it is existential), and a regular-variation predicate satisfied by the zero function. The properties of $\Pi$ and the representation (2.1) are stated for $\mathcal F_{1,\alpha}$, the instance the paper uses, rather than for a general finite-mean ambiguity set. In Proposition 4.1 the optimal cost is the cost at the chosen optimizer, the statement holds for every selection of optimizers, and $\sim$ means that the ratio of the two sides tends to $1$ as $\eta\uparrow1$. These analytic conventions and the probability and measure infrastructure can be reused beyond this mission. Contributions to any of the ten source milestones, including the difficult root assertion in Proposition 3.4(b), are welcome.

Selected references

• B. Das, A. Dhara, and K. Natarajan, On the Heavy-Tail Behavior of the Distributionally Robust Newsvendor, Operations Research 69(4), 2021; preprint arXiv:1806.05379v2, 2019. Preprint, DOI.
• H. Scarf, A min-max solution of an inventory problem, in K. Arrow, S. Karlin and H. Scarf (eds.), Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958, pp. 201–209.
• A. Shapiro and A. Kleywegt, Minimax analysis of stochastic problems, Optimization Methods and Software 17, 2002, pp. 523–542. DOI.
• N. H. Bingham, C. M. Goldie and J. L. Teugels, Regular Variation, Cambridge University Press, 1987. DOI.

Why market size changes prices

Two-sided intermediaries charge buyers and pay sellers while trying to match the two groups. A larger arrival stream on one side changes both the number of possible matches and the prices that clear the market. Chen and Hu study this in a model of buyers and sellers who arrive over time and may wait before requesting a match. Their market-size theorem concerns the deterministic fluid benchmark used to choose fixed prices for the dynamic system. This mission formalizes that theorem from the submitted manuscript, main text §6, rather than the performance of the waiting-adjusted policy itself.

The fluid benchmark matters because it supplies an interpretable price and quantity for each pair of arrival rates. When buyers become more numerous, the model predicts that both the buyer price and the seller payment rise. When sellers become more numerous, both prices fall. In either direction, more arrivals raise the maximum matching quantity and the fluid profit. These claims concern the same valuation and cost distributions as the rates vary, so they isolate the effect of market size.

The two-sided fluid market

Buyer valuations lie in $[\underline v,\bar v]$, with density $f^d$ and distribution function $F^d$. Seller costs lie in $[\underline c,\bar c]$, with density $f^s$ and distribution function $F^s$. Write $\bar F^d=1-F^d$. Buyer and seller arrival rates are $\lambda^d>0$ and $\lambda^s>0$, and the horizon has length $T>0$. A buyer accepts a fixed ask price $p$ when the valuation is at least $p$; a seller accepts a fixed bid price $w$ when the cost is at most $w$. Thus $\lambda^d\bar F^d(p)$ and $\lambda^s F^s(w)$ are the corresponding acceptance rates.

The buyer virtual value is $V^d(v)=v-\bar F^d(v)/f^d(v)$, and the seller virtual cost is $V^s(c)=c+F^s(c)/f^s(c)$. Assumptions 1 and 2 of the manuscript say these functions are weakly increasing on their respective supports. The supports overlap in the sense $\underline c\le\bar v$. The density assumptions ensure that the survival and cost distribution functions have inverse quantiles on $[0,1]$. For a candidate volume $\mu$, the virtual surplus is

$$V(\mu)=V^d\!\left(\bar F^{d,-1}\!\left(\frac{\mu}{\lambda^dT}\right)\right)-V^s\!\left(F^{s,-1}\!\left(\frac{\mu}{\lambda^sT}\right)\right).$$

The optimal fluid matching quantity $\mu^*$ is the largest $\mu$ in $[0,\min\{\lambda^dT,\lambda^sT\}]$ for which $V(\mu)\ge0$. The corresponding fixed prices are $p^*=\bar F^{d,-1}(\mu^*/(\lambda^dT))$ and $w^*=F^{s,-1}(\mu^*/(\lambda^sT))$.

The fluid program (D) permits any measurable nonnegative ask and bid price path $(\hat\pi^d_t,\hat\pi^s_t)$ on $[0,T]$ that clears the market at every time: $\lambda^d\bar F^d(\hat\pi^d_t)=\lambda^sF^s(\hat\pi^s_t)$. Its value $\bar J^*$ is the supremum of buyer revenue minus seller payments, integrated over the horizon. Proposition 1 states that the constant path $(p^*,w^*)$ attains this value and that $\bar J^*=(p^*-w^*)\mu^*$.

Formalization targets

The goal is Theorem 3, the eight weak comparisons of prices, volume, and fluid profit. For $0<\lambda^d_1\le\lambda^d_2$ with $\lambda^s$ fixed, it asserts

$$p^*_1\le p^*_2,\quad w^*_1\le w^*_2,\quad \mu^*_1\le\mu^*_2,\quad \bar J^*_1\le\bar J^*_2.$$

For $0<\lambda^s_1\le\lambda^s_2$ with $\lambda^d$ fixed, the two price inequalities reverse while the volume and profit inequalities retain their directions. The goal leaves the rates and the two distributions as variables, so it states the market-size result across all systems meeting the paper's assumptions.

The milestones follow the source's dependency structure: Proposition 1 identifies the fluid optimizer; the proof of Lemma S.5 notes that $V(\mu)$ decreases in $\mu$; Lemma S.5 establishes the volume and profit comparisons; and the two parts of the proof of Theorem 3 compare the fractions $\mu^*/(\lambda^dT)$ and $\mu^*/(\lambda^sT)$ served on the growing side. The paper's proofs are in the Supplemental Note, with related proofs in the Online Appendix.

What the result provides

The theorem gives directional predictions without differentiating optimal prices with respect to arrival rates. A platform comparing two otherwise identical markets can infer which way its fluid ask and bid prices move, whether it matches more units, and whether the benchmark profit increases. Proposition 1 also connects the optimization over time-varying paths to a fixed price pair, so the static claims apply to the entire feasible fluid program.

The result is proved in the manuscript; this mission asks for a machine-checked proof of the same statement. The formal development would make the inverse-quantile construction, attainment of the optimal volume, and the nonempty bounded fluid optimization problem explicit. Those objects can be reused in other two-sided pricing or matching models. This mission does not claim that the corresponding stochastic system has identical comparative statics; the manuscript itself focuses on the fluid regime in §6.

Where the proof is difficult

Increasing one arrival rate expands the feasible number of matches, but the two optimal prices do not follow from that fact alone. The buyer price depends on the fraction of buyers served, and the seller price depends on the fraction of sellers served. A growing side can have a larger matched volume yet a smaller matched fraction. The proof must control both quantities under the appropriate inverse distribution function. Profit also needs a comparison of two separate fluid optimization problems, rather than only a comparison of their candidate fixed-price formulas.

Formalization scope

The Lean model reuses the published bilateral-trade environment for the two positive densities, interval supports, cumulative distributions, and virtual values. The new definitions clamp both cumulative distributions to their supports so a price outside the support still has the correct acceptance probability. Inverse quantiles are supported level-set infima, used only at arguments in $[0,1]$. All rates and the horizon are positive; both densities are continuous on their supports; the virtual functions satisfy the paper's regularity assumptions; and $\underline c\le\bar v$. Density continuity is a disclosed addition needed for the asserted inverse-quantile and maximum properties.

The claims involving the value of (D) assume a nonnegative seller cost support. This disclosed domain correction puts the fixed seller price in (D), whose price paths take values in $\mathbb R_+^2$; the imported bilateral-trade environment itself permits negative supports. The virtual-surplus and served-fraction inequalities hold without this condition. Every feasible path is measurable, nonnegative on $[0,T]$, clears the market at every point of that interval, and has integrable buyer and seller revenue terms. The fluid value is defined as the supremum over those paths. It is never defined by Proposition 1's fixed-price identity, which would erase the optimization claim. The volume set is restricted to $[0,\min\{\lambda^dT,\lambda^sT\}]$, so its supremum has the source's intended domain. The source uses “increasing” and “decreasing” in the weak sense.

Useful contributions include lemmas showing the clamped distributions are monotone, their supported inverses have the stated identities, the candidate volume set has a greatest member, the fluid feasible set is nonempty and bounded above, and the two fraction comparisons. These are substantive mathematical obligations: no arbitrary inverse, empty feasible set, non-integrable path, or preassigned fluid value should satisfy the goal by a default value.

Selected references

• Y. Chen and M. Hu, Pricing and Matching with Forward-Looking Buyers and Sellers, submitted manuscript, SSRN 2859864, 2020; published in Manufacturing & Service Operations Management 22(4), 717–734. SSRN manuscript.
• T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, §3.4.1. Publisher.

Why a cloudlet price matters

Mobile devices can divide work between local execution, a nearby shared cloudlet, and a remote cloud. A cloudlet has limited capacity, so one user's choice changes the delay faced by the others. Cardellini and coauthors model this as a generalized Nash equilibrium problem, in which each user's feasible choices depend on the aggregate cloudlet load. The shared utilization cap makes a direct distributed solution awkward: a user must know how much capacity all other users consume before choosing a feasible deviation. The paper therefore introduces an additional player who sets a cloudlet price. This mission formalizes the relationship between the original coupled game and that extended, ordinary Nash game Cardellini et al., accepted manuscript, pp. 10–16.

The offloading game

There are $N$ users and $n$ cloudlet servers. User $u$ chooses fractions $x_{u,m}$, $x_{u,\mathrm{clet}}$, and $x_{u,\mathrm{cloud}}$ for local, cloudlet, and remote-cloud execution. These fractions are nonnegative and sum to one. At most a fraction $\chi$ can be offloaded, and a user-specific linear power constraint applies. The set $\widetilde K_u$ contains these private feasible choices. The cloudlet load and the shared feasible set are

$$L(x)=\frac1n\sum_{u=1}^{N}\delta_u x_{u,\mathrm{clet}},\qquad \Omega=\{x:L(x)\le U_{\max}\},\qquad K=\left(\prod_{u=1}^{N}\widetilde K_u\right)\cap\Omega.$$

Each user's cost $\lambda_u R_u$ is the response-time expression on p. 10, with coefficients $\alpha_u,\beta_u,\gamma_u,\delta_u$. The VI map $F$ is the stack of the user's partial gradients, written in closed form on p. 11. A variational solution $\bar x$ belongs to $K$ and satisfies $\langle F(\bar x),x-\bar x\rangle\ge0$ for every $x\in K$. The pairing sums all three coordinates for each user. Section 5 assumes $0<U_{\max}<1$ and $0<\alpha_u,\delta_u<1$ for every user; the model also has $n>0$ and $0<\chi\le1$ Cardellini et al., pp. 7, 9–11.

The extended game replaces the joint cap in each user's feasible set by a price. User $u$ minimizes $\lambda_uR_u(x)+\rho(\delta_u/n)x_{u,\mathrm{clet}}$ over $\widetilde K_u$. A cloudlet manager chooses $\rho\ge0$ to maximize $\rho(L(x)-U_{\max})$. The manager's choice is part of the Nash equilibrium condition, not a preimposed complementary-slackness equation. The extended game's VI set is $K_e=(\prod_u\widetilde K_u)\times\mathbb R_+$ and its map is $F_e(x,\rho)=(F(x)+\operatorname{price}(\rho),U_{\max}-L(x))$ Cardellini et al., p. 15.

Formalization targets

The goal is the two-part assertion of Theorem 2. Under the standing assumptions and a strict load bound on the full product of private feasible sets, its equilibrium characterization is

$$\bar x\in\operatorname{SOL}(K,F) \quad\Longleftrightarrow\quad \exists\bar\rho,\; (\bar x,\bar\rho)\in\operatorname{NE}_{\mathrm{ext}}.$$

The same goal states that monotonicity of $F$ on $\prod_u\widetilde K_u$ implies monotonicity of $F_e$ on $K_e$. The three milestones follow the paper's path: the extended Nash game is equivalent to its VI; the shared affine constraint has a scalar multiplier at a VI solution; and the price-load coupling cancels in the monotonicity pairing. The source states the first as a classical result and gives the last two in its proof Cardellini et al., pp. 15–16.

What the result provides

The characterization lets a variational solution of a game with coupled feasible sets be found as an equilibrium of a game whose $N$ users have separate feasible sets. The additional scalar has a concrete interpretation: it is the multiplier of the shared cloudlet-utilization cap. The monotonicity assertion connects the paper's analysis of the original VI to methods for the extended one. The paper uses this relationship as the entry point for its distributed algorithms in the next section Cardellini et al., pp. 16–17.

The result is proved in the paper but is not yet machine checked in this mission. A complete development would give reusable Lean interfaces for a finite-dimensional VI on an intersection of a product polytope and one affine half-space, a multiplier characterization for that intersection, and an equilibrium-to-VI conversion for separable player constraints. Those components could support other capacity-sharing games. The theorem drafts remain proof obligations; the definitions compile locally.

Where the proof is delicate

A Nash equilibrium requires each user to be optimal against every privately feasible deviation, including deviations that violate the original shared cap. Consequently, the user's cloudlet cost must remain well defined throughout $\widetilde K_u$ for the equivalence to hold. A load bound only on $K$ does not cover those deviations. The multiplier comparison must also account for the manager's maximization condition and the sign of the load term in $F_e$. For monotonicity, $F_e$ evaluates $F$ on the whole product $\prod_u\widetilde K_u$, a larger domain than $K$. These domain distinctions explain why the statement needs two explicit repairs to the printed theorem Cardellini et al., pp. 15–16.

Formalization scope

Lean represents the users as Fin N and the three processing locations as a finite tier type. Indices therefore start at zero. The costs, the map $F$, the private sets, $\Omega$, and $K$ are separate definitions. The Euclidean pairing is written as a finite sum; no Pi-type sup norm is used. The extended Nash predicate quantifies over user deviations in $\widetilde K_u$ and over every nonnegative manager price. The VI predicates are in their own module so the game is not built into their meaning. The theorem's statement remains meaningful at $N=0$; no positive-user hypothesis is added to Section 5's assumptions.

The first repair requires $L(x)<1$ at every $x\in\prod_u\widetilde K_u$. The paper's Theorem 1 condition (18) implies this bound, but is stronger than needed. Without the bound, a private deviation can cross the pole of $\delta_u x_{u,\mathrm{clet}}/(1-L(x))$; Lean's total division then assigns a value at a zero denominator even though the paper's cost has none. In a two-user instance with $n=1$, $\delta_u=0.9$ and $U_{\max}=0.5$, the pole can lie within one user's private feasible interval. The second repair reads “the original game is monotone” on $\prod_u\widetilde K_u$, because that is precisely the $x$-domain of $K_e$. Monotonicity on $K$ alone is insufficient. Both repairs are disclosed in the item notes, and the source wording remains visible in the milestone quotations.

An empty $K$ would make a solution statement vacuous; the formal development should retain concrete feasible parameter instances. The map $F$ is the paper's displayed formula, rather than a derivative chosen to make a milestone tautological. The VI uses all user coordinates, and the extended game does not silently reinstate the shared constraint in user deviations. Contributions toward the stated multiplier theorem, Nash-to-VI equivalence, and the cancellation identity are welcome, along with reusable finite-dimensional convex-analysis lemmas.

Selected references

• V. Cardellini, V. De Nitto Personé, V. Di Valerio, F. Facchinei, V. Grassi, F. Lo Presti, and V. Piccialli, A game-theoretic approach to computation offloading in mobile cloud computing, accepted manuscript for Mathematical Programming, 2015, DOI 10.1007/s10107-015-0881-6.