Operations Research

Why online linear programming under random order

Many resource-allocation problems are decided one request at a time: a seller of airline seats or hotel nights, an ad platform allocating advertiser budgets, a network operator admitting bandwidth requests. Each request asks for a bundle of resources and offers a price. It must be accepted or rejected on arrival, before the later requests are seen. The online linear program is the common model. If the order of arrivals is adversarial, no online algorithm can guarantee more than an $O(1/n)$ fraction of the offline optimum (Babaioff et al. 2008). Under the weaker random permutation model the adversary picks the requests but not their order, and near-optimal guarantees are possible.

Timeline, as surveyed in §1.3 of the paper. Kleinberg (2005) gave a $1-O(1/\sqrt B)$ competitive algorithm for the one-dimensional multiple-choice secretary problem and showed that this ratio is best possible, so $B\ge1/\varepsilon^2$ is necessary for a $1-O(\varepsilon)$ ratio. Devanur and Hayes (2009) solved a linear program once and used its dual solution as a threshold price for the AdWords problem, with ratio $1-O(\sqrt[3]{\pi_{\max}m^2\log n/\mathrm{OPT}})$. Feldman et al. (2010) extended one-time learning to general online packing, with a ratio depending on both $B$ and $\mathrm{OPT}$ and of order $1-O(\sqrt[3]{m\log n/B})$ in $B$. Agrawal, Wang and Ye (Oper. Res. 2014) re-learn the dual price every time the history doubles and obtain $1-O(\sqrt{m\log n/B})$, a guarantee that depends on $B$ alone and matches Kleinberg's dependence on $B$ up to the factor $m\log n$.

Setting

An instance has $n$ columns and $m\ge1$ constraints. Column $t$ carries an objective coefficient $\pi_t\ge0$ and a constraint column $a_t=(a_{1t},\dots,a_{mt})\in[0,1]^m$, and $b\in\mathbb R^m$ is the right-hand side. The offline program is

$$\mathrm{OPT}=\max\Big\{\sum_{t=1}^n\pi_tx_t:\ \sum_{t=1}^na_{it}x_t\le b_i\ (i=1,\dots,m),\ 0\le x_t\le1\Big\}.$$

In the random permutation model the columns arrive in the order of a uniformly random permutation $\sigma$ of $\{1,\dots,n\}$, and $n$ is known in advance. At time $t$ the algorithm sees $(\pi_t,a_t)$ and must fix $x_t$ so that $\sum_{j\le t}a_{ij}x_j\le b_i$ for every $i$. An algorithm is $c$-competitive if $\mathbb E_\sigma[\sum_t\pi_tx_t]\ge c\cdot\mathrm{OPT}$. Inputs are assumed in general position: for any price vector $p\in\mathbb R^m$ at most $m$ columns satisfy $p^\top a_t=\pi_t$.

For a price vector $p$ the threshold rule sets $x_t(p)=1$ if $\pi_t>p^\top a_t$ and $x_t(p)=0$ otherwise. Fix $\varepsilon=2^{-E}$ with $\varepsilon n$ an integer, and let $L=\{\varepsilon n,2\varepsilon n,\dots,2^{E-1}\varepsilon n\}$ and $h_\ell=\varepsilon\sqrt{n/\ell}$. For $\ell\in L$, $\hat p^{\ell}$ is an optimal dual price of the partial program

$$\max\sum_{t=1}^{\ell}\pi_tx_t\quad\text{s.t.}\quad\sum_{t=1}^{\ell}a_{it}x_t\le(1-h_\ell)\tfrac{\ell}{n}b_i,\quad0\le x_t\le1 .$$

The dynamic learning algorithm (DLA) accepts nothing up to time $\varepsilon n$. At a time $t\in(\ell,2\ell]$ it proposes $x_t(\hat p^{\ell})$ and executes the proposal unless a constraint would be violated, in which case $x_t=0$. $\mathrm{OPT}_s(d)$ is the optimal value of the program on the first $s$ arrivals with right-hand side $d$.

Formalization targets

Goal: Theorem 1

There are absolute constants $C_1,C_2>0$ such that, whenever $B=\min_ib_i\ge C_1m\log(n/\varepsilon)/\varepsilon^2$,

$$\mathbb E_\sigma\Big[\sum_{t=1}^n\pi_tx_t^{\mathrm{DLA}}\Big]\ge(1-C_2\varepsilon)\,\mathrm{OPT}.$$

The constants are left unfixed, so the target states only the shape of the result, $1-O(\varepsilon)$ under $B\ge\Omega(m\log(n/\varepsilon)/\varepsilon^2)$, and survives any improvement of the constants.

Milestones

1. Lemma 1 (p. 881). For an optimal primal $x^*$ and an optimal dual price $p^*$, $x_t(p^*)\le x^*_t$ for every $t$, and under general position the two differ in at most $m$ places.
2. Lemma 10 (p. 887). The Hoeffding–Bernstein inequality for sampling without replacement: $\mathbb P(|\sum_{i\le r}u_i-r\bar c|\ge t)\le2\exp(-t^2/(2r\sigma_R^2+t\Delta_R))$.
3. Lemma 5 (p. 884). With probability $1-\varepsilon$, $\sum_{t=\ell+1}^{2\ell}a_{it}x_t(\hat p^\ell)\le\frac{\ell}{n}b_i$ for all $i$ and all $\ell\in L$.
4. Lemma 6 (p. 884). With probability $1-\varepsilon$, $\sum_{t\le2\ell}\pi_tx_t(\hat p^\ell)\ge(1-2h_\ell-\varepsilon)\,\mathrm{OPT}_{2\ell}(\frac{2\ell}{n}b)$ for all $\ell\in L$.
5. Lemma 7 (p. 884). $\mathbb E[\mathrm{OPT}_\ell(\frac{\ell}{n}b)]\le\frac{\ell}{n}\mathrm{OPT}$.
6. Final display of the proof of Theorem 1 (p. 885). $\sum_{\ell\in L}\ell/n=1-\varepsilon$ and $\sum_{\ell\in L}h_\ell\ell/n\le2.5\varepsilon$.

