The OR Formalization Drive

Motivation

Stochastic approximation finds a root $x^*$ of an unknown map $R:\mathbb R^N\to\mathbb R^N$ from noisy evaluations $y_t=R(x_{t-1})+\xi_t$, by the Robbins–Monro recursion $x_t=x_{t-1}-\gamma_ty_t$. It underlies stochastic gradient descent, recursive estimation in statistics, adaptive control and simulation-based optimization. The classical theory (Sacks 1958) shows that the fastest attainable rate, $\sqrt t(x_t-x^*)\Rightarrow N(0,G^{-1}S(G^{-1})^T)$ with $G=R'(x^*)$ and $S$ the noise covariance, is achieved by the matrix step $\gamma_t=t^{-1}G^{-1}$, which requires knowing $G$.

Polyak and Juditsky (SIAM J. Control Optim. 30 (1992) 838–855) proved that the same optimal covariance is attained without any knowledge of $G$: run the recursion with scalar steps that decrease more slowly than $1/t$ and output the running average $\bar x_t$ of the iterates. Ruppert (Cornell ORIE technical report, 1988) obtained the one-dimensional case independently. The method, known as Polyak–Ruppert averaging, is the standard device for variance reduction in stochastic approximation.

Timeline:

• 1951, Robbins and Monro: the recursion and its convergence in probability.
• 1958, Sacks: asymptotic normality of $x_t$ for $\gamma_t=\gamma/t$.
• 1988, Ruppert: averaging in one dimension, i.i.d.-type noise.
• 1990–1992, Polyak; Polyak and Juditsky: averaging in $\mathbb R^N$ for linear problems with martingale-difference noise (Theorem 1) and nonlinear problems (Theorem 2).

Setting

Let $(\Omega,\mathcal F,(\mathcal F_t)_{t\ge0},P)$ be a filtered probability space and $(\xi_t)_{t\ge1}$ an adapted $\mathbb R^N$-valued noise process. Given a nonrandom $x_0\in\mathbb R^N$ and step sizes $\gamma_t>0$, algorithm (7) is

$$x_t=x_{t-1}-\gamma_t\bigl(R(x_{t-1})+\xi_t\bigr),\qquad\bar x_t=\frac1t\sum_{i=0}^{t-1}x_i .$$

The error is $\Delta_t=x_t-x^*$ and the estimation error is $\bar\Delta_t=\bar x_t-x^*$.

The hypotheses are:

• Assumption 3.1: a Lyapunov function $V$ with $V(x)\ge\alpha|x|^2$, Lipschitz gradient, $V(0)=0$, $\nabla V(x-x^*)^TR(x)>0$ for $x\neq x^*$, and $\nabla V(x-x^*)^TR(x)\ge\lambda_1V(x-x^*)$ near $x^*$.
• Assumption 3.2: $|R(x)-G(x-x^*)|\le K_1|x-x^*|^{1+\lambda}$ near $x^*$, with $0<\lambda\le1$ and every eigenvalue of $G$ having positive real part.
• Assumption 3.3: $\xi_t$ is a martingale difference with $E(|\xi_t|^2\mid\mathcal F_{t-1})+|R(x_{t-1})|^2\le K_2(1+|x_{t-1}|^2)$. It splits as $\xi_t=\xi_t(0)+\zeta_t$, where $\xi_t(0)$ is a martingale difference whose conditional covariance tends to $S\succ0$ in probability and whose conditional second moments are uniformly integrable, and $E(|\zeta_t|^2\mid\mathcal F_{t-1})\le\delta(x_{t-1}-x^*)$ with $\delta(x)\to0$ as $x\to0$.
• Assumption 3.4: $(\gamma_t-\gamma_{t+1})/\gamma_t=o(\gamma_t)$, $\sum_t\gamma_t^{(1+\lambda)/2}t^{-1/2}<\infty$, $\gamma_t\to0$ and $\sum_t\gamma_t^2<\infty$.

The linear case, algorithm (2), is $R(x)=Ax-b$ with every eigenvalue of $A$ having positive real part.

Formalization targets

Goal: Theorem 2

Under Assumptions 3.1–3.4,

$$\bar x_t\to x^*\ \text{a.s.},\qquad\sqrt t\,(\bar x_t-x^*)\xrightarrow{D}N\bigl(0,\;G^{-1}S(G^{-1})^T\bigr).$$

Milestones

• Lemma 1, Part 2: under condition (4) on the steps, $t\gamma_t\to\infty$.
• Lemma 1: the matrices $\varphi_j^t=A^{-1}-\gamma_j\sum_{i=j}^{t-1}\prod_{k=j}^{i-1}(I-\gamma_kA)$ are uniformly bounded, and $\frac1t\sum_{j<t}\|\varphi_j^t\|\to0$.
• Lemma 2: the representation (A9) of $\sqrt t\,\bar\Delta_t$ for the linear error recursion.
• Theorem 1(a): the linear case, $\sqrt t(\bar x_t-x^*)\Rightarrow N(0,A^{-1}S(A^{-1})^T)$.
• Proof of Theorem 2, Part 1: $V(\Delta_t)$ converges almost surely to a finite limit.
• Proof of Theorem 2, p. 850: $x_t\to x^*$ almost surely.
• Proof of Theorem 2, Part 4: the average of the linearised process $\Delta^1_t=\Delta^1_{t-1}-\gamma_t(G\Delta^1_{t-1}+\xi_t)$ satisfies $\sqrt t(\bar\Delta^1_t-\bar\Delta_t)\to0$ almost surely.

Significance

Theorem 2 shows that averaging turns a robust, slowly-stepped recursion into an asymptotically efficient estimator. The covariance $G^{-1}S(G^{-1})^T$ is the lower bound for this class of problems: for linear recursive estimates with independent noise it is the bound of [26] in the paper. Downstream, the result is what is invoked for the asymptotic efficiency of averaged stochastic gradient descent (Theorem 3 of the paper) and of recursive M-estimators in regression (Theorem 4).

The result is proved, with a published proof, but has no machine-checked version. As far as a search of the platform shows, no statement of Theorem 1 or Theorem 2 exists on Prove2Me. The platform does have a scalar martingale central limit theorem (Martingale.clt_of_mds, proved, with unconditional Lindeberg condition), which is usable through the Cramér–Wold device. Formalizing Theorem 2 also requires the Robbins–Siegmund almost-supermartingale theorem, a multivariate CLT for martingale differences under conditional Lindeberg and conditional covariance conditions, and the Kronecker lemma. Mathlib has none of these three in the required form, and each is reusable well beyond this mission. Non-asymptotic SGD rates already on the platform (the Bottou–Curtis–Nocedal and Lan missions) are different results.

Difficulty

The obvious approach analyses $x_t$ directly. It fails: with steps decreasing more slowly than $1/t$, $\sqrt t(x_t-x^*)$ diverges, and only the average has the $\sqrt t$ rate. The average must be compared with the averaged noise through the matrix sums of Lemma 1, whose bounds are uniform in both indices. Those bounds rely on the step condition $(\gamma_t-\gamma_{t+1})/\gamma_t=o(\gamma_t)$ in a quantitative way.

The nonlinear case adds a second difficulty. The iterates are first shown to converge almost surely, by a Lyapunov argument. The nonlinear error is then transferred to a linearised process at the $\sqrt t$ scale, which needs a summability estimate on $|\Delta_i|^{1+\lambda}i^{-1/2}$ obtained through stopping times. A central limit theorem for the linear process alone does not give the result, because the linearisation error must vanish after multiplication by $\sqrt t$.

Formalization scope

Points are in EuclideanSpace ℝ (Fin N) and matrices are Matrix (Fin N) (Fin N) ℝ, acting through Matrix.toEuclideanLin. Matrix norms are operator norms. Conditional expectations are MeasureTheory.condExp on a Filtration ℕ. "Given $\mathcal F_{t-1}$" is written with shifted indices ($\xi_{t+1}$ given $\mathcal F_t$). The algorithm is a recursive definition from $(x_0,\gamma,R,\xi)$, with $\gamma_0,\xi_0$ unused and $\bar x_t$ averaging $x_0,\dots,x_{t-1}$. Convergence in distribution is TendstoInDistribution to multivariateGaussian 0 V. Convergence of conditional covariances in probability is entrywise TendstoInMeasure. A limsup or supremum "tending to 0 in probability" is unfolded into its $\eta$–$\delta$ definition.

