Motivation

Fast and fault-tolerant logical measurements: Auxiliary hypergraphs and transversal surgery.

Target

Lemma 2.7

Let $C_\bullet,D_\bullet$ be finite based chain complexes over $\mathbb F_2$, and let $l\in\mathbb Z$. Their tensor complex has differential $\partial_C\otimes I+I\otimes\partial_D$. There exists an $\mathbb F_2$-linear isomorphism

$$H_l(C_\bullet\otimes D_\bullet)\cong\bigoplus_{i\in\mathbb Z} H_i(C_\bullet)\otimes_{\mathbb F_2}H_{l-i}(D_\bullet).$$

The direct sum is algebraic; the finite based complexes have only finitely many nonzero graded components. No particular isomorphism or representative map is asserted.

Lemma 3.2

Let binary check matrices $H_X,H_Z$ satisfy $H_XH_Z^T=0$, and let $D_X,D_Z$ be the prescribed pair-reading matrices of Eq. (2). Write $L_Z=\ker H_X/\operatorname{im}H_Z^T$ and $L_X=\ker H_Z/\operatorname{im}H_X^T$. Then

$$L_Z(D_X,D_Z)\cong L_Z(H_X,H_Z),\qquad L_X(D_X,D_Z)\cong L_X(H_X,H_Z).$$

The deformation of two identical memories therefore retains exactly $k$ logical qubits, with no additional logical classes. All spaces and isomorphisms are over $\mathbb F_2$.

Lemma 3.3

Let $H_X\in\mathbb F_2^{m_X\times n}$ and $H_Z\in\mathbb F_2^{m_Z\times n}$ satisfy $H_XH_Z^T=0$, and let $P=(1\;1)$. In the product bases, the three coboundaries of the pair-reading deformation are

$$D_X^T=\begin{bmatrix}I_2\otimes H_X^T\\P\otimes I_{m_X}\end{bmatrix},\quad D_Z^T=\begin{bmatrix}I_2\otimes H_Z^T&P^T\otimes I_n\\0&I_1\otimes H_X\end{bmatrix},\quad D_M^T=\begin{bmatrix}P^T\otimes I_{m_Z}\\I_1\otimes H_Z^T\end{bmatrix}.$$

Here old data precede new data, and old Z checks precede new Z checks; $D_M$ denotes the metachecks. These are the explicit tensor-product differentials, retaining the final degree as in pp.21-22.

Lemma 3.4

Let $H_X,H_Z$ define a binary CSS memory with X and Z distances at least $d\in\mathbb N$. Its prescribed pair-reading deformation has check matrices $D_X,D_Z$ satisfying

$$d_X(D_X,D_Z)\ge d,\qquad d_Z(D_X,D_Z)\ge d.$$

A lower distance bound quantifies over every nontrivial normalizer class modulo stabilizers; the distance is infinite when no such class exists. This is a spatial code-distance assertion.

Lemma 3.8

Let $H_X,H_Z$ define a binary CSS memory with both distances at least $d\in\mathbb N$. Let $P\in\mathbb F_2^{r\times c}$ have full row rank and every row of Hamming weight greater than one. The prescribed Z-pattern deformation of $c$ identical memories, with $r m_X$ new data qubits indexed by pattern rows and memory X checks, satisfies

$$d_X(D_X,D_Z)\ge d,\qquad d_Z(D_X,D_Z)\ge d.$$

The conclusion includes CSS commutation and every nontrivial logical class. Sparsity belongs to the separate resource claim.

Theorem 7.8

Let $G\in\mathbb F_2^{V\times E}$ be a finite incidence matrix, $W\le\mathbb F_2^V$, and $U$ its support union. Put $D_W(v)=\min_{w\in W}\lvert(v|_U)+w\rvert$, where restriction to $U$ is zero extended and bars denote Hamming weight. For $t,M>0$, suppose $|G^Tv|\ge M\min(t,D_W(v))$ for every binary vector $v$. Let the integer $L\ge1$ satisfy $L\ge1/M$, and form $G_L=[G\otimes I_L,I_V\otimes R_L]$, with $R_L$ the path incidence on $L$ vertices. At any selected level $\ell<L$, embed $W$ as $W_\ell$. Then

$$|G_L^Tv|\ge\min(t,D_{W_\ell}(v))\quad\text{for every }v.$$

Thus the thickening has certified modular expansion at least one at every choice of a single level. Cut certificates avoid asserting a largest finite expansion on degenerate inputs.

Lemma 7.9

Let $G\in\mathbb F_2^{V\times E}$ be finite, let $W\le\mathbb F_2^V$ contain $\ker G^T$, and let $t>0$. Let $U$ be the support union of $W$, and let $D_W(v)=\min_{w\in W}\lvert(v|_U)+w\rvert$, using zero-extended restriction and Hamming weight. Then

$$|G^Tv|\ge t^{-1}\min(t,D_W(v))\quad\text{for all }v.$$

Hence $1/t$ is a certified modular-expansion lower bound, even when no largest finite expansion exists.

Corollary 7.10

Let $G\in\mathbb F_2^{V\times E}$ be finite and $\ker G^T\subseteq W\le\mathbb F_2^V$. For an integer $t\ge1$, form $G_t=[G\otimes I_t,I_V\otimes R_t]$. Embed $W$ at any one level $\ell<t$ as $W_\ell$, and write $U_\ell$ for its support union. Then

$$|G_t^Tv|\ge\min\{t,\min_{w\in W_\ell}\lvert(v|_{U_\ell})+w\rvert\}\quad\text{for every }v.$$

Restrictions are zero extended and weights are Hamming weights. Integer $t$-fold thickening thus certifies modular expansion one.

Lemma B.4

Let $H\in\mathbb F_2^{m\times n}$ satisfy $HH^T=0$, defining a self-dual CSS code with $H_X=H_Z=H$. Let $E$ isometrically encode all $k$ logical qubits onto its entire codespace. Suppose matching binary supports $v_i\in\ker H$ satisfy $v_i\cdot v_j=\delta_{ij}$, and their physical X and Z products implement the corresponding logical $X_i,Z_i$ through $E$. There exists a physical Pauli correction $P$, independent of the encoded state, such that