Lemmas 5 and 6 carry the paper's condition $B\ge10m\log(n/\varepsilon)/\varepsilon^2$ with the $10$ replaced by an absolute constant; their probabilities and bounds are exact.

Significance

Theorem 1 gives a $1-O(\varepsilon)$ guarantee for general online packing linear programs under a requirement on $B$ alone that grows as $1/\varepsilon^2$, the order Kleinberg showed necessary. Together with the paper's Theorem 2, which shows that $B$ of order $\log m/\varepsilon^2$ is necessary, it fixes the dependence on $\varepsilon$ and shows that a dependence on $m$ cannot be avoided. The paper notes (§5.2) that the guarantee transfers to online integer programs, because the threshold rule outputs integral decisions.

The result is proved on paper but has no machine-checked proof. A formalization adds three things. It gives a verified statement of the exact model: random order as an average over permutations, the online feasibility rule, and the selection among non-unique dual optima. It settles the constants: the paper's proof aims at $C_1=10$, $C_2=15$, but its union-bound step does not close with $10$, and a formal proof will record constants that do. Finally, it produces reusable infrastructure: complementary slackness for box-constrained packing programs and a Bernstein inequality for sampling without replacement.

Difficulty

The algorithm is simple. The analysis is not. The learned price $\hat p^\ell$ depends on the same random sample whose later behaviour must be controlled, so no fixed-price concentration bound applies directly. A statement uniform over all prices is needed, and prices must be grouped by the decision patterns they induce, which calls for a combinatorial count of those patterns. The concentration tool itself is not in Mathlib: Mathlib's Hoeffding inequality is for independent summands, and samples drawn without replacement are dependent. On top of these, the per-period bounds have to be combined with the algorithm's executed decisions. Those decisions differ from the threshold decisions whenever a constraint would be violated, and the loss has to be charged to an event of probability at most $2\varepsilon$.

Formalization scope

Columns are Fin n, constraints are Fin m, and all data are real. Time is 0-based in Lean: Lean time $\tau$ is the paper's time $\tau+1$. The arrival order is a permutation $\sigma$ of Fin n, with column $\sigma(\tau)$ arriving at time $\tau$. Every expectation and probability over the order is a finite average over all $n!$ permutations. No measure theory is involved. $\mathrm{OPT}$ and $\mathrm{OPT}_s(d)$ are real suprema over feasible sets that are nonempty and bounded whenever $d\ge0$, and every statement uses them only at such $d$. The standing assumptions $\varepsilon=2^{-E}$ with $E\ge1$, $2^E\mid n$ with $n\ge1$, $m\ge1$ and general position (for any price vector, as in the paper) are hypotheses. $\log$ is the natural logarithm.

Optimal dual prices are not unique. The DLA is therefore parametrized by a dual-selection rule, and the theorems hold for every valid rule: one that returns an optimal dual price of the partial program and whose output depends only on the first $\ell$ arrivals. A rule that may return an arbitrary price, or that looks at future arrivals, is excluded. The conclusion of the goal is a lower bound $(1-C_2\varepsilon)\,\mathrm{OPT}$ with absolute constants quantified before every instance parameter. It is not satisfied by the algorithm that accepts nothing, and no hypothesis restricts $b$ from above.

A complete development needs LP duality and complementary slackness for finite linear programs, a Bernstein-type inequality for sampling without replacement (reusable well beyond this mission), a bound on the number of threshold patterns induced by price vectors, and the combinatorics of uniformly random prefixes of a permutation. Contributions of any of these as standalone results are welcome.

Selected references

• S. Agrawal, Z. Wang, Y. Ye, A Dynamic Near-Optimal Algorithm for Online Linear Programming, Operations Research 62(4):876–890, 2014. https://doi.org/10.1287/opre.2014.1289
• R. Kleinberg, A multiple-choice secretary algorithm with applications to online auctions, SODA 2005. https://dl.acm.org/doi/10.5555/1070432.1070519
• N. Devanur, T. Hayes, The AdWords problem: online keyword matching with budgeted bidders under random permutations, ACM EC 2009. https://doi.org/10.1145/1566374.1566384
• J. Feldman, M. Henzinger, N. Korula, V. Mirrokni, C. Stein, Online stochastic packing applied to display ad allocation, ESA 2010. https://doi.org/10.1007/978-3-642-15775-2_16
• M. Babaioff, N. Immorlica, D. Kempe, R. Kleinberg, Online auctions and generalized secretary problems, SIGecom Exchanges 7(2), 2008. https://doi.org/10.1145/1399589.1399596
• A. W. van der Vaart, J. A. Wellner, Weak Convergence and Empirical Processes, Springer, 1996. https://doi.org/10.1007/978-1-4757-2545-2

Motivation

Interior-point methods solve linear programs by moving through the interior of the feasible region instead of along its edges, as the simplex method does. The methods used in practice are path-following methods: they track a curve, the central path, that runs through the interior of the feasible region and ends at an optimal solution. Before any such method can be analysed, the curve has to exist. This mission formalizes Chapter 17 of R. J. Vanderbei, Linear Programming: Foundations and Extensions (4th ed., Springer 2014), which defines the central path through the logarithmic barrier problem and proves that it exists exactly when the primal and the dual problem both have strictly positive feasible points.

The chapter's results have a short history. Barrier methods for nonlinear programming go back to Fiacco and McCormick (1968). Interest in interior-point methods for linear programming began with Karmarkar (1984), whose projective algorithm does not mention a central path; the connection between Karmarkar's method and the primal–dual central path was found by Megiddo (1989), with central points traced back to Huard (1967) and an extended study of the path by Bayer and Lagarias (1989). The chapter is the textbook entry point to this line of work and the foundation for the path-following algorithm of Chapter 18.

Setting

Let $A$ be a real $m \times n$ matrix, $b \in \mathbb{R}^m$ and $c \in \mathbb{R}^n$. The primal linear program is to maximize $c^T x$ subject to $Ax \le b$, $x \ge 0$; its dual is to minimize $b^T y$ subject to $A^T y \ge c$, $y \ge 0$. With slack variables $w \in \mathbb{R}^m$ and $z \in \mathbb{R}^n$ they read (17.1)

