Optimization

Motivation

Negative dynamic programming is the study of infinite-horizon sequential decision problems in which every one-stage reward is non-positive and nothing is discounted. Equivalently, a non-negative cost accumulates forever and the controller minimizes its expected total. Stochastic shortest-path problems, optimal stopping with a cost per step, and inventory or replacement models without discounting all have this form. The total cost of a policy can be infinite, and none of the contraction arguments of discounted dynamic programming apply.

Blackwell settled the discounted case on Borel state and action spaces (Blackwell 1965). There the optimal return is Borel measurable and is the unique bounded solution of the optimality equation. Strauch's paper (Strauch 1966) treats the negative case on the same Borel model. One of its main results is that the optimal return still satisfies the optimality equation, even though it need not be Borel measurable.

Timeline. Blackwell (1965): discounted case, Borel spaces. Blackwell (1967, Positive dynamic programming): positive bounded case. Strauch (1966): negative case on Borel spaces. The optimal return is absolutely measurable, $(p,\varepsilon)$-optimal Markov policies exist, and the optimality equation holds. Bertsekas and Shreve (1978, Stochastic Optimal Control: The Discrete-Time Case) later recast the theory with universally measurable policies, a lower semianalytic optimal cost, and Bellman's equation $J^* = T(J^*)$ under (P), (N) and (D).

Setting

The states $S$ and actions $A$ are non-empty Borel sets. A law of motion $q(\cdot\mid s,a)$ is a probability kernel from $S\times A$ to $S$. The return $r(s,a,t)$ is a Borel function with $-\infty < r \le 0$ whose expectation $\int r(s,a,t)\,dq(t\mid s,a)$ is finite for every $(s,a)$. A policy $\pi = (\pi_1,\pi_2,\dots)$ draws the $n$th action from a kernel $\pi_n(\cdot\mid s_1,a_1,\dots,s_n)$ that may depend on the whole history. A Markov policy $(f_1,f_2,\dots)$ uses measurable maps $f_n:S\to A$, and a stationary policy $f^{(\infty)}$ uses one map at every stage. The expected return from the initial state $s$ is

$$I(\pi)(s) = \sum_{n\ge1} E^\pi_s\, r(s_n,a_n,s_{n+1}) \in [-\infty,0],$$

and the optimal return is

$$v^*(s) = \sup_\pi I(\pi)(s),$$

the supremum over all policies. Write $M(S)$ for the non-positive, extended real-valued Borel functions on $S$. For $u\in M(S)$ and an action $a$,

$$T_a u(s) = \int \big[r(s,a,t) + u(t)\big]\,dq(t\mid s,a).$$

$T$ denotes the same operator for a measurable rule $f$ in place of $a$, and $U = \sup_n T_n$ for a Markov policy $(f_1,f_2,\dots)$. A policy $\pi^*$ is $(p,\varepsilon)$-optimal, for a probability $p$ on $S$, if $p\{I(\pi^*) \ge v^* - \varepsilon\} = 1$. The Lean development uses the same names: Problem, I, In, vstar, T, Ta, U, IsPEOptimal, Conserves.

Formalization targets

Goal: the optimality equation (Theorem 8.2, negative case)

$$v^*(s) = \sup_{a\in A} T_a v^*(s) \qquad\text{for all } s\in S.$$

The equation involves no constants and no regularity hypotheses on $v^*$.

Milestones

1. Theorem 5.2 (a)–(g): monotonicity, translation, sup-, limit- and selection properties of $U$.
2. Theorem 6.1: if $Uv\ge v$ for $v\in M(S)$, some Markov policy generated from $\hat\pi$ has $I(\pi)\ge v-\varepsilon$.
3. Lemma 6.2: $U$ conserves $\sup_n I({}^n\pi)$ and $\lim_n U^n \sup_n I({}^n\pi)$.
4. Theorem 6.2: one Markov policy comes within $\varepsilon$ of the supremum of the returns of countably many Markov policies.
5. Lemma 7.1, Lemma 7.2: measurability of $(s,\nu)\mapsto\int u(s,x)\,d\nu(x)$, and Borel measurability of the set of pairs $(s, e_\pi(s))$, where $e_\pi(s)$ is the law of the future under $\pi$.
6. Theorem 7.1: $v^*$ is absolutely measurable.
7. Theorem 8.1: for every $p$ and $\varepsilon>0$ a $(p,\varepsilon)$-optimal Markov policy exists.

Optional extras: Corollary 6.1 and Theorems 6.3, 6.4, 6.5 and 8.4 (bounds and characterizations for Markov policies).

Significance

The result. The optimality equation is the entry point to every structural statement about optimal policies in the negative case. With it, a stationary policy whose rule attains the supremum in $\sup_a T_a v^*$ can be tested for optimality. Value iteration and policy improvement can be compared with $v^*$. The gap between the negative case and the discounted and positive cases can be located precisely: in the negative case $v^*$ satisfies the equation, but it need not be its unique or extremal solution. Along the way the paper proves that $v^*$ is absolutely measurable and that nearly optimal Markov policies exist for every initial distribution. These two facts are used repeatedly in later Borel-space dynamic programming.

Formalizing it. The results are proved; none is machine-checked. A formal development would contain the first Lean treatment of a total-reward Markov decision process on Borel spaces with possibly infinite returns. It would include the policy-dependent law of the future via Ionescu-Tulcea, the measurability of the optimal return over all randomized history-dependent policies, and the Bellman equation for a non-measurable value function. Bertsekas–Shreve's version of the optimality equation (universally measurable policies) appears on the platform as a separate open statement. It concerns a different policy class and is not the statement posed here.

Difficulty

Two steps of the obvious argument fail. First, the classical proof of the optimality equation picks, at each next state $t$, a policy that is $\varepsilon$-optimal from $t$ and concatenates. Without measurable selection this concatenation is not a policy. The set of $t$ where a given policy is $\varepsilon$-optimal need not be Borel, and $v^*$ itself need not be Borel measurable, so even $\int v^*\,dq$ needs justification. Second, the contraction argument of the discounted case is unavailable. $U$ does not contract, it conserves $v+c$ along with $v$, and value iteration from $0$ can converge to a function strictly above $v^*$. The paper's Example 6.1 shows that the limit of $U^n0$, the best return of generated Markov policies, and the best stationary return can all differ. Any argument has to work with policies that are only nearly optimal, and only outside sets of measure zero that depend on the initial distribution.

Formalization scope

• States and actions are non-empty standard Borel types. Policies are the published Blackwell plans (DiscountedDP.Stationary.Plan): randomized and history-dependent, one Markov kernel per decision, with decisions numbered from $0$ (Lean's π.κ n is the paper's $\pi_{n+1}$). Markov policies are MarkovPlan; "$\pi$-generated" and $G(\hat\pi)$ are the published IsGenerated and IsGeneratedPlan.
• Only the negative case is formalized: $r\le0$ real-valued, $qr$ integrable, $\beta=1$. The discounted and positive parts of Theorems 5.2, 7.1, 8.1 and 8.2, including the uniqueness and minimality clauses of Theorem 8.2, are not stated.
• Returns take values in EReal and are computed as minus a lower Lebesgue integral (lintegral) of the non-negative loss. A Bochner integral is never used for a return: it would map $-\infty$ to $0$ and make the goal false or vacuous.
• $v^*$ is the supremum over all plans. It is not assumed measurable and is never replaced by a measurable modification. $T_a v^*$ is a lintegral of a possibly non-measurable function, which equals the completion integral because $v^*$ is absolutely measurable (Theorem 7.1).
• Explicit readings of the page: the hypothesis $u\in M(S)$ of each operator statement is IsNegM u. Theorem 5.2(b) assumes $u+c\in M(S)$. "$U$ conserves $v$" includes $v\in M(S)$. Lemma 6.2 asserts that the limit defining $v_\pi$ exists. Theorem 6.2 states $\ge$ everywhere and $>$ where $\sup_j I(\pi^j) > -\infty$ (the printed $>$ fails where the supremum is $-\infty$). $(p,\varepsilon)$-optimality is "$p$-almost everywhere". Absolute measurability is NullMeasurable for every probability measure. $P(X)$ carries the Giry σ-field. The extra Theorem 8.4 reads the printed "$I(\pi) < u$" as "$\le$" (the strict reading is false).
• Reusable infrastructure: the negative model, the Ionescu-Tulcea law of the future (futureLaw), and the measurability lemmas for integrals against random measures. Contributions of measurable-selection and analytic-set results (projections of Borel sets are universally measurable; von Neumann selection) are welcome and needed.