$$P S^{\otimes n}E=E S^{\otimes k}.$$

Here $S=\operatorname{diag}(1,i)$, and $P$ includes its Pauli phase. The matrix equality holds on the entire encoded space, implementing S on every logical qubit.

§7

Let $G\in\mathbb F_2^{V\times E}$ have finite nonempty vertex and edge sets, with every column weight at most $\omega\in\mathbb N$. Let $t>0$ and $M,\rho\in\mathbb R$. Write $\mathrm{Mod}(W,t,M)$ for the modular cut inequality using the support union of $W$, and let $1_U$ indicate $U\subseteq V$. Then

$$\mathrm{Mod}(\langle1_U\rangle,t,M)\ \Longleftrightarrow\ |G^Tv|\ge M\min(t,|v\cap U|,|U\setminus v|)\quad(\forall v).$$

If $t\ge|V|$, the relative inequality at $U=V$ is equivalent to global expansion $|G^Tv|\ge M\min(|v|,|V|-|v|)$. If also the support union of $\ker G^T$ is all of $V$, then

$$\mathrm{Mod}(\ker G^T,t,\rho|E|/|V|)\ \Longleftrightarrow\ \frac{|G^Tv|}{|E|}\ge\frac{\rho}{|V|}d(v,\ker G^T)\quad(\forall v).$$

The last inequality, with locality $\omega$, is classical soundness $\rho$. The support condition implements the source's explicit $U=V$ specialization.

AppendixA Eq4

Let $f:A_\bullet\to C_\bullet$ be a chain map of finite based binary complexes and $i\in\mathbb Z$. Let $H_j(f)$ be its induced homology map. Then

$$\dim H_i(\operatorname{cone}f)+\operatorname{rank}H_i(f)+\operatorname{rank}H_{i-1}(f)=\dim H_i(C)+\dim H_{i-1}(A).$$

All dimensions are over $\mathbb F_2$, and map images are constructed from $f$. The addition form avoids truncated subtraction of natural dimensions.

AppendixA.1

Let $C_\bullet$ be a finite binary CSS complex supported in degrees $0,1,2$, and let $\ell>0$ be the repetition length. Let $F=R\otimes C$, and let $F'_X$ be its prescribed two-endpoint cone. Let $F_{\rm dual}$ and $F'_Z$ be the cochain-oriented bulk and cone obtained by the specified degree-reversing dual constructions. Put $m_X=\dim C_0$ and $m_Z=\dim C_2$. Then

$$\begin{aligned}\dim H_1(F'_X)+\dim H_0(C)&=\dim H_1(F)+2m_X,&\dim H_0(F'_X)&=0,\\\dim H_2(F'_Z)+\dim H_2(C)&=\dim H_2(F_{\rm dual})+2m_Z,&\dim H_3(F'_Z)&=0.\end{aligned}$$

These retain all boundary homology classes, including immediately terminating classes. They imply no operational fault-distance bound by themselves.

Formalization scope

Only these reviewed original-paper statements are in scope. Definitions have reviewed bodies; target proofs remain open (sorry). Reviewed deferrals are excluded. No theorem proof or whole-paper formal proof is claimed.

Motivation

A simple formula for the average gate fidelity of a quantum dynamical operation establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.

Setting

Let $d$ be a positive integer and let $\mathcal E$ be a trace-preserving quantum operation on a $d$-dimensional quantum system $Q$. Define its average fidelity by $\overline F(\mathcal E)=\int \langle\psi|\mathcal E(|\psi\rangle\langle\psi|)|\psi\rangle\,d\psi$, where $d\psi$ is the uniform Haar probability measure on normalized pure states. Let $R$ be a $d$-dimensional reference system, let $|\phi_d\rangle=d^{-1/2}\sum_{j=0}^{d-1}|j\rangle_R|j\rangle_Q$, and define $F_e(\mathcal E)=\langle\phi_d|(\mathrm{id}_R\otimes\mathcal E)(|\phi_d\rangle\langle\phi_d|)|\phi_d\rangle$. Then

$$\overline F(\mathcal E)=\frac{d F_e(\mathcal E)+1}{d+1}.$$

This identity converts entanglement fidelity into the average probability of preserving a uniformly distributed pure state.

Formalization Note The frozen channel predicate supplies complete positivity, trace preservation and linearity through a normalized Kraus representation. The Haar state measure is the image of normalized full-unitary Haar measure applied to a fixed unit vector; channel integrability is established in the imported definition module. Entanglement fidelity is an overlap probability, independent of the choice of maximally entangled state.

Target

Equation (3); proof on PDF pages 1–2

Let $d$ be a positive integer and let $\mathcal E$ be a trace-preserving quantum operation on a $d$-dimensional quantum system $Q$. Define its average fidelity by $\overline F(\mathcal E)=\int \langle\psi|\mathcal E(|\psi\rangle\langle\psi|)|\psi\rangle\,d\psi$, where $d\psi$ is the uniform Haar probability measure on normalized pure states. Let $R$ be a $d$-dimensional reference system, let $|\phi_d\rangle=d^{-1/2}\sum_{j=0}^{d-1}|j\rangle_R|j\rangle_Q$, and define $F_e(\mathcal E)=\langle\phi_d|(\mathrm{id}_R\otimes\mathcal E)(|\phi_d\rangle\langle\phi_d|)|\phi_d\rangle$. Then

$$\overline F(\mathcal E)=\frac{d F_e(\mathcal E)+1}{d+1}.$$

This identity converts entanglement fidelity into the average probability of preserving a uniformly distributed pure state.

Formalization Note The frozen channel predicate supplies complete positivity, trace preservation and linearity through a normalized Kraus representation. The Haar state measure is the image of normalized full-unitary Haar measure applied to a fixed unit vector; channel integrability is established in the imported definition module. Entanglement fidelity is an overlap probability, independent of the choice of maximally entangled state.

Significance

These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.

Difficulty

A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.

Formalization scope

Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.

Selected references

• A simple formula for the average gate fidelity of a quantum dynamical operation, arXiv:quant-ph/0205035v2. Exact result labels, PDF pages and source SHA-256 values accompany each theorem.