$$Ax + w = b,\ x, w \ge 0 \qquad\text{and}\qquad A^T y - z = c,\ y, z \ge 0.$$

For a vector $\xi$, $\xi > 0$ means that every component is strictly positive. The primal feasible region has nonempty interior when some $(\bar x, \bar w)$ satisfies $A\bar x + \bar w = b$ with $\bar x > 0$, $\bar w > 0$; the dual feasible region has nonempty interior when some $(\bar y, \bar z)$ satisfies $A^T \bar y - \bar z = c$ with $\bar y > 0$, $\bar z > 0$.

For a parameter $\mu > 0$, the barrier function (17.7) is

$$f(x, w) = c^T x + \mu \sum_{j=1}^n \log x_j + \mu \sum_{i=1}^m \log w_i ,$$

and the barrier problem (17.2) is to maximize $f(x, w)$ subject to $Ax + w = b$, over the domain $x > 0$, $w > 0$ where the logarithms are finite. A solution of the barrier problem is a point of that domain at which $f$ attains its maximum over the domain.

Writing $X, Z, Y, W$ for the diagonal matrices carrying $x, z, y, w$ and $e$ for the all-ones vector, the primal–dual central-path system (17.6) is

$$Ax + w = b, \qquad A^T y - z = c, \qquad XZe = \mu e, \qquad YWe = \mu e,$$

with $x, w, y, z > 0$. The last two equations say $x_j z_j = \mu$ and $y_i w_i = \mu$ for all $j$ and $i$. The set of its solutions $(x_\mu, w_\mu, y_\mu, z_\mu)$, $\mu > 0$, is the primal–dual central path.

The chapter also uses one fact from nonlinear programming: for the problem "maximize $f(x)$ subject to $g_i(x) = 0$, $i = 1, \dots, m$", a critical point is a feasible $x^*$ with $\nabla f(x^*) = \sum_i y_i \nabla g_i(x^*)$ for some Lagrange multipliers $y_i$ (17.3), and $H_f(x^*)$ is the Hessian of $f$ at $x^*$.

Formalization targets

Goal: Theorem 17.2 (p. 265)

For each fixed $\mu > 0$,

$$\exists\, (x, w) \text{ solving the barrier problem} \iff \big(\exists\, \bar x, \bar w > 0 : A\bar x + \bar w = b\big) \wedge \big(\exists\, \bar y, \bar z > 0 : A^T\bar y - \bar z = c\big).$$

Both directions are part of the goal. The statement fixes no constants and no rate; it asserts only when the barrier problem is solvable.

Milestones

1. Theorem 17.1 (p. 261), second-order sufficiency under linear constraints: if the constraints are linear, a critical point $x^*$ with $\xi^T H_f(x^*)\xi < 0$ for every $\xi \ne 0$ satisfying $\xi^T \nabla g_i(x^*) = 0$ for all $i$ is a local maximum on the feasible set.
2. Exercise 10.7 (p. 150): if the primal is feasible and its feasible set $\{x : Ax \le b,\ x \ge 0\}$ is bounded, then there are $y > 0$, $z > 0$ with $A^T y - z = c$.
3. Corollary 17.3 (p. 266): if the primal feasible set (or the dual feasible set) has nonempty interior and is bounded, then for each $\mu > 0$ the system (17.6) has exactly one solution with $x, w, y, z > 0$.

The corollary is stronger than the goal in one direction (it adds uniqueness and the dual variables) and weaker in another (it assumes boundedness).

Significance

The result itself. Theorem 17.2 gives an exact criterion for the barrier problem to be solvable for a fixed $\mu$, and Corollary 17.3 turns it into the statement that the central path is a well-defined curve $\mu \mapsto (x_\mu, w_\mu, y_\mu, z_\mu)$ for all $\mu > 0$. Every path-following method, including the one analysed in Chapter 18 of the same book, targets points on this curve; without existence and uniqueness the "target" of an iteration is undefined. The system (17.6) is also the starting point of the primal–dual Newton step.

Formalizing it. These results are classical and proved in the book; none is formalized in the $Ax \le b$, $x \ge 0$ form used here. The platform has the converse fact in the standard form $Ax = b$, $x \ge 0$ (a solution of the central-path conditions minimizes the barrier, Introduction to Linear Optimization), but not existence. A formal proof of Theorem 17.2 and Corollary 17.3 produces a reusable existence theorem for the central path that downstream missions on path-following and self-dual methods can import.

Difficulty

The "if" direction of Theorem 17.2 is an existence claim on a set that is neither closed nor bounded: the domain $x > 0$, $w > 0$ is open, and the feasible region itself may be unbounded, so the obvious appeal to "a continuous function on a compact set attains its maximum" does not apply directly. The example "maximize $0$ subject to $x \ge 0$" (p. 264), whose barrier $\mu \log x$ has no maximum, shows that the dual hypothesis cannot be dropped. The "only if" direction, which the book calls trivial and does not prove, needs first-order conditions at a maximizer over a relatively open set.

Theorem 17.1 needs a second-order Taylor expansion with a remainder that is $o(\|\xi\|^2)$ uniformly along the constraint subspace, not along individual lines. Exercise 10.7 is a theorem of the alternative and is not a consequence of weak duality alone. Uniqueness in Corollary 17.3 requires the positivity of the solution: the equations $x_j z_j = \mu$, $y_i w_i = \mu$ admit sign-flipped solutions.

Formalization scope

Vectors are Fin n → ℝ and Fin m → ℝ; $A$ is a Matrix (Fin m) (Fin n) ℝ. The book's primal–dual pair in $Ax \le b$, $x \ge 0$ form with slacks is used throughout; there are no explicit constants in this chapter.

Conventions committed to:

• "Nonempty interior" means a feasible point with every component strictly positive, as the proof of Theorem 17.2 says. The topological interior of $\{(x, w) : Ax + w = b,\ x, w \ge 0\}$ in $\mathbb{R}^{n+m}$ is empty whenever $m \ge 1$; reading the theorem that way would make its right-hand side always false for $m \ge 1$, and that reading is ruled out.
• The barrier problem is posed over $x > 0$, $w > 0$ explicitly; Real.log returns $0$ at nonpositive arguments and is never evaluated there.
• Solutions of (17.6) are required to be strictly positive, as in Exercise 17.3 (p. 267).
• "Bounded" is Bornology.IsBounded of the feasible set in $\mathbb{R}^n$ (resp. $\mathbb{R}^m$).
• In Theorem 17.1 the constraints are $Gx = \beta$; $f$ is differentiable near $x^*$ with derivative differentiable at $x^*$, and $\xi^T H_f(x^*) \xi$ is the second Fréchet derivative applied to $(\xi, \xi)$. The local maximum is relative to the feasible set.

Infrastructure a complete development needs: attainment of maxima on compact sets (IsCompact.exists_isMaxOn in Mathlib), first-order conditions on relatively open sets, a theorem of the alternative for Exercise 10.7, and concavity facts about the logarithm. A second-order sufficient condition under affine constraints is not in Mathlib and is reusable beyond linear programming. Proofs of any milestone, including the "only if" half of the goal separately, are welcome contributions.

Selected references

• R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., International Series in Operations Research & Management Science 196, Springer, 2014, Chapter 17 and Exercise 10.7. https://doi.org/10.1007/978-1-4614-7630-6
• A. V. Fiacco and G. P. McCormick, Nonlinear Programming: Sequential Unconstrained Minimization Techniques, Wiley, 1968. https://doi.org/10.1137/1.9781611971316
• N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4 (1984), 373–395. https://doi.org/10.1007/BF02579150
• N. Megiddo, Pathways to the optimal set in linear programming, in Progress in Mathematical Programming, Springer, 1989, 131–158. https://doi.org/10.1007/978-1-4613-9617-8_8
• D. A. Bayer and J. C. Lagarias, The nonlinear geometry of linear programming I, II, Transactions of the AMS 314 (1989), 499–526 and 527–581. https://doi.org/10.1090/S0002-9947-1989-1005525-6

Motivation

The r-algorithm of N. Z. Shor is a variable-metric method for minimizing functions that are not differentiable everywhere, such as maxima of smooth functions, penalty functions and Lagrangian dual functions of integer and decomposition problems. It combines a subgradient step with a space dilation along the difference of two successive almost-gradients, and the book reports it competitive with the best variable-metric and conjugate-gradient methods on "gully"-shaped test problems (Shor 1985, §3.6, pp. 68–77). Its convergence theory is limited. Section 3.7 of Shor's book gives a convergence proof only for an idealized version with exact directional minimization, on a class of piecewise smooth functions, and the book itself calls a weakening of the assumptions and rate estimates desirable (p. 85). This mission formalizes that section.

Timeline. Shor and Zhurbenko introduced the r-algorithm in 1971 (Kibernetika, no. 3, 51–59). Shor analysed the convergence of its exact-line-search version in 1975 (Kibernetika, no. 4, 48–53). Section 3.7 of the 1979 Russian monograph, translated in 1985, gives that analysis for piecewise smooth functions. The book states on p. 85 that weaker assumptions and rate estimates would be desirable.

Setting

Let $E_n$ be $n$-dimensional Euclidean space with inner product $(x, y)$, $n \ge 1$. For a unit vector $\xi$ and $\alpha > 0$ the operator of space dilation is $R_\alpha(\xi)x = x + (\alpha - 1)(x, \xi)\xi$.

Widths. For a compact convex set $W$ and a unit vector $\eta$, the width in direction $\eta$ is $d_\eta(W) = \max_{x \in W}(\eta, x) - \min_{x \in W}(\eta, x)$. The width is $d(W) = \min_{\|\eta\| = 1} d_\eta(W)$ and the diameter is $D(W) = \max_{\|\eta\| = 1} d_\eta(W)$. With $e_\rho(W) = \inf_{z \in W}|(\rho, z)|$ put $K_\rho(W) = d_\rho(W)/e_\rho(W)$ (or $+\infty$ when $e_\rho(W) = 0$) and $p(W) = \inf_{\|\rho\| = 1} K_\rho(W)$.

The class $K$. $E_n$ is partitioned into closed sets $\bar D_1, \dots, \bar D_m$, each the closure of its interior, whose interiors are disjoint and homeomorphic to an open ball or open halfspace; $f_i$ is continuously differentiable on an open set containing $\bar D_i$; and $f = f_i$ on $\bar D_i$. At a point $x$, the set of almost-gradients $G_f(x)$ is the set of gradients $\nabla f_i(x)$ of the pieces with $x \in \bar D_i$. For $\delta, \varepsilon > 0$, $\bar P_{\delta,\varepsilon}(x)$ is the closed convex hull of all $G_f(y)$, $\|y - x\| < \delta$, together with the $\varepsilon$-balls around the elements of $G_f(x)$.

The $r(\alpha)$-algorithm. Fix $\alpha > 1$, $\beta = 1/\alpha$. Start from $x_0$, $\tilde g_0 = 0$ and a nonsingular $B_0$. At iteration $k + 1$ choose $g_f(x_k) \in G_f(x_k)$ with $(B_k^* g_f(x_k), \tilde g_k) \le 0$; set $g_k^* = B_k^* g_f(x_k)$, $r_k = g_k^* - \tilde g_k$, $\xi_{k+1} = r_k/\|r_k\|$, $B_{k+1} = B_k R_\beta(\xi_{k+1})$, $\tilde g_{k+1} = R_\beta(\xi_{k+1}) g_k^*$, and $x_{k+1} = x_k - h_{k+1}B_{k+1}\tilde g_{k+1}$ with $h_{k+1} \ge 0$ such that $f$ does not increase along the step and some almost-gradient at $x_{k+1}$ makes a non-acute angle with $\tilde g_{k+1}$ in the transformed metric. The standing assumption is $f(x) \to +\infty$ as $\|x\| \to \infty$ (3.50).

