Optimization

Motivation

Many estimation problems in statistics, machine learning and signal processing minimize a composite function, the sum of a smooth loss and a convex but nonsmooth regularizer or constraint: the lasso and $\ell_1$-regularized logistic regression, the graphical lasso for sparse inverse covariance estimation, and constrained least squares, where the nonsmooth part is the indicator function of a convex set. First-order proximal gradient methods (ISTA, FISTA, SpaRSA) are the standard tools, and their convergence is at best linear. Practical solvers such as glmnet, newGLMNET and QUIC instead minimize a local quadratic model of the smooth part plus the nonsmooth part at every iteration, and in practice they need far fewer iterations.

Lee, Sun and Saunders (arXiv:1206.1623, SIAM J. Optim. 2014) put these methods into one framework, proximal Newton-type methods, and proved that they inherit the local convergence rates of Newton and quasi-Newton methods for smooth problems. This mission formalizes the exact-subproblem half of their analysis, ending with q-superlinear convergence of proximal quasi-Newton methods whose Hessian approximations satisfy the Dennis–Moré criterion.

Timeline. Dennis and Moré (1974) characterized superlinear convergence of quasi-Newton methods for smooth equations and minimization by what is now called the Dennis–Moré condition. Tseng and Yun (2009) analyzed coordinate gradient descent for composite problems with a scaled quadratic model. Byrd, Nocedal and Oztoprak (2013) studied inexact proximal Newton methods for $\ell_1$-regularized problems. Lee, Sun and Saunders (2012–2014) proved quadratic and superlinear local convergence for a generic closed convex $h$.

Setting

The problem is

$$\min_{x\in\mathbb R^n} f(x) := g(x) + h(x). \qquad (1.1)$$

The smooth part $g:\mathbb R^n\to\mathbb R$ is twice continuously differentiable and strongly convex with constant $m>0$, meaning $g(y)\ge g(x)+\nabla g(x)^T(y-x)+\tfrac m2\|x-y\|^2$ for all $x,y$ (Definition 3.2). Its gradient $\nabla g$ and Hessian $\nabla^2 g$ are Lipschitz continuous with constants $L_1$ and $L_2$. The nonsmooth part $h$ is a proper closed convex function that may take the value $+\infty$. Its effective domain $D=\operatorname{dom} h$ is nonempty and convex, and $x^\star$ denotes the optimal solution of (1.1), which is unique by strong convexity.

At an iterate $x_k$ the method chooses a symmetric positive definite matrix $H_k$ and computes the search direction $\Delta x_k$, the minimizer of the model subproblem

$$\Delta x_k=\arg\min_d\ \nabla g(x_k)^Td+\tfrac12 d^TH_kd+h(x_k+d). \qquad (2.9)$$

The predicted decrease is $\lambda_k=\nabla g(x_k)^T\Delta x_k+h(x_k+\Delta x_k)-h(x_k)$. A step length $t$ satisfies the sufficient descent condition (2.19) if $f(x_k+t\Delta x_k)\le f(x_k)+\alpha t\lambda_k$ for a fixed $\alpha\in(0,\tfrac12)$. A backtracking line search with factor $\beta\in(0,1)$ takes $t_k=\beta^{j}$ for the least $j\ge0$ that passes, so the unit step is tried first. The update is $x_{k+1}=x_k+t_k\Delta x_k$ (Algorithm 1). With $H_k=\nabla^2 g(x_k)$ this is the proximal Newton method. With any other choice of $H_k$ it is a proximal quasi-Newton method. The sequence $\{H_k\}$ satisfies the Dennis–Moré criterion if

$$\frac{\|(H_k-\nabla^2 g(x^\star))(x_{k+1}-x_k)\|}{\|x_{k+1}-x_k\|}\to0. \qquad (3.2)$$

Formalization targets

Goal: Theorem 3.7

If $mI\preceq H_k\preceq MI$ for all $k$, with $0<m\le M$, and $\{H_k\}$ satisfies (3.2), then every run of Algorithm 1 from any $x_0\in D$ satisfies

$$x_k\to x^\star,\qquad \|x_{k+1}-x^\star\|=o(\|x_k-x^\star\|).$$

The goal fixes no rate constant. It asserts only the shape of the convergence.

Milestones

In the order the proof uses them:

1. Proposition 2.4: $\lambda\le-\Delta x^TH\Delta x$ and $f(x+t\Delta x)\le f(x)+t\lambda+O(t^2)$.
2. Proposition 2.5: $x$ is optimal if and only if $\Delta x=0$ at $x$.
3. Lemma 2.6: every $t\le\min\{1,(2m/L_1)(1-\alpha)\}$ satisfies (2.19).
4. Theorem 3.1 (global convergence), restated under the assumptions of §3.3: $x_k\to x^\star$.
5. Lemma 3.3: the proximal Newton method eventually accepts the unit step.
6. Theorem 3.4: the proximal Newton method converges q-quadratically, with eventually

$$\|x_{k+1}-x^\star\|\le\frac{L_2}{2m}\|x_k-x^\star\|^2 .$$

7. Lemma 3.5 / A.1: under (3.2) the unit step is eventually accepted.
8. Proposition 3.6: $\|\Delta x_1-\Delta x_2\|\le\sqrt{(1+\bar\theta)/m}\,\|(H_2-H_1)\Delta x_1\|^{1/2}\|\Delta x_1\|^{1/2}$, with $\bar\theta$ depending only on the eigenvalue bounds.

Significance

The result. Theorem 3.7 is the composite counterpart of the Dennis–Moré theorem. It says that the rate of a proximal quasi-Newton method is governed by how well $H_k$ approximates the Hessian of the smooth part along the steps actually taken, whatever the nonsmooth part is. It covers proximal BFGS-type methods for $\ell_1$-regularized and constrained problems, and it explains why solvers built on these methods reach high accuracy in few iterations. Theorem 3.4 gives the corresponding quadratic rate when the exact Hessian is used.

Formalizing it. The results are proved in the paper. None of them has a machine-checked proof: the platform currently has Newton's method only for smooth objectives (Boyd–Vandenberghe's quadratic phase in the mission Convex Optimization V: Newton's Method), and nothing on proximal or composite Newton-type methods. The formalization also settles two defects of the printed text. Theorem 3.1 is false as printed, since it lacks an upper bound on $H_k$: with $g(x)=x^2/2$, $h=0$ and $H_k=2^{k+1}$ the iterates stall at about $0.289\,x_0$. It is therefore stated here under the assumptions of §3.3. Proposition 3.6 uses an undefined constant $m_1$ (read as $m$), and the first-order inequalities in its printed proof contain a typo. The explicit constant $L_2/(2m)$ in Theorem 3.4 is the one the paper's proof derives.

Difficulty

The difficulty is the nonsmooth part. For smooth $g$ the Newton step solves a linear system, and the classical analysis works with that closed form. Here $\Delta x_k$ is defined only as the minimizer of a nonsmooth subproblem, and every estimate on it has to come from the optimality of that minimizer, i.e. from the firm nonexpansiveness of scaled proximal maps in a norm that changes with $H_k$. A natural first idea is to apply the smooth Dennis–Moré argument to $\nabla f$. It fails because $f$ is not differentiable and may be $+\infty$ outside $D$. The superlinear rate also depends on the line search eventually accepting the unit step. That acceptance comes only from a third-order Taylor bound combined with (2.15) and the Dennis–Moré residual, and a line search that may return any admissible step does not give it.

Formalization scope