Corrections of the printed text, each used by the paper's own proof:

1. Assumption 3.1 prints $V(x^*)=0$ and $\ge\lambda V(x)$. Stated as $V(0)=0$ and $\ge\lambda_1V(x-x^*)$ (as printed they force $x^*=0$). The drift constant is renamed $\lambda_1$, since the paper uses $\lambda$ also in Assumption 3.2.
2. Eq. (10) is garbled as printed. It is stated as $\sum\gamma_t^{(1+\lambda)/2}t^{-1/2}<\infty$, the form of Assumptions 4.7 and 5.6 and of p. 851.
3. Assumption 3.3's $\delta(x_{t-1})$ is stated as $\delta(x_{t-1}-x^*)$.
4. $\gamma_t\to0$ and $\sum\gamma_t^2<\infty$ are added to Assumption 3.4. The proof uses them (p. 849), and they do not follow from it.
5. $R$ is assumed continuous. The paper states no regularity of $R$, but its proof of almost sure convergence (pp. 849–850) needs $\nabla V(x-x^*)^TR(x)$ bounded away from $0$ on annuli around $x^*$, which continuity and Assumption 3.1 provide.
6. Lemma 1 and Theorem 1(a) are stated under condition (4) only. The constant-step condition (3) is false as printed ($A=\mathrm{diag}(1,10)$, $\gamma=1$), and Theorem 2 does not use it.
7. (A3) is stated with the norm inside, as its proof establishes.
8. (A9) and the linearised process of Part 4 are stated with $-\gamma_t\xi_t$ noise signs, and with $\Delta^1_0=\Delta_0$. The printed $+$ signs contradict (A8) at $t=2$.

Several formalizations would make the goal trivial, and all are ruled out:

• conditional expectations of non-integrable functions, which are $0$ in Lean (every noise process is required to be in $L^2$);
• a real supremum for the uniform integrability in Assumption 3.3, which is $0$ on unbounded families;
• an arbitrary process with a property in place of the recursion (7);
• a degenerate Dirac target (the covariance $G^{-1}S(G^{-1})^T$ is positive definite under the hypotheses).

Welcome contributions: the Robbins–Siegmund theorem, a vector martingale CLT under conditional Lindeberg conditions, the Kronecker lemma, and the matrix estimates of Lemma 1.

Selected references

• B. T. Polyak, A. B. Juditsky, Acceleration of stochastic approximation by averaging, SIAM J. Control Optim. 30(4), 838–855, 1992. https://doi.org/10.1137/0330046
• H. Robbins, S. Monro, A stochastic approximation method, Ann. Math. Statist. 22, 400–407, 1951. https://doi.org/10.1214/aoms/1177729586
• J. Sacks, Asymptotic distribution of stochastic approximation procedures, Ann. Math. Statist. 29, 373–405, 1958. https://doi.org/10.1214/aoms/1177706619
• D. Ruppert, Efficient estimations from a slowly convergent Robbins–Monro process, Cornell University ORIE Technical Report 781, 1988 (no stable online link located).
• H. Robbins, D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics, Academic Press, 233–257, 1971. https://doi.org/10.1016/B978-0-12-604550-5.50015-8

Motivation

Semidefinite programming (SDP) optimizes a linear function over the intersection of the cone of positive semidefinite matrices with an affine subspace. It contains linear programming as the diagonal case and is the computational core of relaxations in combinatorial optimization, control theory and polynomial optimization. Its standard duality theory, however, is weaker than that of linear programming. The Lagrangian dual of an SDP can have a strictly positive duality gap, can fail to attain its optimal value, and an infeasible semidefinite system need not have a certificate of infeasibility of the naive Farkas form. All the classical strong duality theorems for SDP therefore assume a constraint qualification such as Slater's condition (a strictly feasible point).

M. V. Ramana (1997, Math. Program. 77, 129–162) constructed a dual, the Extended Lagrange–Slater Dual (ELSD), whose size is polynomial in the data and which enjoys every property of linear programming duality for every SDP, with no constraint qualification. The same construction yields an exact theorem of the alternative for semidefinite feasibility and the complexity consequence that semidefinite feasibility lies in NP if and only if it lies in co-NP in the Turing model.

Timeline:

• 1980s–1990s: Lagrangian (Slater-type) duality for SDP, with strong duality under strict feasibility (see e.g. the surveys of Vandenberghe and Boyd, SIAM Rev. 38 (1996)).
• 1981: Borwein and Wolkowicz, facial reduction for general convex programs, which regularizes a problem by passing to the minimal face containing the feasible set; not of polynomial size in the SDP data (J. Math. Anal. Appl. 83 (1981)).
• 1997: Ramana, the ELSD, an explicit polynomial-size dual with zero gap and dual attainment for every SDP.
• 1997: Ramana, Tunçel and Wolkowicz relate the ELSD to facial reduction (SIAM J. Optim. 7 (1997)).

Setting

Let $n, m$ be natural numbers, $\mathcal M_n$ the space of real $n\times n$ matrices, and $\mathcal S_n\subseteq\mathcal M_n$ the symmetric ones. On $\mathcal M_n$ the inner product is $A\bullet B = \sum_{i,j}A_{ij}B_{ij}$. For symmetric $A$, $A\succeq 0$ means $A$ is positive semidefinite. The data are symmetric $Q_0, Q_1,\dots,Q_m\in\mathcal S_n$ and $c\in\mathbb R^m$. The primal SDP is

$$(\mathrm P)\qquad \sup\ c^{\mathsf T}x\quad\text{s.t.}\quad Q(x) := Q_0-\sum_{i=1}^m x_iQ_i\succeq 0 ,$$

with feasible region $G = \{x\mid Q(x)\succeq 0\}$, a spectrahedron. Define $Q^*:\mathcal M_n\to\mathbb R^m$ by $Q^*(U) = (U\bullet Q_i)_{i=1}^m$ and write $Q^\#(U) = 0$ for "$Q_0\bullet U = 0$ and $Q^*(U) = 0$".

For $k\ge 1$ let $\mathcal C_k$ be the set of tuples $(U_i, W_i)_{i=1}^k$ of real $n\times n$ matrices with $W_0 = 0$ and, for $i = 1,\dots,k$,

$$Q^\#(U_i+W_{i-1}) = 0,\qquad U_i\succeq W_iW_i^{\mathsf T}.$$

The $W_i$ need not be symmetric. $\mathcal U_k$ and $\mathcal W_k$ are the sets of last components $U_k$ and $W_k$; $\mathcal W_0 = \{0\}$. The ELSD is

$$\inf\ (U+W)\bullet Q_0\quad\text{s.t.}\quad Q^*(U+W) = c,\quad W\in\mathcal W_m,\quad U\succeq 0,$$

and Weak-ELSD is the same program with $\mathcal W_{m-1}$. For the milestones: the polar $G^\circ = \{y\mid x^{\mathsf T}y\le 1\ \forall x\in G\}$, the algebraic polar $G^* = \{Q^*(U)\mid U\bullet Q_0\le 1,\ U\succeq 0\}$, and $S_k = Q^*(\mathcal W_k)$.

Formalization targets

Goal: Theorem 6 (Duality Theorem)

For all data $(Q_0,\dots,Q_m,c)$:

1. weak duality: $c^{\mathsf T}x\le (U+W)\bullet Q_0$ for $x\in G$ and $(U,W)$ feasible for ELSD or Weak-ELSD;
2. if $G\neq\emptyset$, then $\sup_{x\in G}c^{\mathsf T}x<\infty$ iff ELSD is feasible, iff Weak-ELSD is feasible;
3. if $G\ne\emptyset$ and ELSD (or Weak-ELSD) is feasible, there is $v\in\mathbb R$ with

$$v = \sup_{x\in G}c^{\mathsf T}x = \inf_{\mathrm{ELSD}}(U+W)\bullet Q_0 = \inf_{\mathrm{Weak\text{-}ELSD}}(U+W)\bullet Q_0;$$

