Optimization

Motivation

In distributed optimization a network of $m$ agents minimizes a sum of private functions while each agent talks only to its neighbours. Applications include federated and decentralized learning, sensor networks and multi-robot systems, where the data cannot be pooled at one site. Many of these networks are directed (communication links are one-way, for instance because transmission powers differ) and time-varying (links come and go). On such networks no doubly stochastic mixing matrix is available in general, and plain averaging drifts toward a weighted average instead of the true one. The push-sum protocol corrects this drift by carrying an auxiliary weight $\phi_i$ at every agent (Kempe, Dobra & Gehrke 2003; Nedić & Olshevsky 2015).

Y. Sun, A. Daneshmand and G. Scutari (arXiv:1905.02637v2) analyse SONATA, a gradient-tracking method in which each agent solves a strongly convex surrogate of its local problem instead of taking a gradient step, for composite problems (a convex, possibly nonsmooth regulariser $G$ and a convex constraint set). They prove linear convergence on undirected graphs (their Theorem 3.9, the companion mission of this series) and, in Section 4, for a push-sum version over time-varying digraphs (Theorem 4.5). This mission formalizes the second result.

Timeline. Gradient tracking with push-sum over time-varying digraphs appears in NEXT/SONATA (Di Lorenzo & Scutari 2016; Scutari & Sun 2019), where convergence was proved without rates for nonconvex problems. Linear rates for smooth unconstrained strongly convex problems over time-varying digraphs were obtained for Push-DIGing (Nedić, Olshevsky & Shi 2017). Sun, Daneshmand and Scutari (2019, revised 2020) extend the linear rate to the composite, constrained setting with surrogates, and require only the average $F$, not every $f_i$, to be strongly convex.

Setting

Problem (P). Agent $i\in[m]$ holds $f_i:\mathbb R^d\to\mathbb R$; the agents solve

$$\min_{x\in\mathcal K}U(x)\triangleq F(x)+G(x),\qquad F=\frac1m\sum_{i=1}^mf_i .$$

Assumption A: $\mathcal K$ is nonempty, closed and convex; each $f_i$ is twice differentiable on an open set $\mathcal O\supseteq\mathcal K$ and convex; $\mu I\preceq\nabla^2F(x)\preceq LI$ on $\mathcal K$ with $\mu>0$; $G$ is convex on $\mathcal K$. $x^\star$ is the solution and $U^\star=U(x^\star)$.

Surrogates (Assumption C). Each agent has $\tilde f_i(x;z)$, $C^2$ on $\mathcal O\times\mathcal O$, with $\nabla\tilde f_i(x;x)=\nabla f_i(x)$, $\nabla\tilde f_i(\cdot;x)$ $\tilde L_i$-Lipschitz and $\tilde f_i(\cdot;x)$ $\tilde\mu_i$-strongly convex on $\mathcal K$. Constants $D^\ell_i\le D^u_i$ satisfy $D^\ell_iI\preceq\nabla^2\tilde f_i(x;y)-\nabla^2F(x)\preceq D^u_iI$ on $\mathcal K\times\mathcal K$ (15); $\tilde\mu_{\rm mn}=\min_i\tilde\mu_i$, $D^\ell_{\rm mn}=\min_iD^\ell_i$.

Network (Assumption B′). At time $\nu$ the digraph $\mathcal G^\nu$ has edge set $\mathcal E^\nu$; $(i,j)\in\mathcal E^\nu$ is a link from $i$ to $j$. There is an integer $B>0$ such that the union of the edge sets over every window $[\nu B,(\nu+1)B-1]$ is strongly connected.

Weights (Assumption E). $C^\nu=(c^\nu_{ij})$ is column stochastic, $c^\nu_{ii}\ge c_\ell>0$, $c^\nu_{ij}\ge c_\ell$ if $(j,i)\in\mathcal E^\nu$ and $c^\nu_{ij}=0$ for other $j\ne i$.

Algorithm 3. From $x_i^0\in\mathcal K$, $y_i^0=\nabla f_i(x_i^0)$, $\phi_i^0=1$, each agent computes

$$\hat x_i^\nu\in\operatorname*{argmin}_{x_i\in\mathcal K}\ \tilde f_i(x_i;x_i^\nu)+(y_i^\nu-\nabla f_i(x_i^\nu))^\top(x_i-x_i^\nu)+G(x_i),\qquad x_i^{\nu+1/2}=x_i^\nu+\alpha(\hat x_i^\nu-x_i^\nu),$$

then $\phi_i^{\nu+1}=\sum_jc^\nu_{ij}\phi_j^\nu$, $x_i^{\nu+1}=\frac1{\phi_i^{\nu+1}}\sum_jc^\nu_{ij}\phi_j^\nu x_j^{\nu+1/2}$ and $y_i^{\nu+1}=\frac1{\phi_i^{\nu+1}}\sum_jc^\nu_{ij}(\phi_j^\nu y_j^\nu+\nabla f_j(x_j^{\nu+1})-\nabla f_j(x_j^\nu))$.

The analysis uses the weighted gap $p_\phi^\nu=\sum_i\phi_i^\nu(U(x_i^\nu)-U^\star)$, the tracking error $\delta_i^\nu=\nabla F(x_i^\nu)-y_i^\nu$, and the consensus errors $x^\nu_{\phi,\perp}$, $y^\nu_{\phi,\perp}$ measured against the $\phi$-weighted averages.

Formalization targets

Goal: Theorem 4.5

If $\tilde\mu_{\rm mn}\ge D^\ell_{\rm mn}$, there is $\bar\alpha\in(0,1]$ such that for every $\alpha\in(0,\bar\alpha)$, every run and every agent $i$,

$$\exists\,C,\ z\in[0,1):\qquad|U(x_i^\nu)-U^\star|\le C\,z^\nu\quad\forall\nu .$$

The goal is qualitative: neither $\bar\alpha$ nor the rate is fixed, so it survives any improvement of the constants.

Milestones

In attack order: the weighted tracking identity (74) and its consequence $\bar y^\nu_\phi=\overline{\nabla f}^\nu$; the bounds $\phi_{lb}\le\phi_i^\nu\le\phi_{ub}$ (p. 29); the per-agent descent inequality (Lemma I.1); the lower bound on the weighted step length (Lemma I.2); the tracking-error bound $\|\delta^\nu\|^2\le8L^2_{\rm mx}\|x^\nu_{\phi,\perp}\|^2+2\|y^\nu_{\phi,\perp}\|^2$ (Lemma I.3); the contraction $p_\phi^{\nu+1}\le\sigma(\alpha)p_\phi^\nu+\eta(\alpha)\phi_{ub}(\cdots)$ (Proposition 4.1); the bound of $\|d^\nu\|^2$ by $p_\phi^\nu$ and $\|y^\nu_{\phi,\perp}\|^2$ (Proposition 4.3).

Significance