• Space. The space is EuclideanSpace ℝ (Fin n), and matrices are continuous linear operators. $\nabla g$ is Mathlib's gradient, and $\nabla^2 g$ is fderiv ℝ (gradient g). "Positive definite" includes symmetry, and $mI\preceq H\preceq MI$ is stated through quadratic forms of a symmetric $H$.
• The nonsmooth part. $h$ is encoded by its domain $D$ and its values on $D$: $D$ is nonempty and convex, $h$ is convex on $D$, and the $+\infty$-extension of $h$ is lower semicontinuous. The objective $f$ is extended-valued. Only comparisons are made in EReal, never arithmetic. Replacing $h$ by a real-valued function on all of $\mathbb R^n$ would exclude indicator functions and is not the paper's setting.
• Algorithm. The search direction is a predicate: it minimizes (2.9) over $\{d : x+d\in D\}$. Backtracking is the least-$j$ rule with factor $\beta\in(0,1)$, the convention of Boyd and Vandenberghe, whom the paper cites for its line search. Runs are infinite and indexed from $k=0$, with no stopping test.
• Rates. $o(\cdot)$ and (3.2) are stated without quotients: for every $\varepsilon>0$ the inequality holds eventually.
• Ruling out trivial versions. A line search allowed to return any step satisfying (2.19) would make Theorems 3.4 and 3.7 false. Taking $x^\star$ to be an arbitrary point instead of the minimizer, or letting $\bar\theta$ in Proposition 3.6 depend on the data, would empty the statements. None of these readings is used.
• Infrastructure. A complete development needs: existence and uniqueness of minimizers of strongly convex, lower semicontinuous extended functions; first-order optimality for the subproblem; firm nonexpansiveness of scaled proximal maps in the $H$-norm; and second- and third-order Taylor bounds from Lipschitz derivatives. These pieces are reusable across proximal methods. Contributions of any milestone, of these supporting lemmas, or of the goal directly are welcome.

Selected references

• J. D. Lee, Y. Sun, M. A. Saunders, Proximal Newton-type methods for minimizing composite functions, arXiv:1206.1623v13 (2014); SIAM J. Optim. 24(3), 2014. https://arxiv.org/abs/1206.1623
• J. E. Dennis, J. J. Moré, A characterization of superlinear convergence and its application to quasi-Newton methods, Math. Comp. 28 (1974), 549–560. https://doi.org/10.1090/S0025-5718-1974-0343581-1
• P. Tseng, S. Yun, A coordinate gradient descent method for nonsmooth separable minimization, Math. Program. 117 (2009), 387–423. https://doi.org/10.1007/s10107-007-0170-0
• R. H. Byrd, J. Nocedal, F. Oztoprak, An inexact successive quadratic approximation method for convex L-1 regularized optimization, Math. Program. 157 (2016), 375–396; arXiv:1309.3529. https://arxiv.org/abs/1309.3529
• S. Boyd, L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://web.stanford.edu/~boyd/cvxbook/

Motivation

The maximum-flow problem asks how much of a commodity can be sent from a source to a sink through a network whose edges have capacities. It is a basic model in operations research (transportation, scheduling, bipartite matching) and a standard subroutine in combinatorial optimization.

Classical algorithms, from Ford and Fulkerson (1956) through Edmonds–Karp and Dinic (1970–1972) and Karzanov (1974), increase a feasible flow along augmenting paths or blocking flows. Goldberg and Tarjan, A New Approach to the Maximum-Flow Problem (J. ACM 35(4), 1988, doi:10.1145/48014.61051), replaced this global view by a local one: the push-relabel method maintains a preflow, which may violate conservation at intermediate vertices, and moves excess along edges toward vertices with smaller distance labels. The generic method, with the basic operations applied in any order, is the starting point of the FIFO, highest-label and dynamic-tree implementations analysed later in the same paper, and push-relabel codes remain among the fastest practical maximum-flow solvers.

This mission formalizes §2–§3 of the paper: the generic algorithm is correct, and it stops after a number of basic operations bounded by an explicit polynomial in the numbers of vertices and edges, whatever order of operations is chosen.

Setting

A flow network has a finite vertex set $V$ with $n = |V|$, a source $s$ and a sink $t \ne s$, and a capacity $c(v,w) \ge 0$ for every ordered pair of vertices, positive exactly on the edges $E = \{(v,w) : c(v,w) > 0\}$; $m = |E|$, and there are no loops, $c(v,v) = 0$.

Flows are real functions on all vertex pairs. A function $f$ satisfies the capacity constraint if $f(v,w) \le c(v,w)$ and antisymmetry if $f(v,w) = -f(w,v)$ for all pairs. The excess of $v$ is $e(v) = \sum_{u} f(u,v)$. A flow also has $e(v) = 0$ for $v \notin \{s,t\}$; a preflow only $e(v) \ge 0$ for $v \ne s$. The value of a flow is $|f| = \sum_v f(v,t)$, and a maximum flow is a flow of maximum value.

The residual capacity is $r_f(v,w) = c(v,w) - f(v,w)$; pairs with $r_f(v,w) > 0$ are the edges of the residual graph $G_f$. A valid labeling is $d : V \to \mathbb{N} \cup \{\infty\}$ with $d(s) = n$, $d(t) = 0$ and $d(v) \le d(w) + 1$ on every residual edge. A vertex $v$ is active if $v \notin \{s,t\}$, $d(v) < \infty$ and $e(v) > 0$.

The two basic operations (Fig. 1 of the paper) are:

• Push$(v,w)$, applicable when $v$ is active, $r_f(v,w) > 0$ and $d(v) = d(w)+1$: send $\delta = \min(e(v), r_f(v,w))$, i.e. $f(v,w) \mathrel{+}= \delta$, $f(w,v) \mathrel{-}= \delta$. It is saturating if $r_f(v,w) = 0$ afterwards and nonsaturating otherwise.
• Relabel$(v)$, applicable when $v$ is active and $d(v) \le d(w)$ for every residual edge $(v,w)$: set $d(v) \leftarrow \min\{d(w)+1 : (v,w) \in E_f\}$ ($\infty$ if there is none).

The generic algorithm (Fig. 2) starts from the preflow that saturates every edge leaving $s$ and is zero elsewhere, with the simple labeling $d(s) = n$, $d(v) = 0$ otherwise, and applies applicable basic operations in any order while one exists. An execution with $K$ basic operations is a sequence of states $(f_0,d_0),\dots,(f_K,d_K)$ from the initial state, each obtained from the previous one by one applicable operation.

Formalization targets

Goal: Theorems 3.11 and 3.4

Assume the paper's standing assumption $m \ge n-1$. For every execution with $K$ basic operations,

$$K \le (2n-1)(n-2) + 2nm + 4n^2 m,$$

and if no basic operation applies in the final state, then $f_K$ is a maximum flow. The paper states the bound as $O(n^2m)$ and proves it as "immediate from Lemmas 3.8, 3.9, and 3.10"; the goal states the sum of those three printed bounds. Since every execution is this short, no order of operations runs forever.

Milestones

In the order the proof uses them: Lemma 2.1 (at an active vertex a push or a relabel applies); Lemma 3.1 (the labeling stays valid); Theorem 3.2 (Ford–Fulkerson: a flow is maximum iff $t$ is unreachable from $s$ in $G_f$); Lemma 3.3 (under a valid labeling $t$ is unreachable from $s$); Lemma 3.5 (from any vertex with positive excess, $s$ is reachable); Lemma 3.6 (labels never decrease; a relabeling increases the label); Lemma 3.7 ($d(v) \le 2n-1$ throughout); Theorem 3.4 (termination with finite labels gives a maximum flow); Lemma 3.8 ($\le 2n-1$ relabelings per vertex, $\le (2n-1)(n-2) < 2n^2$ in total); Lemma 3.9 ($\le 2nm$ saturating pushes); Lemma 3.10 ($\le 4n^2m$ nonsaturating pushes, under $m \ge n-1$). A further, non-milestone item states the unnumbered invariant that every $f_k$ is a preflow.

Significance

The generic bound shows that push-relabel terminates in a polynomial number of steps without any rule for choosing the next operation; the specific orderings of §4–§5 of the paper (first-in first-out, $O(n^3)$; dynamic trees, $O(nm\log(n^2/m))$) refine only the count of nonsaturating pushes, and reuse Lemmas 3.1–3.9 unchanged. The correctness argument, a valid labeling excludes augmenting paths, is the template for the push-relabel minimum-cost flow and assignment algorithms that followed.