Additional independently reviewed proof targets

Unnumbered claim following Eq. (2): unit average gate fidelity iff perfect implementation

Let $d>0$, let $\mathcal E$ be a completely positive trace-preserving map on $d$-dimensional matrices, and let $U$ be a unitary target. Let $\overline F(\mathcal E,U)$ denote the normalized Haar average of $\langle\psi|U^\dagger\mathcal E(|\psi\rangle\langle\psi|)U|\psi\rangle$. Then

$$\overline F(\mathcal E,U)=1\quad\Longleftrightarrow\quad\mathcal E(X)=UXU^\dagger\text{ for every matrix }X.$$

Thus unit overlap fidelity characterizes exact implementation of the target channel, including its action on all density inputs.

Twirled channel: channel property, fidelity invariance, and unitary covariance; Eqs. (6), (8), (10)

Let $d>0$ and let $\mathcal E$ be a completely positive trace-preserving map. Define its normalized unitary Haar twirl by $\mathcal E_T(X)=\int U^\dagger\mathcal E(UXU^\dagger)U\,dU$. Then $\mathcal E_T$ is completely positive and trace preserving, and

$$\overline F(\mathcal E_T)=\overline F(\mathcal E),\qquad F_e(\mathcal E_T)=F_e(\mathcal E),\qquad V\mathcal E_T(\rho)V^\dagger=\mathcal E_T(V\rho V^\dagger)$$

for every density matrix $\rho$ and unitary $V$. Here $\overline F$ is the normalized pure-state Haar overlap average, and $F_e$ is the normalized maximally entangled overlap with identity action on the reference register.

These properties allow the fidelity calculation to be reduced to a unitarily covariant channel.

Unnumbered central proof result: the twirl is depolarizing

Let $d>0$ and let $\mathcal E$ be a completely positive trace-preserving map. Its normalized unitary Haar twirl $\mathcal E_T(X)=\int U^\dagger\mathcal E(UXU^\dagger)U\,dU$ has a real parameter $p$, independent of the density input, such that

$$\mathcal E_T(\rho)=\frac p d I+(1-p)\rho\qquad\text{for every density matrix }\rho.$$

No additional interval constraint on $p$ is imposed. This identifies the twirl as a depolarizing channel.

Eq. (16): entanglement fidelity in an orthogonal unitary operator basis

Let $d>0$ and let $\mathcal E$ be a completely positive trace-preserving map. Let $(U_j)_{j=1}^{d^2}$ be a complex operator basis consisting of unitaries with $\operatorname{tr}(U_j^\dagger U_k)=d\delta_{jk}$. With $F_e$ the overlap of the normalized maximally entangled state before and after applying $\mathcal E$ to its system register,

$$F_e(\mathcal E)=\frac{1}{d^3}\sum_{j=1}^{d^2}\operatorname{Re}\operatorname{tr}(U_j^\dagger\mathcal E(U_j)).$$

This expresses entanglement fidelity using the channel action on an operator basis.

Eq. (17): the paper's general qudit average gate fidelity formula

Let $d>0$, let $\mathcal E$ be a completely positive trace-preserving map, and let $U$ be a unitary target. Let $(U_j)_{j=1}^{d^2}$ be a complex operator basis of unitaries satisfying $\operatorname{tr}(U_j^\dagger U_k)=d\delta_{jk}$. The normalized Haar average gate overlap is

$$\overline F(\mathcal E,U)=\frac{\sum_{j=1}^{d^2}\operatorname{Re}\operatorname{tr}(U U_j^\dagger U^\dagger\mathcal E(U_j))+d^2}{d^2(d+1)}.$$

The target inverse conjugates the channel output. This is the paper's general qudit formula, with no unitality assumption.

Eq. (18): qubit Pauli specialization

Let $\mathcal E$ be a completely positive trace-preserving map on a qubit, let $U$ be a unitary target, and let $\sigma_1=X$, $\sigma_2=Y$, $\sigma_3=Z$ be the Pauli matrices, with $Y=\begin{pmatrix}0&-i\\i&0\end{pmatrix}$. Then the normalized Haar gate overlap satisfies

$$\overline F(\mathcal E,U)=\frac12+\frac1{12}\sum_{j=1}^{3}\operatorname{Re}\operatorname{tr}(U\sigma_jU^\dagger\mathcal E(\sigma_j)).$$

This specializes the general operator-basis formula to three nonidentity Pauli operators; trace preservation suffices.

Eq. (19): average gate fidelity from a preparable state operator basis

Let $d>0$, let $\mathcal E$ be a completely positive trace-preserving map, and let $U$ be a unitary target. Let $(U_j)_{j=1}^{d^2}$ be a complex operator basis of unitaries with $\operatorname{tr}(U_j^\dagger U_k)=d\delta_{jk}$. Let $(\rho_k)_{k=1}^{d^2}$ be a complex operator basis whose elements are density matrices. Define the unique complex coordinates $\alpha_{jk}$ by $U_j=\sum_k\alpha_{jk}\rho_k$. Then

$$\overline F(\mathcal E,U)=\frac{\sum_{j,k}\operatorname{Re}\!\left[\alpha_{jk}\operatorname{tr}(U U_j^\dagger U^\dagger\mathcal E(\rho_k))\right]+d^2}{d^2(d+1)}.$$

This gives an exact algebraic determination from the outputs on the state basis. It asserts no finite-shot accuracy or sample-cost guarantee.

These additional statements have current no-edit source review. Their formal proofs remain open; deferred results are excluded.

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

Display advertising is sold one impression at a time, mostly through second-price auctions with reserve prices. A reserve tailored to each buyer and to the features of the impression can raise the seller's revenue considerably, but the right reserve depends on the buyers' valuations, which the seller does not know and must learn from past auctions. The buyers participate in the same exchange day after day and know that their bids feed the seller's learning, so a patient buyer may bid untruthfully today to obtain lower reserves tomorrow. Learning reserve prices from strategic buyers is therefore a joint problem of statistics and incentives.