Theorem 4.5 gives a linear rate for distributed composite and constrained optimization over time-varying directed networks. Two features matter: the individual $f_i$ need not be strongly convex, and the surrogates cover proximal-gradient steps, DANE-type local solves and mirror-descent steps under one analysis. The rate depends on the surrogate-mismatch constants $D_i$, which is the mechanism by which the paper shows that local computation helps when the $f_i$ are similar.

The result is proved in the paper; the proof of Theorem 4.5 refers to the undirected argument, and several of its supporting statements (Propositions 4.1 and 4.3) have their proofs omitted or relegated to the supplement, with consensus estimates quoted from Scutari & Sun (2019). To our knowledge none of it is machine-checked. A formalization produces a checked proof of the directed result together with reusable statements about push-sum weights over $B$-strongly connected digraphs.

Difficulty

The obvious argument is to repeat the undirected proof with weighted averages. Two steps fail. First, the $\phi$-weighted average is not the minimiser of $\sum_i\|x_i-c\|^2$, so consensus errors measured against it lose a constant (the 8 in Lemma I.3 instead of 4), and every passage between weighted and unweighted sums needs the bounds $\phi_{lb}\le\phi_i^\nu\le\phi_{ub}$, which rest on a product-of-matrices argument over windows of length $(m-1)B$. Second, the matrices change with $\nu$, so there is no single contraction factor; geometric decay of the consensus errors holds only over windows, and the coupling between the optimality gap, the consensus errors and the step lengths must be closed by a small-gain argument whose constants are uniform over the run. The step-size threshold must not depend on the starting point.

Formalization scope

Points are EuclideanSpace ℝ (Fin d); stacked vectors are Fin m → ℝ^d with the Euclidean norm $\|v\|^2=\sum_i\|v_i\|^2$, never Lean's sup norm. The Hessian is the derivative of the gradient, and Loewner bounds are quadratic-form inequalities. Time is 0-based. A run is a relational predicate: $\hat x_i^\nu$ is some minimizer of the subproblem, whose existence the paper takes for granted; $x^\star$ is assumed to exist. The divisions by $\phi_i^{\nu+1}$ appear as in the paper and are genuine, since Assumption E keeps the weights positive. $f_i$ is convex on $\mathcal K$ and locally convex on $\mathcal O$ (positive semidefinite Hessian; $\mathcal O$ need not be convex), $\tilde\mu_i>0$, and $D^\ell_i,D^u_i$ are parameters: the statements hold for every valid choice. The graph sequence, $B$, $c_\ell$ and the matrices $C^\nu$ come before $\bar\alpha$; the starting point and the run come after $\alpha$. The bounds on $\phi$ are stated for $m\ge2$ (the printed $\phi_{ub}$ is $0$ at $m=1$), and positivity of $\sigma(\alpha)$ is claimed only when $D_{\rm mx}>0$ or $\alpha<1$.

The following do not count as a formalization of the goal: an unsatisfiable run predicate (a sorry-free verification file exhibits a run satisfying every hypothesis), a $\bar\alpha$ chosen after the run, the $\phi$ bounds or a contraction factor assumed in place of Assumptions B′ and E, and dropping the $1/\phi_i^{\nu+1}$ normalisation.

Not posed: the explicit rate (Theorem III.1), the complexity corollaries, and the consensus estimates Lemma 4.2 and Proposition 4.4, whose constants $c_0,\rho_B$ come from Scutari & Sun (2019) (as printed, $c_0$ is negative). A complete development needs Taylor expansions with integral remainder along segments, first-order optimality for composite problems on convex sets, and products of column-stochastic matrices over strongly connected windows; the last is reusable for any push-sum method. Contributions to any milestone, and to the missing consensus estimates as auxiliary lemmas, are welcome.

Selected references

• Y. Sun, A. Daneshmand, G. Scutari, Distributed Optimization Based on Gradient-tracking Revisited: Enhancing Convergence Rate via Surrogation, arXiv:1905.02637v2, 2020; SIAM J. Optim. 32(2), 2022. https://arxiv.org/abs/1905.02637v2
• G. Scutari, Y. Sun, Distributed nonconvex constrained optimization over time-varying digraphs, Math. Program. 176, 2019. https://doi.org/10.1007/s10107-018-01357-w
• P. Di Lorenzo, G. Scutari, NEXT: In-Network Nonconvex Optimization, IEEE Trans. Signal Inf. Process. Netw. 2(2), 2016. https://doi.org/10.1109/TSIPN.2016.2524588
• A. Nedić, A. Olshevsky, W. Shi, Achieving Geometric Convergence for Distributed Optimization over Time-Varying Graphs, SIAM J. Optim. 27(4), 2017. https://doi.org/10.1137/16M1084316
• A. Nedić, A. Olshevsky, Distributed optimization over time-varying directed graphs, IEEE Trans. Autom. Control 60(3), 2015. https://doi.org/10.1109/TAC.2014.2364096
• D. Kempe, A. Dobra, J. Gehrke, Gossip-based computation of aggregate information, FOCS 2003. https://doi.org/10.1109/SFCS.2003.1238221

Motivation

Finsler's lemma (P. Finsler, 1937) states that for symmetric matrices $M,N\in\mathbb S^n$, the quadratic form $x^\top Mx$ is positive on every nonzero $x$ with $x^\top Nx=0$ if and only if $M-\alpha N>0$ for some real $\alpha$. Together with the S-lemma of Yakubovich it is one of the basic tools for converting a statement about all vectors satisfying a quadratic constraint into a single linear matrix inequality (LMI) in a multiplier, which can then be checked by semidefinite programming. Both results are used throughout robust control, where uncertainty is described by quadratic constraints.

In data-driven control the unknown object is a matrix, not a vector: the system matrices $(A,B)$ consistent with noisy measurements form a set of the form

$$\mathcal Z_r(N)=\Big\{Z\in\mathbb R^{r\times q}:\begin{bmatrix}I\\ Z\end{bmatrix}^\top N\begin{bmatrix}I\\ Z\end{bmatrix}\geqslant0\Big\},$$

and a controller has to work for every element of such a set. H. J. van Waarde, M. K. Camlibel, J. Eising and H. L. Trentelman (arXiv:2203.12959, SIAM J. Control Optim. 2023) develop matrix-valued versions of the S-lemma and of Finsler's lemma for exactly this purpose. Their matrix S-lemma (Theorem 4.7) requires a Slater-type condition: $N$ must have a positive eigenvalue. This mission concerns the complementary case in which $N$ has no positive eigenvalue, where the inequality defining $\mathcal Z_r(N)$ degenerates into an equality and a Finsler-type statement is needed.

Setting

All matrices are real. For a symmetric matrix $A$, $A\geqslant0$ ($A>0$) means positive semidefinite (definite); $A\leqslant0$ means $-A\geqslant0$. $A^\dagger$ is the Moore–Penrose pseudo-inverse, the unique matrix $X$ with $AXA=A$, $XAX=X$ and $AX$, $XA$ symmetric.