These results are proved in the paper and are textbook material. Their machine-checked counterparts are, as far as is known here, not on the Prove2Me platform: the platform's network-flow statements (from Introduction to Linear Optimization, e.g. LinearOptimization.max_flow_min_cut) use a different model, with arc-indexed nonnegative flows and extended-real capacities, and contain nothing about preflows, labels or operation counts. This mission produces a formal account of the antisymmetric-flow model, of Ford–Fulkerson in that model, and of the amortized counting arguments, with the constants the paper prints.

Difficulty

The correctness half is short once the invariants are in place; the difficulty is in the counting. The label bound (Lemma 3.7) is a statement about the whole execution, and it depends on a structural fact about preflows (Lemma 3.5) whose truth rests on antisymmetry and on the nonnegativity of excesses. The obvious first idea for the push counts, bounding pushes per edge or per vertex locally, fails for nonsaturating pushes: flow pushed across a pair can be pushed back later, and nothing local limits how often this happens, so Lemma 3.10 holds only as an amortized statement over the entire execution and depends on both earlier counts. Saturating pushes on a pair can also recur, in both directions, and Lemma 3.9 has to control the interaction between the two directions.

Formally, all of this is reasoning about arbitrary interleavings of operations, with labels in $\mathbb{N} \cup \{\infty\}$ and real-valued flows.

Formalization scope