Golrezaei, Javanmard and Mirrokni (arXiv:2002.11137, Operations Research 69(1), 2021) study this problem in a contextual model and propose the policy CORP (Contextual Robust Pricing). Earlier work on learning against strategic buyers considered a single buyer facing posted prices, without contexts: Amin, Rostamizadeh and Syed (NeurIPS 2013) introduced the discounted strategic buyer, and contextual and revenue-optimization variants followed (Amin, Rostamizadeh and Syed, NeurIPS 2014; Mohri and Muñoz Medina, NeurIPS 2015). Personalized reserves in second-price auctions were studied by Paes Leme, Pál and Vassilvitskii (2016). The present paper treats many buyers, personalized reserves, contexts in $\mathbb R^d$ and censored observations (the seller sees who won, not the valuations).

Setting

In every period $t=1,2,\dots$ the seller observes a feature vector $x_t\in\mathbb R^d$, drawn i.i.d. from a law $\mathcal D$ supported in the unit ball. Each of $N$ buyers has the valuation

$$v_{it}=\langle x_t,\beta_i\rangle+z_{it},$$

where $\beta_i\in\mathbb R^d$ is an unknown preference vector with $\|\beta_i\|\le B_p$ and the noises $z_{it}$ are i.i.d. with a known density $f$ on $[-B_n,B_n]$, mean zero, and distribution function $F$. Assumption 1 asks $F$ and $1-F$ to be log-concave on $[-B_n,B_n]$.

Each period runs a lazy second-price auction with personalized reserves $r_{it}$: the highest bidder $i^\star$ gets the item if $b_{i^\star t}\ge r_{i^\star t}$ and pays $\max\{r_{i^\star t},\max_{j\neq i^\star}b_{jt}\}$; nobody else pays. The benchmark knows the $\beta_i$ and sets $r^\star_i(x)=\arg\max_y y\,(1-F(y-\langle x,\beta_i\rangle))$ (4); its expected revenue against truthful buyers is $\mathrm{rev}^\star_t$ (5).

CORP works in episodes $E_k=\{\ell_k,\dots,\ell_{k+1}-1\}$ with $\ell_k=2^{k-1}$. At the start of episode $k$ it computes, for each buyer, a maximum-likelihood estimate $\hat\beta_{ik}$ over $\|\beta\|\le B_p$ from the censored outcomes of episode $k-1$ (8)–(9). In each period of episode $k$, with probability $1/\ell_k$ it explores: one uniformly chosen buyer is offered the item at a price uniform on $[0,B_p+B_n]$. Otherwise it exploits with reserves $r_{it}=\arg\max_y y\,(1-F(y-\langle x_t,\hat\beta_{ik}\rangle))$ (10).

Buyer $i$'s bid may depend on his own history of valuations, bids, allocations and payments, on $x_t$, on $v_{it}$ and on private randomness. His utility is $\sum_t\gamma^t\,\mathbb E[v_{it}q_{it}-p_{it}]$ with a discount factor $\gamma\in(0,1)$, and buyers are utility-maximizing. The regret after $T$ periods is $\sum_{t=1}^T(\mathrm{rev}^\star_t-\mathrm{rev}_t)$, worst case over $\beta$ and $\mathcal D$ (7).

Formalization targets

Goal: Theorem 4.1 (p. 23)

There is $C$, depending only on $B_p,B_n,M,f,c_{\min},c_{\max}$, such that for all $N,d\ge1$, $T\ge2$, $\gamma\in(0,1)$, all admissible $\mathcal D,\beta$ and all utility-maximizing buyers,

$$\mathrm{Regret}(T)\le C\,N d\Big(\log(Td)\log T+\frac{\log^2T}{\log^2(1/\gamma)}\Big).$$

Milestones, in the order the proof uses them

• Proposition 3.1 (p. 15): the reserves (4) are revenue-optimal against truthful buyers.
• Lemma 1 (p. 56): the conditional revenue $W_{it}$ is flat at $r^\star_{it}$ and has a bounded second derivative.
• Lemma 2 (p. 56): $|r^\star_{it}-r_{it}|\le|\langle x_t,\beta_i-\hat\beta_{ik}\rangle|$.
• Lemma 3 (p. 57): the second-highest bid and the competing bid move by at most the shading and overbidding.
• Proposition 9.2 (p. 53): per episode, a utility-maximizing buyer lies $O(\log(\ell/\delta)+\log(\ell N)/\log(1/\gamma))$ times, and his total shading and overbidding are $O(\log(\ell N)/\log(1/\gamma))$, with high probability.
• Corollary 18.2 (p. 88): the vector Freedman inequality.

Significance

If true, Theorem 4.1 says that a seller can learn personalized, contextual reserves from censored data at a cost logarithmic in $T$ and linear in $Nd$, even when buyers manipulate their bids. The strategic term vanishes as buyers become impatient. The episodic delay between a bid and its effect on reserves, together with the random exploration prices, is what makes untruthful bidding unprofitable. The lemmas are of independent use. Proposition 3.1 and Lemma 2 concern the monopoly price under log-concave noise. Lemma 3 is a deterministic fact about second-price auctions. Corollary 18.2 is a vector concentration inequality.

Status. None of these results is machine-checked anywhere known to us. The paper's printed proof has gaps. Proposition 9.1 (p. 52), which bounds the estimation error of the MLE by the number of lies, fails as printed. With uniform noise a single lie per episode keeps the estimate a constant distance from $\beta_i$. Its supporting Lemma 5 uses a constant $u_F$ that is infinite for every compactly supported $F$ (p. 71). Its curvature bound (89) also fails when a likelihood term leaves the support of $f$. Lemma 6 (p. 76) conditions on an event the exploration lottery itself moves. A proof of Theorem 4.1, or a counterexample to it, would settle the question. The goal is stated as the paper states it, and is neither asserted nor denied here.

Difficulty

The natural route is the paper's. First bound the estimation error of the censored MLE in terms of the number of lies. Then bound the number of lies by comparing a lie's discounted future gain with its immediate loss under the exploration lottery. Finally sum over episodes.