Selected references

• R. E. Strauch, Negative Dynamic Programming, Ann. Math. Statist. 37(4) (1966) 871–890. https://doi.org/10.1214/aoms/1177699369
• D. Blackwell, Discounted Dynamic Programming, Ann. Math. Statist. 36(1) (1965) 226–235. https://doi.org/10.1214/aoms/1177700285
• D. Blackwell, Positive Dynamic Programming, Proc. Fifth Berkeley Symp. Math. Statist. Probab. 1 (1967) 415–418. https://projecteuclid.org/euclid.bsmsp/1200512999
• L. E. Dubins and L. J. Savage, How to Gamble If You Must, McGraw-Hill, 1965.
• 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

Many linear programs that arise in combinatorial optimization ask only whether a convex set contains a point satisfying a family of nonnegative linear constraints. In the fractional covering problem the constraints have the form $Ax\ge b$ with $A\ge 0$: the fractional relaxation of set cover, the Held–Karp lower bound for the travelling salesman problem, and the cutting-stock relaxation all have this shape. General-purpose LP methods solve such problems exactly but slowly. Plotkin, Shmoys and Tardos showed that when a fast subroutine can optimize a linear function over the convex set, a Lagrangean-relaxation scheme with an exponential potential finds an approximate solution with a number of subroutine calls that depends on a width parameter and on the accuracy, not on the dimension of the set (Plotkin, Shmoys, Tardos, Cornell ORIE TR 999, 1992; journal version Math. Oper. Res. 20(2), 1995).

The covering half of that paper (§3) is the object of this mission. It is the template for later covering and mixed packing–covering solvers, including those of Garg and Könemann (SIAM J. Comput. 2007) and Young (FOCS 2001).

Setting

Fix integers $m\ge1$, $n$. Let $A$ be a real $m\times n$ matrix with nonnegative entries and rows $a_1,\dots,a_m$, write $a_ix=\sum_j A_{ij}x_j$, let $b\in\mathbb R^m$ with $b>0$, and let $P\subseteq\mathbb R^n$ be a nonempty convex set contained in the nonnegative orthant.

• COVERING asks whether there is $x\in P$ with $Ax\ge b$; such an $x$ is an exact solution. For $\varepsilon>0$, an $\varepsilon$-approximate solution is $x\in P$ with $Ax\ge(1-\varepsilon)b$.
• For $x\in\mathbb R^n$, $\lambda(x)=\min_i a_ix/b_i$ is the largest $\lambda$ with $Ax\ge\lambda b$, and $\lambda^*=\max\{\lambda(x):x\in P\}$. A point $x\in P$ is $\varepsilon$-optimal when $\lambda(x)\ge(1-\varepsilon)\lambda^*$.
• The width is $\max_i\max_{x\in P}a_ix/b_i$; a number $\rho>0$ with $a_ix\le\rho\,b_i$ for all $x\in P$ and all $i$ is a width bound.
• Subroutine (7) receives $y\in\mathbb R^m$, $y\ge0$, and returns $\tilde x\in P$ maximizing $y^tAx$ over $P$; $C_{\mathcal C}(y)$ is that maximum.
• For $\alpha>0$, the dual solution corresponding to $x$ is $y_i=\frac1{b_i}e^{-\alpha a_ix/b_i}$, and the potential is $\Phi=y^tb=\sum_ie^{-\alpha a_ix/b_i}$.
• The relaxed optimality conditions are $(\mathcal C1)$: $(1+\varepsilon)\lambda\,y^tb\ge y^tAx$, and $(\mathcal C2)$: $C_{\mathcal C}(y)-y^tAx\le\varepsilon\,(C_{\mathcal C}(y)+y^tb)$.
• IMPROVE-COVER$(x,\varepsilon)$ (Figure 3) sets $\lambda_0=\lambda(x)$, $\alpha=4\lambda_0^{-1}\varepsilon^{-1}\ln(4m\varepsilon^{-1})$ and $\sigma=\varepsilon/(4\alpha\rho)$; while $\lambda(x)\le2\lambda_0$ and $\mathcal C2$ fails, it moves $x$ to $(1-\sigma)x+\sigma\tilde x$, $\tilde x$ the subroutine's answer for the current dual solution.
• The covering algorithm obtains a start with $Ax\ge\frac1mb$ from $m$ subroutine calls, calls IMPROVE-COVER with $\varepsilon=1/6$ until $\mathcal C2$ holds or an exact solution appears, then halves $\varepsilon$ phase by phase.

The Lean names match: rowVal, lam, WidthBound, IsMaxOracle, C1, C2, dualY, potential, improveCover, initCover, coverAlgorithm, in the namespace FracPackCover.Covering.

Formalization targets

Goal: Theorem 3.7 (p. 21)

For every instance as above, every width bound $\rho$, every exact maximization oracle and every $0<\varepsilon_0<1$, the covering algorithm stops after at most

$$N=m+\big(\lceil\log_2m\rceil+1\big)\big(2+4320\,\rho\ln(24m)\big)+2\lceil\log_2\varepsilon_0^{-1}\rceil+9408\,\rho\,\varepsilon_0^{-2}\ln\frac{24m}{\varepsilon_0}$$

calls to subroutine (7), and either returns $x\in P$ with $Ax\ge(1-\varepsilon_0)b$, or reports that no $x\in P$ has $Ax\ge b$, correctly. This is the paper's $O(m+\rho\log^2m+\varepsilon^{-2}\rho\log(m\varepsilon^{-1}))$ with the constants of its proof.

Milestones

In the order the proof uses them:

• Lemma 3.1: $\mathcal C1$ and $\mathcal C2$ imply that no exact solution exists if $\lambda\le1-3\varepsilon$, and that $x$ is $3\varepsilon$-optimal if $\lambda\ge1-3\varepsilon$.
• Lemma 3.2: if $\alpha\ge2\lambda^{-1}\varepsilon^{-1}\ln(4m\varepsilon^{-1})$, the dual solution corresponding to $x$ satisfies $\mathcal C1$.
• Lemma 3.3: while $\mathcal C2$ fails, a step of size $\sigma\le\varepsilon/(4\alpha\rho)$ lowers the potential: $\Phi-\hat\Phi\ge\varepsilon\alpha\sigma\Phi$.
• Lemma 3.4: during IMPROVE-COVER, $\lambda\ge\frac34\lambda_0$.
• Theorem 3.5: one call of IMPROVE-COVER makes at most $2+20\rho\varepsilon^{-3}\ln(4m/\varepsilon)$ oracle calls, and at most $2+196\rho\varepsilon^{-2}\ln(4m/\varepsilon)$ from a $6\varepsilon$-optimal start with $\varepsilon\le1/12$.
• Lemma 3.6: $m$ oracle calls give $x\in P$ with $Ax\ge\frac1mb$, or prove that no exact solution exists.

Significance