Formalization targets

Goal: convergence to an isolated local minimum (Theorem 3.13)

Assume (3.50) and $\|x_{k+1} - x_k\| \to 0$ (3.52). If $x^*$ is an isolated local minimum, the component of $\{x : f(x^*) \le f(x) \le f(x_0)\}$ containing $x_0$ also contains $x^*$, and no other point $z$ of that component has linearly dependent $G_f(z)$, then

$$\lim_{k \to \infty} x_k = x^* .$$

Milestones

• Lemma 3.2 (p. 80): for $B = SO$ with minimum eigenvalue $\lambda(B)$ of $S$, $\lambda(B)d(W) \le d(BW) \le \lambda(B)D(W)$.
• Lemma 3.3 (p. 80): for $z_1, z_2 \in W$, $0 < \beta \le 1$ and $\gamma = \|z_1 - z_2\|/d(W) \ge 1$,

$$d\Big(R_\beta\big(\tfrac{z_1 - z_2}{\|z_1 - z_2\|}\big)W\Big) \ge \frac{d(W)}{\sqrt{1 + (1-\beta^2)/(\beta^2\gamma^2)}} .$$

• Theorem 3.11 (p. 82): for every $\sqrt[n]{\beta} < v < 1$, $\varepsilon, \delta > 0$ and $r \ge 1$ there is $\bar k > r$ with

$$p\big(\bar P_{\delta,\varepsilon}(x_{\bar k})\big) \ge \sqrt{\frac{v^2\sqrt[n]{\alpha^2} - 1}{\alpha^2 - 1}} .$$

• Theorem 3.12 (p. 84): the level set $\{f = f_\infty\}$, $f_\infty = \lim_k f(x_k)$, contains a point $x^*$ with $G_f(x^*)$ linearly dependent.

Significance

Theorem 3.13 is the only convergence theorem the book gives for the r-algorithm. Theorems 3.11 and 3.12 hold for any function of the class $K$, convex or not, and say that iterates of the exact version cannot stall at a point where the local almost-gradients are linearly independent: linear dependence of $G_f(x)$ is a generalized stationarity condition that includes $0 \in \operatorname{conv} G_f(x)$. Lemmas 3.2 and 3.3 are statements about widths of convex bodies under linear maps and single dilations, and apply to any analysis of space-dilation methods, including the ellipsoid method.

All four results and the goal are proved in the book, the goal as a corollary without a written proof. None of them is formalized. The formalization adds a machine-checked definition of the class $K$ and of the algorithm as a relation on sequences covering every admissible choice of almost-gradients and stepsizes, a verified proof of the book's argument, and a check of the corollary step, which the book leaves to the reader.

Difficulty

The obvious argument for descent methods is that the function value drops by a fixed amount at every step unless the gradient is small. That argument fails here. The r-algorithm can make null steps, with $x_{k+1} = x_k$ while $B_k$ and $\tilde g_k$ change, and its steps are measured in a metric that degenerates as the dilations accumulate ($\det B_k = \beta^k \det B_0$). A small step does not certify near-stationarity, and a large accumulated dilation does not certify progress.

The difficulty is to relate the geometry of the transformed almost-gradient sets $B_k^*\bar P_{\delta,\varepsilon}(x_k)$ to the decay forced on $B_k$. This needs width estimates for convex bodies under linear maps and single dilations, which Mathlib does not have. Theorem 3.12 also needs a uniform lower bound, near a compact level set, on the Gram determinants of the piece gradients, and the book's proof of it is only sketched. Theorem 3.13 is stated as a corollary with no proof at all. Deriving it requires showing that the iterates cannot leave the prescribed component of $\{f(x^*) \le f \le f(x_0)\}$, and that their accumulation points reduce to $x^*$.

Formalization scope

• $E_n$ is EuclideanSpace ℝ (Fin n) with $n \ge 1$; operators are continuous linear maps; $B_k^*$ is the adjoint. $K_\rho$ and $p$ are valued in $[0, +\infty]$, so $K_\rho(W) = +\infty$ is represented exactly. Widths are sInf/sSup of support values, equal to the book's minima and maxima on nonempty compact sets.
• A function of class $K$ is given with its representation (pieces, open domains, smooth $f_i$), and $G_f(x)$ is the set of gradients of the incident pieces, as on p. 79. Linear dependence of $G_f(x)$ is the negation of linear independence of that set.
• A run of the algorithm is a predicate on sequences $x_k, \tilde g_k, B_k, g_f(x_k), h_{k+1}$; every theorem holds for every run. Step (3) divides by $\|r_k\|$, so $r_k \ne 0$ is part of the run: a run that reaches a point where no admissible choice gives $r_k \ne 0$ has no continuation, as in the book. The stepsize $h_{k+1} = \operatorname{argmin}$ is one admissible choice, not the definition.
• The standing assumption (3.50) is a hypothesis of Theorem 3.11 as well as of 3.12 and 3.13, because the book imposes it for the rest of the section on p. 79.
• In Lemma 3.3, $\beta > 0$ is added (the bound divides by $\beta^2$). "Body" means nonempty interior. An isolated local minimum is a local minimum with a neighbourhood containing no other local minimum.
• Runs exist, so the hypotheses are not vacuous. For $f(t) = |t_1| + 2|t_2|$ (four quadrant pieces), started at the minimizer $x_0 = 0$ with null steps, one can choose $g_f(x_{k+1}) = -g_f(x_k)$ at every step, and $0 \notin G_f$ keeps $r_k \neq 0$. A formalization under which no infinite run exists would make every theorem vacuous. The run predicate also forbids the degenerate reading $h_{k+1} < 0$, under which the monotonicity condition (a) would hold vacuously on an empty segment.
• Needed infrastructure: widths of compact convex sets under linear maps (via the singular values of $B$), the effect of a rank-one dilation on widths, determinant bounds for products of dilations, and Gram-determinant continuity. The first three apply to any space-dilation method and are welcome as independent lemmas.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer 1985, §3.7, pp. 77–85. doi:10.1007/978-3-642-82118-9
• N. Z. Shor, N. G. Zhurbenko, A minimization method using the operation of space dilation in the direction of the difference of two successive gradients, Kibernetika (Kiev), no. 3, 51–59, 1971 (listed in the bibliography of Shor 1985; no online copy known).
• N. Z. Shor, The analysis of convergence of a gradient type method with space dilation in the direction of the difference of two successive gradients, Kibernetika (Kiev), no. 4, 48–53, 1975 (listed in the bibliography of Shor 1985; no online copy known).