The first step is where it breaks. With noise supported on $[-B_n,B_n]$, an observation whose threshold falls outside the support carries no curvature. Its likelihood term is constant or $+\infty$, so the minimizer of (9) is in general a set, not a point. A minimizer at the wrong end of that set can keep the reserve below the benchmark for many episodes, even with truthful buyers. Any proof must say which minimizer CORP takes, or show that all of them work. The second step must handle buyers who react to one another through their histories; the paper's proof holds the other buyers' bids fixed. The concentration steps need a vector martingale inequality and a covariance concentration bound, neither of which is in Mathlib.

Formalization scope

Lean represents features as EuclideanSpace ℝ (Fin d) and buyers as Fin N. Periods are indexed from $0$ internally (Lean's $n$ is the paper's $t=n+1$), and episodes likewise (Lean's $e$ is the paper's $k=e+1$, so $\ell_k=2^e$). Period $1$ always explores. The per-period randomness consists of the features, the noises, the exploration coin, the chosen buyer, the exploration price and the buyers' seeds. It is independent across periods, under Measure.infinitePi, and the play is defined by recursion over periods. The likelihood (9) takes values in $[0,+\infty]$ with $-\log 0=+\infty$; a real-valued Real.log would make impossible observations free and change the estimator. The estimator (8) and the reserve rule (10) are arbitrary measurable selections of the argmin and argmax, quantified universally. No tie-break or uniqueness is added. The same reserve rule defines the benchmark (4).

Standing assumptions and added hypotheses.

• The noise density is continuous on $[-B_n,B_n]$, with mass one and mean zero, and Assumption 1 holds.
• $\|x\|\le1$ almost surely, and $c_{\min}/d\,\|u\|^2<\mathbb E\langle x,u\rangle^2\le c_{\max}/d\,\|u\|^2$; the proof uses these eigenvalue bounds (pp. 57, 72–73).
• Bids are at most $M$ (p. 14) and pairwise distinct almost surely (p. 20).
• Strategies and selections are measurable, $N,d\ge1$ and $T\ge2$.
• Utility-maximizing is pinned as the inequality the proof uses on p. 77: no buyer gains by switching to truthful bidding from the start of any episode on. Every best-response profile satisfies it, and the all-truthful profile does too.
• Exploration is a posted price to the chosen buyer.
• Lemma 1 adds $f\in C^1(\mathbb R)$, which its proof uses.
• Lemma 2 adds that both indices exceed $-B_n$; without that, the argmax is unbounded.
• Lemma 3's (45) adds that another buyer wins; as printed it fails when nobody wins.
• Corollary 18.2 adds $u_0=0$.

Ruled out. The constant $C$ comes before every instance, horizon, selection and strategy, so a bound depending on $T$ or on the instance does not count. The policy is CORP as defined, not any reserve-setting rule. The rationality hypothesis is satisfiable.

Infrastructure. A complete development needs the following.

• Measurability of the recursive play.
• The monopoly price under log-concavity (Proposition 3.1, Lemma 2).
• Censored-likelihood estimation with compactly supported noise.
• A vector Freedman inequality (Corollary 18.2, reusable).
• Covariance concentration for bounded vectors.

Contributions on any milestone are welcome. So is a formal counterexample to the goal in the model as stated, for example with one truthful buyer, uniform noise and the smallest minimizer of (9).

Out of scope. CORP-II and SCORP (Theorems 5.1–5.3, Propositions 11.1–11.2) and the extensions of Appendix 8 are not part of this mission. Proposition 9.1, Lemma 5, Lemma 6 and Theorem 18.1 are not posed (see Significance).

Selected references

• N. Golrezaei, A. Javanmard, V. Mirrokni, Dynamic Incentive-Aware Learning: Robust Pricing in Contextual Auctions, Operations Research 69(1), 2021; read as arXiv:2002.11137v1. https://arxiv.org/abs/2002.11137
• K. Amin, A. Rostamizadeh, U. Syed, Learning Prices for Repeated Auctions with Strategic Buyers, NeurIPS 2013. https://papers.nips.cc/paper/2013/hash/1e6e0a04d20f50967c64dac2d639a577-Abstract.html
• R. Paes Leme, M. Pál, S. Vassilvitskii, A Field Guide to Personalized Reserve Prices, WWW 2016. https://doi.org/10.1145/2872427.2883071
• J. A. Tropp, Freedman's inequality for matrix martingales, Electronic Communications in Probability 16, 2011. https://doi.org/10.1214/ECP.v16-1624
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58

Motivation

A clinical trial that compares several treatments for the same condition must decide, patient by patient, which treatment the next patient receives. When the treatments are related (doses of one drug, drugs of one class), an outcome observed on one arm is informative about the others, and a good allocation rule should exploit that correlation. Chick, Gans and Yapar (SSRN 3184758, version of August 31, 2020; later in Management Science) model this as Bayesian sequential sampling with a correlated Gaussian prior and propose the cPDE allocation policy, which samples the arm with the largest value of an adaptive-lookahead optimal-stopping index. Their one theorem, Theorem 1, says that cPDE is asymptotically consistent: run forever, it learns every arm's mean and identifies the best arm.

Consistency is the minimal guarantee asked of an allocation heuristic: a rule that can stop sampling an arm whose value is still uncertain may settle on the wrong treatment forever. The argument follows the consistency proof of Xie, Frazier and Chick (Operations Research 64(2):542–559, 2016; "XFC") for one-step knowledge-gradient (cKG) policies, extended to an index whose lookahead is itself an optimal stopping time.

Setting

There are $M\ge2$ arms. Arm $i$ has unknown mean $\theta_i$; an observation of arm $i$ is $Y\mid\theta_i\sim N(\theta_i,\lambda_i)$ with known $\lambda_i>0$, independent across observations. The prior is $\theta\sim N(\mu^0,\Sigma^0)$ with $\Sigma^0$ positive definite, and sampling arm $i$ costs $c_i>0$. After $t$ observations the belief is $(\mu^t,\Sigma^t)$; one observation $y$ of arm $i$ updates it by Bayes' rule (8):

$$\mu'=\mu+\frac{y-\mu_i}{\lambda_i+\Sigma_{i,i}}\Sigma e_i,\qquad \Sigma'=\Sigma-\frac{\Sigma e_ie_i^\top\Sigma}{\lambda_i+\Sigma_{i,i}}.$$