Fix integers $q\geqslant1$ and $r\geqslant0$. A symmetric matrix $M\in\mathbb S^{q+r}$ is partitioned as

$$M=\begin{bmatrix}M_{11}&M_{12}\\ M_{21}&M_{22}\end{bmatrix},$$

with $M_{11}$ of size $q\times q$ and $M_{22}$ of size $r\times r$, and likewise $N$. For $Z\in\mathbb R^{r\times q}$ write $F_M(Z):=\begin{bmatrix}I\\ Z\end{bmatrix}^\top M\begin{bmatrix}I\\ Z\end{bmatrix}\in\mathbb S^q$, and define

$$\mathcal Z_r(M)=\{Z: F_M(Z)\geqslant0\},\qquad \mathcal Z_r^0(N)=\{Z: F_N(Z)=0\}.$$

The generalized Schur complement is $M\,|\,M_{22}:=M_{11}-M_{12}M_{22}^\dagger M_{21}$, and the class $\boldsymbol\Pi_{q,r}$ consists of the symmetric $M$ with $M_{22}\leqslant0$, $M\,|\,M_{22}\geqslant0$ and $\ker M_{22}\subseteq\ker M_{12}$. For $N\in\boldsymbol\Pi_{q,r}$, the condition $N\,|\,N_{22}=0$ is equivalent to $N$ having no positive eigenvalue; then $\mathcal Z_r(N)=\mathcal Z_r^0(N)$. Finally, set

$$\Theta:=\begin{bmatrix}I\\ -N_{22}^\dagger N_{21}\end{bmatrix}^\top M\begin{bmatrix}I\\ -N_{22}^\dagger N_{21}\end{bmatrix}=F_M(-N_{22}^\dagger N_{21}).\qquad(4.4)$$

Formalization targets