Theorem 3.7 says that approximate fractional covering is no harder, in subroutine calls, than about $\rho\varepsilon^{-2}\log(m/\varepsilon)$ linear optimizations over $P$, plus lower-order terms in $m$. In §6 of the paper this yields fast approximation algorithms for covering-type relaxations such as the Held–Karp bound and the bin-packing and cutting-stock relaxations, where $P$ is a product of simple sets and the subroutine is a minimum-spanning-tree or knapsack computation. The result also certifies infeasibility: when the algorithm reports that no exact solution exists, the dual vector at hand proves it.

The result has been proved since 1991 and has been reproved in several later frameworks. As far as is known, it has not been machine-checked. A formal development contributes the explicit constants and a precise statement of the driver, which the paper gives only in prose. It also provides a reusable Lean account of exponential-potential methods with an optimization oracle.

Difficulty

The obvious argument tracks the potential $\Phi$ and stops when it is small. This does not work directly, because $\alpha$ is tied to $\lambda_0$, and the guarantee $\mathcal C1$ depends on $\lambda$ staying close to $\lambda_0$ throughout. Lemma 3.4 controls that, and it is a statement about the reachable states of a while loop, not about an arbitrary point. Two further points are delicate. Unlike packing, condition $\mathcal C2$ is not scaled by $\lambda$, so $\mathcal C1$ and $\mathcal C2$ give $\varepsilon$-optimality only when $\lambda$ is near $1$; the first phase must first raise $\lambda$ from $1/m$ by repeated doubling. And the cost of $\varepsilon$-scaling is bounded only because each phase starts from a $6\varepsilon$-optimal point, which requires carrying Lemma 3.1 across phase boundaries. The bookkeeping that turns per-call bounds into a single explicit $N$, over a fuel-bounded run, is substantial.

Formalization scope

Rows are Fin m with [NeZero m], coordinates Fin n; $A$ is a Matrix (Fin m) (Fin n) ℝ; $P$ is a Set (Fin n → ℝ), convex, nonempty and in the nonnegative orthant. $\lambda(x)$ is a Finset.inf' over the rows. Conventions committed to:

• Width. $\rho$ is any upper bound with $\rho>0$, not a supremum; the theorems hold for every such bound, the exact width included.
• Oracle. Subroutine (7) is a function that, for every $y\ge0$, returns a maximizer of $y^tAx$ over $P$; every theorem quantifies over all such functions. Box (7) of the report prints "min", but every use maximizes; the maximizer reading is adopted.
• Optimality without $\lambda^*$. "$x$ is $c\varepsilon$-optimal" is stated as $(1-c\varepsilon)\lambda(x')\le\lambda(x)$ for every $x'\in P$.
• Runs. IMPROVE-COVER and the driver are fuel-bounded functions returning some (result, oracle calls) when they stop within the fuel. Each while-test that reaches the $\mathcal C2$ check costs one oracle call; the loop body reuses that answer. The goal asserts that the run with fuel $\lceil N\rceil$ stops; it does not assume termination.
• Driver. The prose of pp. 20–21 is written down as initCover, firstPhase and scalingPhases with $\varepsilon_k=\frac16 2^{-k}$.
• Constants replacing $O(\cdot)$. Theorem 3.5: $2+20\rho\varepsilon^{-3}\ln(4m/\varepsilon)$ and $2+196\rho\varepsilon^{-2}\ln(4m/\varepsilon)$ oracle calls. Theorem 3.7: the $N$ above.
• Implicit hypotheses made explicit. $y\ne0$ and $\varepsilon<\frac13$ in Lemma 3.1; $\lambda>0$ in Lemmas 3.2–3.4 and Theorem 3.5; $\sigma\ge0$ in Lemma 3.3.
• Misprint. Theorem 3.5's second sentence names IMPROVE-PACKING; it is stated for IMPROVE-COVER.

A trivializing formalization is ruled out: the goal requires the run to return an outcome within the stated number of oracle calls, for every exact oracle and every width bound, and each outcome must be correct.

A complete development needs elementary real analysis (the second-order bound $e^{x+\delta}\le e^x+\delta e^x+\frac\varepsilon2|\delta|e^x$ for $|\delta|\le\varepsilon/4$), geometric-decay counting arguments, and induction over fuel-bounded loops. The potential-decrease and termination lemmas are reusable for the packing and general missions of the same paper. Proofs of any milestone, and alternative arguments with better constants, are welcome.

Selected references

• S. A. Plotkin, D. B. Shmoys, É. Tardos, Fast Approximation Algorithms for Fractional Packing and Covering Problems, Cornell University School of ORIE Technical Report No. 999, February 1992. https://core.ac.uk/download/79020349.pdf
• S. A. Plotkin, D. B. Shmoys, É. Tardos, Fast Approximation Algorithms for Fractional Packing and Covering Problems, Mathematics of Operations Research 20(2), 257–301, 1995. https://doi.org/10.1287/moor.20.2.257
• N. Garg, J. Könemann, Faster and Simpler Algorithms for Multicommodity Flow and Other Fractional Packing Problems, SIAM Journal on Computing 37(2), 630–652, 2007. https://doi.org/10.1137/S0097539704446232
• N. E. Young, Sequential and Parallel Algorithms for Mixed Packing and Covering, Proc. 42nd IEEE FOCS, 538–546, 2001. https://arxiv.org/abs/cs/0110040

Motivation

Lagrangian duality turns a constrained minimization problem into the maximization of a dual function over multipliers. For convex programs the duality is clean: under mild conditions the dual optimal value equals the primal one, and an optimal multiplier vector $\bar y$ exists. Computationally, however, the ordinary Lagrangian has a well-known defect. Knowing an optimal $\bar y$ does not tell where the primal optimum is, because the minimizers of $x \mapsto L_0(x, \bar y)$ over $X$ typically include points that are not optimal and not even feasible. A linear program is the extreme case: $L_0(\cdot, \bar y)$ is then often constant.

The penalty Lagrangian (also called the augmented Lagrangian) of Hestenes, Powell and Rockafellar repairs this defect. R. T. Rockafellar's 1973 paper Math. Programming 5, 354–373 develops its duality theory for convex programs in an arbitrary real vector space. This mission formalizes the "exactness" part of that theory, §3 of the paper: for $r > 0$, minimizing the penalty Lagrangian at an optimal multiplier gives exactly the optimal solutions of the original problem. The paper puts it as "a strong property whose well-known absence for $L_0$ has been a serious impediment to computational approaches based on duality" (p. 362). Together with the smoothness of the dual function (Theorem 3.2, another mission of this series), this property is what justifies the method of multipliers as an algorithm for constrained optimization.

Timeline. Hestenes (1969) and Powell (1969) proposed the multiplier method for equality constraints. Rockafellar (1973, this paper) gave the inequality-constrained penalty Lagrangian $L_r$ below and its convex duality theory. Bertsekas's monograph Constrained Optimization and Lagrange Multiplier Methods (1982) systematized the theory.

Setting

Let $E$ be a real vector space, $X \subseteq E$ a nonempty convex set, and $f_0, f_1, \dots, f_m : X \to \mathbb R$ convex functions. The problem is

$$\text{(P)}\qquad \text{minimize } f_0(x) \text{ over } x \in X \quad\text{subject to } f_i(x) \le 0,\ i = 1, \dots, m.$$

A point is feasible if it lies in $X$ and satisfies the constraints. The optimal value "inf in (P)" is the infimum of $f_0$ over the feasible points, an element of $[-\infty, +\infty]$. An optimal solution is a feasible $\bar x$ with $f_0(\bar x) \le f_0(x)$ for every feasible $x$.

For $y \in \mathbb R^m$ (no sign restriction), $\theta(t) = \max\{0, t\}$ and $r > 0$, the penalty Lagrangian is

$$L_r(x, y) = f_0(x) + \frac{1}{4r}\sum_{i=1}^m \big[\theta(y_i + 2 r f_i(x))^2 - y_i^2\big].$$

The ordinary Lagrangian is $L_0(x, y) = f_0(x) + \sum_i y_i f_i(x)$ for $y \ge 0$, and $-\infty$ otherwise. The dual objectives are $g_r(y) = \inf_{x \in X} L_r(x, y)$ and $g_0(y) = \inf_{x \in X} L_0(x, y)$. Problem $(D_r)$ maximizes $g_r$ over $\mathbb R^m$.

• A dual optimal solution is a maximizer $\bar y$ of $g_r$ with $g_r(\bar y) > -\infty$.
• (P) is normal if the dual optimal value $\sup g_0$ equals the optimal value of (P).
• $\bar y$ is a Kuhn–Tucker vector relative to $L_r$ if $-\infty < \inf_{x \in X} L_r(x, \bar y) = \inf$ in (P).
• $(\bar x, \bar y)$ is a saddle point of $L_r$ if $\bar x \in X$ and $L_r(\bar x, y) \le L_r(\bar x, \bar y) \le L_r(x, \bar y)$ for all $x \in X$, $y \in \mathbb R^m$.

In Lean these are Lr, L0, gr, g0, primalValue, dualValue, IsNormal, IsDualOptimal, IsKTVector, IsSaddle, IsOptimal and KuhnTuckerConditions, in the namespace PenaltyLag.Exact.

Formalization targets

Goal: Theorem 3.5 (p. 362)

Assume (P) is normal, $\bar y$ is a dual optimal solution, and $r > 0$. Then for every $\bar x \in E$

$$\bar x \text{ is optimal for (P)} \iff \bar x \in X \text{ and } L_r(\bar x, \bar y) \le L_r(x, \bar y) \ \ \forall x \in X.$$

Milestones (attack order)

1. §3 after (3.17), pp. 361–362: for $r > 0$, $\bar y$ is a Kuhn–Tucker vector relative to $L_r$ iff $\bar y$ is optimal for $(D_r)$ and (P) is normal.
2. §3, p. 362: for $r > 0$, $(\bar x, \bar y)$ is a saddle point of $L_r$ iff $\bar x$ is optimal for (P) and $\bar y$ is a Kuhn–Tucker vector.
3. Corollary 3.4, $r > 0$ (p. 362): $L_r$ and $L_0$ have the same Kuhn–Tucker vectors and the same saddle points, and the saddle points of $L_r$ are exactly the pairs satisfying the ordinary Kuhn–Tucker conditions

$$\bar y_i \ge 0,\ f_i(\bar x) \le 0,\ \bar y_i f_i(\bar x) = 0\ (\forall i), \qquad \bar x \in \operatorname{argmin}_X \Big(f_0 + \sum_i \bar y_i f_i\Big).$$

4. Corollary 3.4, $r = 0$: the saddle points of $L_0$ are exactly the pairs satisfying the ordinary Kuhn–Tucker conditions.
5. Proof of Theorem 3.5, pp. 362–363: if $\bar y$ is optimal for $(D_r)$ and $\bar x \in X$ minimizes $L_r(\cdot, \bar y)$ over $X$, then $\nabla_y L_r(\bar x, \bar y) = 0$ and $\bar y$ maximizes $L_r(\bar x, \cdot)$ over $\mathbb R^m$.

Significance

The result. Theorem 3.5 turns a constrained problem into an unconstrained one with no loss of exactness. Once an optimal multiplier is known, every minimizer of $L_r(\cdot, \bar y)$ over $X$ solves (P), and conversely. Section 4 of the paper builds the computational scheme on this: maximize the smooth concave function $g_r$ over $\mathbb R^m$, then minimize $L_r(\cdot, \bar y)$ over $X$. For the ordinary Lagrangian the corresponding statement is false (p. 363), so the theorem marks precisely what the quadratic penalty term adds. Corollary 3.4 records the other half of the picture: in Kuhn–Tucker vectors and saddle points, $L_r$ behaves exactly like $L_0$.

Formalizing it. All results are proved in the paper, partly by citation of Rockafellar's Convex Analysis (§§28–30, 36). On the Prove2Me platform, saddle-point characterizations exist only for the ordinary Lagrangian on $\mathbb R^n$ (for instance ConvexOptimization.lagrangian_saddle_iff_strong_duality, and Beck's Theorem 2.7 as FirstOrderOpt.ConvexTheory.saddle_point_sufficient / saddle_point_necessary). This mission adds the penalty Lagrangian, convex sets in an arbitrary real vector space, extended-real dual values, and the exactness theorem itself. None of these statements is known to us to be machine-checked elsewhere.