From a belief $(\mu,\Sigma)$, imagine sampling arm $i$ alone. The predictive change $Z^\tau_i=\mu^{t+\tau}_i-\mu^t_i$ after $\tau$ samples is a centred Gaussian with variance $\lambda_i\tau/(n_i(n_i+\tau))$, $n_i=\lambda_i/\Sigma_{i,i}$ ((9)–(10)). The cPDE allocation index is (EC.8):

$$\nu^*_i(\mu,\Sigma)=\sup_{T_i\ge1}\mathbb E\Big[-T_i+\frac1{c_i}\max_j\Big\{\mu_j+\frac{\Sigma_{i,j}}{\Sigma_{i,i}}Z^{T_i}_i\Big\}\Big]-\frac1{c_i}\max_j\mu_j,$$

the supremum over stopping times of the sampling of arm $i$. The one-step index $\nu^{cKG_1}_i$ is the same expression with $T_i\equiv1$ ((EC.6)). The cPDE policy allocates observation $t+1$ to an arm maximizing $\nu^*_i(\mu^t,\Sigma^t)$; the trial never stops.

Formalization targets

Goal: Theorem 1 (p. 13)

For each arm $i$, almost surely,

$$\Sigma^T_{i,i}\to0,\qquad \nu^*_i(\mu^T,\Sigma^T)\to-1,\qquad \mu^T_i\to\theta_i\ \text{(also in }L^2),$$

and almost surely $\theta$ has a unique maximizer which, for all large $T$, is also the unique maximizer of $\mu^T$.

Milestones

1. Prop. 3 (p. 12): $Z^\tau_i$ is a uniformly integrable martingale and $\mathbb E[Z^{T}_i]=0$ for a.s. finite stopping times.
2. Lemma EC.1, first inequality (p. ec3): $\nu^{cKG_1}_i\le\nu^*_i$.
3. Lemma EC.3 (p. ec6): if $\liminf_T\nu^{cKG_1}_i(\mu^T,\Sigma^T)=-1$ for all $i$, then every $\Sigma^T_{i,i}\to0$.
4. Lemma EC.4 (p. ec7): an arm sampled infinitely often has $\Sigma^T_{i,i}\to0$, and $\Sigma^T_{i,i}\to0$ forces $\nu^*_i(\mu^T,\Sigma^T)\to-1$.
5. Lemma EC.5 (p. ec7): if $\liminf_T\nu^*_i(\mu^T,\Sigma^T)=-1$ for all $i$, then every $\Sigma^T_{i,i}\to0$.

Significance

Theorem 1 is the only theoretical guarantee the paper gives for cPDE; the rest of the paper is computational (bounds, comparators, experiments). It also covers, through the same sandwich argument, the cheaper variants cPDELower and cPDEUpper (Corollary 1), which are not part of this mission. A consistent policy cannot lock onto a wrong treatment, which is the property a trial designer needs before comparing finite-horizon performance.

The result is proved on paper but has no machine-checked proof. Formalizing it requires a correlated-Gaussian Bayesian learning model, optimal stopping indices defined as suprema over stopping times, and the XFC consistency argument, none of which exist in Lean. The paper's proof also routes Lemma EC.4 through an upper bound that is false as printed (see below), so a checked proof replaces that step with a correct one.

Difficulty

The obvious route bounds $\nu^*_i$ above by a one-step index with a fixed lookahead $\bar\tau$, as the paper's Lemma EC.1 does. That bound fails: $\bar\tau$ of (EC.11) changes under a change of currency while every index is invariant. For $M=2$, $\mu=(0,10^{-3})$, $\Sigma=\mathrm{diag}(10^{-6},10^{-6})$, $\lambda=(10^{-4},10^{-4})$, $c=(10^{-7},10^{-7})$, the formula gives $\bar\tau=1$ and $\nu^{cKG_1:1}_1\approx-1$, while the lookahead $T\equiv242$ already yields a value above $240$. Any upper bound on $\nu^*_i$ must instead be uniform over stopping times of unbounded length, and showing that it tends to $-1$ needs $(\Sigma^T_{i,j})^2/\Sigma^T_{i,i}\to0$ along posterior covariances, not only $\Sigma^T_{i,i}\to0$.

The second difficulty is the "finitely sampled arms" half of the argument (Lemmas EC.3, EC.5): an arm whose variance stays positive must keep a one-step value of sampling bounded away from zero, even while correlated arms are learned. This uses almost sure convergence of the posterior means and the structure of the piecewise linear terminal reward.

Formalization scope

Arms are Fin M (0-based) and time $t$ counts observations, $t=0$ being the prior. The trial lives on the canonical space $\theta\in\mathbb R^M$ times an array of standard normal noises $\varepsilon_{i,k}$, with law multivariateGaussian µ0 Σ0 times an infinite product of gaussianReal 0 1; the $k$-th sample of arm $i$ is $\theta_i+\sqrt{\lambda_i}\,\varepsilon_{i,k}$. The index $\nu^*_i$ is built on its own auxiliary space (a prior draw of $\theta_i-\mu_i$ and i.i.d. noise), not as a conditional expectation on the trial space.

Committed conventions, each a disclosed reading of the page:

• $\nu^*_i$ is (EC.8). The printed definition (15) omits $-\frac1{c_i}\max_j\mu_j$; with (15) Theorem 1 ii) would be false.
• The supremum in (EC.8) is a real sSup over stopping times of the auxiliary filtration with $1\le T_i\le N$ for some $N$; this has the paper's value and keeps every expectation finite.
• Ties in the cPDE argmax go to the least index (the paper: randomly). Every arm is eligible at every time ($\mathcal M_t=\mathcal M$), so Assumption 1 iii) is trivial.
• Theorem 1 ii) and Lemmas EC.4–EC.5 are read with $(\mu^T,\Sigma^T)$. Theorem 1 iv) is uniqueness of the maximizer of $\theta$ plus eventual agreement of the unique maximizer of $\mu^T$. The $L^2$ claim is MemLp plus eLpNorm → 0.
• "liminf $=-1$" in Lemmas EC.3, EC.5 is "for every $\varepsilon>0$, the index is below $-1+\varepsilon$ infinitely often"; since both indices are $\ge-1$ this is the printed hypothesis. Lemma EC.4 is stated for every sample path.