4. if $G\ne\emptyset$ and the primal is bounded, ELSD attains $v$.

Milestones

Propositions 7(vi) and 7(vii) (facts on PSD matrices), Lemma 9 (annihilation $Q(x)U = Q(x)W = 0$), weak duality over every $\mathcal W_k$, Lemma 10 (nested subspaces), Lemma 13 ($G^\circ = \mathrm{Cl}(G^*)$), Corollary 14, Claims 17 and 16, the central Theorem 12,

$$G^\circ = \{Q^*(U+W)\mid W\in\mathcal W_k,\ U\succeq 0,\ U\bullet Q_0\le 1\}\qquad(0\in G,\ k\ge m-1),$$

the translation invariance of $\mathcal C_k,\mathcal U_k,\mathcal W_k$ (§2.5), and system (14) (dual attainment at value 0). Theorems 19–21 (Farkas lemma for SDP, optimality condition, primal attainment) are further items stated on the same definitions.

Significance

The Duality Theorem gives SDP a dual with the full strength of linear programming duality for every instance, at polynomial size. Consequences in the paper: an exact theorem of the alternative for semidefinite feasibility (Theorem 19); semidefinite characterizations of optimality of a given point and of primal attainment (Theorems 20, 21); and the complexity results that semidefinite feasibility is in NP iff it is in co-NP in the Turing model and in NP ∩ co-NP in the Blum–Shub–Smale model (Theorem 25, not part of this mission). Theorem 12 separately gives an exact semidefinite description of the polar of any spectrahedron containing the origin.

The results are proved on paper and are classical. No machine-checked version is known to exist; the platform's existing SDP duality theorem assumes Slater's condition. A formalization would provide the first constraint-qualification-free SDP duality in Lean, together with reusable infrastructure on PSD matrices (range inclusion, $A\bullet B = 0\Rightarrow AB = 0$) and on polars of convex sets.

Difficulty

The obvious route to SDP strong duality separates the primal's value from the image of the PSD cone under a linear map and invokes a closed-cone Farkas lemma. That step fails: the linear image of the PSD cone need not be closed, which is exactly why Lagrangian duality has gaps. In this mission the obstruction reappears as the non-closedness of the algebraic polar $G^*$ (Lemma 13 only gives $G^\circ = \mathrm{Cl}(G^*)$). The difficulty is to show that finitely many, and at most $m-1$, corrections by the sets $S_k$ close $G^*+S_k$ (Claims 16, 17), and to control dimensions in doing so. A proof by assuming closedness, strict feasibility or a Slater point is a different theorem.

Formalization scope

Everything lives in the namespace ExactSDPDuality.ELSD, in one definition file. Matrices are Matrix (Fin n) (Fin n) ℝ, vectors Fin m → ℝ; "$\succeq 0$" is Mathlib's PosSemidef (which over ℝ includes symmetry); $A\bullet B$ is the entrywise sum on all of $\mathcal M_n$; $c^{\mathsf T}x$ is the dot product. The data $Q_0,\dots,Q_m$ carry symmetry hypotheses in every statement, as the paper assumes throughout. $\mathcal C_k$ is encoded by sequences $U, W:\mathbb N\to\mathcal M_n$ with $U_0 = W_0 = 0$, so $\mathcal U_0 = \mathcal W_0 = \{0\}$; for $m = 0$ the index $m-1$ is $0$. Optimal values are least upper and greatest lower bounds of the value sets, never real sSup/sInf. The polar is the one-sided polar. In §2.4 statements the standing assumption $0\in G$ is a hypothesis. In Claim 16 the index satisfies $k+1\le m$, the range where $S_{k+1}$ is introduced, and $\dim S_k$ is the rank of the span of $S_k$.

Theorems 20 and 21 are printed with $Q^*(U+W) = 0$; both are false as printed (counterexamples in the items) and are stated with the corrected $Q^*(U+W) = c$ that the paper's derivation from Theorem 6 gives.