Motivation

Servers in manufacturing lines, communication links and service systems break down, are taken offline for maintenance, or go on vacation. When the interruptions are rare but long, they dominate congestion. A single down period can build a backlog that takes a long time to clear, and in a network that backlog propagates downstream. Standard heavy-traffic diffusion approximations, which describe queue lengths by reflected Brownian motion, do not capture this effect.

Chen and Whitt (Queueing Systems 13, 1993) identify a regime in which the effect survives in the limit. Up times are of order $n$ and down times of order $\sqrt n$, while the load is within $1/\sqrt n$ of capacity. Under the diffusion scaling each down period then becomes a jump, and the limit of the queue-length process is a reflected jump-diffusion. The paper generalises the single-station result of Kella and Whitt (Adv. Appl. Probab. 22, 1990; reference [22] of the paper) to open networks.

Timeline:

• 1981: Harrison and Reiman define the multidimensional reflection map on continuous paths (Ann. Probab. 9). Reiman (Math. Oper. Res. 9, 1984) extends it to paths with jumps.
• 1990: Kella and Whitt prove the one-station jump-diffusion limit for long up and down times.
• 1991: Chen and Mandelbaum give fluid and diffusion limits of open networks without interruptions (Math. Oper. Res. 16 and Ann. Probab. 19; references [5], [6] of the paper).
• 1993: Chen and Whitt prove the network case with interruptions (this mission), in Skorohod's $M_1$ topology.

Setting

A network has $J$ single-server stations. Customers arrive from outside station $j$ according to a counting process $A_j$. Station $j$ completes $S_j(t)$ services in its first $t$ units of busy time. The $l$th departure from station $k$ is routed to station $j$ when the indicator $\chi_{kj}(l)=1$, and $R_{kj}(m)=\sum_{l\le m}\chi_{kj}(l)$ counts such departures. Station $j$ alternates up periods $u^j_1,u^j_2,\dots$ and down periods $d^j_1,d^j_2,\dots$, starting up, and $D_j(t)$ is its cumulative down time in $[0,t]$. With a work-conserving discipline, the queue length $Z$ and the busy time $B$ satisfy

$$Z_j(t)=Z_j(0)+A_j(t)+\sum_{k}R_{kj}\big(S_k(B_k(t))\big)-S_j(B_j(t)),\qquad B_j(t)=\int_0^t 1[Z_j(s)>0,\ j\text{ up at }s]\,ds ,$$

and the idle time is $Y_j(t)=t-D_j(t)-B_j(t)$.

The reflection map $(\psi,\phi)$ associated with a matrix $Q$ takes a path $x$ to the pair $(y,z)$ with $z=x+(I-Q)y\ge 0$, $y$ nondecreasing, and $y_j$ increasing only when $z_j=0$.

A sequence of networks is indexed by $n$. The arrival, service and routing processes satisfy functional central limit theorems with rates $\lambda^n\to\lambda$ and $\mu^n\to\mu$ at speed $1/\sqrt n$. Up and down times scale as $(u^{j,n}_k/n,\ d^{j,n}_k/\sqrt n)\Rightarrow(u^j_k,d^j_k)$. The network is balanced, $\lambda=[I-P^{\mathsf t}]\mu$, with $P$ the routing matrix. The limit down time $\hat D_j(t)$ is the sum of $d^j_k$ over the up periods completed by time $t$, which is a pure-jump process.

The $M_1$ topology on paths with jumps compares completed graphs, in which each jump is filled in by the straight segment from $x(t-)$ to $x(t)$, through their monotone parametrisations.

Formalization targets

Goal: Theorem 4.1, case $J=1$

For a single station with feedback probability $p\in[0,1)$, with $\hat Z^n(t)=n^{-1/2}Z^n(nt)$, $\hat B^n(t)=n^{-1/2}[B^n(nt)-nt]$, $\hat Y^n(t)=n^{-1/2}Y^n(nt)$ and $\hat D^n(t)=n^{-1/2}D^n(nt)$,

$$(\hat Z^n,\hat B^n,\hat Y^n,\hat D^n)\Rightarrow(\hat Z,\hat B,\hat Y,\hat D)\quad\text{in }D((0,\infty),\mathbb R^{4},M_1).$$

Here $\hat Z=\phi(\hat X)$, $\hat Y=\mu^{-1}\psi(\hat X)$ and $\hat B=-\hat D-\hat Y$, with $Q=p$ and

$$\hat X(t)=\hat Z(0)+\hat\xi(t)+\big(c_\lambda-(1-p)c_\mu\big)t+(1-p)\mu\hat D(t).$$

The paper states Theorem 4.1 for $J$ stations, with the analogous formulas and $Q=P^{\mathsf t}$. The mission's goal is its case $J=1$ (see Formalization scope).

Milestones

1. Lemma 4.1: $\hat D^n\Rightarrow\hat D$ in $D((0,\infty),\mathbb R^J,M_1)$.
2. Lemma 4.2: $n^{-1}B^n_j(nt)\to t$ u.o.c.
3. Eq. (4.24): $n^{-1/2}\xi^n(nt)\to\hat\xi(t)$ u.o.c.
4. Eqs. (4.28)–(4.29): $\big(n^{-1/2}X^n(nt),\,n^{-1/2}D^n(nt)\big)\to(\hat X,\hat D)$ jointly in $M_1$.
5. The almost-sure form of Theorem 4.1 on a Skorohod representation space, case $J=1$.

Significance