Goal: Theorem 4.8 (Matrix Finsler's lemma), p. 12

First, if $M-\alpha N\geqslant0$ for some $\alpha\in\mathbb R$, then $\mathcal Z_r^0(N)\subseteq\mathcal Z_r(M)$. Second, if $M,N\in\boldsymbol\Pi_{q,r}$, $N\,|\,N_{22}=0$ and $\ker\Theta\subseteq\ker(M\,|\,M_{22})$, then

$$\mathcal Z_r^0(N)\subseteq\mathcal Z_r(M)\iff\exists\,\alpha\geqslant0:\ M-\alpha N\geqslant0 .$$

Milestones (proof of Theorem 4.8, pp. 12–13)

1. If $\mathcal Z_r^0(N)\subseteq\mathcal Z_r(M)$, then $\ker N_{22}\subseteq\ker M_{22}$.
2. With $T:=\begin{bmatrix}I&0\\ -N_{22}^\dagger N_{21}&I\end{bmatrix}$, $T^\top NT=\operatorname{diag}(0,N_{22})$ and

$$T^\top(M-\alpha N)T=\begin{bmatrix}\Theta&M_{12}-N_{12}N_{22}^\dagger M_{22}\\ M_{21}-M_{22}N_{22}^\dagger N_{21}&M_{22}-\alpha N_{22}\end{bmatrix}.\qquad(4.6)$$

3. If $\ker M_{22}\subseteq\ker M_{12}$, then with $D:=M_{22}^\dagger M_{21}-N_{22}^\dagger N_{21}$, $\Theta=M\,|\,M_{22}+D^\top M_{22}D$ and $M_{22}D=M_{21}-M_{22}N_{22}^\dagger N_{21}$ (4.7a–b).
4. $\Theta\geqslant0$ and $\ker(M\,|\,M_{22})=\ker\Theta\cap\ker(M_{21}-M_{22}N_{22}^\dagger N_{21})$.
5. $T^\top(M-\alpha N)T\geqslant0$ if and only if

$$M_{22}-\alpha N_{22}-(M_{21}-M_{22}N_{22}^\dagger N_{21})\,\Theta^\dagger\,(M_{12}-N_{12}N_{22}^\dagger M_{22})\geqslant0.\qquad(4.8)$$

6. Some $\alpha\geqslant0$ satisfies (4.8), and then $M-\alpha N\geqslant0$.

A companion item formalizes Example 4.9 (p. 13): for $N=\begin{bmatrix}-1&1\\1&-1\end{bmatrix}$ and $M=\begin{bmatrix}1&0\\0&-1\end{bmatrix}$ all hypotheses except the one on $\Theta$ hold, the inclusion holds, and no $\alpha\geqslant0$ works.

Significance

The theorem turns an inclusion between two sets of matrices, a statement quantified over infinitely many $Z$, into feasibility of a scalar-multiplier LMI. In the paper it is one of four matrix S-lemma variants (Theorems 4.7, 4.8, 4.10, 4.11) that together cover the cases arising in data-based control: whether the data-consistent set $\mathcal Z_r(N)$ has a Slater point, and whether the conclusion is non-strict or strict. Theorem 4.8 is the variant for noise models whose quadratic description has no interior, for instance exact equality constraints on the noise. Example 4.9 shows that the kernel hypothesis on $\Theta$ is genuinely needed, so the statement marks the boundary of when the lossless reduction holds.

The paper gives a complete proof. No machine-checked proof of this theorem, of the matrix S-lemma, or of Finsler's lemma in matrix form is known to exist, in Lean or elsewhere. Formalizing it produces reusable infrastructure: the Moore–Penrose pseudo-inverse of real matrices with its Penrose identities, the generalized Schur complement criterion for positive semidefiniteness of a block matrix, and congruence manipulations of $2\times2$ block matrices, none of which is currently in Mathlib in this form.

Difficulty

The "if" direction is a one-line computation. For the "only if" direction the classical vector Finsler lemma is not directly applicable: it concerns vectors $x$ with $x^\top Nx=0$, while the hypothesis here only controls matrices $Z$ with $F_N(Z)=0$, which is a much smaller family when $q>1$, and the conclusion is non-strict. The natural first idea, applying the vector S-lemma, fails because $N$ has no positive eigenvalue, so its Slater condition is violated. Instead one must exploit the structure of $\boldsymbol\Pi_{q,r}$: the pseudo-inverse appears because $N_{22}$ and $M_{22}$ are typically singular, and every manipulation must track kernels and ranges exactly.

Formalization scope

The blocks are indexed by arbitrary finite types ι (size $q$) and κ (size $r$); a matrix in $\mathbb S^{q+r}$ is Matrix (ι ⊕ κ) (ι ⊕ κ) ℝ, its blocks are toBlocks₁₁ etc., and $\mathbb R^{r\times q}$ is Matrix κ ι ℝ. $A\geqslant0$ is Mathlib's PosSemidef, which includes symmetry. The pseudo-inverse is defined by Hilbert's choice among matrices satisfying the four Penrose conditions; since such a matrix exists and is unique, this is the pseudo-inverse and not a junk value. Kernel inclusions are stated with matrix–vector products.

One hypothesis is added and disclosed: $q\geqslant1$ (Nonempty ι) in the second statement of Theorem 4.8 and in the milestones that need it. The proof picks a nonzero vector of $\mathbb R^q$, and at $q=0$ the equivalence is false ($r=1$, $N=[0]$, $M=[-1]$). The first statement keeps a real multiplier of any sign; the second requires $\alpha\geqslant0$, as printed. The hypothesis $N\,|\,N_{22}=0$ together with $N\in\boldsymbol\Pi_{q,r}$ makes $\mathcal Z_r^0(N)$ nonempty, so the inclusion is never vacuous; a formalization in which $\mathcal Z_r^0(N)$ could be empty, or in which $N_{22}^\dagger$ were replaced by the inverse (which is $0$ on singular blocks in Lean), would not be this theorem.

Needed infrastructure: existence and uniqueness of the Moore–Penrose pseudo-inverse (needed to work with the definition at all), symmetry of $A^\dagger$ for symmetric $A$, the generalized Schur complement criterion for $\begin{bmatrix}A&B\\B^\top&C\end{bmatrix}\geqslant0$, and positive semidefiniteness under congruence by an invertible matrix. These lemmas are reusable beyond this mission and contributions of them are welcome, as are proofs of the companion Example 4.9.

Selected references

• H. J. van Waarde, M. K. Camlibel, J. Eising, H. L. Trentelman, Quadratic matrix inequalities with applications to data-based control, SIAM J. Control Optim., 2023; preprint arXiv:2203.12959v3. https://arxiv.org/abs/2203.12959
• P. Finsler, Über das Vorkommen definiter und semidefiniter Formen in Scharen quadratischer Formen, Comment. Math. Helv. 9 (1937), 188–192. https://doi.org/10.1007/BF01258188
• I. Pólik, T. Terlaky, A survey of the S-lemma, SIAM Review 49 (2007), 371–418. https://doi.org/10.1137/S003614450444614X
• H. J. van Waarde, J. Eising, H. L. Trentelman, M. K. Camlibel, Data informativity: a new perspective on data-driven analysis and control, IEEE Trans. Automat. Control 65 (2020), 4753–4768. https://doi.org/10.1109/TAC.2020.2966717

Motivation

Many planning problems combine a discrete choice with a continuous one. A robot moving through a cluttered room chooses which free regions to traverse and where exactly to cross between them; a vehicle chooses a sequence of operating modes and a trajectory within each mode. Marcucci, Umenberger, Parrilo and Tedrake (arXiv:2101.11565, SIAM J. Optim. 2024, doi:10.1137/22M1523790) abstract this as the shortest-path problem in a graph of convex sets (SPP in GCS): a shortest-path problem in which each vertex is not a point but a convex set, and the length of an edge depends on where in its two sets the path enters and leaves. The paper shows that the problem is NP-hard even in simple cases, and then gives a mixed-integer convex formulation that is exact and whose convex relaxation is strong in practice. That formulation underlies the GCS motion planners developed later by the same group.

Setting

A graph of convex sets consists of a finite directed graph $G = (\mathcal V, \mathcal E)$, a source vertex $s$, a target vertex $t \neq s$, a nonempty compact convex set $\mathcal X_v \subseteq \mathbb R^n$ for each vertex $v$, and for each edge $e = (u,v)$ an edge length $\ell_e : \mathbb R^n \times \mathbb R^n \to \mathbb R_{\ge 0}\cup\{\infty\}$, which is proper, closed and convex. No symmetry or triangle inequality is assumed. An $s$-$t$ path is a sequence $p = (v_0,\dots,v_K)$ of distinct vertices with $v_0 = s$, $v_K = t$ and $(v_k, v_{k+1}) \in \mathcal E$; $\mathcal E_p$ is the set of its edges. The SPP in GCS (2.1) is

$$\operatorname{SPP}(G) := \inf\Big\{ \sum_{e=(u,v)\in\mathcal E_p} \ell_e(x_u,x_v) : p \text{ an } s\text{-}t\text{ path},\ x_v \in \mathcal X_v \text{ for } v \in p \Big\}.$$

The perspective of a set $\mathcal X$ is the closed cone $\tilde{\mathcal X} := \operatorname{cl}\{(x,\lambda) : \lambda \ge 0,\ x \in \lambda\mathcal X\}$ (Definition 4.1). The perspective of a function $f$ is $\tilde f(x,\lambda) := \inf\{\sigma : (x,\sigma,\lambda) \in \widetilde{\operatorname{epi} f}\}$, the function whose epigraph is the perspective of the epigraph of $f$ (Definition 4.4). For $\lambda > 0$ it equals $\lambda f(x/\lambda)$.

With $\mathcal E^{\mathrm{in}}_v$ and $\mathcal E^{\mathrm{out}}_v$ the edges entering and leaving $v$, the MICP (5.5) has a flow $y_e \in \{0,1\}$ and two vectors $z_e, z'_e \in \mathbb R^n$ per edge:

$$\begin{aligned} \text{minimize}\ & \textstyle\sum_{e\in\mathcal E}\tilde\ell_e(z_e,z'_e,y_e)\\ \text{s.t.}\ & \textstyle\sum_{\mathcal E^{\mathrm{out}}_s} y_e = 1,\ \sum_{\mathcal E^{\mathrm{in}}_t} y_e = 1,\ \ \sum_{\mathcal E^{\mathrm{out}}_v} y_e \le 1,\ \ \sum_{\mathcal E^{\mathrm{in}}_v}(z'_e,y_e) = \sum_{\mathcal E^{\mathrm{out}}_v}(z_e,y_e)\ \ (v\ne s,t),\\ & (z_e,y_e)\in\tilde{\mathcal X}_u,\ (z'_e,y_e)\in\tilde{\mathcal X}_v,\ y_e\in\{0,1\}\ \ (e=(u,v)\in\mathcal E). \end{aligned}$$

Its optimal value is $\operatorname{MICP}(G)$. The paper derives (5.5) from a biconvex program (5.2), the shortest-path LP (5.1) together with vertex positions $x_v \in \mathcal X_v$ and the bilinear constraints $z_e = y_e x_u$, $z'_e = y_e x_v$. Lemma 5.4 turns every valid linear inequality on the flows at a vertex into a valid perspective constraint.

Formalization targets

Goal: Theorem 5.7 (p. 10)

Under the standing assumptions of §2 and the assumption of p. 7 that no edge enters $s$ and no edge leaves $t$,

$$\operatorname{MICP}(G) = \operatorname{SPP}(G).$$

Both sides are infima in the extended reals and equal $+\infty$ when there is no $s$-$t$ path.

Milestones

1. Remark 4.2 (p. 5): for bounded closed $\mathcal X$, $\tilde{\mathcal X} = \{(x,\lambda): \lambda\ge0,\ x\in\lambda\mathcal X\}$.
2. Remark 4.5 (p. 6): $\tilde f(x,\lambda) = \lambda f(x/\lambda)$ for $\lambda>0$, $\tilde f = \infty$ for $\lambda<0$, $\tilde f(0,0)=0$ for proper closed convex $f$.
3. Lemma 5.4 (p. 9): a valid inequality $\sum_{e\in\mathcal E_v} c_e y_e + d \ge 0$ for (5.2) lifts to the valid constraint $\big(\sum_{\mathcal E^{\mathrm{in}}_v} c_e z'_e + \sum_{\mathcal E^{\mathrm{out}}_v} c_e z_e + d x_v,\ \sum_{\mathcal E_v} c_e y_e + d\big)\in\tilde{\mathcal X}_v$.
4. Remark 5.5 (p. 9): the equality version of Lemma 5.4.
5. Path and cycles (proof of Theorem 5.7): binary flows satisfying (5.5b)–(5.5d) form the vertex-disjoint union of an $s$-$t$ path and cycles.
6. Simplification of (5.5e) (proof of Theorem 5.7): $y_e = 0$ forces $z_e = z'_e = 0$ at cost $0$; $y_e = 1$ forces $z_e\in\mathcal X_u$, $z'_e\in\mathcal X_v$ at cost $\ell_e(z_e,z'_e)$.
7. Flow along the path (proof of Theorem 5.7): for consecutive path edges $e, f$, $z'_e = z_f$.

A companion item states the recovery part of Theorem 5.7 (second and third sentences): an optimal MICP solution yields an optimal path and optimal positions $x_u = z_e$, $x_v = z'_e$.

Significance

Theorem 5.7 is what makes (5.5) usable: it says that the mixed-integer program, whose only nonconvexity is $y_e\in\{0,1\}$, solves the SPP in GCS exactly. The SPP in GCS is NP-hard by Theorem 3.1, so exactness is the most one can ask of a polynomial-size formulation, and dropping integrality gives a convex program whose value is a lower bound for branch and bound. The perspective construction of Lemma 5.4 is a general recipe, closely related to the reformulation-linearization technique, for convexifying products of flows and positions.

On the formal side, the paper's proof is half a page and leaves several points to the reader: why the integer flows decompose into a path and cycles, why the closure in the perspective cone disappears for compact sets, and why the perspective function vanishes at the origin. A machine-checked proof makes these steps explicit. The result has not been formalized before, and the mission also produces reusable statements about perspectives of sets and functions in extended-real arithmetic and about the decomposition of unit $s$-$t$ flows with degree bounds.

Difficulty

The inequality $\operatorname{MICP}(G) \le \operatorname{SPP}(G)$ is the routine half: a path and its positions give a feasible point of (5.5) of the same cost. The other half requires reading a path out of an arbitrary feasible point. Integer flows satisfying (5.5b)–(5.5d) need not be a path: they may also contain disjoint cycles, and the degree constraint (5.5c) is what prevents a cycle from sharing a vertex with the path (Example 5.10 shows the value drops without it). The cost of a cycle must be shown to be nonnegative, and the perspective constraints must be shown to collapse to $z_e = z'_e = 0$ on zero-flow edges. That step uses compactness of $\mathcal X_v$. For unbounded sets the zero slice of $\tilde{\mathcal X}_v$ is the recession cone, and the argument fails. The cost at zero flow is $\tilde\ell_e(0,0,0)$, defined by a closure, and its value $0$ uses properness and convexity of $\ell_e$, not just the formula $\lambda\ell_e(\cdot/\lambda)$.

Formalization scope

• $\mathbb R^n$ is Fin n → ℝ. Edge lengths and all optimal values are EReal; optimal values are infima (⨅/sInf), equal to $+\infty$ on an empty feasible set. Attainment is not assumed.
• The graph is a structure with a finite edge set E : Finset (V × V) over a finite vertex type, a source, a target, sets X v and lengths ℓ e. The standing assumptions of §2 ($s\ne t$; $\mathcal X_v$ nonempty, compact, convex; $\ell_e \ge 0$ proper closed convex) are the predicate IsGCS. The assumption $|\mathcal E^{\mathrm{in}}_s| = |\mathcal E^{\mathrm{out}}_t| = 0$ of p. 7 is the separate predicate NoInSNoOutT, a hypothesis of the goal, of the path-and-cycles milestone and of the recovery item.
• Paths are duplicate-free vertex lists from $s$ to $t$ along edges; $\mathcal E_p$ is the list of consecutive pairs.
• The perspective of a function is Definition 4.4's infimum over the closed perspective cone of the epigraph. The formula $\lambda f(x/\lambda)$ is not used as a definition: in Lean it would evaluate to $0$ at $\lambda = 0$ for every argument and erase the content of (5.5e). The integrality constraint $y_e \in\{0,1\}$ is part of the feasible set; without it the goal is false (§9.4 reports relaxation gaps).
• Disclosed additions: Lemma 5.4 and Remark 5.5 assume no self-loop at $v$, which the page's partition of $\mathcal E_v$ into incoming and outgoing edges presupposes. The recovery item takes the $s$-$t$ path contained in $\{e : y_e = 1\}$, since the page's claim that this set is itself a path fails when an optimal solution carries a zero-length cycle.
• Needed infrastructure: closures of cones over compact sets, extended-real infima, and the combinatorics of unit flows on finite digraphs. Proofs of any milestone, and reusable lemmas on perspectives, are welcome.

Selected references

• T. Marcucci, J. Umenberger, P. A. Parrilo, R. Tedrake, Shortest Paths in Graphs of Convex Sets, SIAM Journal on Optimization 34(1), 2024; arXiv:2101.11565v5. https://arxiv.org/abs/2101.11565
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (perspectives and recession cones, §8). https://doi.org/10.1515/9781400873173
• R. K. Ahuja, T. L. Magnanti, J. B. Orlin, Network Flows: Theory, Algorithms, and Applications, Prentice Hall, 1993 (flow decomposition, shortest-path LP).
• T. Marcucci, M. Petersen, D. von Wrangel, R. Tedrake, Motion Planning around Obstacles with Convex Optimization, Science Robotics 8(84), 2023. https://doi.org/10.1126/scirobotics.adf7843

Motivation

Hotel rooms, rental cars, cloud servers, operating rooms and rental equipment are reusable resources: a customer occupies capacity for a fixed service time, and the capacity returns to the firm afterwards. Many of these settings also allow advance reservation, where a request made today is for a service that starts later. Lei and Jasin study dynamic pricing in this setting. Prices are posted period by period, demand is non-stationary, and the firm wants revenue close to the best achievable while never booking more units than it owns.

Classical network revenue management, where capacity is sold once and never returns, has an extensive asymptotic theory. In that literature, controls that re-solve or adjust a fluid (deterministic) plan are known to lose a vanishing fraction of the optimal revenue as demand and capacity grow (Gallego and van Ryzin 1997; Jasin 2014). Reusable resources break the standard argument, because each sale removes capacity for a window of time and not for the rest of the horizon. Lei and Jasin give the first control for reusable resources with non-stationary arrivals, deterministic service times and advance reservation whose average loss is $o(\theta^{-1/2})$ in the scale parameter $\theta$ (Lei and Jasin, Operations Research 2020).

Setting

A firm manages $I$ resource types with integer capacities $C_i \ge 1$ and sells $K \ge 1$ service types over periods $t = 1, \dots, T$. At most one request arrives per period. A type-$k$ request made at the beginning of period $t$ uses $a_{ik} \in \{0,1\}$ units of resource $i$ during periods $t+\ell_k, \dots, t+\ell_k+n_k-1$. Here $n_k$ is the service time and $\ell_k$ the reservation lead time.

In each period the firm chooses a demand-rate vector $\lambda^t \in \Omega_\lambda = [0,\lambda_U]^K$, which is equivalent to choosing prices. A type-$k$ request then arrives with probability $\lambda^t_k$, independently of the past given $\lambda^t$, and the expected revenue rate is $r^t(\lambda^t)$. The deterministic relaxation DET-H maximizes $\sum_{t=1}^T r^t(\lambda^t)$ over $\lambda^t \in \Omega_\lambda$, subject to

$$\sum_{k=1}^K \sum_{s \,:\, s+\ell_k \le t \le s+\ell_k+n_k-1} a_{ik}\lambda^s_k \le C_i \qquad \text{for every resource } i \text{ and period } t \le T.$$

Its optimal value $J^D_H$ bounds the optimal expected revenue, and the average loss of a control $\pi$ is $\mathcal{L}(\pi) = (J^D_H - \mathbf{E}[R^\pi])/T$. Let $\lambda^D$ be an optimal solution of DET-H. The quantity $\underline{n}_k$ is the smallest number of periods with $\lambda^{t,D}_k > 0$ inside any service cycle of type $k$ that carries positive demand.

The control DPC-B$(m,\epsilon)$ splits the horizon, for each type $k$, into adjacent batches $\mathcal{T}_k^b$, each with $m_k$ positive-rate periods. In period $t$ it posts

$$\lambda^t_k = \mathrm{Proj}_{[0,\lambda_U]}\Bigl[\lambda^{t,D}_k - \Bigl(\frac{\epsilon_k}{\underline{n}_k} + \frac{1}{m_k}\sum_{s \in \mathcal{T}_k^{\beta_k(t)-1}} (D^s_k - \lambda^s_k)\Bigr)\mathbf{1}\{\lambda^{t,D}_k > 0\}\Bigr],$$

where $\beta_k(t)$ is the batch containing $t$. The rate is set to $0$ when fewer than $a_{ik}$ units of some resource $i$ are free at the service start $t+\ell_k$. The buffer $\epsilon_k$ protects capacity, and the batch term corrects for the demand surprises of the previous batch.

Formalization targets

Goal: Theorem 3, display (8)

There is a constant $M_3>0$, depending only on $K$, the curvature constant $\Psi$ of Assumption A5 and a bound $R$ on $|r^t|$, such that for every instance, every valid batch partition with $m_k \le \underline{n}_k$ and every $\epsilon_k$ in the stated range,

$$\mathcal{L}(\text{DPC-B}(m,\epsilon)) \le M_3 \sum_{k=1}^K \Bigl[\frac{\epsilon_k}{\underline{n}_k} + \frac{1}{m_k} + \frac{T}{m_k}\exp\Bigl\{-\frac{(\min_j\epsilon_j-1)^2}{256K^2\min\{\max_i C_i, m_k\}}\Bigr\}\Bigr].$$

The constant is uniform in $T$, $C$, $n_k$, $\ell_k$, $m_k$ and $\epsilon_k$, which is what makes the bound informative.

Milestones

1. Lemma EC.3: on the good event $\mathcal{G}(\epsilon,m,\delta)$, the free capacity satisfies $C^t \succeq e$ and the corrected rates stay inside $(0,\lambda_U)$.
2. (EC.22): on $\mathcal{G}$, the posted rate equals the unprojected corrected rate.
3. Lemma EC.4, as proved in (EC.23): $\mathbf{P}(\bar{\mathcal{G}}) \le \sum_k \frac{4T}{m_k}\exp\{\min\{\max_i C_i, m_k\}\gamma_k^2 - \frac{\min_j\epsilon_j-1}{8K}\gamma_k\}$ for all $\gamma_k \in (0,1]$.
4. $\mathbf{E}[(\sum_{s\in\mathcal{T}_k^b}\Delta^s_k)^2] \le m_k$ for every batch.
5. $\mathbf{E}([\nabla r^t(\lambda^{t,D})]^\top(\eta^t_\delta\odot\eta^t_e)) = 0$.

A companion item states Lemma 2 in this setting: stretching $\lambda^D$ in time solves DET-H for the $\theta$-th system of display (7).

Significance

Along the scaling (7), Theorem 3 with $m_k \approx \underline{n}_k^{2/3}$ gives an average loss of $O(\theta^{-2/3}\log^{1/2}\theta)$. The non-adaptive control DPC of the same paper achieves $O(\theta^{-1/2}\log^{1/2}\theta)$ (its Theorem 1). The result shows that batch-level feedback improves on the square-root barrier for reusable resources, and it does so with heterogeneous service times and advance reservation, which cover car rental and hotel bookings.

Theorem 3 and its lemmas are proved in the paper's e-companion. No machine-checked proof of them, and no formal model of reusable-resource revenue management, is known. The mission produces a Lean model of the setting: capacity windows with lead times, the availability table $\tilde C(t,s)$, an adapted control on finite sample paths, and its exact path law. On top of that model it states the paper's main bound in full. Several printed steps need repair (see the scope section), so a formal proof would also settle the exact constants.

Difficulty

The obvious route bounds each period's loss by a Taylor expansion around $\lambda^{t,D}$ and controls the deviations by a martingale inequality. That route needs the control to coincide with the unprojected corrected rate for the whole horizon, that is, no capacity shortfall and no clipping. Capacity is a moving window of overlapping services with different lengths and lead times, so a shortfall at one period depends on requests made up to $n_k+\ell_k$ periods earlier, in other batches and other types. The batch correction makes the rates depend on past errors, so the errors are martingale differences, not independent variables. The concentration bound must hold uniformly over batches whose number grows with $T$, with a variance proxy $\min\{\max_i C_i, m_k\}$ that is not the batch length. The early periods, before any service of type $k$ has completed, need a separate threshold (the two cases of (EC.17)).

Formalization scope

All objects are defined in the namespace ReusablePricing.DPCB. The conventions are fixed as follows.

• Periods are $1,\dots,T$. A sample path is a function Fin T → Option (Fin K), recording no request or one request of a type in each period. Expectations are finite sums against the exact path law: the product over periods of the one-period law, whose probabilities are the rates posted given the past. The demand law is never left as a hypothesis.
• Decisions are rates. A turn-off is rate $0$. Prices and A1–A3 do not appear. The bound $R$ on $|r^t|$ over $\Omega_\lambda$ replaces the proofs' $r^u$. $K\lambda_U \le 1$ is assumed, as implied by at most one request per period.
• Capacity windows are empty for $t \le \ell_k$. $C^t = \tilde C(t,t)$, and $\tilde C$ is defined by its defining sentence on p. 18, not by the update rule of Step 2a, whose indices do not match its own explanation. Admission is tested for services starting within the horizon.
• $\underline{n}$ in (EC.17) is $\min_k\underline{n}_k$. The events of (EC.16) are read over the batches $\mathcal{T}_k^b$. Statements "on $\mathcal{G}$" are made on paths of positive probability.
• Lemma EC.4 is stated with the $8K$ that its proof establishes, not the printed $4K$.
• Goal statements carry every standing hypothesis of Section 6: optimality of $\lambda^D$, the convention $\lambda^{t,D}_k\in\{0\}\cup(0,\lambda_U)$, A4, A5, and the existence of a demand-carrying cycle for every type, which $\underline{n}_k$ presupposes. The sanity check exhibits instances, with and without lead time, where all hypotheses of Theorem 3 hold and the $\epsilon$-range is nonempty.

The constant $M_3$ is quantified before the instance, after only $K$, $\Psi$ and $R$. Choosing it after the instance would make the bound trivial, because the loss never exceeds $2R$.

A complete development needs Freedman- or Doob-type inequalities for bounded martingale differences on finite path spaces, second-order Taylor bounds for $C^2$ functions on boxes in $\mathbb{R}^K$, and window-counting lemmas for capacity. The first two are reusable well beyond this mission. Contributions of any of the milestones, of general martingale tools for finite adapted processes, or of a proof of the companion Lemma 2 are welcome.

Selected references

• Y. Lei and S. Jasin, Real-Time Dynamic Pricing for Revenue Management with Reusable Resources, Advance Reservation, and Deterministic Service Time Requirements, Operations Research, 2020. https://doi.org/10.1287/opre.2019.1906 (author manuscript: SSRN 2816718, https://ssrn.com/abstract=2816718)
• G. Gallego and G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1), 1997. https://doi.org/10.1287/opre.45.1.24
• S. Jasin, Reoptimization and Self-Adjusting Price Control for Network Revenue Management, Operations Research 62(5), 2014. https://doi.org/10.1287/opre.2014.1276

Motivation

Hotel rooms, rental cars, cloud servers, hospital beds and event spaces are reusable resources: a customer occupies a unit for a while and then returns it. Pricing them differs from classical revenue management, where a sold unit is gone for good. A sale now blocks capacity only for the length of the service, so the binding constraint is how many services overlap at once. Lei and Jasin (Oper. Res. 2020) study dynamic pricing in this setting with deterministic service times and, in the general model, advance reservations. They measure a pricing control by its average loss against a deterministic (fluid) benchmark.

The paper has two main results. Theorem 1 bounds the loss of a static heuristic, the Deterministic Price Control DPC($\epsilon$). Theorem 3 bounds the loss of an adaptive variant and is treated in the companion mission (II). This mission formalizes Theorem 1, the lemmas its proof rests on (Lemmas EC.1–EC.2 and the displays (EC.14), (EC.15) of the e-companion), and two structural lemmas of the model: the fluid upper bound $J^* \le J^D$ (Lemma 1) and the scaling of the fluid solution (Lemma 2).

Setting

A firm manages $I$ resource types with integer capacities $C = (C_i) \succeq e$ and offers $J$ service types over periods $t = 1, \dots, T$. At most one request arrives per period. A type-$j$ request uses $a_{ij} \in \{0,1\}$ units of resource $i$ for $n$ consecutive periods (a service cycle), and $n$ divides $T$.

The firm posts a demand-rate vector $\lambda^t \in \Omega_\lambda = [0,\lambda_U]^J$ with $\lambda_U \le 1$. A type-$j$ request then arrives with probability $\lambda^t_j$, independently of earlier periods given the posted rates, and the firm earns the revenue rate $r^t(\lambda^t)$. Writing $D^s_j \in \{0,1\}$ for realized arrivals and $(x)^+ = \max\{1,x\}$, the capacity free at the beginning of period $t$ is

$$C^t = C - \sum_{s=(t-n+1)^+}^{t-1} A D^s .$$

The deterministic relaxation is

$$\mathbf{DET}:\quad J^D = \max\Big\{\sum_{t=1}^T r^t(\lambda^t) : \lambda^t \in \Omega_\lambda,\ \sum_{s=(t-n+1)^+}^{t} A\lambda^s \preceq C \ \ \forall t \le T\Big\},$$

with optimal solution $\lambda^D = (\lambda^{t,D})$. The revenue rates are strictly concave, bounded by $R$ in absolute value, and have interior maximizers (A4). Near $\lambda^{t,D}$ their gradients and Hessians are bounded by $\Psi$ (A5, with margins $\varphi_L, \varphi_U$).

The quantity $\underline n$ of display (2) is the smallest number of periods with $\lambda^{s,D}_j > 0$ in any service cycle that carries positive demand for some type $j$.

DPC($\epsilon$) posts, in period $t$, the rate $\lambda^{t,D}_j - (\epsilon/\underline n)\mathbf 1\{\lambda^{t,D}_j > 0\}$, clamped to $[0,\lambda_U]$, for every type $j$ with $C^t \succeq A^j$. It turns off every other type (rate $0$). The average loss of a control $\pi$ is $\mathcal L(\pi) = (J^D - \mathbf E[R^\pi])/T$.

Formalization targets

Goal: Theorem 1 (p. 13)

For $\epsilon \in \big(1, \min\{\min\{\varphi_L,\varphi_U\}\underline n,\ 6\min\{\max_i C_i, n\} + 1\}\big]$,

$$\mathcal L(DPC(\epsilon)) \le M_1\Big[\frac{\epsilon}{\underline n} + \frac{T}{n}\exp\Big\{-\frac{(\epsilon-1)^2}{36\min\{\max_i C_i, n\}}\Big\}\Big],$$

with $M_1 > 0$ depending only on $J$, $\Psi$ and $R$, and not on $T$, $C$, $n$, $\epsilon$ or the other data.

Milestones (EC.3)

1. Lemma EC.1. On the event $\mathcal G(\epsilon,\delta)$ that cumulative demand errors stay below $\delta = (\underline n-1)(\epsilon-1)/(3\underline n)$ within every cycle, $C^t \succeq e$ and $\lambda^{t,D}_j - \epsilon/\underline n \in (0,\lambda_U)$.
2. (EC.14). On $\mathcal G(\epsilon,\delta)$, DPC posts exactly $\lambda^{t,D}_j - (\epsilon/\underline n)\mathbf 1\{\lambda^{t,D}_j>0\}$.
3. (EC.15). $\mathbf E[\exp\{\pm\gamma\sum_{s\in\text{cycle }b}\Delta^s_j\}] \le \exp\{\min\{\max_i C_i,n\}\gamma^2\}$ for $\gamma \in (0,1]$.
4. Lemma EC.2. $\mathbf P(\bar{\mathcal G}(\epsilon,\delta)) \le (2JT/n)\exp\{\min\{\max_i C_i,n\}\gamma^2 - \delta\gamma\}$.
5. Step 2. $J^D - \mathbf E[R^{DPC(\epsilon)}] \le T\big(\Psi J\epsilon/\underline n + (4RJT/n)\exp\{\min\{\max_i C_i,n\}\gamma^2 - \delta\gamma\}\big)$.

Companion statements: Lemma 1 ($J^* \le J^D$ for every feasible non-anticipating control) and Lemma 2 (for integer $\theta \ge 1$, $\lambda^{\lceil t/\theta\rceil,D}$ solves the DET of the $\theta$-th system $T^{(\theta)} = \theta T$, $C^{(\theta)} = \theta C$, $n^{(\theta)} = \theta n$).

Significance

Along the scaling (1), choosing $\epsilon$ of order $\sqrt{\theta\log\theta}$ in Theorem 1 gives an average loss of $O(\theta^{-1/2}\log^{1/2}\theta)$. A control computed entirely before the selling horizon is therefore asymptotically optimal for reusable resources, with an explicit rate. This bound is the baseline against which the paper's adaptive control (Theorem 3, rate $O(\theta^{-2/3}\log^{1/2}\theta)$) is measured.

The proof shows a pattern common to fluid-based revenue management: a high-probability event on which the heuristic follows the fluid plan exactly, a martingale maximal inequality bounding the complement, and a Taylor bound for the cost of the buffer. Reusable resources add one ingredient: capacity is checked over sliding windows of length $n$.

The results are proved on paper; none is machine-checked. The formalization would provide a checked version of the model (sliding-window capacity, at most one arrival per period, turn-off), of the high-probability analysis, and of the uniform constant. The printed proof has slips that a checked proof must repair. In particular, the exponent obtained by EC.3's choice of $\gamma$ is $-\frac{\underline n-2}{\underline n}\cdot\frac{(\epsilon-1)^2}{36\min\{\cdot\}}$; it differs from the printed one by an amount that a larger $M_1$ absorbs.

Difficulty

The obvious argument says that DPC keeps an $\epsilon$ buffer, so it rarely runs out of capacity. The difficulty is that "rarely" has to hold uniformly over every sliding window of $n$ periods. The rates DPC posts are themselves random, because a type is turned off whenever the realized free capacity is short.

Lemma EC.1 breaks this circularity by induction over periods on a fixed event. A capacity window of length $n-1$ straddles two consecutive cycles, which costs a factor $3$ in $\delta$, and only the periods with positive deterministic demand carry a buffer, which is why $\underline n$ appears. The demand errors form a martingale-difference sequence with predictable, path-dependent rates, so (EC.15) needs a pathwise bound on the cumulative rate within a cycle. That bound comes from the DET constraint, not from independence.

Finally, the constant $M_1$ must not depend on the instance. A bound in which $M_1$ may depend on $T$ or $C$ is trivial, since the loss never exceeds $2R$.

Formalization scope

Everything is stated in demand rates, as the paper does for DET and in all its proofs. Prices, A1–A3 and the price-derivative part of A5 do not appear. A turned-off type has rate $0$.

A sample path is a function from $\{1,\dots,T\}$ to "no request" or "one request of type $j$". Its probability is the product of the per-period probabilities under the rates the control posts, so expectations are finite sums. Expected revenue is $\mathbf E[\sum_t r^t(\lambda^t)]$, the tower-property form of the proofs. Periods are $1,\dots,T$, and window sums whose upper limit falls below the lower limit are empty.

The standing hypotheses, bundled as Standing φL φU Ψ R n̲, are:

• $I, J, n, T \ge 1$, $n \mid T$, $a_{ij} \in \{0,1\}$ with a $1$ in every column, $C \succeq e$, $\lambda_U \in (0,1]$;
• $J\lambda_U \le 1$ (added: one arrival per period on all of $\Omega_\lambda$);
• $\lambda^D$ optimal for DET, with $\lambda^{t,D}_j \in \{0\} \cup (0,\lambda_U)$;
• A4 with the explicit bound $R$ on $|r^t|$, which replaces the paper's $r^u$;
• A5, with the Hessian condition as a bound on the quadratic form;
• $\underline n$ as in (2), stated as an attained minimum, so $\underline n \ge 1$;
• the cycle assumption of p. 11.

The statements "on $\mathcal G(\epsilon,\delta)$" are claimed for every path of positive probability in the event. Theorem 1 quantifies $M_1$ after $J$, $\Psi$, $R$ and before everything else. This rules out the trivial reading in which $M_1$ is chosen per instance. Step 2 uses $\underline n$ where the printed line has $n$, and $R$ for $r^u$. $\theta$ in Lemma 2 is an integer.

Two definition files carry the model: ReusablePricing.DPC.Model holds the instance, DET, A4–A5, $\underline n$ and the $\theta$-th system; ReusablePricing.DPC.Control holds the path law, DPC, loss, events and general controls. A complete proof needs a finite-path martingale toolkit: a Doob-type maximal inequality for exponential submartingales on a finite product space, and the Bernoulli moment-generating-function bound. It also needs a multivariate mean-value or Taylor estimate on a box and an induction over sliding capacity windows. The martingale tools are reusable beyond this mission. Contributions of those general lemmas, of proofs of individual milestones, and of the optional asymptotic corollary (4) are welcome.

Selected references

• Y. Lei and S. Jasin, Real-Time Dynamic Pricing for Revenue Management with Reusable Resources, Advance Reservation, and Deterministic Service Time Requirements, Operations Research 68(3), 2020. https://doi.org/10.1287/opre.2019.1906 (author manuscript: SSRN 2816718, https://ssrn.com/abstract=2816718)
• G. Gallego and G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1), 1997. https://doi.org/10.1287/opre.45.1.24
• S. Jasin, Reoptimization and Self-Adjusting Price Control for Network Revenue Management, Operations Research 62(5), 2014. https://doi.org/10.1287/opre.2014.1294
• D. Williams, Probability with Martingales, Cambridge University Press, 1991. https://doi.org/10.1017/CBO9780511813658