Trivializing formalizations are ruled out: $\nu^*_i$ is defined from $(\mu,\Sigma,\lambda_i,c_i)$, not a parameter, a fixed-lookahead index or a supremum over non-adapted times; the policy is defined, not assumed; $\mu^t$ and $\Sigma^t$ both come from (8); the $L^2$ part does not use an integral that is $0$ for non-integrable functions; iv) asserts uniqueness; and the false upper bound of Lemma EC.1 is not posed or used.

A complete development needs Gaussian conditioning for the update (8) (that $\mu^t=\mathbb E[\theta\mid\mathcal F_t]$), the closed form $\Sigma^t=(\Sigma_0^{-1}+\mathrm{diag}(n^t_k/\lambda_k))^{-1}$, optional stopping for uniformly integrable martingales, measurability of the index, and the XFC argument. The Gaussian-update and optional-stopping parts are reusable for other Bayesian ranking-and-selection results; contributions of those as separate lemmas are welcome.

Selected references

• S. E. Chick, N. Gans, Ö. Yapar, Bayesian Sequential Learning for Clinical Trials of Multiple Correlated Medical Interventions, SSRN 3184758 (INSEAD Working Paper 2020/40/TOM/ACGRE), version of August 31, 2020. https://ssrn.com/abstract=3184758
• J. Xie, P. I. Frazier, S. E. Chick, Bayesian Optimization via Simulation with Pairwise Sampling and Correlated Prior Beliefs, Operations Research 64(2):542–559, 2016.
• P. I. Frazier, W. B. Powell, S. Dayanik, The Knowledge-Gradient Policy for Correlated Normal Beliefs, INFORMS Journal on Computing 21(4):599–613, 2009.
• S. E. Chick, P. I. Frazier, Sequential Sampling for Selection with Economics of Selection Procedures, Management Science 58(3):550–569, 2012.
• D. Williams, Probability with Martingales, Cambridge University Press, 1991.

Motivation

Many services rent out a fixed stock of units that come back after use: hotel rooms, rental cars, cloud servers, hospital beds, parking spaces. Such reusable resources differ from perishable inventory because a unit sold now returns to the stock later, so the provider's pricing problem is a queueing control problem rather than a stock-depletion problem. A provider can change its price with the number of free units (dynamic pricing), or post one price and keep it (static pricing). Static prices are simpler to run, and easier to explain to customers, but they forgo the gains of reacting to congestion. How much a single price can lose is the question.

For perishable inventory, Gallego and van Ryzin (1994) showed that under a concave revenue rate a static price loses a vanishing fraction in large systems and at most a fraction $1/e$ in every regime. For reusable resources the evidence for static pricing was numerical or asymptotic: Paschalidis and Tsitsiklis (2000) reported numerical results for multi-class systems, and Gans and Savin (2007) showed near-optimality of static pricing in rental systems whose offered load and capacity are both large. Besbes, Elmachtoub and Sun (arXiv:1905.00731) gave a guarantee that does not depend on the scale of the system: a constant fraction $15/19 \approx 78.9\%$ that holds for every capacity, service rate, demand curve and weighting of the provider's objectives.

Setting

A provider owns $C \ge 1$ identical units. Customers arrive as a Poisson process of rate $\Lambda > 0$, and at price $p$ a customer buys with probability $\bar F(p)$; the effective arrival rate is $\lambda(p) = \Lambda \bar F(p)$. Prices and rates are in one-to-one correspondence, so the provider chooses a rate $\lambda \in [0,\Lambda]$ and charges $p(\lambda)$. A buyer holds one unit for an exponential time of mean $1/\mu$, pays $p(\lambda)$, and costs the provider $c > 0$. A customer who finds every unit busy is lost.

A stationary policy is a vector of rates $\lambda_1, \dots, \lambda_C \in [0,\Lambda]$, with $\lambda_i$ used while $i$ units are free; a static policy uses one rate $l$ in every state. The number of free units is a birth–death process with steady-state probabilities

$$\mathbb P_i(\pi) = \frac{\frac{C!}{(C-i)!}\prod_{j=i+1}^{C}\frac{\lambda_j}{\mu}}{\sum_{k=0}^{C}\frac{C!}{(C-k)!}\prod_{j=k+1}^{C}\frac{\lambda_j}{\mu}}, \qquad i = 0, \dots, C .$$

The profit rate, market share and service level of the policy are

$$\mathcal P^\pi = \sum_{i=1}^{C}\lambda_i(p(\lambda_i)-c)\,\mathbb P_i(\pi),\qquad \mathcal{MS}^\pi = \sum_{i=1}^{C}\lambda_i\,\mathbb P_i(\pi),\qquad \mathcal{SL}^\pi = 1-\mathbb P_0(\pi),$$

and the provider maximizes $\alpha_1\mathcal P^\pi+\alpha_2\mathcal{MS}^\pi+\alpha_3\mathcal{SL}^\pi$ for weights $\alpha_i \ge 0$ summing to $1$. The instance class $\Omega$ requires the profit rate $\lambda(p(\lambda)-c)$ to be concave in $\lambda$.

For a policy $\lambda$, the static rate $\tilde\lambda = \sum_{i\ge1}\lambda_i\mathbb P_i/\sum_{i\ge1}\mathbb P_i$ is its average rate over the states with a free unit. The proof works in the variables $z_i = \prod_{j=i}^{C}\lambda_j/\mu$ (with $z_{C+1} = 1$), $a_i = C!/(C-i)!$, $x = \sum_{k=1}^{C}a_kz_{k+1}$ and $y = \sum_{k=2}^{C}a_kz_k$, in which the ratio of service levels of $\tilde\lambda$ and $\lambda$ becomes a rational function $R(z_1,\dots,z_C)$, and in a truncation $\tilde R \le R$ used for $C \ge 4$.

Formalization targets

Goal: Theorem 1 (p. 11)

For every instance of $\Omega$ and every optimal stationary policy $\pi^*$ there is a static rate $l \in [0,\Lambda]$ with