The theorem yields a tractable approximation for networks with rare long interruptions: a reflected Lévy-type process driven by a Brownian part and a compound jump part. Its distribution can be studied through the reflection map. The jump directions $[I-P^{\mathsf t}]\operatorname{diag}(\mu)e_j$ make explicit how an outage at one station drains its downstream stations while its own queue builds up. Remark (4.3) of the paper derives a diffusion analogue of Little's law from the same limit.

The theorem is proved in the paper, and no part of it has been formalized. A formalization would produce the first machine-checked $M_1$ topology on paths with jumps, a heavy-traffic limit theorem for a queueing network, and the random-time-change argument for counting processes.

Difficulty

The obvious argument chains three facts: the primitive processes converge, hence so does the scaled free process $X$, and the reflection map is continuous. Two steps break. First, subtraction is not continuous in $M_1$ when the two paths jump at the same time in opposite directions, so the joint convergence of $\hat D^n$ across stations needs (4.11) and one common parametrisation. Second, the reflection map is Lipschitz in the uniform topology, but the uniform topology cannot see jumps that occur at nearby times. Carrying the convergence through the reflection map in the $M_1$ topology requires controlling how the regulator and the regulated process move along each jump segment of $\hat X$, jointly for all coordinates.

Formalization scope

Stations are Fin J; the network index is n : ℕ, and only $n\to\infty$ enters. Durations are indexed from $0$ in Lean. The queue length is integer valued, (3.2) is computed in $\mathbb Z$, and a solution satisfies $Z\ge 0$.

• Solutions, not constructions. Every statement quantifies over all solutions $(Z^n,B^n)$ of (3.2)–(3.3) and all reflection pairs of $\hat X$. Existence and uniqueness are asserted in the paper by citation and are not assumed or proved here.
• $M_1$. Parametric representations are monotone in the order of the completed graph, which is the standard definition. The page states only that the time component is nondecreasing. Convergence on $(0,\infty)$ means convergence on every $[a,b]$ with $0<a<b$ continuity points of the limit. Jump segments are segments in $\mathbb R^d$ (strong $M_1$). Convergence in $D((0,\infty),\cdot,M_1)$ includes the requirement that every path be càdlàg on $(0,\infty)$, so a copy of the limit that is continuous nowhere cannot satisfy the continuity-point condition vacuously.
• Weak convergence is in coupling form: one probability space carries copies with the right laws that converge almost surely. The limits in (4.1)–(4.4) are continuous, so there the mode is u.o.c.
• Corrected printed errors. Lemma 4.2 is stated with $n^{-1}$ in place of the printed $n^{-1/2}$, as in its proof. The map on p. 346 is read as $\phi(X)=Z$, $\psi(X)=\operatorname{diag}(\mu)Y$, following (4.13). The reflection map allows $y(0)\ge 0$, because $\hat X(0)$ may leave the orthant when $\hat D(0)>0$; when $x(0)\ge 0$ this agrees with (2.2).
• Added hypotheses. The processes $Z^n,B^n,\hat Z,\hat Y$ are assumed to be stochastic processes (measurable at each time). All networks share one probability space, so that the routing is literally common. No independence is assumed.
• The goal is the case $J=1$ of Theorem 4.1. The printed theorem claims strong $M_1$ convergence, with one parametric representation for all $4J$ coordinates, for every $J$. For $J\ge 2$ that claim fails: during an upstream outage, a downstream queue that empties part-way through the jump bends the prelimit graph of $(\hat D_j,\hat Y_k)$, while the limit's completed graph is a straight segment. For $J=1$ every coordinate moves linearly through each jump. The milestones Lemma 4.1, Lemma 4.2, (4.24) and (4.28)–(4.29) are stated for general $J$, and the almost-sure core of the proof for $J=1$.

A trivializing formalization is excluded. The hypotheses are satisfiable (for example by deterministic arrival and service processes), $\hat N$ is used only when $\sum_ku^j_k=\infty$, and laws are compared only for measurable path maps.

Needed infrastructure: the Skorohod space with the $M_1$ topology and its characterization on $(0,\infty)$, continuity of addition and of composition with continuous time changes, the multidimensional reflection map on paths with jumps, and a Skorohod representation argument. Proofs of Lemma 4.1 and Lemma 4.2 are welcome independently.

Selected references

• H. Chen, W. Whitt, Diffusion approximations for open queueing networks with service interruptions, Queueing Systems 13 (1993) 335–359. https://doi.org/10.1007/BF01149260
• O. Kella, W. Whitt, Diffusion approximations for queues with server vacations, Adv. Appl. Probab. 22 (1990) 706–729 (reference [22] of the paper).
• J. M. Harrison, M. I. Reiman, Reflected Brownian motion on an orthant, Ann. Probab. 9 (1981) 302–308. https://doi.org/10.1214/aop/1176994472
• H. Chen, A. Mandelbaum, Discrete flow networks: diffusion approximations and bottlenecks, Ann. Probab. 19 (1991) 1463–1519 (reference [6] of the paper).
• M. I. Reiman, Open queueing networks in heavy traffic, Math. Oper. Res. 9 (1984) 441–458 (reference [25] of the paper).
• W. Whitt, Some useful functions for functional limit theorems, Math. Oper. Res. 5 (1980) 67–85. https://doi.org/10.1287/moor.5.1.67
• A. V. Skorohod, Limit theorems for stochastic processes, Theory Probab. Appl. 1 (1956) 261–290. https://doi.org/10.1137/1101022

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 makes a hybrid SDE mean-square exponentially stable 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, and proved $H_\infty$-stability, asymptotic stability, and, in Section 4, exponential stability in mean square and almost surely with an explicit rate. This mission formalizes that exponential stability result, Theorem 4.2, and the steps of its proof.

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 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 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).$$

• Assumption 4.1: $c_1|x|^2\le U(x,i,t)\le c_2|x|^2$ with $c_1,c_2>0$.
• 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}$.

Put $\theta=K_3^2/\lambda_1$, $\lambda=\lambda_2-\theta\tau[2\tau(K_1^2+2K_3^2)+K_2^2]$ (positive by (3.5)), and