Difficulty

The "if" direction is the substantive one. A minimizer $\bar x$ of $L_r(\cdot, \bar y)$ is not known to be feasible; feasibility must come from maximality of $\bar y$ in the dual. The natural argument for $L_0$ breaks at exactly this point: $L_0(\bar x, \cdot)$ is affine on the orthant, and minimality in $x$ gives no information about $\nabla_y$. For $L_r$ the link is the differentiability of the dual function $g_r$ with $\nabla g_r(\bar y) = \nabla_y L_r(\bar x, \bar y)$ (Theorem 3.2), which is posed in another mission of this series and is not available as a platform result. Every statement involves extended-real dual values on a vector space with no topology, so $\pm\infty$ must be handled at each step.

Formalization scope

• $E$ is a bare real vector space (AddCommGroup E, Module ℝ E), as in the paper; no norm or topology is used.
• $X$ is a Set E. Each statement assumes the paper's standing hypothesis (p. 358): $X$ convex and nonempty, $f_0, \dots, f_m$ convex on $X$.
• The $f_i$ are total functions E → ℝ, and only their values on $X$ enter. Constraint indices are Fin m (0-based), with $f_0$ a separate argument.
• $\mathbb R^m$ is EuclideanSpace ℝ (Fin m).
• $g_r$, $g_0$, $L_0$, the optimal value of (P) and the dual optimal value are EReal-valued. An infeasible (P) has value $+\infty$, and $g_0 = -\infty$ off $y \ge 0$.
• $r > 0$ is an explicit hypothesis wherever the paper has it. Theorem 3.5 is false for $r = 0$ (p. 363), and the Lean expression Lr at $r = 0$ is not $L_0$.
• "Dual optimal solution" in Theorem 3.5 is read as optimal for $(D_r)$ with the same $r$, with $g_r(\bar y) > -\infty$ (the convention of p. 361). The paper's reading, optimal for $(D_0)$, is equivalent by Theorem 3.2, which is posed in mission 1 of this series.
• "$\bar x$ minimizes $L_r(\cdot, \bar y)$ over $X$" includes $\bar x \in X$. The equivalence is stated for every $\bar x \in E$. No sign condition is imposed on $\bar y$: nonnegativity is a consequence of dual optimality, not a hypothesis.
• Saddle points are taken over $X \times \mathbb R^m$ (Rockafellar's Convex Analysis, §36). For $L_0$ they are taken in the extended reals.
• Trivializing readings ruled out: normality is neither dropped nor replaced by existence of an optimal solution or by Slater's condition, and the minimization on the right of Theorem 3.5 is never over a set containing points outside $X$.

The solver needs the representation $L_r(x, y) = \min_u\{F_r(x, u) + u \cdot y\}$, weak duality, the envelope formula and differentiability of $g_r$ (Theorem 3.2), and a convex-duality fact for normal programs. Those parts are reusable beyond this mission, and proofs of the paper's Theorem 3.2 in this setting are welcome as auxiliary results.

Selected references

• R. T. Rockafellar, A dual approach to solving nonlinear programming problems by unconstrained optimization, Mathematical Programming 5 (1973) 354–373. https://doi.org/10.1007/BF01580138
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
• M. R. Hestenes, Multiplier and gradient methods, Journal of Optimization Theory and Applications 4 (1969) 303–320. https://doi.org/10.1007/BF00927673
• M. J. D. Powell, A method for nonlinear constraints in minimization problems, in R. Fletcher (ed.), Optimization, Academic Press, 1969, 283–298.
• D. P. Bertsekas, Constrained Optimization and Lagrange Multiplier Methods, Academic Press, 1982.

Motivation

Inventory systems in which unmet demand is lost, not backlogged, are the norm in retail: a customer who finds an empty shelf buys elsewhere. With a positive lead time $L$ between ordering and delivery, the optimal policy for such a system depends on the entire pipeline of outstanding orders, so dynamic programming is intractable beyond small $L$. Optimal policies are not of base-stock type, and for decades no policy with a provable guarantee on its expected cost was known for this model.

Levi, Janakiraman and Nagarajan (Math. Oper. Res. 33(2), 2008) gave the first such guarantee. Their dual-balancing policy balances, in every period, the expected holding cost against the expected lost-sales penalty of the units ordered now, and it costs at most twice as much as an optimal policy.

Timeline.

• 2007. Levi, Pál, Roundy and Shmoys (Math. Oper. Res. 32(2)) introduce marginal cost accounting and the dual-balancing policy for the backlogging model, with a worst-case guarantee of 2.
• 2008. Levi, Janakiraman and Nagarajan extend the guarantee to lost sales (this mission). In their model the truncated inventory positions of the two policies can cross back and forth inside a lead time, which the backlogging argument never meets.
• 2009. Huh, Janakiraman, Muckstadt and Rusmevichientong (Management Science, 2009) prove that order-up-to policies are asymptotically optimal in the lost-sales model as the penalty cost grows.
• 2021 onward. Xin (Oper. Res., 2021; SSRN 7134538) analyses capped base-stock policies for i.i.d. lost-sales demand, culminating in a 2.33-approximation guarantee for that policy class, whose main theorem is proved on Prove2Me.

Page and display numbers in this mission refer to the authors' accepted manuscript (28 pages, pp. 1–28), not to the journal's pages 351–374.

Setting

Periods are $t=1,\dots,T$. An order $Q_s\ge0$ placed in period $s$ arrives at the start of period $s+L$, where $L\ge1$ is an integer. Before the horizon there are $x_0\ge0$ units on hand and pipeline orders $Q_j=q_j\ge0$ for $1-L\le j\le0$. Demands $D_1,\dots,D_T\ge0$ have finite means. The information $\mathcal F_s$ available at the start of period $s$ contains $D_1,\dots,D_{s-1}$ and possibly more. A feasible policy chooses $Q_s$ as an $\mathcal F_s$-measurable quantity.

The on-hand inventory $I_t$ at the start of period $t$, after the arrival, satisfies $I_1=x_0+Q_{1-L}$ and

$$I_{t+1}=(I_t-D_t)^+ + Q_{t+1-L}.$$

Demand $(D_t-I_t)^+$ is lost. Costs are a holding rate $h_t\ge0$, a lost-sales penalty $p_t\ge0$ and an ordering cost $c_t\ge0$ per unit, where $p_t$ and $c_t$ are non-increasing in $t$.

Marginal cost accounting. Under first-ordered-first-consumed bookkeeping, $H_s$ is the ordering cost $c_sQ_s$ plus the holding cost that the $Q_s$ units incur until the end of the horizon, and $\Pi_s=p_{s+L}(D_{s+L}-I_{s+L})^+$ is the lost-sales penalty in the period in which they arrive. The cost of a policy $P$ is

$$\mathcal C(P)=\sum_{s=1}^{T-L}\bigl(H^P_s+\Pi^P_s\bigr).$$

It omits only costs that are the same for every policy.

The truncated inventory position of period $s$ with respect to $t\le s$ is $Y_{st}=I_s+\sum_{j=s+1-L}^{t}Q_j$. For two policies $B$ and $P$, the set $\mathcal T_H$ holds the periods $t\le T-L$ with $Y^B_{st}<Y^P_{st}$ for every $s\in[t,t+L]$, and $\mathcal T_\Pi$ holds the remaining periods $t\le T-L$.

A dual-balancing policy $B$ orders, in each period $t\le T-L$, the amount that equalises the two conditional expectations

$$E[H^B_t\mid\mathcal F_t]=E[\Pi^B_t\mid\mathcal F_t]=:Z_t.$$

Formalization targets

Goal: Theorem 3.1

If demands are independent, then for every feasible policy $P$

$$E[\mathcal C(B)]\le 2\,E[\mathcal C(P)].$$

Comparing with every feasible $P$, rather than with an optimal policy, gives the guarantee without assuming that an optimum is attained.

Milestones, in attack order

1. (11) For $t\le s\le t+L$, $I_{t+L}=Y_{st}-D_{[s,t+L)}+\sum_{r=s}^{t+L-1}(D_r-I_r)^+$.
2. Lemma 3.2. On every sample path, $\sum_{t\in\mathcal T_H}H^B_t\le\sum_{t}H^P_t$.
3. Lemma 3.3. On every sample path, $\sum_{t\in\mathcal T_\Pi}\Pi^B_t\le\sum_{t}\Pi^P_t$.
4. (14) $E[\mathcal C(P)]\ge E\bigl[\sum_t(\mathbb 1_{t\in\mathcal T_H}H^B_t+\mathbb 1_{t\in\mathcal T_\Pi}\Pi^B_t)\bigr]$.
5. Lemma 3.1. $E[\mathcal C(B)]=2\sum_{t=1}^{T-L}E[Z_t]$.
6. Lemma 3.4. This lemma characterises the crossing events $A_{st}=[Y^B_{st}<Y^P_{st}]\cap[Y^B_{s+1,t}\ge Y^P_{s+1,t}]$.
7. Lemmas 3.5 and 3.6. Under independence, conditioning on $t\in\mathcal T_H$ (respectively $t\in\mathcal T_\Pi$) does not lower the conditional expected holding (respectively lost-sales) cost of $B$ below $Z_t$.

Significance

The result. The theorem gives a constant-factor guarantee for a lost-sales system with lead times, for arbitrary independent and non-identical demand distributions. The policy is computed online, one period at a time, from one-dimensional conditional expectations, which an optimal policy cannot be. The guarantee holds with time-dependent holding costs and with non-increasing ordering and penalty costs. Section 5 of the paper extends it to correlated demand structures, which are out of this mission's scope.

Formalizing it. The theorem is proved on paper and, to our knowledge, has no machine-checked proof. The mission produces the lost-sales dynamics, the truncated inventory position, marginal cost accounting and the sample-path amortization lemmas as reusable Lean objects. It also produces a formal treatment of the conditional-expectation step under independence, which the backlogging analysis does not need. The sibling mission on the backlogging model, LeviBalancing.DualBalancing, provides the shared instance and policy definitions that are reused here.

Difficulty

In the backlogging model, $t\in\mathcal T_H$ is decided by information available at time $t$, so the cost comparison can be made period by period after conditioning on $\mathcal F_t$. With lost sales this fails: the truncated positions of $B$ and of the benchmark can cross from below to above and back inside the window $[t,t+L]$. Whether $t\in\mathcal T_H$ is therefore not known at time $t$, and conditioning on that event moves the conditional expectations of $H^B_t$ and $\Pi^B_t$ away from $Z_t$. A newcomer's first idea, to reuse the backlogging argument with $\mathcal F_t$-measurable indicators, does not apply. The lost-sales penalty also cannot be charged period by period: Lemma 3.3 is a global amortization over intervals. The non-increasing penalties are what make that amortization possible when $p_t$ varies.

Formalization scope

• Periods are integers. The pipeline $Q_j$, $j\le0$, is shared by every policy through the published order. Instance, cumDemand, order, DemandProcess and IsFeasiblePolicy are reused from LeviBalancing.DualBalancing. The new layer is one definition file, LostSalesBalancing.DualBalancing.Model.
• Orders and demands are real (fractional orders, as in §3.1). The randomized integral-order variant is out of scope.
• Cost generality is that of Theorem 3.1. Rates are only required to be $\ge0$, which strengthens the paper's stationary $h,p>0$. Accordingly (11) is stated in lost units, and Lemma 3.4(iv) is stated as positive lost demand, not positive penalty.
• Independence. The paper assumes independent demands but lets $\mathcal F_s$ hold more than past demands. The formalization requires $\mathcal F_t$ to be independent of $(D_t,\dots,D_T)$ for every $t$, which for the natural filtration is exactly mutual independence. Finite means are integrability.
• "OPT" becomes every feasible policy in Theorem 3.1, (14) and Lemmas 3.5–3.6. In the sample-path statements, (11) and Lemmas 3.2–3.4, it becomes every nonnegative order sequence.
• Conditional events. $\Pr(A\mid\mathcal F)\,E[X\mid\mathcal F,A]$ is written $E[\mathbb 1_AX\mid\mathcal F]$, which never divides by a zero probability.
• Expected costs are lower Lebesgue integrals in $[0,\infty]$. The dual-balancing predicate requires $H^B_t$ and $\Pi^B_t$ to be integrable, so no conditional expectation takes Mathlib's default value $0$.
• Lemma 3.4(iii) is stated with $D_s\ge I^P_s-\Delta Q_s$. The printed strict inequality excludes a tie at which the event $A_{st}$ does occur.
• A trivializing formalization is ruled out: the dual-balancing predicate and the independence hypothesis are jointly satisfiable with $T>L$ (checked locally on an explicit instance), and no statement is meaningful only when $T\le L$, the case in which every cost is zero.

Contributions welcome: proofs of the sample-path lemmas, which need only finite sums and the recursion; the conditional-expectation lemmas, which need a Harris-type argument for independent coordinates; and the existence of a measurable balancing order, which this mission does not pose.

Selected references

• R. Levi, G. Janakiraman, M. Nagarajan, A 2-Approximation Algorithm for Stochastic Inventory Control Models with Lost Sales, Mathematics of Operations Research 33(2), 351–374, 2008. https://doi.org/10.1287/moor.1070.0285
• R. Levi, M. Pál, R. O. Roundy, D. B. Shmoys, Approximation Algorithms for Stochastic Inventory Control Models, Mathematics of Operations Research 32(2), 284–302, 2007. https://doi.org/10.1287/moor.1060.0205
• W. T. Huh, G. Janakiraman, J. A. Muckstadt, P. Rusmevichientong, Asymptotic Optimality of Order-Up-To Policies in Lost Sales Inventory Systems, Management Science, 2009. https://doi.org/10.1287/mnsc.1080.0945
• L. Xin, capped base-stock policies in lost-sales inventory models, Operations Research, 2021. https://doi.org/10.1287/opre.2020.2019
• L. Xin, Capped Base-Stock Policies: A 2.33-Approximation, SSRN working paper 7134538, 2026. https://papers.ssrn.com/sol3/papers.cfm?abstract_id=7134538

Motivation

Many estimation problems ask for a matrix of low rank that is consistent with a small number of linear measurements: completing a partially observed ratings matrix, identifying a low-order linear system, or embedding points from a few pairwise distances. Rank minimization under linear constraints is NP-hard, and the standard convex surrogate replaces the rank by the nuclear norm, the sum of the singular values (Recht, Fazel and Parrilo, 2010). Under incoherence assumptions the surrogate recovers the low-rank matrix exactly (Candès and Recht, 2009).

The surrogate is a semidefinite program, and interior point methods for it do not scale past matrices of a few hundred rows. Ma, Goldfarb and Chen (2009) proposed a first-order method for the regularized form of the problem: a gradient step on the data-fit term followed by singular value shrinkage. Their algorithms FPC and FPCA are built on this two-line iteration, and the paper's one convergence theorem says that the iteration, run with a fixed step size, converges to a minimizer. This mission formalizes that theorem and the lemmas used to prove it.

Timeline of the closest results:

• 2005: Combettes and Wajs prove convergence of forward–backward splitting for the sum of a convex function and a convex function with Lipschitz gradient in a Hilbert space.
• 2008: Hale, Yin and Zhang analyse the fixed point continuation (FPC) method for $\ell_1$-regularized least squares, with vector shrinkage in place of matrix shrinkage.
• 2008–2010: Cai, Candès and Shen introduce singular value thresholding (SVT) for matrix completion, prove that the shrinkage is the proximal map of the nuclear norm, and prove convergence of a different iteration (Uzawa's method on a strongly convex problem with equality constraints).
• 2009: Ma, Goldfarb and Chen state and prove convergence of the matrix shrinkage fixed point iteration for the nuclear norm regularized least squares problem (1.8), following Hale, Yin and Zhang's argument.

Setting

Fix natural numbers $m,n,p$. Matrices $X\in\mathbb R^{m\times n}$ carry the Frobenius norm $\|X\|_F=(\sum_{ij}X_{ij}^2)^{1/2}$ and the nuclear norm $\|X\|_*=\sum_i\sigma_i(X)$. A linear map $\mathcal A:\mathbb R^{m\times n}\to\mathbb R^p$ is given by matrices $A_0,\dots,A_{p-1}$ through $\mathcal A(X)_i=\langle A_i,X\rangle$; equivalently $\mathcal AX=A\,\mathrm{vec}(X)$ for a matrix $A\in\mathbb R^{p\times mn}$. Its adjoint is $\mathcal A^*$, and $\lambda_{\max}(A^\top A)=\|\mathcal A\|_2^2$, the square of its spectral norm. Fix $b\in\mathbb R^p$ and $\mu>0$.

Problem (1.8) is

$$\min_{X\in\mathbb R^{m\times n}}\ \mu\|X\|_*+\tfrac12\|\mathcal A(X)-b\|_2^2 ,$$

and $\mathcal X^*$ denotes its set of optimal solutions. Write $g(X)=\mathcal A^*(\mathcal A(X)-b)$ for the gradient of the data-fit term and $h(X)=X-\tau g(X)$ for a gradient step of size $\tau>0$.

For $\nu>0$, the matrix shrinkage operator $S_\nu$ takes a singular value decomposition $Y=U\,\mathrm{Diag}(\sigma)V^\top$ to $S_\nu(Y)=U\,\mathrm{Diag}(\bar\sigma)V^\top$, where $\bar\sigma_i=\max(\sigma_i-\nu,0)$. The fixed point iterations (2.1) start from an arbitrary $X^0$ and repeat

$$Y^k=X^k-\tau g(X^k),\qquad X^{k+1}=S_{\tau\mu}(Y^k).$$

Formalization targets

Goal: Theorem 4

For $\tau\in(0,2/\lambda_{\max}(A^\top A))$ and every starting point, there is $X^*\in\mathcal X^*$ with

$$\lim_{k\to\infty}\|X^k-X^*\|_F=0 .$$

The goal fixes no rate and no particular limit: it asserts convergence of the whole sequence to some minimizer.

Milestones, in attack order

1. Theorem 3. $S_\nu(Y)$ is an optimal solution of $\min_X\nu\|X\|_*+\tfrac12\|X-Y\|_F^2$. This is already posed on the platform as Cai, Candès and Shen's Theorem 2.1 (which adds uniqueness) and is referenced, not restated.
2. Corollary 1. For every $\tau>0$: $X^*\in\mathcal X^*$ if and only if $X^*=S_{\tau\mu}(h(X^*))$.
3. Lemma 1. $\|S_\nu(Y_1)-S_\nu(Y_2)\|_F\le\|Y_1-Y_2\|_F$, with equality if and only if $Y_1-Y_2=S_\nu(Y_1)-S_\nu(Y_2)$.
4. Lemma 2. For $\tau$ in the step range, $\|h(X)-h(X')\|_F\le\|X-X'\|_F$, and $h(X)-h(X')=X-X'$ if and only if equality holds.
5. Lemma 3. If $X^*\in\mathcal X^*$, then $X\in\mathcal X^*$ if and only if $\|S_{\tau\mu}(h(X))-X^*\|_F=\|X-X^*\|_F$.

The mission also contains the paper's Theorem 2, the optimality condition for (1.8) written with a reduced singular value decomposition $X=U\,\mathrm{Diag}(\sigma)V^\top$: $X\in\mathcal X^*$ if and only if some $W$ satisfies $\mu(UV^\top+W)+g(X)=0$, $U^\top W=0$, $WV=0$ and $\|W\|_2\le1$. The chain to Theorem 4 does not use it.

Significance

Theorem 4 is the correctness guarantee for FPC and FPCA, which were among the first algorithms to solve nuclear norm regularized problems with matrices in the thousands of rows. It certifies that the output of the plain iteration is an exact minimizer in the limit, for every starting point and every step below $2/\lambda_{\max}(A^\top A)$. Lemmas 1–3 are the reusable part: non-expansiveness of the matrix shrinkage with a precise equality case, and the fixed point characterization of the optimal set, are the ingredients of every proximal gradient analysis with nuclear norm regularization.

Status: the theorem is proved on paper, and it is also a special case of the general convergence of forward–backward splitting. No machine-checked proof of it is known. The platform holds general forward–backward and inertial forward–backward convergence statements in Hilbert space (for example NesterovFB.Weak.theorem_3, InertialFB.IFB.theorem1_convergence) and the nonexpansiveness of abstract proximal maps (MoreauProx.Characterization.prox_nonexpansive). None is stated for the nuclear norm, for matrix shrinkage defined through the SVD, or with Ma, Goldfarb and Chen's equality cases. Formalizing this mission connects Mathlib's singular values to these operator-theoretic statements.

Difficulty

The obvious route goes through Fejér monotonicity: every step brings the iterate no farther from any minimizer, so the iterates are bounded and have a limit point. Two steps of this route do not come for free. First, the argument presupposes a minimizer; nothing in the hypotheses provides one, so the existence of an optimal solution of (1.8) has to be established from the data. Second, a limit point must be shown to be optimal, which requires the equality cases of Lemmas 1 and 2, not just the inequalities. Lemma 1's equality case concerns the singular value decompositions of two unrelated matrices whose singular vectors need not be aligned; non-expansiveness alone does not deliver it. Nonexpansive maps in general need not have convergent iterates (a rotation is nonexpansive), so continuity plus boundedness is not enough.

Formalization scope

• Matrices are Matrix (Fin m) (Fin n) ℝ. The Frobenius norm, the nuclear norm (the sum of Mathlib's LinearMap.singularValues), the linear map $\mathcal A$ as $p$ matrices Aop, its adjoint and spectral norm, and the shrinkage relation IsShrink are reused from the published Cai–Candès–Shen definitions.
• $S_\nu$ is a relation, IsShrink ν Y X: $X$ is the shrinkage of $Y$ for some reduced SVD (orthonormal columns, positive singular values). Every statement takes the shrinkage output as a variable with an IsShrink hypothesis. The paper's Definition 4 also allows zero singular values, which shrink to zero and change nothing.
• The step range $\tau\in(0,2/\lambda_{\max}(A^\top A))$ is written $0<\tau$ and $\tau\|\mathcal A\|_2^2<2$, without division. For $\mathcal A=0$ this is the range $(0,\infty)$, as on paper, rather than the empty range that Lean's $2/0=0$ would give.
• $\mu>0$ is an explicit hypothesis, and so is $\nu>0$ in Lemma 1; in Corollary 1, $\tau>0$ is the only condition on the step, as on the page ("for any $\tau>0$"). $\nu=\tau\mu$ is built into the statements.
• The run of (2.1) is a predicate on the whole sequence with an arbitrary $X^0$; it is not the continuation scheme FPC and does not fix $X^0=0$.
• Convergence is in the Frobenius norm to some minimizer chosen after the run. Neither $\mathcal X^*\neq\emptyset$ nor boundedness of the iterates is a hypothesis; a statement that assumes either is a different, weaker theorem and is ruled out.
• No statement assumes $m\le n$; the paper's "without loss of generality" belongs to its proofs.

A complete development needs the SVD of real matrices in terms of Mathlib's singular values, the subdifferential of the nuclear norm, and a Fejér-monotone convergence argument in finite dimension. The first two are reusable for any nuclear norm or spectral function result, and contributions of general lemmas about singular value shrinkage (functionality of IsShrink, its proximal characterization) are welcome.

Selected references

• S. Ma, D. Goldfarb, L. Chen, Fixed point and Bregman iterative methods for matrix rank minimization, Math. Program. 128 (2011); preprint arXiv:0905.1643v2, 2009. https://arxiv.org/abs/0905.1643
• J.-F. Cai, E. J. Candès, Z. Shen, A singular value thresholding algorithm for matrix completion, SIAM J. Optim. 20(4), 2010. https://arxiv.org/abs/0810.3286
• E. T. Hale, W. Yin, Y. Zhang, Fixed-point continuation for ℓ1-minimization: methodology and convergence, SIAM J. Optim. 19(3), 2008. https://doi.org/10.1137/070698920
• P. L. Combettes, V. R. Wajs, Signal recovery by proximal forward-backward splitting, Multiscale Model. Simul. 4(4), 2005. https://doi.org/10.1137/050626090
• B. Recht, M. Fazel, P. A. Parrilo, Guaranteed minimum-rank solutions of linear matrix equations via nuclear norm minimization, SIAM Review 52(3), 2010. https://arxiv.org/abs/0706.4138
• E. J. Candès, B. Recht, Exact matrix completion via convex optimization, Found. Comput. Math. 9, 2009. https://arxiv.org/abs/0805.4471

Motivation

Many problems of operations research reduce to a system of nonsmooth equations $F(x)=0$ with $F:\mathbb R^n\to\mathbb R^n$ locally Lipschitz but not differentiable: the nonlinear complementarity problem $h(x)\ge 0$, $f(x)\ge0$, $h(x)^Tf(x)=0$ becomes $F(x)=\min\{h(x),f(x)\}=0$ componentwise, and variational inequalities, KKT systems and max-type equations admit similar reformulations. Newton's method is the natural local solver, but it needs a substitute for the Jacobian at points where $F$ is not differentiable.

Timeline:

• 1977. Mifflin introduces semismooth functionals.
• 1987–1990. Robinson proposes B-derivatives; Pang (1990) and Harker–Xiao (1990) study Newton methods based on directional derivatives (Math. Oper. Res. 15; Math. Programming 48).
• 1993. Qi and Sun (Math. Programming 58) prove local superlinear convergence of $x^{k+1}=x^k-V_k^{-1}F(x^k)$, $V_k\in\partial F(x^k)$, assuming every element of Clarke's generalized Jacobian $\partial F(x^*)$ is nonsingular.
• 1993. Qi (Math. Oper. Res. 18), the source of this mission, observes that this assumption already fails for $f(x)=|x|$, where $\partial f(0)=[-1,1]$ contains $0$, and restricts $V_k$ to the smaller B-subdifferential. Nonsingularity is then needed only on $\partial_B F(x^*)$.

Setting

A map $F:\mathbb R^n\to\mathbb R^m$ is locally Lipschitz throughout; the norm is the Euclidean 2-norm. Let $D_F$ be the set of points where $F$ is differentiable (almost every point, by Rademacher's theorem). The B-subdifferential of $F$ at $x$ is

$$\partial_B F(x)=\Big\{\lim_{i\to\infty}\nabla F(x_i)\;:\;x_i\to x,\ x_i\in D_F\Big\},$$

and Clarke's generalized Jacobian is its convex hull, $\partial F(x)=\operatorname{conv}\partial_B F(x)$. The directional derivative is $F'(x;h)=\lim_{t\downarrow0}(F(x+th)-F(x))/t$. $F$ is semismooth at $x$ if $\lim Vh'$ over $V\in\partial F(x+th')$, $h'\to h$, $t\downarrow 0$, exists for every $h$. A map $F:\mathbb R^n\to\mathbb R^n$ is strongly BD-regular at $x$ if every $V\in\partial_B F(x)$ is nonsingular.

The $\partial_B$ Newton method is

$$x^{k+1}=x^k-V_k^{-1}F(x^k),\qquad V_k\in\partial_B F(x^k), \tag{3.2}$$

with any choice of $V_k$, and the directional-derivative Newton method is $x^{k+1}=x^k+d^k$ with $F(x^k)+F'(x^k;d^k)=0$ (3.11)–(3.12). In Lean, $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), $\partial_B F$ is NonsmoothNewton.Shared.bJac F, $\partial F$ is clarkeJac F, semismoothness is NonsmoothNewton.Local.SemismoothAt, and a run of (3.2) is IsBDNewtonRun F x V.

Formalization targets

Goal: Theorem 3.1 (p. 234)

If $F(x^*)=0$ and $F$ is semismooth and strongly BD-regular at $x^*$, there is $\delta>0$ such that every $V\in\partial_B F(y)$, $\|y-x^*\|<\delta$, is nonsingular with $\|y-V^{-1}F(y)-x^*\|<\delta$, and every run of (3.2) from $\|x^0-x^*\|<\delta$ satisfies

$$x^k\to x^*,\qquad \|x^{k+1}-x^*\|=o(\|x^k-x^*\|),$$

and, when $F(x^k)\ne0$ for all $k$,

$$\lim_{k\to\infty}\frac{\|F(x^{k+1})\|}{\|F(x^k)\|}=0. \tag{1.9}$$

Milestones

1. Lemma 2.6 (p. 233): near a strongly BD-regular point, every $V\in\partial_B F(y)$ is nonsingular with $\|V^{-1}\|\le c$, and $\|h\|\le c\|F'(y;h)\|$ where $F$ is semismooth.
2. Lemma 2.2 (1) ⇔ (3) (p. 230): semismoothness at $x$ is equivalent to $Vh-F'(x;h)=o(\|h\|)$ for $V\in\partial F(x+h)$. This is the published item NonsmoothNewton.Local.theorem_2_3.
3. (2.2) (p. 229) at a semismooth point: $F(x+h)=F(x)+F'(x;h)+o(\|h\|)$. This is the published item NonsmoothNewton.Local.remark_2_17.
4. Corollary 3.2 (p. 235): for every $\varepsilon>0$, one $\partial_B$ Newton step near $x^*$ contracts $\|x-x^*\|$ and $\|F(x)\|$ by the factor $\varepsilon$.

Further statements of the paper in this mission

Lemma 2.3 (degree-2 semicontinuity, p. 230); the quadratic second paragraph of Theorem 3.1; Corollary 3.3 (the directional-derivative method, p. 235); Lemma 2.2 (1) ⇔ (2); and the counterexample of Final Remark (6) (pp. 243–244), which shows that (3.12) need not be solvable near a semismooth, strongly BD-regular zero.

Significance

Theorem 3.1 is the local convergence theorem for the semismooth Newton method in the form most used later: the B-subdifferential version under strong BD-regularity is what generalized Newton methods for complementarity problems (through the min and Fischer–Burmeister reformulations) rely on, because $\partial_B F$ is finite in typical piecewise-smooth examples while $\partial F$ is a polytope that may contain singular matrices. The statement (1.9) makes the method a descent method for $\|F\|$ near the solution, which is how the paper later globalizes it (damped Newton, §4; hybrid method, §6). Corollary 3.2 is reused verbatim in the analysis of the damped method.

The results are proved in the paper; none of them is formalized. The mission produces a machine-checked version of the local theory, on top of the published B-subdifferential and semismoothness definitions of the Qi–Sun series, and makes the Clarke-to-B-subdifferential refinement available to later missions.

Difficulty

The Clarke-Jacobian argument cannot be copied. There, nonsingularity of the compact convex set $\partial F(x^*)$ propagates to a neighbourhood by upper semicontinuity of $\partial F$. Here only the extreme set $\partial_B F(x^*)$ is assumed nonsingular, and its convex hull may contain singular matrices. Lemma 2.6 therefore has to work with limits of genuine Jacobians, and the error estimate (3.3) has to combine an estimate stated for $\partial F(x^k)$, namely Lemma 2.2, with the bound on $V_k^{-1}$, which exists only for $V_k\in\partial_B F(x^k)$. A second subtlety is (1.9), which needs a lower bound $\|x^k-x^*\|\le\frac{c}{1-\varepsilon}\|F(x^k)\|$ that does not follow from superlinear convergence alone.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), with the 2-norm and the spectral operator norm, as the paper fixes ("we use 2-norms"). The dimension $n=0$ is allowed.

• Standing assumption. Every statement carries LocallyLipschitz F (§1, p. 227).

• Nonsingularity is the existence of a two-sided inverse $W$ (IsInverse V W), never a junk inverse. A run of (3.2) is written $V_k(x^{k+1}-x^k)=-F(x^k)$ without an inverse, so nonsingularity of $V_k$ is a conclusion.

• Quantifier order. $\delta$ is chosen before the run and serves every starting point within $\delta$ and every choice $V_k\in\partial_B F(x^k)$. Writing "for every run there is a $\delta$" would trivialize the theorem and is ruled out.

• (1.9) is stated under the paper's hypothesis $F(x^k)\ne0$ for all $k$, since otherwise the quotient is not defined.

• Disclosed deviations.

  • Corollary 3.2 is stated for $\varepsilon>0$ (the page prints $\varepsilon\ge0$, false at $0$).
  • Corollary 3.3 adds semismoothness of $F$ on a neighbourhood of $x^*$, which its printed proof uses through Lemma 2.6's (2.16).
  • $O(\cdot)$ and "quadratic" are pinned to explicit constants.

• Infrastructure needed.

  • Rademacher-type facts for $\partial_B F$: nonemptiness, compactness and closed graph. The platform already has WillR's proved lemmas NonsmoothNewton.Shared.exists_local_bJac_control, bJac_mem_of_tendsto, isCompact_bJac.
  • Perturbation bounds for inverses.
  • The relation between directional derivatives and $\partial_B F$ at semismooth points.

  These are reusable for the other two missions of this series and for later semismooth Newton developments. Proofs of the milestones, and alternative arguments, are welcome.

Selected references

• L. Qi, Convergence analysis of some algorithms for solving nonsmooth equations, Math. Oper. Res. 18(1):227–244, 1993. https://doi.org/10.1287/moor.18.1.227
• L. Qi and J. Sun, A nonsmooth version of Newton's method, Math. Programming 58:353–367, 1993. https://doi.org/10.1007/BF01581275
• J.-S. Pang, Newton's method for B-differentiable equations, Math. Oper. Res. 15(2):311–341, 1990. https://doi.org/10.1287/moor.15.2.311
• R. Mifflin, Semismooth and semiconvex functions in constrained optimization, SIAM J. Control Optim. 15(6):959–972, 1977. https://doi.org/10.1137/0315061
• A. Shapiro, On concepts of directional differentiability, J. Optim. Theory Appl. 66:477–487, 1990. https://doi.org/10.1007/BF00940933