• Vertices form a finite type with decidable equality; $n$ is its cardinality, $s \ne t$, so $n \ge 2$ and the natural-number subtractions $2n-1$ and $n-2$ are exact. Capacities are a real function on all pairs, nonnegative, zero on the diagonal; $E$ is its support and $m$ its cardinality.
• Flows and preflows are antisymmetric real functions on all pairs (not nonnegative arc flows); the excess is computed from $f$, never stored. A maximum flow is a flow whose value is at least that of every flow.
• Labels live in ℕ∞, with $\infty + 1 = \infty$; the relabel value is an infimum, which is $\infty$ on the empty set.
• An execution is a sequence of states σ : ℕ → State V with a length $K$, starting at the Fig. 2 state with the simple labeling (the paper's own assumption for its proofs), each step an applicable push or relabel. "Terminates" means that no basic operation applies, the loop guard of Fig. 2. The three counts are cardinalities of the sets of step indices of each kind.
• Explicit constants: $2n-1$ per-vertex relabelings, $(2n-1)(n-2) < 2n^2$ total relabelings, $2nm$ saturating pushes, $4n^2m$ nonsaturating pushes, label bound $2n-1$, and the total $(2n-1)(n-2)+2nm+4n^2m$. The standing assumption $m \ge n-1$ appears only on Lemma 3.10 and the goal.
• A trivializing formalization is ruled out: the step relation fixes the pushed amount $\delta = \min(e(v), r_f(v,w))$ and the new label exactly as in Fig. 1, termination is the loop guard rather than "the result is a flow", and a sorry-free check exhibits a concrete network $s \to a \to t$ with a two-step execution (relabel $a$, then push $(a,t)$), so the run hypotheses are satisfiable.

Welcome contributions: proofs of the invariants (preflow, valid labeling, label monotonicity), of Ford–Fulkerson for antisymmetric flows (reusable beyond this mission), and of the counting lemmas. The FIFO bound of §4 is the subject of a companion mission.

Selected references

• A. V. Goldberg, R. E. Tarjan, A New Approach to the Maximum-Flow Problem, Journal of the ACM 35(4):921–940, 1988. doi:10.1145/48014.61051
• L. R. Ford, D. R. Fulkerson, Flows in Networks, Princeton University Press, 1962.
• J. Edmonds, R. M. Karp, Theoretical improvements in algorithmic efficiency for network flow problems, Journal of the ACM 19(2):248–264, 1972. doi:10.1145/321694.321699
• R. K. Ahuja, T. L. Magnanti, J. B. Orlin, Network Flows: Theory, Algorithms, and Applications, Prentice Hall, 1993.

Motivation

Large retailers pay their suppliers weeks or months after delivery, and small suppliers fill the gap with short-term finance. In factoring the supplier sells the receivable to a factor for immediate cash; in reverse factoring the retailer arranges the program with a bank, which pays the supplier early at a rate priced on the retailer's credit rating. Retailers commonly attach a condition: the supplier must accept a longer payment term. Wuttke et al. (Journal of Operations Management, 2019) report that buyers extended payment terms by 54 days on average on adopting reverse factoring and that many suppliers delayed adoption; Corsten (2010) reports suppliers resisting a program because of the demanded payment delay (both as cited by Kouvelis and Xu, pp. 6082–6083). How long an extension a retailer can demand, and what it gains by demanding it, is therefore a practical design question.

Kouvelis and Xu (Management Science 67(10), 2021) answer it inside a Stackelberg supply chain model with credit and liquidity risk. This mission formalizes their answer, Proposition 6 of §5.3: the retailer's optimal payment extension when she keeps the existing wholesale price.

Setting

Demand $D\ge0$ has density $f$, distribution function $F$ and $\bar F=1-F$; $f>0$ on $[0,\mathbb Z]$ with $\mathbb Z\le+\infty$ the upper end of the support, $f$ is continuous there, the mean is finite, and the failure rate $z(\xi)=f(\xi)/\bar F(\xi)$ is strictly increasing. Write $S(q)=\int_0^q\bar F(\xi)\,d\xi$ for expected sales and $k(q)=S(q)/\bar F(q)$.

A retailer (the leader) sets a wholesale price $w$, and a capital-constrained supplier (the follower) chooses a production quantity $q\ge0$; the retail price $p$ exceeds the unit cost $c$. Each firm $j\in\{s,r\}$ has a credit rating $C_j\in(C_{\min},C_{\max})$, a default probability $\rho_j=\rho(C_j)\in[0,1]$ with $\rho$ strictly decreasing, and an interest premium $\eta_j=\eta(C_j)>0$ with $\eta$ decreasing. The lead time is $t_1$, the payment term $t_2$, and $\lambda_s,\lambda_r\ge0$ are the liquidity risks.

Under a post-shipment scheme with coefficient $\Lambda$ the supplier earns

$$\pi(q;w)=(1-\rho_s)\bigl(\Lambda e^{-\lambda_s t_1}wS(q)-c\,q\,e^{\eta_s t_1}\bigr),$$

with $\Lambda_{\mathcal F}=(1-\rho_r)+(1-\rho_s)-e^{\eta_s t_2}$ (recourse factoring), $\Lambda_{\mathcal N}=e^{-\eta_r t_2}(1-\rho_r)$ (non-recourse factoring) and $\Lambda_{\mathcal R}=e^{-\eta_r(t_2+\tau)}$ (reverse factoring with payment extension $\tau\ge0$). The retailer earns $\Pi=e^{-\lambda_s t_1}(1-\rho_r)(p-w)S(q)$ under factoring and

$$\Pi_{\mathcal R}(w,\tau)=e^{-\lambda_s t_1}(1-\rho_r)(2-e^{-\lambda_r\tau})(p-w)S(q_{\mathcal R})$$

under reverse factoring, where $q_{\mathcal R}$ is the supplier's best response. Its first-order condition is $w\bar F(q_{\mathcal R})=c_{\mathcal R}(\tau)=c\,e^{(\eta_s+\lambda_s)t_1+\eta_r(t_2+\tau)}$ (Eq. (12)).

Before reverse factoring, the supplier uses the better of the two factoring schemes. By Proposition 4 this is non-recourse, with equilibrium $(w^*_{\mathcal N},q^*_{\mathcal N})$, when $\mathbb C_{\mathcal N}<C_s\le\mathbb C_1$, and recourse, with $(w^*_{\mathcal F},q^*_{\mathcal F})$, when $C_s>\mathbb C_{\mathcal F}\vee\mathbb C_1$. The retailer keeps the existing wholesale price $w_s$ and solves problem (13): maximize $\Pi_{\mathcal R}(w_s,\tau)$ over $\tau\ge0$, subject to the supplier's acceptance (his reverse factoring profit is at least his existing one). $\mathbb C^{\max}_{\mathcal R}$ is the rating at which $\Lambda_{\mathcal F}=e^{-\eta_r t_2}$, and $\Xi_{[0,z]}(x)=\max\{0,\min\{z,x\}\}$.

Formalization targets

Goal: Proposition 6

(i) If $C_s\ge\mathbb C^{\max}_{\mathcal R}$, reverse factoring is dominated by recourse factoring. (ii) If $\mathbb C_{\mathcal N}<C_s<\mathbb C^{\max}_{\mathcal R}$, reverse factoring should be offered with

$$\tau^*_{\mathcal R}=\Xi_{[0,\tau_s]}(\tau^*_0),\qquad \lambda_r k(q)z(q)+\eta_r=2\eta_r e^{\lambda_r\tau^*_0},\quad w_s\bar F(q)=c_{\mathcal R}(\tau^*_0),$$

where $\tau_s=-\eta_r^{-1}\ln(1-\rho_r)$ with $w_s=w^*_{\mathcal N}$ in the non-recourse case, and $\tau_s=-\eta_r^{-1}\ln[(1-\rho_r)+(1-\rho_s)-e^{\eta_s t_2}]-t_2$ with $w_s=w^*_{\mathcal F}$ in the recourse case.

Milestones, in attack order

1. Eq. (12): the supplier's best response under reverse factoring.
2. Proposition 4: which factoring scheme is in force before reverse factoring.
3. §5.3, $\tau_s$: acceptance holds exactly on $[0,\tau_s]$.
4. §5.3, $\tau^*_0$: the retailer's unconstrained profit is unimodal around $\tau^*_0$.

A follow-on item states Corollary 3(ii): the retailer's profit strictly increases, and the supplier's profit is unchanged when $\tau^*_0\ge\tau_s$.

Significance

Proposition 6 is the paper's prescription for program design. It says which suppliers should be offered reverse factoring: every supplier below the indifference rating $\mathbb C^{\max}_{\mathcal R}$ and above the non-recourse feasibility threshold. It also gives the extension in closed form, the unconstrained optimum clipped to the supplier's acceptance limit. Two consequences are drawn in the paper: non-recourse factoring is dominated once the extension is optimized, and reverse factoring may leave the supplier exactly as well off as before, so it is not necessarily a win-win (Corollary 3).

The proofs are in the paper's Online Appendix B and have not been machine-checked. A formal proof here produces a checked derivation of the projection formula from the model's primitives. It covers the strict-IFR analysis of the follower's response, the reduction of the acceptance constraint to an interval, and the unimodality of the retailer's objective. The same analysis of the pull game with an effective unit cost recurs across the supply chain finance literature.

Difficulty

The retailer's objective depends on $\tau$ through two opposing channels: the liquidity factor $2-e^{-\lambda_r\tau}$ increases, while expected sales $S(q_{\mathcal R}(\tau))$ decrease because the supplier's effective cost rises. Neither factor is concave in $\tau$, and the objective need not be concave. The natural move, to set the derivative to zero and call the root a maximum, proves nothing without a sign analysis. That analysis needs the monotonicity of $k\cdot z$ along the implicitly defined response $q_{\mathcal R}(\tau)$, which is where strict IFR enters. The acceptance constraint compares the supplier's profits in two different games (reverse factoring at $\tau$ against the existing equilibrium). Reducing it to $\tau\le\tau_s$ requires the supplier's best-response profit as an explicit increasing function of his quantity. Identifying the existing equilibrium requires Proposition 4, whose "adopted" compares equilibrium profits of two Stackelberg games.

Formalization scope

The model is a single Lean structure SupplyChainFactoring.Extension.Model. Demand is a probability measure on $\mathbb R$ with a density $f$, and $\mathbb Z$ is an extended real. "Continuous p.d.f. with $f>0$ in $[0,\mathbb Z]$" is read as continuity on $[0,\mathbb Z]$, with $f=0$ outside the support. Credit functions $\rho,\eta$ are real functions constrained on $(C_{\min},C_{\max})$. The finance derivations behind the profit functions (Eqs. (1), (5), (6), Lemma 1) are not formalized: the profit functions are the model.

Readings of informal words, each also recorded in the item's Formalization Note:

• Best response: a maximizer of the supplier's profit over $q\ge0$; equilibrium: a best response pair from which no nonnegative wholesale price with a best response gives the retailer more. Neither is defined through first-order conditions.
• Feasible: some $w\ge0$ with a best response gives the retailer positive profit; adopted (Proposition 4): feasible, with equilibrium supplier profit at least (non-recourse) or strictly above (recourse) the other feasible scheme's.
• Thresholds "the unique value of $C_s$ that satisfies …" are hypotheses in exactly that form; $c_{\mathcal N}=p$ and $c_{\mathcal F}=p$ are cross-multiplied because $\Lambda_{\mathcal F}$ can be $\le0$.
• In (13) $w$ is fixed at $w_s$ (§5.3's first sentence, footnote 23). $\pi^*_{\mathcal R}$ is the supplier's best-response profit under reverse factoring at $(w_s,\tau)$, and $\max\{\pi^*_{\mathcal F},\pi^*_{\mathcal N}\}$ is his profit in the existing equilibrium.
• Dominated (Proposition 6(i)): at every $\tau\ge0$ and every $w$, the supplier's reverse factoring best-response profit is at most his recourse one. Should be offered (6(ii)): $\tau^*_{\mathcal R}$ solves (13) and the retailer's profit is at least her existing equilibrium profit.
• $\tau^*_0$ is a hypothesis: it and some $q\in(0,\mathbb Z)$ solve the paper's two equations (the paper does not argue existence). Its optimality "without the nonnegativity constraint" is stated as unimodality of $\Pi_{\mathcal R}$ on the set of real $\tau$ with $c_{\mathcal R}(\tau)<w$.
• Always increases (Corollary 3(ii)) is strict; may remain unchanged when $\tau^*_0\ge\tau_s$ is read as "is unchanged whenever $\tau^*_0\ge\tau_s$".

Three misprints of the paper are corrected: $\Xi_{[0,z]}(x)=0$ "if $x<z$" is read as "if $x<0$"; "the retailer's maximization problem in (16)" refers to (13); the middle line of the $\Pi_{\mathcal R}$ display on p. 6082 carries a stray factor $w$, and the last line is used.

The hypotheses on $\tau^*_0$ cannot be met when $\lambda_r=0$, and the goal then says nothing about the case, as in the paper. The existing equilibrium, $\tau_s$ and $\tau^*_0$ are never free parameters: $\tau_s$ is the paper's explicit formula, and the reduction of acceptance to $\tau\le\tau_s$ is a milestone to be proved, not an assumption. Every logarithm is applied to a quantity the hypotheses force positive. A formalization that assumed acceptance equivalent to $\tau\le\tau_s$ or assumed unimodality would be trivial and is excluded.

The pull game with an effective cost has the same structure as Cachon's pull contract without salvage value (platform items CachonPushPull.*), but those items assume IGFR demand with a salvage value, so they are not reused. Reusable infrastructure welcome: the strict-IFR lemmas ($k$, $k\cdot z$ and $k(q)-q$ increasing) and the explicit best response of a newsvendor-type follower.

Selected references

• P. Kouvelis, F. Xu, A Supply Chain Theory of Factoring and Reverse Factoring, Management Science 67(10):6071–6088, 2021. https://doi.org/10.1287/mnsc.2020.3788
• G. P. Cachon, The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts, Management Science 50(2):222–238, 2004. https://doi.org/10.1287/mnsc.1030.0190
• D. A. Wuttke, E. S. Rosenzweig, H. S. Heese, An Empirical Analysis of Supply Chain Finance Adoption, Journal of Operations Management 65(3):242–261, 2019. https://doi.org/10.1002/joom.1023

Motivation

Dynamic programming, as introduced by Bellman in the early 1950s, solves sequential decision problems through a functional equation: the value of a problem started in a given state equals the best one-stage return plus the value of the problem started in the state that decision leads to. In practice the argument usually runs backwards. One writes down the functional equation, finds or characterizes a solution, and reads off the structure of optimal decisions from that solution. This is legitimate only if two things hold: an optimal policy exists at all, and the solution of the functional equation that was found is the optimal value, not some other solution of the same equation.

Samuel Karlin's 1955 paper The Structure of Dynamic Programing Models (Naval Research Logistics Quarterly 2(4):285–294) gives an abstract deterministic model in which both questions can be posed precisely. It proves existence of optimal strategies by a compactness argument (Theorem 1), derives the functional equation, which it calls the Principle of Optimality, and identifies the condition under which a solution of that equation is the optimal return: a tail term must vanish. Later treatments of dynamic programming on general state spaces, such as Blackwell's discounted and positive programming (1965–1967) and the monographs of Bertsekas and Shreve, state their verification theorems in the same form, with a solution of the optimality equation plus a condition at infinity.

Setting

The model has a state space $\Omega$, a Hausdorff topological space, and a decision space $D$, a nonempty compact Hausdorff space. A strategy is a sequence $s = (\delta_1, \delta_2, \dots)$ of decisions, one per stage. The strategy space $S = D \times D \times \cdots$ carries the product topology and is compact by Tychonoff's theorem.

The data are:

• a return function $L : \Omega \times D \to \mathbb{R}$, continuous and non-negative, where $L(\omega, \delta)$ is the return for taking decision $\delta$ in state $\omega$;
• a transition $(\delta, \omega) \mapsto T_\delta\,\omega \in \Omega$, the state faced at the next stage after decision $\delta$ in state $\omega$;
• a normalization factor $P : D \to \mathbb{R}$, continuous and positive.

From an initial state $\omega$, a strategy $s$ generates the trajectory $\omega_1 = \omega$, $\omega_n = T_{\delta_{n-1}}\,\omega_{n-1}$, and the weights $P_n(s) = \prod_{i=1}^{n-1} P(\delta_i)$ with $P_1(s) = 1$. The total yield is

$$\Phi(\omega, s) = \sum_{n=1}^{\infty} L(\omega_n, \delta_n)\, P_n(s),$$

and the optimal return is $K(\omega) = \max_{s \in S} \Phi(\omega, s)$. The standing assumption of the paper, display (1), is that the partial sums $\sum_{n=1}^{k} L(\omega_n, \delta_n) P_n(s)$ converge uniformly in $s \in S$ for each $\omega$.

Formalization targets

Goal: uniqueness of solutions with vanishing tail

Let $M : \Omega \to \mathbb{R}$ solve the functional equation

$$M(\omega) = \max_{\delta \in D} \bigl\{ L(\omega, \delta) + P(\delta)\, M(T_\delta\,\omega) \bigr\} \quad \text{for all } \omega,$$

with the maximum attained, and suppose that for every $\omega$

$$\lim_{n \to \infty} \ \sup_{\delta_1, \dots, \delta_n} |M(\omega_n)| \prod_{i=1}^{n-1} P(\delta_i) = 0.$$

Then $M(\omega) = \max_{s \in S} \Phi(\omega, s)$ for every $\omega$, and the maximum is attained (pp. 290–291, §Uniqueness).

Milestones

1. Theorem 1 (p. 287). If the series (1) converges uniformly in $S$, an optimal strategy $s^*$ exists: $\Phi(\omega, s^*) = \max_S \Phi(\omega, s)$.
2. Shift identity (p. 290, first display). For a strategy $s$ with convergent yield series and the shift $s' = (\delta_2, \delta_3, \dots)$,

$$\Phi(\omega, s) = L(\omega, \delta_1) + P(\delta_1)\, \Phi(T_{\delta_1}\,\omega, s').$$

3. Principle of Optimality, eq. (2) (p. 290). $K(\omega) = \max_{\delta_1} \{ L(\omega, \delta_1) + P(\delta_1) K(T_{\delta_1}\,\omega) \}$.
4. n-step expansion (p. 291, first display). A solution $M$ of (2) satisfies, for every $n$,

$$M(\omega) = \max_{\delta_1, \dots, \delta_n} \Bigl\{ \sum_{m=1}^{n} L(\omega_m, \delta_m) P_m(s) + M(\omega_{n+1}) P_{n+1}(s) \Bigr\}.$$

Significance

Milestone 3 says that the optimal return solves the functional equation. The goal gives the converse on a class of candidate solutions: any solution with a vanishing tail is the optimal return. Together they justify solving a dynamic program by solving its functional equation. The paper's two examples, a two-operation allocation problem with discounting and a resource allocation model driving the state to the origin, obtain uniqueness among bounded solutions and among continuous solutions vanishing at the origin respectively, by checking the tail condition. Without the tail condition the conclusion fails; the paper notes that the limit term "need not be true in general for any solution to the functional equation".

All four milestones and the goal are classical results with published proofs. None of them has a machine-checked proof on this platform: its existing Bellman-equation theorems concern finite-state stochastic models with a constant discount factor, and this model has neither restriction. The mission produces a formal version of the general deterministic model on topological state spaces, with optimality characterized by a verification theorem, which later missions on the paper's examples can reuse.

Difficulty

Existence rests on continuity of $s \mapsto \Phi(\omega, s)$ on the product space. Each term $L(\omega_n, \delta_n) P_n(s)$ depends on the first $n$ decisions through the composite map $\omega_n = T_{\delta_{n-1}} \circ \cdots \circ T_{\delta_1}\,\omega$, and continuity of that composite in all decisions at once does not follow from separate continuity of $T_\delta\,\omega$ in $\delta$ and in $\omega$. The limit of the series is continuous only because the convergence is uniform.

For uniqueness, the paper's display "$M(\omega) = \max_S \Phi(\omega, s) + \lim_n \max M(\omega_n) \prod P(\delta_i)$" is not an identity: a maximum of a sum is not the sum of the maxima. A proof has to bound $M$ from above by the yield of every strategy and from below by the yield of one particular strategy, and the lower bound fails if the tail term is controlled only from above. Attainment of the maximum in the conclusion needs a strategy to be exhibited, not only a supremum computed.

Formalization scope

A strategy is a function s : ℕ → D, with the product topology. Lean's 0-based index $k$ is the paper's stage $k+1$: s 0 is $\delta_1$, trajectory T ω s 0 is $\omega_1 = \omega$, and weight P s k is $P_{k+1}(s)$, so weight P s 0 = 1. The total yield is a tsum and the optimal return a supremum over all strategies. "Maximum" is encoded as IsGreatest of a range, so every stated maximum is attained. Uniform convergence of (1) is TendstoUniformly of the partial sums to $\Phi(\omega, \cdot)$ along atTop.

The formalization commits to the following, relative to the page:

• The model's assumptions (1)–(3) of p. 286, non-negativity of $L$, and positivity and continuity of $P$ appear as hypotheses of every statement.
• A single return function $L$ is used, not stage-dependent $L_n$, as in display (1) and as the functional equation (2) requires. $P_n$ has the product form, which the paper adopts "unless stated to the contrary".
• Assumption (4), separate continuity of $T_\delta\,\omega$ in $\delta$ and in $\omega$, is strengthened to joint continuity of $(\delta, \omega) \mapsto T_\delta\,\omega$. This supports the paper's assertion (p. 287) that each term is a continuous function of $s$, which separate continuity does not give.
• $D$ is assumed nonempty. With $D$ empty there is no strategy and Theorem 1 is false.
• The paper leaves the class of admissible solutions open ("an appropriate class of M's for which the lim = 0"). The goal fixes it as the two-sided condition: for every $\omega$ and $\varepsilon > 0$ there is $N$ with $|M(\omega_n)|\,P_n(s) \le \varepsilon$ for all $n \ge N$ and all $s$. Both of the paper's examples verify this form.

Lean's tsum of a non-summable series is $0$, and a supremum of an unbounded family is $0$. Neither default can make a statement trivially true. The uniform-convergence hypothesis forces the series to converge, and under Theorem 1's hypotheses $\Phi(\omega, \cdot)$ is continuous on a compact space, so the supremum is a maximum. The goal's conclusion is stated without a supremum. A sorry-free check confirms that all hypotheses of the goal hold on a concrete instance with non-zero return: two decisions, constant return $1$, $P \equiv 1/2$, and $M \equiv 2$.

Needed infrastructure: Tychonoff's theorem, continuity of uniform limits, and attainment of maxima on compact spaces, all in Mathlib. The mission's own definitions are the trajectory, weights, partial and total yield, and the optimal return. Contributions of intermediate lemmas are welcome, for example continuity of $s \mapsto \omega_n$, summability from uniform convergence, and the upper and lower tail estimates for $M$. So are formalizations of the paper's Remarks 1 and 3 (Dini's theorem and convergence of the $k$-stage optimal returns).

Selected references

• S. Karlin, The Structure of Dynamic Programing Models, Naval Research Logistics Quarterly 2(4):285–294, 1955. https://doi.org/10.1002/nav.3800020408
• R. Bellman, Dynamic Programming, Princeton University Press, 1957. https://press.princeton.edu/books/paperback/9780691146683/dynamic-programming
• D. Blackwell, Discounted Dynamic Programming, Annals of Mathematical Statistics 36(1):226–235, 1965. https://doi.org/10.1214/aoms/1177700285
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978. https://web.mit.edu/dimitrib/www/soc.html

Motivation

A semidefinite program (SDP) minimizes a linear objective $c^Tx$ subject to a linear matrix inequality (LMI) $F(x) = F_0 + \sum_{i=1}^m x_i F_i \succeq 0$. In applications the coefficient matrices $F_i$ are measured, estimated or rounded. A solution that is feasible for the nominal data can become infeasible for data that differ from it by an arbitrarily small amount.

El Ghaoui, Oustry and Lebret (SIAM J. Optim. 9(1), 1998) introduced robust semidefinite programs (RSDPs): the constraint must hold for every admissible perturbation of the data, and the robust solution is the best point that survives all of them. Their §5 works out the examples in which the robust counterpart has a closed form. The simplest and most widely quoted is the case where every coefficient matrix is perturbed independently and without structure (§5.1): the robust LMI becomes the single convex constraint $F(x) \succeq 2\rho\sqrt{\|x\|^2+1}\,I$. The same computation gives closed-form robust versions of linear programs (§5.3), of largest-eigenvalue minimization (§5.4) and of matrix-norm minimization (§5.6), each of which is the nominal problem plus a Tikhonov-type term $\rho\sqrt{\|x\|^2+1}$. Robust linear programming under ellipsoidal uncertainty was developed at the same time by Ben-Tal and Nemirovski (Math. Oper. Res., 1998); robust least squares, the prototype of §5.6, by El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl., 1997).

Setting

Fix $m, n \in \mathbb{N}$, a level $\rho > 0$, and symmetric matrices $F_0, \dots, F_m \in \mathbb{R}^{n\times n}$. For $x \in \mathbb{R}^m$ write $F(x) = F_0 + \sum_{i=1}^m x_i F_i$ and $\|x\|^2 = \sum_{i=1}^m x_i^2$ (the Euclidean norm). For a matrix $M$, $\|M\|$ is its spectral norm, the largest singular value, and $X \succeq 0$ means that $X$ is symmetric positive semidefinite.

An unstructured perturbation is a block row $\Delta = [\Delta_0 \ \cdots \ \Delta_m]$ of $n\times n$ blocks, viewed as one $n \times n(m+1)$ matrix. It perturbs each coefficient independently:

$$\mathbf{F}(x,\Delta) = F(x) + \Delta_0 + \Delta_0^T + \sum_{i=1}^m x_i(\Delta_i + \Delta_i^T).$$

The robust feasible set is

$$\mathcal{X}_\rho = \{x \in \mathbb{R}^m : \mathbf{F}(x,\Delta) \succeq 0 \text{ for every } \Delta \text{ with } \|\Delta\| \le \rho\},$$

and the RSDP is: minimize $c^Tx$ over $\mathcal{X}_\rho$. With $R(x) = [1;\,x]\otimes I$, the $n(m+1)\times n$ matrix whose $i$-th block is $\tilde x_i I$ for $\tilde x = (1, x_1, \dots, x_m)$, the perturbation reads $\mathbf{F}(x,\Delta) = F(x) + \Delta R(x) + R(x)^T\Delta^T$ (the paper's (19)).

Three further models use the same pattern. In a robust LP, the data $[a_i^T\ b_i]^T$ of each constraint $a_i^Tx \ge b_i$ are shifted by an independent $\delta_i \in \mathbb{R}^{m+1}$ with $\|\delta_i\|_2 \le \rho$. In robust eigenvalue minimization one minimizes the worst case over $\|\Delta\|\le\rho$ of $\lambda_{\max}(\mathbf{F}(x,\Delta))$. In robust maximum-norm minimization, $H(x) = H_0 + \sum_i x_i H_i$ with $H_i \in \mathbb{R}^{p\times q}$, $\mathbf{H}(x,\Delta) = H_0 + \Delta_0 + \sum_i x_i(H_i + \Delta_i)$, and one minimizes $\max_{\|\Delta\|\le\rho}\|\mathbf{H}(x,\Delta)\|$.

Formalization targets

Goal: Theorem 5.1 (first sentence)

For every $x \in \mathbb{R}^m$,

$$x \in \mathcal{X}_\rho \iff F(x) \succeq 2\rho\sqrt{\|x\|^2+1}\; I .$$

The RSDP and problem (21), "minimize $c^Tx$ subject to $F(x) \succeq 2\rho\sqrt{\|x\|^2+1}\,I$", therefore have the same feasible set, optimal value and solutions. The goal fixes no numerical data: $F_0, \dots, F_m$, $m$, $n$ and $\rho > 0$ are arbitrary.

Milestones on the way (§5.1)

1. (19)–(20): $x \in \mathcal{X}_\rho$ iff there is $\tau \in \mathbb{R}$ with $\begin{bmatrix} F(x) - \tau I & \rho R(x)^T \\ \rho R(x) & \tau I\end{bmatrix} \succeq 0$.
2. Positivity of $\tau$ and the Schur form (for $n \ge 1$): that block matrix is $\succeq 0$ iff $\tau > 0$ and $F(x) \succeq \bigl(\tau + \rho^2(1+\|x\|^2)/\tau\bigr) I$.
3. (21): some $\tau > 0$ satisfies the Schur form iff $F(x) \succeq 2\rho\sqrt{\|x\|^2+1}\, I$.

Further milestones: the value halves of Theorems 5.2–5.4

• Theorem 5.2: the robust LP constraints hold iff $a_i^Tx - \rho\sqrt{\|x\|_2^2+1} \ge b_i$ for all $i$ (problem (23)).
• Theorem 5.3: for every $t$, $tI \succeq \mathbf{F}(x,\Delta)$ for all $\|\Delta\| \le \rho$ iff $\bigl(t - 2\rho\sqrt{\|x\|^2+1}\bigr) I \succeq F(x)$; that is, the worst-case largest eigenvalue is $\lambda_{\max}(F(x)) + 2\rho\sqrt{\|x\|^2+1}$ (problem (25)).
• Theorem 5.4: for $p, q \ge 1$, $\max_{\|\Delta\|\le\rho}\|\mathbf{H}(x,\Delta)\| = \|H(x)\| + \rho\sqrt{\|x\|^2+1}$, and the maximum is attained (problem (29)).

Significance

The goal shows that robustness against unstructured perturbations costs no more than the nominal problem: the robust counterpart is an LMI of the same size $n\times n$, with a right-hand side that is a convex function of $x$ and grows like $2\rho\|x\|$. The sets $\mathcal{X}_\rho$ have no flat faces, which the paper's §5.2 uses to define the robust center of an LMI and which underlies the uniqueness and continuity of the robust solution (the second sentences of Theorems 5.1–5.4, from §4 under hypotheses H1–H3). Theorems 5.3 and 5.4 exhibit robustification as a Tikhonov regularization with parameter $2\rho$ or $\rho$, and Theorem 5.2 turns a robust LP into a second-order cone program.

All four closed forms are proved in the paper, partly by appeal to the general SDP reformulation of its §3. No machine-checked version of any of them exists, to our knowledge. The mission produces the robust counterparts as identities of feasible sets, stated for every $x$, together with the three intermediate steps of §5.1, so that later missions on the uniqueness and stability halves can import them.

Difficulty

The goal is an exchange of a universal quantifier over an infinite family of matrices with a single matrix inequality. The inequality $\mathbf{F}(x,\Delta) \succeq F(x) - 2\rho\sqrt{\|x\|^2+1}\,I$ bounds each perturbation, but the converse needs, for each failing direction, one admissible perturbation that attains the bound; the constant $2$ comes from the two copies $\Delta R(x)$ and $R(x)^T\Delta^T$, and the constant $\sqrt{\|x\|^2+1}$ is the spectral norm of $R(x)$, which holds only because $\Delta$ is normed as one block row. Normed block by block, the worst case and the constant change. In the milestone route, the positivity of $\tau$ needs a separate argument before any Schur complement can be taken, since the Schur complement with respect to $\tau I$ is undefined at $\tau = 0$, and the elimination of $\tau$ needs the attainment of $\min_{\tau>0} \tau + a/\tau$. For Theorem 5.4 the difficulty is the attainment: an upper bound on the maximum is immediate, while the lower bound requires exhibiting an admissible perturbation that attains it.

Formalization scope

Matrices are Matrix (Fin r) (Fin c) ℝ. Coefficients are indexed by Fin (m + 1) with index 0 the constant term. A block row $\Delta$ is one matrix with columns indexed by pairs (i, b) : Fin (m + 1) × Fin n (or Fin q), and $\|\Delta\|$ is Mathlib's $\ell^2$ operator norm (open scoped Matrix.Norms.L2Operator), the largest singular value, never the default entrywise norm. The vector norm $\|x\|^2$ is written as $\sum_i x_i^2$, never as Mathlib's sup norm on Fin m → ℝ. $A \succeq B$ is (A - B).PosSemidef. Standing assumptions made explicit: $F_0, \dots, F_m$ symmetric; $\rho > 0$ (§3, p. 36); $n \ge 1$ in milestone 2 (at $n = 0$ every $\tau$ is feasible); $p, q \ge 1$ in Theorem 5.4 (empty matrices have norm $0$).

Readings and corrections of the printed text:

1. "The optimal value of the RSDP can be computed by solving (21)" is stated as the identity of the two feasible sets for every $x$, which implies equality of values and of solutions. Theorems 5.2 and 5.4 are stated the same way (5.4 through the pointwise worst-case value, with attainment), and Theorem 5.3 in epigraph form, $\lambda_{\max}(M) \le t \iff tI - M \succeq 0$.
2. Only the first sentence of each theorem is in scope. Uniqueness, regularity, Lipschitz stability and the limit $\rho \to 0$ rest on Theorem 4.3 and on external results ([31], [3]) and are not stated.
3. In (19) the paper writes $\mathcal D = \mathbb R^{n\times nm}$ and "the representation in section 5"; $\Delta$ has $m+1$ blocks, so $\mathcal D = \mathbb R^{n\times n(m+1)}$, and the representation is that of §2.2.
4. The paper derives (20) from Lemma 3.2 and (29) from Theorem 3.2, which give only sufficient conditions; the exact equivalences are the full-perturbation Lemma 3.1 / Theorem 3.1.
5. Before (21) the paper says "the scalar in the left-hand side" (it is on the right) and "the RSDP (1)" (it means the RSDP (4)). Theorem 5.3's "min-max problem (24)" is the robust version of the nominal problem (24).

A formalization in which $\|\Delta\|$ is an entrywise or blockwise norm, $\|x\|$ is the sup norm, or the robust set quantifies over a single block, changes the constant $2\rho\sqrt{\|x\|^2+1}$ and is not this theorem; the statements here rule these out by construction.

Useful, reusable infrastructure: the spectral norm of $[1;\,x] \otimes I$, Schur complements for positive semidefinite block matrices, and spectral norms of rank-one matrices. Proofs of the three §5.1 milestones and direct proofs of the goal are both welcome.

Selected references

• L. El Ghaoui, F. Oustry, H. Lebret, Robust Solutions to Uncertain Semidefinite Programs, SIAM J. Optim. 9(1):33–52, 1998. https://doi.org/10.1137/S1052623496305717
• L. El Ghaoui, H. Lebret, Robust Solutions to Least-Squares Problems with Uncertain Data, SIAM J. Matrix Anal. Appl. 18(4):1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
• A. Ben-Tal, A. Nemirovski, Robust Convex Optimization, Math. Oper. Res. 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769

Motivation

A semidefinite program (SDP) minimizes a linear objective $c^Tx$ subject to a linear matrix inequality (LMI) $F(x) = F_0 + \sum_{i=1}^m x_iF_i \succeq 0$. SDPs model problems in control, combinatorial optimization, statistics and engineering design, and they are solved efficiently by interior-point methods. In applications the data $F_0,\dots,F_m$ are rarely known exactly: they come from measurements, from linearized models, or from rounding. A solution that is optimal for the nominal data may violate the constraint for data that differ only slightly.

El Ghaoui, Oustry and Lebret (SIAM J. Optim. 9(1), 1998) asked for robust solutions: points $x$ that satisfy the constraint for every admissible value of an unknown but bounded perturbation, and among them one that minimizes $c^Tx$. Their paper, together with the contemporaneous work of Ben-Tal and Nemirovski on robust convex optimization (Math. Oper. Res. 23(4), 1998), founded robust semidefinite programming. The perturbation model they use, the linear-fractional representation (LFR), is the standard uncertainty model of robust control, where the same exact reformulation appears as the multiplier characterization of quadratic stability under norm-bounded uncertainty.

This mission formalizes the first main result of the paper: when the perturbation is full (an arbitrary matrix of bounded spectral norm), the robust problem is exactly an SDP with one extra scalar variable.

Setting

Fix natural numbers $m, n, p, q$ and a decision vector $x \in \mathbb{R}^m$. The data are:

• symmetric matrices $F_0,\dots,F_m \in \mathbb{R}^{n\times n}$, defining the affine map $F(x) = F_0 + \sum_i x_iF_i$;
• matrices $R_0,\dots,R_m \in \mathbb{R}^{q\times n}$, defining $R(x) = R_0 + \sum_i x_iR_i$;
• fixed matrices $L \in \mathbb{R}^{n\times p}$ and $D \in \mathbb{R}^{q\times p}$;
• a level $\rho > 0$.

For a matrix $X$, $\|X\|$ denotes its largest singular value (the spectral norm), and $X \succeq 0$ means that $X$ is symmetric positive semidefinite. A perturbation is a matrix $\Delta \in \mathbb{R}^{p\times q}$. The perturbed constraint matrix is the LFR (5)

$$\mathbf{F}(x,\Delta) = F(x) + L\Delta(I - D\Delta)^{-1}R(x) + R(x)^T(I - \Delta^TD^T)^{-1}\Delta^TL^T,$$

which is well defined exactly when $\det(I - D\Delta) \neq 0$. For a linear subspace $\mathcal{D}$ of $\mathbb{R}^{p\times q}$, the robust feasible set (2) is

$$\mathcal{X}_\rho = \bigl\{x \in \mathbb{R}^m : \text{for every } \Delta \in \mathcal{D} \text{ with } \|\Delta\| \le \rho,\ \mathbf{F}(x,\Delta) \text{ is well defined and } \mathbf{F}(x,\Delta) \succeq 0\bigr\},$$

and the robust SDP (4) is: minimize $c^Tx$ subject to $x \in \mathcal{X}_\rho$, for a given $c \in \mathbb{R}^m \setminus \{0\}$. In this mission $\mathcal{D} = \mathbb{R}^{p\times q}$, the full perturbation case, and the paper's standing assumption of §3.1 is $\|D\| < \rho^{-1}$.

Formalization targets

Goal: Theorem 3.1 (p. 36), as a set identity

Under $\rho > 0$, $\|D\| < \rho^{-1}$, $q \ge 1$ and $L \ne 0$, for every $x \in \mathbb{R}^m$,

$$x \in \mathcal{X}_\rho \iff \exists\,\tau \in \mathbb{R}:\ \begin{bmatrix} F(x) - \tau LL^T & R(x)^T - \tau LD^T \\ R(x) - \tau DL^T & \tau(\rho^{-2}I - DD^T)\end{bmatrix} \succeq 0. \qquad (10)$$

The paper states that the robust SDP and a corresponding solution can be computed by solving the SDP "minimize $c^Tx$ subject to (10)" in the variables $(x, \tau)$. Both problems have the objective $c^Tx$, so the identity above, between $\mathcal{X}_\rho$ and the $x$-projection of the feasible set of (10), is the content of that sentence. A companion item states the solution correspondence explicitly: $x$ is optimal for the robust SDP if and only if $(x,\tau)$ is optimal for (10) for some $\tau$.

Milestones

1. Well-posedness (§3.1, p. 36). For $\rho > 0$: $\det(I - D\Delta) \ne 0$ for every $\Delta$ with $\|\Delta\| \le \rho$ if and only if $\|D\| < \rho^{-1}$.
2. Lemma 3.1 (p. 36). For $F = F^T$, $q \ge 1$ and $L \ne 0$: $\det(I - D\Delta) \ne 0$ and $F + L\Delta(I - D\Delta)^{-1}R + R^T(I - D\Delta)^{-T}\Delta^TL^T \succeq 0$ for every $\|\Delta\| \le 1$ if and only if $\|D\| < 1$ and some scalar $\tau$ satisfies

$$\begin{bmatrix} F - \tau LL^T & R^T - \tau LD^T \\ R - \tau DL^T & \tau(I - DD^T)\end{bmatrix} \succeq 0.$$

The paper cites the S-procedure as the classical result behind Lemma 3.1; it is already proved on the platform (ConvexOptimization.s_procedure) and is included as a reference item.

Significance

The robust feasible set is defined by infinitely many matrix inequalities, one per perturbation, each rational in $\Delta$; in general such a set is convex but has no tractable description, and the paper notes that the structured version of the problem is NP-hard. Theorem 3.1 shows that for full perturbations nothing is lost by replacing that semi-infinite constraint with a single LMI of size $n + q$ in one extra variable. Consequences: the robust problem is solved by a standard SDP solver; the largest admissible perturbation level is a generalized eigenvalue problem; and the exact result is the benchmark against which the paper's sufficient conditions for structured perturbations (Theorem 3.2) and its closed-form counterparts for unstructured perturbations (Theorem 5.1) are measured.

The result is proved in the paper (from the S-procedure, with the details deferred to a cited report). To the best of available knowledge it has no machine-checked proof. The mission produces a formal statement of the LFR model and of the robust feasible set that later missions on robust SDPs can reuse, a formal proof of the well-posedness condition, and a formal proof of the exact reformulation built on the platform's S-procedure. Formalizing it also records two points the printed statement leaves implicit: the result needs $L \ne 0$ and a nonempty perturbation output dimension $q \ge 1$.

Difficulty

The direction from the LMI to robust feasibility is elementary. The converse is the substance: robust feasibility is a statement about a continuum of perturbations, each entering rationally, and testing the LMI against finitely many extreme perturbations does not produce a multiplier $\tau$. The exactness of the reformulation rests on a lossless certificate for an implication between quadratic inequalities, which holds only under a strict feasibility condition; that condition is where $L \ne 0$ enters, and without it the lemma is false. The well-posedness milestone requires showing that $\|D\| < \rho^{-1}$ is also necessary, which is not a norm estimate but needs a perturbation that makes $I - D\Delta$ singular.

Formalization scope

Matrices are Mathlib Matrix (Fin a) (Fin b) ℝ. The affine maps are given by coefficient lists indexed by Fin (m + 1), the constant term first. The norm on matrices is the $\ell^2$ operator norm, opened with open scoped Matrix.Norms.L2Operator; it is the largest singular value, and no other matrix norm is used. $X \succeq 0$ is Matrix.PosSemidef, which includes symmetry. Block matrices are Matrix.fromBlocks over the index type Fin n ⊕ Fin q, with $R(x)^T - \tau LD^T$ top-right and $R(x) - \tau DL^T$ bottom-left. Mathlib's matrix inverse returns $0$ at a singular matrix, so the condition $\det(I - D\Delta) \ne 0$ appears in the robust feasible set in the same universally quantified clause as positive semidefiniteness, as the paper's "well defined" requires; dropping it, or using an entrywise matrix norm, would change the set and is excluded.

Readings and corrections of the printed statements:

• "The RSDP (4) and a corresponding solution $x$ can be computed by solving the SDP" is read as the identity of $\mathcal{X}_\rho$ with the $x$-projection of the feasible set of (10), for every $x$, together with the solution correspondence item. A statement of equal optimal values alone would be weaker and is not used.
• Correction: $L \ne 0$ is added to Lemma 3.1 and Theorem 3.1. The printed statements fail for $L = 0$: with $n = p = q = 1$, $F = 0$, $L = 0$, $D = 0$, $R = 1$, the perturbation does not enter, so the robust condition holds, while the LMI reads $\begin{bmatrix}0 & 1\\1 & \cdot\end{bmatrix} \succeq 0$, which is infeasible.
• $q \ge 1$ makes "matrices of appropriate size" explicit; for $q = 0$ the lower-right block is empty and the equivalence fails.
• The standing assumptions $\rho > 0$ (§3) and $\|D\| < \rho^{-1}$ (§3.1) are hypotheses of the goal. In Lemma 3.1, $\|D\| < 1$ is part of the conclusion, as printed, and $\tau$ carries no sign constraint, as printed.
• The paper's standing assumption that the nominal problem is feasible ($\mathcal{X}_0 \ne \emptyset$) is not needed for the identity and is not added.

Welcome contributions: proofs of the well-posedness milestone (a spectral-norm and singular-vector argument, reusable wherever $I - D\Delta$ must be invertible); of Lemma 3.1 from the S-procedure (the reachability lemma for norm-bounded perturbations is reusable in robust control); of the goal from Lemma 3.1 by rescaling; and general lemmas on the spectral norm of rank-one matrices and on Schur complements of block matrices.

Selected references

• L. El Ghaoui, F. Oustry and H. Lebret, Robust Solutions to Uncertain Semidefinite Programs, SIAM J. Optim. 9(1), 33–52, 1998. https://doi.org/10.1137/S1052623496305717
• A. Ben-Tal and A. Nemirovski, Robust Convex Optimization, Math. Oper. Res. 23(4), 769–805, 1998. https://doi.org/10.1287/moor.23.4.769
• S. Boyd, L. El Ghaoui, E. Feron and V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994. https://doi.org/10.1137/1.9781611970777
• S. Boyd and L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004, Appendix B.2 (the S-procedure). https://web.stanford.edu/~boyd/cvxbook/