$$H_1=\theta\tau\big(2\tau(K_1^2+2K_3^2)+K_2^2\big)+\frac{24\theta\tau^4K_3^4}{1-6\tau^2K_3^2},\qquad H_2=\frac{12\theta\tau^2K_3^2(\tau K_1^2+K_2^2)}{1-6\tau^2K_3^2}.$$

In Lean these are Assumption21, Assumption22, C21, LU, Assumption31, Assumption41, Condition35, theta, lam, H1, H2, rateEquationLHS; the basis is HybridSetup, the Itô integral IsItoIntegral, the sampling time delta, solutions SolvesSampledHybridSDE, and the functional (4.7) Vbar, all in the namespace You2015.Expo.

Formalization targets

Goal: Theorem 4.2 (exponential stability)

Under the hypotheses above, the equation

$$2\tau\gamma e^{2\tau\gamma}(H_1+\tau H_2)+\gamma c_2=\lambda\tag{4.4}$$

has a unique root $\gamma>0$, and every solution of (2.1) satisfies

$$\limsup_{t\to\infty}\frac1t\log\big(\mathbb E|x(t)|^2\big)\le-\gamma,\qquad\limsup_{t\to\infty}\frac1t\log|x(t)|\le-\frac\gamma2\quad\text{a.s.}$$

for all $x_0\in\mathbb R^n$, $r_0\in S$.

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. (4.11) $\mathbb E\bar V(\hat x_z,\hat r_z,z)\le(H_1+\tau H_2)\int_{z-2\tau}^z\mathbb E|x(y)|^2dy$ for $z\ge2\tau$.
5. (4.14) $c_1e^{\gamma t}\mathbb E|x(t)|^2\le C$ for $t\ge2\tau$.
6. (4.14) $\Rightarrow$ (4.3), the mean-square-to-almost-sure transfer cited from Mao–Yuan [23, Theorem 8.8].

Significance

The result. Theorem 4.2 gives a quantitative guarantee: a controller that samples the state every $\tau$ units makes the switching system decay exponentially, with a rate $\gamma$ computable from the constants of the assumptions. Asymptotic stability (Section 3 of the paper) says nothing about how fast trajectories settle; the rate is what a designer trades against the sampling cost when choosing $\tau$. The almost sure statement concerns individual trajectories, which is what an operator observes.

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 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). Formalization also checks the constants: it found that the printed $H_1$ in (4.5) disagrees with the paper's own derivation (see below).

Difficulty

Equation (2.1) is a stochastic differential delay equation whose delay $t-\delta_t$ is bounded but jumps at every observation time, so the delay-equation stability theorems that require a differentiable delay with derivative below one (Mao–Yuan, p. 285) do not apply. A Lyapunov function of the current state alone 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. An exponential rate requires controlling this delay term with an exponential weight, and the weight inflates the delay contribution by a factor $e^{2\tau\gamma}$; the rate equation (4.4) records exactly this balance. The almost sure part does not follow from the mean-square part by Chebyshev's inequality at fixed times alone: a pathwise bound needs control of the supremum of $|x|$ over each unit interval, which involves the martingale part of the solution.

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), (3.21), (4.5) 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 of a nonnegative quantity ($\mathbb E|x|^2$, $\mathbb E\bar V$) and every time integral of one is a lower Lebesgue integral in $[0,\infty]$, so a non-integrable process cannot produce a junk value $0$.
• Logarithms. The paper's $\log$ takes the value $-\infty$ at $0$. For a finite $a(t)\ge0$, $\limsup_{t\to\infty}\frac1t\log a(t)\le-\gamma$ is stated in the equivalent form "for every $\gamma'<\gamma$, eventually $a(t)\le e^{-\gamma't}$". Lean's Real.log 0 = 0 never enters. In (4.3) the almost-sure quantifier is outside the quantifier over $\gamma'$.
• Correction of (4.5). The page prints the last term of $H_1$ as $24\tau^3K_3^4/(1-6\tau^2K_3^2)$. Substituting (3.21) into (4.9), as the proof does, gives $24\theta\tau^4K_3^4/(1-6\tau^2K_3^2)$ (the same computation reproduces the printed $H_2$). The mission uses the corrected $H_1$ in the goal, (4.11) and (4.14). With the printed value the claimed rate could exceed what the proof yields whenever $\theta\tau>1$.
• "The unique root" is a conjunct of the goal ($\exists!\,\gamma>0$); the stability conclusions are stated for every positive root. "(so $\lambda>0$)" is a consequence of (3.5), not a hypothesis. (4.4) is kept as an equality.
• "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,c_1,c_2,\tau$ are data. The constant $C$ of (4.14) is chosen after $x_0$, $r_0$, the solution and $\gamma$, and before $t$.
• (3.15), (3.21) and the transfer (4.14) $\Rightarrow$ (4.3) 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. $\bar V$ of (4.7) is used only for $z\ge2\tau$, where no extension of the solution to negative times is needed. Other misprints on the page ($g(x,i,s)=f(x,i,0)$ on p. 909, $V(\hat x_0,\hat r_0,t)$ for $V(\hat x_0,\hat r_0,0)$ on p. 918, the swapped $\vee,\wedge$ on p. 907) are not formalized.

A trivializing formalization is ruled out: the expectations are not Bochner integrals, $\log 0$ is never evaluated, the goal asserts that the rate equation has exactly one positive root (so the stability clauses are not vacuous), the solution notion admits the true solution and requires path continuity, and the derivative witnesses of $U$ are tied to $U$. A sorry-free local check confirms that Assumptions 2.1, 2.2, 4.1, condition (3.5) and $\lambda>0$ hold for $n=m=N=1$, $f=g=0$, $u(x)=-x$, $U=|x|^2$, $K_1=K_2=K_3=1$, $\lambda_1=1/4$, $\lambda_2=1$, $c_1=c_2=1$, $\tau=1/10$; for these data $\mathcal LU+\lambda_1|U_x|^2=-|x|^2$ by hand.

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, the Burkholder–Davis–Gundy inequality, and the Borel–Cantelli argument that turns mean-square exponential decay into almost sure decay. These are reusable far beyond this mission. Section 3 of the paper (asymptotic 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