$$\mathcal{MS}^{l} \ge \tfrac{15}{19}\,\mathcal{MS}^{\pi^*},\qquad \mathcal{SL}^{l} \ge \tfrac{15}{19}\,\mathcal{SL}^{\pi^*},\qquad \mathcal P^{l} \ge \tfrac{15}{19}\,\mathcal P^{\pi^*}\ \text{ if } \mathcal P^{\pi^*} \ge 0 .$$

One price serves all three objectives at once, whatever the weights.

Milestones

• Lemma 1 (p. 11): optimal rates are non-decreasing in the number of free units on the states the optimal policy reaches, and $\lambda^*_C$ is at most the myopic rate $\bar\lambda$.
• (11), (12) (pp. 12–13): for the static rate $\tilde\lambda$ of any policy, the market-share ratio equals the service-level ratio and the profit ratio is at least it.
• Step 2 (p. 13): the service-level ratio equals $R(z_1,\dots,z_C)$.
• Step 2a (p. 14): $R \ge 4/5$ for $C = 2$ and $R \ge 15/19$ for $C = 3$.
• Step 2b (p. 14): $\tilde R \le R$ for $C \ge 4$.
• Lemmas 2–4 (p. 15): $\partial\tilde R/\partial z_1 \ge 0$ when $y \ge a_1z_1$; $\tilde R(0,z_2,\dots,z_C) \ge 104/131$; $\tilde R \ge 6/7$ when $y \le a_1z_1$.
• Combination (p. 15): $R \ge \tilde R \ge \min\{104/131, 6/7\} \ge 15/19$ for $C \ge 4$.

Significance

The theorem bounds the value of dynamic pricing for reusable resources by a universal constant: dynamic pricing can improve each objective by at most a factor $19/15$, so a provider can adopt a single price at a known, bounded cost. Since the same price works for all weights, the optimal static price also earns at least $15/19$ of the optimal weighted objective. Section 3.2 of the paper shows that the constructed static rate $\tilde\lambda$ attains exactly $15/19$ in a limit, so the analysis of that rate cannot be improved.

The result is proved in the paper (arXiv v3, 2020; Operations Research, 2022). No part of it has a machine-checked proof. Formalizing it checks a proof whose second half is a case analysis of high-degree rational functions spread over ten pages of an e-companion, and produces closed-form, reusable statements about the stationary distribution of finite birth–death chains with state-dependent rates.

Difficulty

Step 1 is algebra and one application of Jensen's inequality. The difficulty is in bounding $R$ for every $C$. For $C \le 3$ the bound is coefficient matching between two explicit polynomials. For $C \ge 4$ the numerator and denominator of $R$ have degree growing with $C$, and no term-by-term comparison works uniformly; the paper's lemmas each cover a regime of $y/z_1$ and require bookkeeping that is uniform in $C$.

A second difficulty is Lemma 1. It is a statement about the average-reward optimal policy of a controlled birth–death chain, proved in the paper by value iteration. In the formal statement optimality is a maximization over the closed-form objective, so a proof must either develop the average-reward optimality equation for this chain or argue directly on the closed form. The goal itself quantifies over every optimal policy, including any that is not monotone; the paper's combination step assumes the monotone structure that Lemma 1 provides only on reached states, so a complete proof of the goal must handle this gap.

Formalization scope

The model is posed over stationary state-dependent pricing policies with the closed-form steady state of §2.3; the paper's reduction from general non-anticipating policies to stationary ones, and the long-run averages (1)–(2), are taken as the model and not re-proved. A policy is a function lam : ℕ → ℝ read at the states $1,\dots,C$ with rates in $[0,\Lambda]$; optimality is IsMaxOn of the weighted objective over this set, and existence of an optimal policy is not assumed. Standing assumptions (the structure Standing): $C \ge 1$; $\mu,\Lambda,c > 0$; $\alpha_i \ge 0$ with $\alpha_1+\alpha_2+\alpha_3 = 1$; $\lambda(p(\lambda)-c)$ concave on $[0,\Lambda]$; $p$ strictly decreasing on $(0,\Lambda]$.

Added hypotheses, each disclosed in its item: Theorem 1's profit bound is conditional on $\mathcal P^{\pi^*} \ge 0$ (the profit ratio is meaningless otherwise); Lemma 1 assumes $\alpha_1 > 0$ and strict concavity, and restricts monotonicity to states of positive probability (the printed version is false without these). Lemma 2 and the combination step are stated for every nonnegative $z$, as printed. Identities (11), (12) and the $R$ identity are stated for every stationary policy, since their derivations use no optimality.

The objectives are the closed forms above, not free functions constrained by hypotheses; ratios are cross-multiplied so that no objective is divided by a possibly zero quantity; $z_{C+1} = 1$ is built into the definitions so that $R$ and $\tilde R$ never divide by zero for $z \ge 0$; the derivative in Lemma 2 is asserted with HasDerivAt, not deriv. Every constant ($15/19$, $4/5$, $104/131$, $6/7$) appears as stated.

Needed beyond Mathlib's finite sums and products, Nat.descFactorial, ConcaveOn and HasDerivAt: nothing. Theorem 2 (the 95.5% guarantee for two units and linear demand), its Lemmas 5–6, the tightness example of §3.2 and the numerical experiments are out of scope. Proofs of any milestone, and alternative proofs of the bound on $R$, are welcome.

Selected references

• O. Besbes, A. N. Elmachtoub, Y. Sun, Static Pricing: Universal Guarantees for Reusable Resources, arXiv:1905.00731v3, 2020; Operations Research, 2022. https://arxiv.org/abs/1905.00731
• I. Ch. Paschalidis, J. N. Tsitsiklis, Congestion-dependent pricing of network services, IEEE/ACM Transactions on Networking 8(2), 2000. https://doi.org/10.1109/90.842141
• G. Gallego, G. van Ryzin, Optimal dynamic pricing of inventories with stochastic demand over finite horizons, Management Science 40(8), 1994. https://doi.org/10.1287/mnsc.40.8.999
• N. Gans, S. Savin, Pricing and capacity rationing for rentals with uncertain durations, Management Science 53(3) 390–407, 2007 (cited on p. 11 for the monotonicity of optimal prices in a discounted setting).