Trivializing formalizations are ruled out: no Slater or other constraint qualification appears; the dual is the ELSD built from the recursively defined $\mathcal W_m$, not the Lagrangian dual or an arbitrary subspace; the $W_i$ range over all of $\mathcal M_n$, not only symmetric matrices (the paper's Example 4 needs a nonsymmetric $W_2$).

Needed infrastructure: PSD matrix facts (Proposition 7), bipolar theorem for closed convex sets containing the origin (Proposition 11), closedness arguments for linear images of cones, and dimension counting of subspaces of $\mathbb R^m$. Contributions of any milestone, of these general lemmas, and of alternative proofs (for instance via facial reduction) are welcome.

Selected references

• M. V. Ramana, An exact duality theory for semidefinite programming and its complexity implications, Mathematical Programming 77 (1997) 129–162. https://doi.org/10.1007/BF02614433
• M. V. Ramana, L. Tunçel, H. Wolkowicz, Strong duality for semidefinite programming, SIAM Journal on Optimization 7 (1997) 641–662. https://doi.org/10.1137/S1052623495288350
• J. M. Borwein, H. Wolkowicz, Regularizing the abstract convex program, Journal of Mathematical Analysis and Applications 83 (1981) 495–530. https://doi.org/10.1016/0022-247X(81)90138-4
• L. Vandenberghe, S. Boyd, Semidefinite programming, SIAM Review 38 (1996) 49–95. https://doi.org/10.1137/1038003
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

A Fisher market is the simplest model of a market in which prices are set by supply and demand: buyers bring money, sellers bring goods, and a price vector is an equilibrium when every buyer, spending her money optimally at those prices, leaves every good exactly sold out. Computing equilibria is one of the central questions of algorithmic game theory, because a polynomial-time algorithm is what would make the equilibrium concept usable as a prediction or as a pricing mechanism.

For linear utilities an equilibrium always exists, is rational, and can be computed in polynomial time (Eisenberg and Gale 1959; Devanur, Papadimitriou, Saberi and Vazirani, J. ACM 2008, https://doi.org/10.1145/1411509.1411512). The next natural class, additively separable, piecewise-linear, concave utilities, captures diminishing marginal utility and is the class studied by Vazirani and Yannakakis (J. ACM 58(3), Article 10, 2011, https://doi.org/10.1145/1970392.1970394). Their paper shows that equilibria in this class are hard to compute (PPAD-complete) and that deciding whether one exists is NP-complete. Both results rest on a structural fact proved first: whenever such a market has an equilibrium at all, it has one whose prices are rational numbers of polynomial bit length. That fact is the subject of this mission.

Timeline:

• 1959, Eisenberg and Gale: a convex program whose optimal solutions are the equilibria of linear Fisher markets; equilibrium prices are rational.
• 2008, Devanur, Papadimitriou, Saberi and Vazirani: a combinatorial polynomial-time algorithm for linear Fisher markets, based on a max-flow test of candidate prices.
• 2009, Chen, Dai, Du and Teng, and Chen and Teng (FOCS 2009; ISAAC 2009): PPAD-hardness for additively separable piecewise-linear concave utilities in Arrow–Debreu and Fisher markets.
• 2011, Vazirani and Yannakakis: rationality of equilibria with polynomial bit size (Theorem 4.1 for Fisher markets, Theorem 5.1 for Arrow–Debreu markets), PPAD membership, and NP-completeness of existence.

Setting

There are $n$ buyers $B=\{1,\dots,n\}$ and $g$ divisible goods $G=\{1,\dots,g\}$, one unit of each good. Buyer $i$ has a rational budget $e(i)>0$. For each buyer $i$ and good $j$ a function $f^i_j:\mathbb R_+\to\mathbb R_+$ gives the utility that $i$ derives from an amount of good $j$. It is piecewise linear and concave: it is given by a finite list of bounded segments $(c_1,a_1),\dots,(c_m,a_m)$ with rational amounts $a_k>0$, followed by a last, unbounded segment, with rational slopes $c_1\ge c_2\ge\dots\ge c_m\ge c_\infty\ge 0$. The function has slope $c_k$ on $[a_1+\dots+a_{k-1},\,a_1+\dots+a_k]$ and slope $c_\infty$ afterwards. Buyer $i$'s utility for a bundle $x=(x_1,\dots,x_g)$ is additively separable:

$$u_i(x)=\sum_{j\in G}f^i_j(x_j).$$

Given prices $p\in\mathbb R^g_{\ge0}$, a bundle $x\ge0$ is optimal for buyer $i$ if $\sum_jp_jx_j\le e(i)$ and no bundle $y\ge0$ with $\sum_jp_jy_j\le e(i)$ has $u_i(y)>u_i(x)$. The prices $p$ are equilibrium prices if there is an allocation $(x_{ij})$ that gives each buyer an optimal bundle and sells every good exactly: $\sum_ix_{ij}=1$ for every $j$.

The bit size of a rational number $a/b$ in lowest terms is the binary length of $|a|$ plus that of $b$. The encoding size $\|M\|$ of a market $M$ is $n+g$ plus the bit sizes of all budgets, slopes and amounts, plus the number of bounded segments.

For the intermediate results, fix positive prices $p$. The bang per buck of a segment $s$ of good $j$ is $\mathrm{slope}(s)/p_j$ and its value is $\mathrm{amount}(s)\cdot p_j$ (infinite for an unbounded segment). Sorting buyer $i$'s segments by decreasing bang per buck into classes of equal bang per buck, the first class at which the cumulative value exceeds $e(i)$ is her flexible class. Segments of strictly larger bang per buck are forced, the others undesirable. From these the paper defines $\mathrm{spent}(i)$ (value of the forced segments), $\mathrm{unspent}(i)=e(i)-\mathrm{spent}(i)$, $\mathrm{unsold}(j)$ (the part of good $j$ not taken by forced segments), and a network $N(p)$ from a source through goods and buyers to a sink.

Formalization targets

Goal: Theorem 4.1 (p. 10:9)

There is a polynomial $P$ such that for every Fisher market $M$ as above,

$$M\text{ has equilibrium prices }p\in\mathbb R^g\ \Longrightarrow\ M\text{ has equilibrium prices }q\in\mathbb Q^g\text{ with }\sum_{j}\operatorname{bits}(q_j)\le P(\|M\|).$$

The polynomial is fixed before the market. Nothing beyond the existence of some real equilibrium is assumed.

Milestones

1. Lemma 3.1 (p. 10:8). For positive prices with $\sum_jp_j=\sum_ie(i)$, $\mathrm{unspent}\ge0$ and $\mathrm{unsold}\ge0$: $p$ are equilibrium prices iff the max-flow value of $N(p)$ is $\sum_i\mathrm{unspent}(i)$.
2. Proof of Theorem 4.1, first sentence (p. 10:9). From a positive equilibrium $p'$ with $\sum_jp'_j=\sum_ie(i)$, build the linear program of §4, whose variables are prices and flows and whose combinatorial data are fixed by $p'$. Then $p'$, with a suitable flow, is an optimal solution of value $\sum_ie(i)$.
3. §4, second paragraph (p. 10:8). Every optimal solution of that LP with positive prices gives equilibrium prices.

Significance

The result is what makes the existence problem for these markets a problem in NP: a rational equilibrium of polynomial size is a certificate that can be checked, with Lemma 3.1, by one max-flow computation. The same rationality statement underlies the paper's PPAD-membership proof and its NP-completeness result for existence. It also marks the boundary with markets whose equilibria can be irrational, as happens for some non-separable utilities. In that sense it shows that separable piecewise-linear concave utilities keep the "linear" character of the problem even though computing an equilibrium becomes hard.

All three statements are proved in the source, and none of them has a machine-checked proof on the platform or, as far as is known, anywhere else. The mission produces the first formal account of piecewise-linear Fisher markets: the model, the forced/flexible/undesirable classification of segments, the max-flow test for equilibrium, and the linear program of §4. It also forces precision where the paper is informal. The §4 bang-per-buck inequalities are printed with their directions reversed, and the claim about optimal LP solutions needs positive prices. The formal statements record each of these choices.

Difficulty

The obvious argument is: "equilibria are solutions of a linear system, so a rational one exists". It fails as stated, because the set of equilibrium prices is not a polyhedron. Which segments a buyer buys depends on the prices themselves, through the ordering of the ratios $\mathrm{slope}/p_j$, so the equilibrium conditions are a finite union of polyhedral pieces glued along the price-dependent ordering. The work is to freeze the combinatorial structure of one given equilibrium and to show that the resulting fixed linear program still certifies equilibrium at every one of its optimal points. That second step is what Lemma 3.1 is for. The polynomial bit bound then needs a quantitative bound on the vertices of a rational LP, uniform in the market's encoding.

Formalization scope

Buyers and goods are Fin n and Fin g. Budgets, slopes and amounts are rationals (ℚ). Prices and allocations are reals (ℝ), so that "admits rational prices" is a real conclusion: the goal returns q : Fin g → ℚ whose cast is an equilibrium. The committed conventions are:

• each good has unit supply;
• budgets are positive;
• each $f^i_j$ is a list of (slope, amount) pairs of bounded segments together with the slope of its last, unbounded segment ("the last (infinite) segment", §6), with nonnegative slopes, positive amounts and nonincreasing slopes, stored inside the market structure;
• the unbounded segment has infinite value and, when flexible, gives its network edge infinite capacity; this is encoded logically (no upper bound on that edge);
• equilibrium requires exact clearing of every good, which by the paper's footnote 3 gives the same equilibrium prices as leaving zero-price goods partly unsold;
• the classes $Q_l$ are represented by the bang per buck of the flexible class, not by an index;
• parallel network edges are merged;
• max-flow is the supremum of the values of feasible flows on the good–buyer edges.

Hypotheses added relative to the page, each disclosed in its statement:

• positivity of the LP solution's prices (milestone 3).

The §2 condition on p. 10:7 is a sufficient condition for existence and is deliberately not a hypothesis of the goal, which assumes only that an equilibrium exists. Complexity-class statements ("in NP", "PPAD-complete") are out of scope. What is formalized is the explicit polynomial bit bound, with a polynomial chosen before the market. A goal with the polynomial chosen after the market, an encoding size that ignores the bits of the data, or an equilibrium notion without utility-maximizing bundles would be trivially satisfiable. The statements rule all three out.

Beyond this mission, a complete development needs LP theory with rational data: existence of optimal basic solutions and determinant bounds on their bit size. Existing platform results that may serve as substrate include SmaleNinth.exists_square_subsystem and SmaleNinth.abs_det_le_factorial_mul_pow. Contributions welcome: proofs of the milestones, a reusable bit-size theory for rational LP vertices, and the Arrow–Debreu analogue (Theorem 5.1).

Selected references

• V. V. Vazirani and M. Yannakakis, Market Equilibrium under Separable, Piecewise-Linear, Concave Utilities, J. ACM 58(3), Article 10, 2011. https://doi.org/10.1145/1970392.1970394
• N. R. Devanur, C. H. Papadimitriou, A. Saberi and V. V. Vazirani, Market Equilibrium via a Primal–Dual Algorithm for a Convex Program, J. ACM 55(5), 2008. https://doi.org/10.1145/1411509.1411512
• E. Eisenberg and D. Gale, Consensus of Subjective Probabilities: The Pari-Mutuel Method, Ann. Math. Statist. 30(1), 1959. https://doi.org/10.1214/aoms/1177706369
• X. Chen, D. Dai, Y. Du and S.-H. Teng, Settling the Complexity of Arrow–Debreu Equilibria in Markets with Additively Separable Utilities, FOCS 2009. https://doi.org/10.1109/FOCS.2009.29
• W. C. Brainard and H. E. Scarf, How to Compute Equilibrium Prices in 1891, Cowles Foundation Discussion Paper 1272, 2000. https://cowles.yale.edu/research/cfdp-1272

Motivation

Market equilibrium is the central solution concept of general equilibrium theory: prices at which every agent buys a utility-maximizing bundle and supply meets demand. Arrow and Debreu (1954) proved that equilibria exist under mild conditions on endowments and utilities, and a line of work in algorithmic game theory asks how hard it is to compute them. For linear utilities an equilibrium can be computed in polynomial time, and there is an efficiently checkable condition for its existence. The next natural class, additively separable piecewise-linear concave utilities, models diminishing marginal utility and is the class most used in applications.

Vazirani and Yannakakis (J. ACM 58(3), 2011) settle the complexity of this class. They show that equilibria are rational whenever they exist (Theorems 4.1 and 5.1), that computing an equilibrium under the standard sufficient conditions is PPAD-complete (Theorems 6.1 and 7.1, building on Chen, Dai, Du and Teng 2009), and — the subject of this mission — that deciding whether an equilibrium exists at all is NP-complete (Theorem 8.1). The hardness half rests on an explicit construction: from an instance of Exact Cover by 3-Sets, a market whose equilibria encode exact covers.

Setting

An Arrow–Debreu market has a finite set $B$ of agents and a finite set $G$ of divisible goods. Agent $i$ owns an endowment $w_{ij}\ge 0$ of each good $j$ and has utility $u_i(y)=\sum_{j} f^i_j(y_j)$, where each $f^i_j$ is a piecewise-linear concave utility function: slopes $c_1\ge c_2\ge\dots\ge c_m>0$ on consecutive pieces of lengths $a_1,\dots,a_m$, followed by a last piece of slope $t\in[0,c_m]$ until infinity ($t=0$ means the function goes flat).

At prices $p$, agent $i$'s income is $\sum_j p_j w_{ij}$. An optimal bundle is an affordable $y\ge 0$ maximizing $u_i$ among affordable bundles, bought only along the pieces of $f^i_j$ that carry utility. A price equilibrium is a price vector $p$ in the unit simplex ($p\ge 0$, $\sum_j p_j=1$) together with an allocation of optimal bundles such that $\sum_i x_{ij}=\sum_i w_{ij}$ for every good $j$. It is an $\epsilon$-approximate equilibrium if instead $|\sum_i x_{ij}-\sum_i w_{ij}|\le\epsilon\sum_i w_{ij}$ for every $j$.

An X3C instance is a family $\mathcal C=(C_1,\dots,C_n)$ of $3$-element subsets of $X=\{x_1,\dots,x_n\}$; an exact cover is a subfamily in which every element of $X$ lies in exactly one set. Following the paper, $n$ is a multiple of $3$, $n>35$, and $\bigcup_i C_i=X$.

The market $D(\mathcal C)$ has $2n+1$ goods (good $0$, goods $C_i$, goods $x_j$) and $2n+2$ agents, with $e_0=n^3$:

1. agent $0$ owns $e_0$ units of every good; his utility for every good has slope $2$ up to $e_0$ units and slope $1$ beyond;
2. agent $C_i$ owns one unit of good $C_i$; segments of slope $1$, length $1/2$ for good $0$, slope $1/3$, length $1/6$ for each good $x_j\in C_i$, slope $1/9$, length $1/4$ for good $C_i$;
3. agent $x_j$ owns $1/6$ unit of good $x_j$; one segment of slope $1$, length $1/12$ for good $0$;
4. the extra agent owns $n/2$ units of good $0$; one segment of slope $1$, length $3/4$ for each good $C_i$.

All other utility functions are flat.

Formalization targets

Goal: the reduction statement

$$\mathcal C\ \text{has an exact cover}\iff D(\mathcal C)\ \text{has an equilibrium}\iff D(\mathcal C)\ \text{has an } n^{-5}\text{-approximate equilibrium}.$$

This is the mathematical content of the NP-hardness half of Theorem 8.1, assembled by the paper from Lemmas 8.2 and 8.3.

Milestones

1. Lemma 8.2: an exact cover yields an equilibrium of $D(\mathcal C)$.
2. Lemma 7.2, as applied in Lemma 8.3: in an $n^{-5}$-approximate equilibrium of $D(\mathcal C)$ all prices are positive and within a factor $2$ of each other.
3. Claims 8.4–8.7: in such an equilibrium, with $p_m$ the minimum price, $p(0)=2p_m$; $p(x_j)<2p_m$; with $S=\{i: p(C_i)\ge p_m+\tfrac16\sum_{x_j\in C_i}p(x_j)\}$, every $i\notin S$ has $p(C_i)=p_m$; and the sets indexed by $S$ are pairwise disjoint.
4. Lemma 8.3: an equilibrium, or an $n^{-5}$-approximate equilibrium, of $D(\mathcal C)$ yields an exact cover.

Significance

Theorem 8.1 shows that there is no efficiently checkable necessary and sufficient condition for the existence of an equilibrium in piecewise-linear concave markets unless P = NP, in contrast with the linear case. Together with the PPAD results of the same paper it separates two questions: under the classical sufficient conditions an equilibrium exists and finding one is PPAD-complete; without them, even deciding existence is NP-hard, and remains so for $n^{-5}$-approximate equilibria. The construction illustrates the technique the paper uses for both of its negative results: well-chosen piecewise-linear pieces make an agent buy a segment wholly or not at all, depending on how prices compare, which gives the equilibrium problem a discrete character.

The result is proved in the paper. To our knowledge no part of it has been machine-checked. This mission formalizes the reduction's correctness at full strength, including the approximate version, which requires quantitative control of clearing errors that the exact version does not.

Difficulty

The direction "exact cover ⇒ equilibrium" is an explicit verification: prescribed prices and an allocation, and a check that every bundle is optimal, which for separable piecewise-linear utilities is a bang-per-buck comparison. The converse is the substantial part. An arbitrary approximate equilibrium must be shown to have the rigid price structure — every price in $[p_m,2p_m]$, good $0$ at $2p_m$, unused sets at $p_m$ — before a counting argument on agent $0$'s savings forces $|S|=n/3$. Each step is an excess-demand argument in which the error $\epsilon$ times the supply must be compared with quantities of order $1/n$; this is where $n>35$ and the exponent $5$ enter, and why the approximate statement does not follow from the exact one. Optimality of bundles is a statement about all affordable bundles, so each claim needs the structure of optimal bundles under piecewise-linear concave utility, which is not in Mathlib.

Formalization scope

Lean namespace PLCMarkets.ExactCover. Market data (endowments, slopes, lengths) are rationals; prices and allocations are reals. Goods and agents of $D(\mathcal C)$ are small inductive types named as in the paper; indices are 0-based. Supplies are not normalized to $1$, so clearing is $\sum_i x_{ij}=\sum_i w_{ij}$; prices are normalized to the simplex in both equilibrium notions, as in the proof of Lemma 8.3. The family $\mathcal C$ is indexed and may repeat a set; exact cover and the disjointness of $S$ count indices.

Standing hypotheses of every theorem: each $C_i$ has three elements, $3\mid n$, $n>35$, $\bigcup_i C_i=X$ — the paper's own "without loss of generality" assumptions (p. 10:19). Two conventions depart from the printed page, both necessary and both disclosed on the items:

• Optimal bundles buy only utility-bearing pieces. If a utility function is flat beyond its segments, the agent does not buy beyond them. The paper uses this throughout (an agent "can only spend $p_m/6$ on the single segment", Claim 8.5). Without it, agents can spend leftover income on goods worth nothing to them; then setting $p(0)=2p_m$ and every other price to $p_m$ gives an exact equilibrium of every $D(\mathcal C)$, and the goal is false.
• The extra agent's segments have length $3/4$. The page prints $3n/4$; every computation in the paper (Lemma 8.2, Claim 8.6, the end of Lemma 8.3) uses $3/4$ per good, and with $3n/4$ the prices of Lemma 8.2 are not an equilibrium.

Trivializing encodings are excluded: optimality of bundles is part of both equilibrium notions (without it the endowment itself clears every market), clearing is relative and per good, and the goal quantifies only over $n$ and $\mathcal C$, with $D(\mathcal C)$ an explicit function of $\mathcal C$.

Out of scope: the complexity-class statement "NP-complete" and NP membership (which comes from the rationality theorems of the companion mission); polynomial-time computability of the construction and string encodings of markets; and the Fisher market $F$ of §8, whose half of Lemmas 8.2 and 8.3 is a natural follow-up. Reusable infrastructure: piecewise-linear concave utilities, Arrow–Debreu markets with exact and approximate equilibria, and bang-per-buck characterizations of optimal bundles. Contributions proving that characterization as a standalone lemma are welcome.

Selected references

• V. V. Vazirani and M. Yannakakis, Market Equilibrium under Separable, Piecewise-Linear, Concave Utilities, Journal of the ACM 58(3), Article 10, 2011. https://doi.org/10.1145/1970392.1970394
• X. Chen, D. Dai, Y. Du and S.-H. Teng, Settling the Complexity of Arrow–Debreu Equilibria in Markets with Additively Separable Utilities, Proceedings of the IEEE Symposium on Foundations of Computer Science (FOCS), 2009 (reference [Chen et al. 2009a] of the paper).
• M. R. Garey and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
• K. J. Arrow and G. Debreu, Existence of an Equilibrium for a Competitive Economy, Econometrica 22(3), 1954. https://doi.org/10.2307/1907353

Motivation

Firms that can buy the same item from two suppliers, a cheap slow one and a fast expensive one, face the dual-sourcing inventory problem: how much to order from each source in every period when demand is random and unmet demand is backlogged. Global sourcing (offshore regular supply plus a near-shore express supply) is the standard example (Allon and Van Mieghem 2010). When the two lead times differ by more than one period, the optimal policy depends on the whole pipeline of outstanding orders. No simple optimal policy is known, and dynamic programming is intractable for long lead times.

The tailored base-surge (TBS) policy orders a constant amount from the slow source and uses the fast source to bring the expedited inventory position up to a fixed level. It is simple, and it is used in practice. Janakiraman, Seshadri and Sheopuri (JSS, Management Science 2015) showed that its best parameters solve a convex program that does not depend on the regular lead time, and they conjectured, with numerical support, that TBS is near-optimal when that lead time is long.

Timeline:

• Karlin and Scarf (1958), Scarf (1960): structure of optimal single-source backlog policies with a lead time.
• Sheopuri, Janakiraman and Seshadri (2010): reduction of dual-sourcing policies to the truncated regular pipeline and the expedited inventory position (Lemma 1 here).
• Allon and Van Mieghem (2010): the TBS policy, with conjectures and numerical evidence.
• JSS (2015): the TBS cost formula and a convex program for its parameters.
• Xin and Goldberg (2018): proof of the conjecture with an explicit rate (Management Science 64(1), 2018). This mission formalizes that result.

Setting

Let $D$ be a nonnegative random variable with finite mean $\mathbb E[D]$ that is not almost surely constant. Demands $D_1, D_2, \dots$ are i.i.d. copies of $D$. The regular source has lead time $L$, the express source has lead time $L_0 \ge 0$, and $L > L_0 + 1$. In period $t$ the controller orders $q^R_t \ge 0$ and $q^E_t \ge 0$; then $q^R_{t-L} + q^E_{t-L_0}$ arrives and $D_t$ is realized, so the on-hand inventory evolves as $I_{t+1} = I_t + q^R_{t-L} + q^E_{t-L_0} - D_t$ and may be negative. Initially nothing is on order and $I_1 = -\sum_{i=1}^{\hat G} D'_{-i}$, where the $D'_{-i}$ are further i.i.d. copies of $D$ and $\mathbb P(\hat G = k) = 2^{-k}$, $k \ge 1$.

The per-period cost is $c\,q^E_{t-L_0} + G(I_{t+1})$ with $G(y) = h y^+ + b y^-$, where $b, h > 0$ and $c > 0$ is the express premium (the regular unit cost is normalized to $0$). An admissible policy $\pi \in \Pi$ chooses the two orders in period $t$ as deterministic measurable functions of $(q^R_{t-L}, \dots, q^R_{t-1}, q^E_{t-L_0}, \dots, q^E_{t-1}, I_t)$. Its long-run average cost is

$$C(\pi) = \limsup_{T\to\infty}\frac1T\sum_{t=L_0+1}^T \mathbb E[C^\pi_t], \qquad \mathrm{OPT}(L) = \inf_{\pi\in\Pi}C(\pi).$$

With the expedited inventory position $\hat I_t = I_t + \sum_{k=t-L_0}^{t-1}q^E_k + \sum_{k=t-L}^{t-L+L_0}q^R_k$, the TBS policy $\pi_{r,S}$ orders $q^R_t = r$ and $q^E_t = \max(0, S - \hat I_t)$. A best TBS pair $(r^*, S^*)$ minimizes $C(\pi_{r,S})$ over $0 \le r \le \mathbb E[D]$ and $S \in \mathbb R$ (first in $r$ through $F^\infty(r) = \inf_S C(\pi_{r,S})$, then in $S$).

The constants $\epsilon_0$ and $Y_0$ are explicit functionals of the law of $D$ and of $L_0, b, h, c$. They are built from $g = \inf_x\mathbb E[G(x - \sum_{i=1}^{L_0+1}D'_i)]$, $U = c\,\mathbb E[D] + \mathbb E[G(-\sum_{i=1}^{L_0+1}D'_i)]$, $p_0 = \mathbb P(D < \mathbb E[D])$, the mean absolute deviation $\eta_0$, and the large-deviation quantities $\gamma_\epsilon, \vartheta_\epsilon$ of $\phi_\epsilon(\theta) = e^{\theta(\mathbb E[D]-\epsilon)}\mathbb E[e^{-\theta D}]$ (p. 441).

Formalization targets

Goal: Theorem 1 (p. 441)

For all $L_0 \ge 0$, $\epsilon \in (0,1)$ and $L > \epsilon_0^{-2} + Y_0\epsilon^{-2}$,

$$\frac{C(\pi_{r^*,S^*})}{\mathrm{OPT}(L)} < 1 + \epsilon.$$

The threshold does not depend on $L$, so the statement gives an explicit, inverse-polynomial rate. Its limit form $C(\pi_{r^*,S^*})/\mathrm{OPT}(L) \to 1$ is Corollary 1 of the paper.

Milestones

In the order the proof uses them:

• the bound $g \le \mathrm{OPT}(L) \le U$;
• Lemma 1, the reduction to $\hat\Pi$ (quoted from Sheopuri et al.);
• Eq. (3), the TBS cost formula $C(\pi_{r,S}) = c(\mathbb E[D]-r) + \mathbb E[G(I^r_\infty + S - \sum_{i=1}^{L_0+1}D'_i)]$ (quoted from JSS);
• Theorem 2, the existence of a stationary-like vector $(\chi^{*,L}, q^{*,L}, \mathcal I^{*,L})$ with $r_L = \mathbb E[\chi^{*,L}_1]$;
• Corollary 2 and Lemma 2, the lower bound $\mathrm{OPT}(L) \ge c(\mathbb E[D]-r_L) + (1-\alpha)V^{L-L_0}_\alpha(r_L,-\infty)$ through a discounted single-source problem;
• Lemma 3, the Bellman equation and structure of that problem (quoted from JSS and Scarf 1960);
• Lemma 4 (8) and (9), and Corollary 3, the passage to the infinite horizon and to base-stock policies;
• Lemma 5, the random-walk maxima $M^r_k$ (proof omitted in the paper);
• Lemmas 8–9 and Corollary 4: $r_L < \mathbb E[D] - \epsilon_0$ once $L > \epsilon_0^{-2} + L_0 + 1$.

Significance

The theorem shows that one of the simplest dual-sourcing heuristics is asymptotically optimal as the regular lead time grows. This is the regime where exact dynamic programming is hopeless. The best TBS parameters come from a convex program independent of $L$, so the result yields an algorithm whose running time does not grow with $L$ and whose optimality gap is bounded explicitly for every finite $L$. It extends the lower-bounding technique of Xin and Goldberg's lost-sales work (Operations Research 2016) from a static to a dynamic relaxation.

Formalization adds the following. To the best of available knowledge, none of the objects involved (average-cost inventory control with backlog, TBS policies, Lindley-type maxima of random walks with their Spitzer identity) exists in Mathlib or on the platform. The paper's proof defers several ingredients to the literature or omits them: Lemma 1, Eq. (3), Lemma 3, and the details of Lemmas 5 and 7. A complete formal proof must supply them. The result is proved on paper but not formalized anywhere.

Difficulty

An optimal dual-sourcing policy need not be stationary, its induced Markov chain need not have a stationary distribution, and the inventory is unbounded below. The natural argument would compare the optimal policy's steady state with the TBS steady state, and it fails at its first step. Theorem 2 replaces the steady state by a vector with a few distributional properties, built from time averages. That construction, and the independence structure it must carry, is the central technical step. The conditional Jensen step then leads to a single-source problem with possibly negative demand, where textbook interchange-of-limits theorems do not apply directly. Finally, bounding $r_L$ away from $\mathbb E[D]$ requires a quantitative lower bound on the growth of random-walk maxima under only a first-moment assumption.

Formalization scope

Conventions of the Lean development (namespace XinGoldbergTBS.Asymptotic):

• The law of $D$ is a probability measure on $\mathbb R$ with no mass on $(-\infty,0)$, finite mean, and no atom of mass $1$. The paper's "strictly positive (possibly infinite) variance" is read as "not almost surely constant".
• $c_R = 0$, $b > 0$, $h > 0$, $c > 0$, and $L, L_0$ are natural numbers. The paper's standing assumption $L > L_0 + 1$ is a hypothesis wherever the paper states it; in Theorem 1 it follows from the threshold.
• Costs, expectations, $C(\pi)$, $\mathrm{OPT}(L)$, $V^n_\alpha$ and $V^\infty_\alpha$ take values in $[0,\infty]$, so infinite costs are never truncated. The ratio in Theorem 1 is stated as $C(\pi_{r^*,S^*}) < (1+\epsilon)\mathrm{OPT}(L)$, which is equivalent because $0 < g \le \mathrm{OPT}(L) \le U < \infty$.
• $\Pi$ is exactly the paper's class: deterministic, time-dependent, measurable, nonnegative orders that depend on the pipeline and inventory. It is neither restricted to stationary policies nor enlarged to randomized ones. TBS policies are members, so $C(\pi_{r,S}) \ge \mathrm{OPT}(L)$ by construction.
• $\vartheta_\epsilon \in [0,\infty]$ is the supremum of the minimizers of $\phi_\epsilon$ on $[0,\infty)$, and it is $\infty$ if the infimum is not attained; $1/\infty = 0$.
• The existence of a best TBS pair is asserted in the paper via JSS. The goal therefore also asserts that some TBS policy with $0 \le r \le \mathbb E[D]$ meets the bound, so it cannot hold vacuously when no minimizer exists.
• $r_L$ belongs to a witness of Theorem 2, and the results that use it hold for every witness.
• The single-source class $\bar\Pi$ ("feasible nonanticipative policies, as typically defined") is read as nonnegative orders that are measurable functions of past demands. In Lemma 3 "increasing" is read as nondecreasing, and convexity in $x$ includes finiteness.
• The paper states Eq. (3) without a range for $r$; it is stated here for $0 \le r \le \mathbb E[D]$, the TBS parameters over which the paper optimizes. At $r = \mathbb E[D]$ both sides are $+\infty$. In Lemma 8, the range's upper end is $+\infty$ when $\epsilon = 0$.
• Differences such as $V^\infty_\alpha - V^n_\alpha$ and $M^r_\infty - M^r_n$ are stated additively, and the negative terms of (9) and Corollary 3 are moved to the other side.

Lemma 1, Eq. (3) and Lemma 3 are results the paper quotes from Sheopuri et al. (2010), JSS and Scarf (1960). Proposition 1 (conditional-expectation form of the bound) is not included.

A trivializing formalization is ruled out: $\mathrm{OPT}(L)$ ranges over the full admissible class, the constants are definitions rather than hypotheses, and the goal includes an existence clause.

Reusable beyond this mission: average-cost inventory models with lead times, discounted single-source backlog value functions, and Spitzer-type identities for random-walk maxima. Contributions to any milestone are welcome.

Selected references

• L. Xin and D. A. Goldberg, Asymptotic Optimality of Tailored Base-Surge Policies in Dual-Sourcing Inventory Systems, Management Science 64(1):437–452, 2018. https://doi.org/10.1287/mnsc.2016.2607
• G. Janakiraman, S. Seshadri and A. Sheopuri, Analysis of Tailored Base-Surge Policies in Dual Sourcing Inventory Systems, Management Science 61(7):1547–1561, 2015.
• G. Allon and J. A. Van Mieghem, Global Dual Sourcing: Tailored Base-Surge Allocation to Near- and Offshore Production, Management Science 56(1):110–124, 2010.
• A. Sheopuri, G. Janakiraman and S. Seshadri, New Policies for the Stochastic Inventory Control Problem with Two Supply Sources, Operations Research 58(3):734–745, 2010.
• H. Scarf, The Optimality of (s, S) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960, pp. 196–202.
• L. Xin and D. A. Goldberg, Optimality Gap of Constant-Order Policies Decays Exponentially in the Lead Time for Lost Sales Models, Operations Research 64(6):1556–1565, 2016.

Motivation

Many engineered systems switch between a finite number of operating modes at random times: a power grid after a line failure, a networked controller whose links drop, a manufacturing plant whose machines break down and are repaired. A standard model for such systems is a hybrid stochastic differential equation, also called an SDE with Markovian switching: the state follows an Itô equation whose coefficients depend on a mode that evolves as a continuous-time Markov chain. The monograph of Mao and Yuan (Stochastic Differential Equations with Markovian Switching, 2006) develops the stability theory of these equations.

A controller that stabilizes such a system usually needs the current state. In practice the state is sampled: it is observed at times $0,\tau,2\tau,\dots$ and the control is held between observations. Mao (Automatica 49, 2013) showed that, under a global Lipschitz condition on the drift and diffusion, a feedback control based on discrete-time observations stabilizes a hybrid SDE in the sense of mean-square exponential stability when $\tau$ is small enough. You, Liu, Lu, Mao and Qiu (SIAM J. Control Optim. 53(2), 2015) replaced that condition by local Lipschitz continuity plus linear growth, gave an explicit bound (3.5) on the admissible observation interval $\tau$, and proved $H_\infty$-stability, mean-square asymptotic stability, almost sure asymptotic stability and exponential stability of the controlled system. This mission formalizes the almost sure asymptotic stability result, Theorem 3.4, and the results it is built on.

Setting

Let $(\Omega,\mathcal F,\{\mathcal F_t\}_{t\ge0},\mathbb P)$ be a probability space with a filtration satisfying the usual conditions (increasing, right-continuous, $\mathcal F_0$ contains the null sets). On it live an $m$-dimensional $\{\mathcal F_t\}$-Brownian motion $w$ and a right-continuous $\{\mathcal F_t\}$-Markov chain $r$ on $S=\{1,\dots,N\}$ with generator $\Gamma=(\gamma_{ij})$ ($\gamma_{ij}\ge0$ for $i\ne j$, zero row sums), independent of $w$. Fix $\tau>0$ and the sampling time $\delta_t=[t/\tau]\tau$, the last observation time up to $t$. The controlled system is

$$dx(t)=\big(f(x(t),r(t),t)+u(x(\delta_t),r(t),t)\big)dt+g(x(t),r(t),t)\,dw(t),\qquad x(0)=x_0,\ r(0)=r_0,\tag{2.1}$$

with $f,u:\mathbb R^n\times S\times\mathbb R_+\to\mathbb R^n$ and $g:\mathbb R^n\times S\times\mathbb R_+\to\mathbb R^{n\times m}$. The feedback $u$ sees the state only at the observation times.

The hypotheses are:

• Assumption 2.1: $f,g$ locally Lipschitz in $x$, and $|f(x,i,t)|\le K_1|x|$, $|g(x,i,t)|\le K_2|x|$ ($|g|$ the trace norm).
• Assumption 2.2: $|u(x,i,t)-u(y,i,t)|\le K_3|x-y|$ and $u(0,i,t)=0$.
• Assumption 3.1: there are $U\in C^{2,1}(\mathbb R^n\times S\times\mathbb R_+;\mathbb R_+)$ and $\lambda_1,\lambda_2>0$ with $\mathcal LU(x,i,t)+\lambda_1|U_x(x,i,t)|^2\le-\lambda_2|x|^2$, where

$$\mathcal LU=U_t+U_x[f+u]+\tfrac12\operatorname{trace}[g^TU_{xx}g]+\sum_j\gamma_{ij}U(x,j,t).$$

• Condition (3.5): $\lambda_2>\frac{\tau K_3^2}{\lambda_1}\big[2\tau(K_1^2+2K_3^2)+K_2^2\big]$ and $\tau\le\frac1{4K_3}$.

In Lean these are Assumption21, Assumption22, C21, LU, Assumption31, Condition35, in the namespace You2015.Asymp; the basis is HybridSetup, the Itô integral IsItoIntegral, the sampling time delta, and solutions SolvesSampledHybridSDE, in the namespace You2015.Shared shared with the companion mission.

Formalization targets

Goal: Theorem 3.4 (almost sure asymptotic stability)

Under the hypotheses above, every solution of (2.1) satisfies

$$\lim_{t\to\infty}x(t)=0\quad\text{a.s.}$$

for all $x_0\in\mathbb R^n$ and $r_0\in S$. No rate is claimed; the statement is the qualitative convergence of almost every path.

Milestones, in the order the proof uses them

1. (3.15) $\mathbb E|x(t)-x(\delta_t)|^2\le2\mathbb E\int_{\delta_t}^t[\tau|f+u(x(\delta_s),\cdot)|^2+|g|^2]ds$.
2. Theorem 3.2 ($H_\infty$-stability): $\int_0^\infty\mathbb E|x(s)|^2ds<\infty$.
3. (3.21) $\mathbb E|x(s)-x(\delta_s)|^2\le\frac{3(\tau K_1^2+K_2^2)}{1-6\tau^2K_3^2}\int_{\delta_s}^s\mathbb E|x(z)|^2dz+\frac{6\tau^2K_3^2}{1-6\tau^2K_3^2}\mathbb E|x(s)|^2$.
4. (3.23) $\sup_{t\ge0}\mathbb E|x(t)|^2<\infty$.
5. $|\mathbb E|x(t_2)|^2-\mathbb E|x(t_1)|^2|\le C(t_2-t_1)$.
6. Theorem 3.3: $\lim_{t\to\infty}\mathbb E|x(t)|^2=0$.
7. (3.24)–(3.25): $\mathbb E\int_0^\infty|x(t)|^2dt<\infty$ and $\liminf_{t\to\infty}|x(t)|=0$ a.s.
8. (3.28): $\mathbb P(\exists t:|x(t)|\ge h)\le C/h^2$ for $h>|x_0|$.

Significance

The result. Theorem 3.4 says that a controller sampling the state at rate $1/\tau$ makes almost every trajectory of the switching system converge to the equilibrium, with an explicit, checkable bound (3.5) on $\tau$. Mean-square convergence (Theorem 3.3) does not imply almost sure convergence in general, and a single trajectory is what an operator observes, so the pathwise statement is the one relevant to a deployed system. Condition (3.5) is stated in terms of the constants of Assumptions 2.1, 2.2 and 3.1, so for a concrete system (Section 6 of the paper) it gives a numerical bound on the observation interval.

Formalizing it. The results are proved in the paper; none of them is machine-checked. Mathlib has real Brownian motion but no Itô integral, no stochastic differential equations and no continuous-time Markov chains. The mission therefore also produces a reusable definition layer: a filtration under the usual conditions, a multidimensional $\{\mathcal F_t\}$-Brownian motion, an $\{\mathcal F_t\}$-Markov chain with a given generator, the $L^2$ Itô integral of vector-valued integrands, and the solution notion of an SDE with Markovian switching and a sampled-state delay. A related but different layer exists on Prove2Me for Ethier–Kurtz (EthierKurtz_IsStandardBrownian, EthierKurtz_HasBrownianItoIntegral, EthierKurtz_SolvesBrownianSDE); it has no mode switching and no sampled state, so it cannot express (2.1).

Difficulty

Equation (2.1) is a stochastic differential delay equation with the delay $t-\delta_t$, which is bounded but jumps at every observation time and has derivative $1$ in between. The stability theorems for hybrid delay equations in the literature require a differentiable delay with derivative less than one (Mao–Yuan, p. 285), so they do not apply. Applying $\mathcal LU$ directly to $U(x(t),r(t),t)$ leaves the term $U_x[u(x(t))-u(x(\delta_t))]$, which has no sign and depends on the path over a whole observation interval, so a Lyapunov function of the current state alone does not close the argument.

For the goal, the natural first idea, deducing almost sure convergence from $\mathbb E|x(t)|^2\to0$ or from $\int_0^\infty|x(t)|^2dt<\infty$ a.s., fails: both are compatible with paths that make ever shorter excursions away from $0$. The obstacle is to exclude infinitely many excursions of a fixed size, which neither moment statement controls.

Formalization scope

Conventions committed to in Lean:

• The state space is EuclideanSpace ℝ (Fin n), so $|x|$ is the Euclidean norm; the explicit constants in (3.5) and (3.21) depend on it. The diffusion $g$ is given by its $m$ columns and $|g|^2=\sum_k|g_k|^2$ (trace norm). Modes are Fin N (0-based). Time is ℝ≥0; time integrals are over subsets of $\mathbb R$ at s.toNNReal.
• Every expectation $\mathbb E|\cdot|^2$ and every time integral of a nonnegative quantity is a lower Lebesgue integral in $[0,\infty]$, so a non-integrable process cannot produce a junk value $0$.
• "The solution of (2.1)" is read as every process satisfying the solution definition: progressively measurable, almost surely continuous paths, $\mathbb E|x(t)|^2<\infty$ for each $t$, and for each $t$, almost surely, the integral equation with Itô integrals in the $L^2$ sense. Existence and uniqueness (cited from Mao–Yuan on p. 908) are not asserted.
• "An $m$-dimensional Brownian motion" and "a Markov chain with generator $\Gamma$" are read in the Mao–Yuan framework the paper cites: an $\{\mathcal F_t\}$-Brownian motion with independent coordinates and increments independent of the past, and an $\{\mathcal F_t\}$-Markov chain with transition matrix $e^{t\Gamma}$. The usual conditions are kept as hypotheses.
• "Locally Lipschitz" is uniform in the mode and time on each ball. $C^{2,1}$ carries its derivatives $U_t,U_x,U_{xx}$ as witnesses tied to $U$ by derivative relations and joint continuity.
• "$\tau>0$ sufficiently small for (3.5)" means every $\tau>0$ satisfying both inequalities of (3.5). $U,\lambda_1,\lambda_2,\tau$ are data of each statement. The paper's "$C$ denotes a positive constant" is an existential chosen after $x_0$, $r_0$ and the solution, and before the time variables and $h$.
• (3.15) and (3.21) are stated under fewer hypotheses than the surrounding proof has (Assumptions 2.1, 2.2, $\tau>0$, and for (3.21) $\tau\le1/(4K_3)$), because their derivations use no more. Misprints on the page (for example $g(x,i,s)=f(x,i,0)$ on p. 909 and the swapped definitions of $\vee,\wedge$ on p. 907) are not formalized.

A trivializing formalization is ruled out: the expectations are not Bochner integrals (which vanish for non-integrable integrands), the solution notion admits the true solution and requires path continuity, the derivative witnesses of $U$ are tied to $U$, and a sorry-free check shows that the data hypotheses (Assumptions 2.1, 2.2, 3.1, $C^{2,1}$, (3.5)) are satisfiable, for example by $n=m=N=1$, $f=g=0$, $u(x)=-x$, $U=|x|^2$, $\lambda_1=1/4$, $\lambda_2=1$, $\tau=1/10$.

Welcome contributions: the Itô isometry and Itô's formula for the $L^2$ integral defined here, a generalized Itô formula for functions of a Markov-modulated Itô process, and Doob's maximal inequality in continuous time. These are reusable far beyond this mission. Section 4 of the paper (exponential stability) is a separate mission of the same series.

Selected references

• S. You, W. Liu, J. Lu, X. Mao, Q. Qiu, Stabilization of Hybrid Systems by Feedback Control Based on Discrete-Time State Observations, SIAM J. Control Optim. 53(2), 905–925, 2015. https://doi.org/10.1137/140985779
• X. Mao, C. Yuan, Stochastic Differential Equations with Markovian Switching, Imperial College Press, 2006. https://doi.org/10.1142/p473
• X. Mao, Stabilization of continuous-time hybrid stochastic differential equations by discrete-time feedback control, Automatica 49(12), 3677–3681, 2013. https://doi.org/10.1016/j.automatica.2013.09.005