Operations Research

Motivation

The multi-armed bandit problem with discounted rewards asks how to allocate effort among $n$ independent projects, only one of which can be worked on at a time, when the project worked on evolves randomly and the others stay frozen. It models job scheduling, research planning, search, and sequential clinical experimentation. Gittins and Jones showed in 1974 that the problem has an index solution: each state of each project has a number, computed from that project alone, and it is optimal always to work on the project whose current state has the largest number. The result turns an $n$-dimensional dynamic program into $n$ one-dimensional computations.

Several proofs followed, each with its own model and its own definition of the index:

• Gittins and Jones (1974) and Gittins (1979): the original interchange proofs, with the index as a supremum over stopping times of a reward-to-time ratio.
• Whittle (1980): a proof through the retirement option and the dynamic-programming equation of the multi-armed problem.
• Varaiya, Walrand and Buyukkoc (1985): the largest-remaining-index algorithm for finite-state Markov bandits, which computes the indices by removing states one at a time.
• Weber (1992): the "prevailing charge" proof.
• Tsitsiklis (1994): the short proof formalized here, for semi-Markov bandits with finite state spaces, by induction on the total number of states, with the indices produced by an index algorithm of the largest-remaining-index type.

Setting

There are $n\ge1$ bandit processes. Bandit $i$ has a finite nonempty state space $\mathcal X_i$, and $\mathcal X=\mathcal X_1\cup\cdots\cup\mathcal X_n$ is their disjoint union. When bandit $i$ at state $x\in\mathcal X_i$ is played, a random reward $R(x)$ is received, the bandit is busy for a random time $T(x)\ge0$, and it then moves to a random state $Y(x)\in\mathcal X_i$; the other bandits do not move. The joint law of $(T(x),R(x),Y(x))$ depends only on $x$, and different plays are independent.

A policy is a map $\pi:\mathcal X_1\times\cdots\times\mathcal X_n\to\{1,\dots,n\}$: at time zero and at every play completion time it chooses the bandit to play from the current states. With $t_i$ the start time and $R_i$ the reward of the $i$-th play and a discount rate $\beta>0$, the expected discounted reward from the initial joint state $z$ is

$$J_\pi(z)=\mathbb E\Big[\sum_{i=1}^{\infty}R_i e^{-\beta t_i}\Big].$$

A policy is optimal if it maximizes $J_\pi(z)$ for every initial state $z$. A priority rule is a policy for which some ordering of $\mathcal X$ makes it always play the bandit whose current state is ordered highest.

The reward rate of a state is

$$r(x)=\frac{\mathbb E[R(x)]}{\mathbb E\big[\int_0^{T(x)}e^{-\beta t}\,dt\big]}. \tag{2.1}$$

Reducing bandit $i^*$ by removing a state $s^*$ merges every play that ends in $s^*$ with the following run of plays at $s^*$ into one composite play, whose reward rate is $\hat r(x)$ of (2.3). The index algorithm repeatedly picks a state $s^*$ of maximal current rate, sets its index $\gamma(s^*)$ to that rate, and reduces its bandit by removing $s^*$ (or removes the bandit if $s^*$ was its last state).

Formalization targets

Goal: Theorem 2.2

Let $\gamma$ be the indices of a run of the index algorithm. Then every priority rule whose ordering satisfies

$$\gamma(y)<\gamma(x)\ \Longrightarrow\ y \text{ is ordered below } x$$

is optimal. Ties in $\gamma$ may be ordered either way, and the run may break ties in its own choices arbitrarily.

Milestones, in the order the proof uses them

1. (2.2), the interchange inequality $\mathbb E\big[(1-e^{-\beta\tau})\int_0^{T(s^*)}r(s^*)e^{-\beta t}dt\big]\ge\mathbb E\big[(1-e^{-\beta T(s^*)})\int_0^{\tau}\bar r(t)e^{-\beta t}dt\big]$ when $\bar r\le r(s^*)$.
2. Lemma 2.1: if $r(s^*)=\max_{x}r(x)$, some optimal policy always plays bandit $i^*$ when it is at $s^*$.
3. Reduction step: optimizing within the policies giving $s^*$ top priority is a bandit problem with one state fewer, the reduced bandit with rates (2.3).
4. Theorem 2.1: some priority rule is optimal.
5. Pick-order optimality: a priority rule that orders the states as a run of the index algorithm picks them is optimal.
6. Index monotonicity: along a run, $\gamma(s^*)\ge\gamma(q^*)$ for consecutive picks $s^*,q^*$.
7. Picked-before characterization: $x$ can be picked before $y$ (in a run with the same indices) if and only if $\gamma(x)\ge\gamma(y)$.

Significance

The theorem shows that the optimal priority order is determined by numbers that, by the reduction formulas, depend only on the statistics of each bandit separately. It is the basis of index policies in scheduling (the $c\mu$ rule and its semi-Markov generalizations), of Klimov's problem and of branching bandits, which the paper's Section 3 obtains by modifying the same argument.

The result has been proved many times, but not in this generality on Prove2Me. The platform has a discrete-time Gittins index theorem for arms sharing one transition kernel and one reward function, with the index defined as a stopping-time supremum. This mission adds semi-Markov dynamics with random play durations and continuous discounting, heterogeneous finite bandits, priority rules, and the index algorithm as the definition of the index. A complete development would also give a machine-checked proof of correctness of a state-elimination algorithm for computing Gittins indices.

Difficulty

Lemma 2.1 compares an optimal stationary policy with a modified policy that is not stationary, and closes the gap by the optimality of stationary policies, which itself requires the dynamic-programming theory of discounted semi-Markov decision problems with finite state spaces. The reduction step requires an exact identification of the values of all top-priority policies with values in a different problem whose plays are composite and may never end. Theorem 2.1 is an induction over a family of problems with shrinking state spaces that are no longer raw semi-Markov bandits. Theorem 2.2 adds ties: a priority order compatible with the indices need not be the order of the given run, and one needs another run with the same indices.

Formalization scope

• Bandits are indexed by Fin n ($0,\dots,n-1$), with $n\ge1$ and each state type finite and nonempty. $\mathcal X$ is the sigma type Σ i, X i, disjoint by construction.
• The law of $(T(x),R(x),Y(x))$ is a probability measure on $\mathbb R\times\mathbb R\times\mathcal X_i$ with $T\ge0$ almost surely and $R$ integrable. The model also assumes $\mathbb P(T(x)>0)>0$, which the page leaves implicit: it makes the denominator of (2.1) nonzero.
• $J_\pi$ is computed from the moments $\mathbb E[R(x)]$ and $D(x,y)=\mathbb E[e^{-\beta T(x)};Y(x)=y]$: it is the limit of the expected discounted reward of the first $k$ plays, given by the first-step recursion. No path space is constructed. The row sums of $D$ are below $1$, so the limit exists; it never mentions rates, indices or reductions.
• Policies are the paper's stationary deterministic maps of the current joint state, and optimality is within that class, for every initial state. An ordering of $\mathcal X$ is an injective ranking into $\mathbb N$.
• The reduced bandit is given by explicit formulas for its expected discounted reward, discounted duration and discounted transition data. These make the page's "transition probabilities are suitably modified" concrete, and the reduced rate is (2.3). Removing a bandit is the reduction of its last state.
• The index is that of any run of the index algorithm, with arbitrary tie choices.

A formalization in which the value of a policy is defined through rates or indices, or in which $\gamma$ is any function compatible with some order rather than the output of the algorithm, would make the goal trivial or empty; both are excluded by the definitions above.

Needed infrastructure: the convergence of the $k$-play values and the first-step (Bellman) equation for $J_\pi$; existence of an optimal stationary policy for finite discounted semi-Markov problems; the value identity for composite plays. The last two are reusable for any finite semi-Markov decision problem. Proofs of individual milestones, alternative arguments (Weber's prevailing charge, the retirement formulation), and the separability statement of p. 198 ("the index algorithm can be carried out separately for each different bandit") are welcome.

Selected references

• J. N. Tsitsiklis, A Short Proof of the Gittins Index Theorem, Annals of Applied Probability 4(1) (1994), 194–199.
• J. C. Gittins and D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (J. Gani et al., eds.), North-Holland, 1974, 241–266.
• J. C. Gittins, Bandit processes and dynamic allocation indices, J. Roy. Statist. Soc. Ser. B 41 (1979), 148–177. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x
• P. Whittle, Multi-armed bandits and the Gittins index, J. Roy. Statist. Soc. Ser. B 42 (1980), 143–149. https://doi.org/10.1111/j.2517-6161.1980.tb01111.x
• P. P. Varaiya, J. C. Walrand and C. Buyukkoc, Extensions of the multiarmed bandit problem: the discounted case, IEEE Trans. Automat. Control 30 (1985), 426–439. https://doi.org/10.1109/TAC.1985.1103989
• R. Weber, On the Gittins index for multiarmed bandits, Annals of Applied Probability 2(4) (1992), 1024–1033. https://doi.org/10.1214/aoap/1177005588

Why wide neighbourhoods

Primal-dual interior-point methods solve a linear program by following, approximately, the central path of strictly feasible primal-dual pairs whose complementarity products $x_js_j$ are all equal. Every such method confines its iterates to a neighbourhood of that path, and the neighbourhood governs both the theory and the practice. The first primal-dual path-following algorithm, by Kojima, Mizuno and Yoshise (1989), used the one-sided neighbourhood $\{x_js_j \ge \tfrac12\,x^Ts/n\}$ and attained precision $t$ in $O(nt)$ iterations. Kojima–Mizuno–Yoshise and Monteiro–Adler then switched to the narrow Euclidean neighbourhood $\mathcal N_2(\beta)$ and improved the bound to $O(\sqrt n\,t)$. Practical codes nevertheless favour wide neighbourhoods, which allow long steps.

Mizuno, Todd and Ye (Cornell ORIE Technical Report 944, 1990, revised 1991; published in Mathematics of Operations Research 18(4), 1993) analyse adaptive-step algorithms, which at every iteration take the longest step that keeps the iterate in the neighbourhood. This mission formalizes their §4: the adaptive-step algorithm in the wide neighbourhoods $\mathcal N_\infty(\beta)$ and $\mathcal N_\infty^-(\beta)$ attains precision $t$ in $O(nt)$ iterations. With $\beta$ close to $1$, $\mathcal N_\infty^-(\beta)$ contains almost all of the strictly feasible set.

Setting

Fix $n\ge1$, $m\ge0$, $A\in\mathbb R^{m\times n}$, $b\in\mathbb R^m$, $c\in\mathbb R^n$, and consider

$$\text{(P)}\ \min\ c^Tx\ \text{ s.t. } Ax=b,\ x\ge0,\qquad \text{(D)}\ \max\ b^Ty\ \text{ s.t. } A^Ty+s=c,\ s\ge0 .$$

The strictly feasible pairs $\mathcal F^0$ are the $(x,s)$ with $x>0$, $s>0$, $Ax=b$, and $A^Ty+s=c$ for some $y$. For such a pair the duality gap is $x^Ts$, and the duality measure is $\mu=x^Ts/n$. Write $X=\operatorname{diag}(x)$, $S=\operatorname{diag}(s)$ and $e=(1,\dots,1)^T$.

Norms: $\|\cdot\|$ is the Euclidean norm, $\|\cdot\|_\infty$ the maximum norm, and $\|z\|^-_\infty:=\|z^-\|_\infty$, $\|z\|^+_\infty:=\|z^+\|_\infty$ with $(z^-)_j=\min\{z_j,0\}$ and $(z^+)_j=\max\{z_j,0\}$. For $\beta\in(0,1)$ the wide neighbourhoods are

$$\mathcal N_\infty(\beta)=\{(x,s)\in\mathcal F^0:\ \|Xs-\mu e\|_\infty\le\beta\mu\},\qquad \mathcal N^-_\infty(\beta)=\{(x,s)\in\mathcal F^0:\ \|Xs-\mu e\|^-_\infty\le\beta\mu\}.$$

The second says only that $x_js_j\ge(1-\beta)\mu$ for every $j$.

The search direction $d=(d_x,d_s)$ with centering parameter $\gamma$ solves, for some $d_y$,

$$Sd_x+Xd_s=\gamma\mu e-Xs,\qquad Ad_x=0,\qquad A^Td_y+d_s=0, \tag{2}$$

and the step is $x(\theta)=x+\theta d_x$, $s(\theta)=s+\theta d_s$. The scaled quantities $p=X^{-1/2}S^{1/2}d_x$, $q=X^{1/2}S^{-1/2}d_s$, $r=(XS)^{-1/2}(\gamma\mu e-Xs)$ satisfy $p+q=r$ and $p^Tq=0$. The componentwise product $Pq=(p_jq_j)_j$ is the second-order term $D_xd_s$.

Algorithm 2 with neighbourhood $\mathcal N$ and $\gamma\in(0,1)$ starts at $(x^0,s^0)\in\mathcal N$ with $(x^0)^Ts^0\le2^t$. While $(x^k)^Ts^k>2^{-t}$, it computes $d$ from (2), takes the largest $\bar\theta$ such that $(x(\theta),s(\theta))\in\mathcal N$ for all $\theta\in[0,\bar\theta]$, and sets $(x^{k+1},s^{k+1})=(x(\bar\theta),s(\bar\theta))$.

Formalization targets

Goal: Theorem 2 with an explicit iteration count

Let $\beta,\gamma\in(0,1)$ with $\gamma\le2(1-\beta)$, and let $\mathcal N$ be $\mathcal N_\infty(\beta)$ or $\mathcal N_\infty^-(\beta)$. Every run of Algorithm 2 reaches $(x^k)^Ts^k\le 2^{-t}$ for some

$$k\ \le\ \Big\lceil\frac{\ln2\cdot n\,t}{2\beta\gamma(1-\gamma)}\Big\rceil .$$

The paper states "$O(nt)$ iterations"; the count above is the one its inequality (15) yields.

Milestones, in the order the proof uses them

• Lemma 1(b): $-\|r\|^2/4\le p_jq_j\le r_j^2/4$ for each $j$.
• Lemma 1(c): $\|Pq\|^-_\infty\le\|r\|^2/4\le n\|r\|^2_\infty/4$, $\|Pq\|^+_\infty\le\|r\|^2_\infty/4$, $\|Pq\|_\infty\le\|r\|^2/4$.
• Lemma 2(c): if $\gamma\le2(1-\beta)$ and $(x,s)\in\mathcal N_\infty^-(\beta)$ then $\|r\|^2\le n\mu$; in $\mathcal N_\infty(\beta)$, $\|r\|_\infty^2\le(1+\beta)\mu$.
• Lemma 5: $\bar\theta\ge\theta_2=\min\{1,\beta\gamma\mu/\|Pq\|_\infty\}$ in $\mathcal N_\infty(\beta)$, and $\bar\theta\ge\theta_2^-=\min\{1,\beta\gamma\mu/\|Pq\|^-_\infty\}$ in $\mathcal N_\infty^-(\beta)$.
• Proof of Theorem 2: $\theta_2^-\ge\theta_2\ge4\beta\gamma/n$ (for $n\ge2$).
• (15): $\mu^{k+1}\le\big(1-4\beta\gamma(1-\gamma)/n\big)\mu^k$.

Significance

Theorem 2 shows that the adaptive long-step method in a neighbourhood covering almost all of $\mathcal F^0$ keeps the worst-case complexity of the original Kojima–Mizuno–Yoshise algorithm. Its per-iteration analysis (Lemma 5, Lemma 1(c)) is also what the paper reuses for its potential-reduction variant (§5, Theorem 3) and for its probabilistic explanation of why such methods take far fewer iterations in practice (§6). Lemma 1(b)–(c) are the standard bounds on the second-order Newton term, and they recur throughout the interior-point literature.

The results are proved in the paper. As far as the platform's corpus shows, none of them has a machine-checked proof: there is no formalization of the wide neighbourhoods $\mathcal N_\infty$, $\mathcal N_\infty^-$, of the Newton system (2), or of an adaptive-step iteration. A complete development yields a reusable layer for primal-dual interior-point analysis in standard form (the neighbourhoods, the scaled direction, the second-order bounds) and the first formally verified iteration bound for a long-step primal-dual method.

Difficulty

Most of the steps are finite-dimensional inequalities. The sticking points are the following.

• The bound $p_jq_j\ge-\|r\|^2/4$ uses the orthogonality $p^Tq=0$, which comes from $Ad_x=0$ and $d_s=-A^Td_y$. Those relations hold only for a solution of the full system (2), not for the first equation alone.
• Lemma 5 needs every point of the segment $[0,\theta_2]$ to lie in the neighbourhood, including strict positivity of $x(\theta)$ and $s(\theta)$ and dual feasibility. Positivity of the products alone does not give positivity of the factors without a continuity argument along the segment.
• "The largest $\bar\theta$" is a maximum over a set defined by infinitely many conditions. The theorem needs only that $\bar\theta$ dominates $\theta_2$, but the formal run must say what $\bar\theta$ is.
• Converting the per-iteration contraction (15) into the explicit count needs $(1-\delta)^k\le e^{-k\delta}$, real powers of $2$, and a ceiling.

Formalization scope

Vectors are Fin n → ℝ, with coordinates indexed $0,\dots,n-1$, and A : Matrix (Fin m) (Fin n) ℝ. Mathlib's default norm on Fin n → ℝ is the sup norm, so the Euclidean norm norm2 and the norms normInf, normInfNeg, normInfPos are defined explicitly. $\mu$ divides by $n$ as a real number. Here $\log$ is the natural logarithm and $2^t$ is a real power with $t\in\mathbb R$.

Committed conventions and repairs:

• The direction is "any $(d_x,d_y,d_s)$ solving (2)". No rank assumption on $A$ is made.
• "The largest $\bar\theta$" is IsGreatest of the set of admissible step lengths, and $\bar\theta$ is not capped at $1$. When no maximum exists (always the case for $n=1$, where $Pq=0$), no iteration exists. A run is then possible only if it has already stopped, and the theorem holds trivially. A sorry-free check confirms that an iteration exists for $n=2$.
• A run is a pair of sequences that starts as required and makes one iteration from every iterate with $(x^k)^Ts^k>2^{-t}$. Its behaviour after the stopping test is unconstrained.
• In $\theta_2$ and $\theta_2^-$, a zero norm makes the quotient $+\infty$ and the minimum $1$. Since Lean's real division by zero is $0$, this case is defined explicitly.
• The bound $\theta_2\ge4\beta\gamma/n$ is stated for $n\ge2$. At $n=1$ it can fail (e.g. $\beta=1/2$, $\gamma=0.9$), and Algorithm 2 makes no iterations there.
• The goal covers both neighbourhoods. A goal for $\mathcal N^-_\infty$ alone would be weaker than the paper.
• Lemma 1 assumes only $x,s>0$ and $\gamma\in[0,1]$ of the pair, which is all its statement uses.

The goal is not to be read with a hidden constant. A statement of the form "there is $C$ with at most $Cnt$ iterations", with $C$ allowed to depend on the instance, would be trivially true and is ruled out by the explicit count. Lemma 1(a) and Lemma 2(a), 2(b) belong to the paper's predictor–corrector analysis, which is a separate mission.

Contributions are welcome at every level: proofs of the milestones, helper lemmas about the norms on Fin n → ℝ, and the run-to-count argument.

Selected references

• S. Mizuno, M. J. Todd, Y. Ye, On adaptive-step primal-dual interior-point algorithms for linear programming, Cornell ORIE Technical Report No. 944 (1990, rev. 1991); Mathematics of Operations Research 18(4):964–981, 1993. https://doi.org/10.1287/moor.18.4.964
• M. Kojima, S. Mizuno, A. Yoshise, A primal-dual interior point algorithm for linear programming, in N. Megiddo (ed.), Progress in Mathematical Programming, Springer, 1989, pp. 29–47. https://doi.org/10.1007/978-1-4613-9617-8_2
• R. D. C. Monteiro, I. Adler, Interior path following primal-dual algorithms. Part I: Linear programming, Mathematical Programming 44:27–41, 1989. https://doi.org/10.1007/BF01587075
• S. J. Wright, Primal-Dual Interior-Point Methods, SIAM, 1997. https://doi.org/10.1137/1.9781611971453

Motivation

The proximal point algorithm replaces a hard optimization or equilibrium problem by a sequence of better-conditioned ones: from the current point $x^n$ it solves the original problem with a quadratic penalty $\|x-x^n\|^2$ added, and takes the solution as $x^{n+1}$. The method is a building block of modern convex optimization. Augmented Lagrangian methods, Douglas–Rachford and ADMM splitting, and many bundle methods are proximal point iterations applied to suitable problems (Rockafellar 1976; Eckstein–Bertsekas 1992).

The algorithm was introduced by B. Martinet in a five-page note in the Revue française d'informatique et de recherche opérationnelle in 1970 (Martinet 1970). The note treats three cases: monotone variational inequalities on a bounded convex set (§II), convex–concave min–max problems (§III), and convex minimization (§IV). This mission formalizes §IV.

Timeline.

• 1970, Martinet: the regularization (13) for convex minimization over a closed convex set in a Hilbert space; Théorème 3 (weak cluster points are minimizers, the sequence is minimizing), stated without proof.
• 1976, Rockafellar (SIAM J. Control Optim. 14): the proximal point algorithm for maximal monotone operators, with inexact steps and weak convergence of the whole sequence when a zero exists.
• 1991, Güler (SIAM J. Control Optim. 29): the rate $f(x^n)-\inf f = O(1/n)$ for convex minimization, and an example in which the iterates converge weakly but not strongly.

Setting

Let $H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. Let $C\subseteq H$ be a nonempty, closed, convex set, and let $f:H\to\mathbb R$ be a convex, lower semicontinuous function such that, for every $a\in\mathbb R$, the sublevel set $\{x\in C \mid f(x)\le a\}$ is bounded. These are the standing hypotheses of §4.1 (Lean: Standing f C). The problem is

$$(12)\qquad \min\,\{\,f(x)\mid x\in C\,\},$$

and its solution set (solSet f C) is the set of $\bar x\in C$ with $f(\bar x)\le f(x)$ for all $x\in C$.

The regularization algorithm (13) starts from $x^0\in C$ and, given $x^n$, takes

$$(13)\qquad x^{n+1}\in C\ \text{ the minimizer of } \ f(x)+\|x-x^n\|^2\ \text{ over } x\in C .$$

Lean encodes one step as IsProxStep f C xn y ($y\in C$ and $f(y)+\|y-x^n\|^2\le f(x)+\|x-x^n\|^2$ for all $x\in C$) and a run as IsProxSeq f C x.

A point $\tilde x$ is a weak cluster point of $(x^n)$ (IsWeakClusterPt) if every neighbourhood of $\tilde x$ in the weak topology of $H$ contains $x^n$ for infinitely many $n$. A sequence is minimizing if $f(x^n)\to\inf_{x\in C} f(x)$.

Formalization targets

Existence for (12) and well-posedness of (13)

$$\exists\,\bar x\in C\ \ \forall x\in C:\ f(\bar x)\le f(x), \qquad \forall x^n\in C\ \ \exists!\,y\in C:\ y \text{ minimizes } f(x)+\|x-x^n\|^2 \text{ over } C .$$

These are the paper's claims in §4.1 ("Ces hypothèses assurent l'existence d'une solution pour (12)") and §4.2 ("solution unique").

Goal: Théorème 3

For every sequence generated by (13),

$$\tilde x \text{ a weak cluster point of } (x^n)\ \Longrightarrow\ \tilde x\in \operatorname{sol}(12), \qquad \lim_{n\to\infty} f(x^n)=\inf_{x\in C} f(x)\in\mathbb R .$$

The goal asserts no rate and no constant. It is the statement the paper makes, with both conclusions in one theorem.

Stronger: Remarque 1

If in addition $f$ is uniformly convex, i.e. $f(ax+by)\le af(x)+bf(y)-ab\,\varphi(\|x-y\|)$ for $a,b\ge0$, $a+b=1$, with $\varphi(t)>0$ for $t>0$, then (12) has a unique solution $\bar x$ and $\|x^n-\bar x\|\to0$.

Significance

The result. Théorème 3 says that the proximal iterates make progress on the objective, not only on the distance to the solution set. A user of the method can stop on a value criterion. The convergence also needs no step-size tuning, no smoothness of $f$, and no bound on $f$ beyond the boundedness of the sublevel sets. The well-posedness of (13) is what makes the method an algorithm. Each step is a strongly convex subproblem with a unique solution, and later inexact and splitting variants rely on that.

Formalizing it. The note gives no proof of Théorème 3 ("On peut faire une démonstration directe de ce théorème") and none of Remarque 1. The mission asks for a complete machine-checked proof of the convex minimization case of the original proximal point paper. To our knowledge, none of these statements has a machine-checked proof. Mathlib has convexity, lower semicontinuity, the weak topology of a normed space and uniform convexity of functions, but no proximal point algorithm.

Difficulty

Each iterate $x^{n+1}$ is defined only implicitly, as the minimizer of a problem that changes with $n$. Monotonicity of $f(x^n)$ follows at once from comparing $x^{n+1}$ with $x^n$. Monotonicity alone gives convergence of $f(x^n)$ to some limit, but not to $\inf_C f$. Closing that gap needs information about the minimizers of (12) and their distance to the iterates.

The cluster-point statement is about the weak topology. A norm-continuity argument does not apply: $f$ is only lower semicontinuous in norm, and passing to weak limits requires the weak lower semicontinuity of convex lower semicontinuous functions. The boundedness that makes weak cluster points exist comes from the sublevel-set hypothesis, not from $C$, which may be unbounded.

For Remarque 1, the obvious argument controls $\varphi(\|x^n-\bar x\|)$, and the hypothesis on $\varphi$ is only positivity. Passing from $\varphi(\|x^n-\bar x\|)\to0$ to $\|x^n-\bar x\|\to0$ is not immediate without a monotone modulus.

Formalization scope

All statements live in MartinetReg.ConvexMin. The conventions the formalization commits to:

• $H$ is a real complete inner product space (InnerProductSpace ℝ H, CompleteSpace H). The paper says "espace de Hilbert", and its inequalities make it real.
• $C\neq\emptyset$ is a standing hypothesis. The paper leaves it implicit, but its existence claim for (12) is false for $C=\emptyset$.
• $f$ is real-valued, convex and lower semicontinuous on all of $H$, as printed. The constraint $x\in C$ stays explicit in (12) and (13). It is not absorbed into an extended-valued indicator.
• The penalty in (13) has weight $1$, as printed, not $\tfrac12$.
• The algorithm is a relation on sequences: IsProxSeq accepts any sequence with $x^0\in C$ satisfying (13) at every step. Existence and uniqueness of the step are a separate milestone, not built into a definition by choice.
• "Minimisante" is stated as: some real $m$ is the greatest lower bound of $f(C)$ and $f(x^n)\to m$. This avoids the junk value sInf takes on sets unbounded below. As a side effect, the theorem asserts that $f$ is bounded below on $C$.
• Weak cluster points are cluster points in WeakSpace ℝ H. A norm cluster point would weaken the conclusion and is not used.
• Remarque 1 uses Mathlib's UniformConvexOn Set.univ φ f with $\varphi(t)>0$ for $t>0$. It keeps every hypothesis of §4.1.

The goal does not assume that (12) has a solution, that $f$ is bounded below on $C$, or that the iterates are bounded. Each of these would remove part of the content of Théorème 3, and the first two are consequences proved as milestones.

Not formalized here: Remarque 2 (p. 158), a comment that convexity seems indispensable; and the Exemple (p. 158). The Exemple's linear system $(A^*A+2I)x^{n+1}=A^*b+2x^n$ corresponds to $f=\tfrac12\|Ax-b\|^2$. For the printed $f=\|Ax-b\|^2$, (13) gives $(A^*A+I)x^{n+1}=A^*b+x^n$. The variational inequality case (§II) is the companion mission I of this series.

Reusable beyond this mission: the existence of minimizers of convex lower semicontinuous functions with bounded sublevel sets on closed convex subsets of a Hilbert space, and the weak lower semicontinuity it rests on. Contributions of these general lemmas, and of strong-convexity facts for $x\mapsto f(x)+\|x-x^n\|^2$, are welcome.

Selected references

• B. Martinet, Brève communication. Régularisation d'inéquations variationnelles par approximations successives, Revue française d'informatique et de recherche opérationnelle, série rouge, 4(R-3), 154–158, 1970. https://doi.org/10.1051/m2an/197004R301541
• R. T. Rockafellar, Monotone operators and the proximal point algorithm, SIAM Journal on Control and Optimization 14(5), 877–898, 1976. https://doi.org/10.1137/0314056
• O. Güler, On the convergence of the proximal point algorithm for convex minimization, SIAM Journal on Control and Optimization 29(2), 403–419, 1991. https://doi.org/10.1137/0329022
• J. Eckstein and D. P. Bertsekas, On the Douglas–Rachford splitting method and the proximal point algorithm for maximal monotone operators, Mathematical Programming 55, 293–318, 1992. https://doi.org/10.1007/BF01581204
• J. L. Lions and G. Stampacchia, Variational inequalities, Communications on Pure and Applied Mathematics 20, 493–519, 1967. https://doi.org/10.1002/cpa.3160200302

Motivation

Inspection and revision cost money, but continued production can allow a deteriorating process to remain in a costly state. A controller therefore needs a rule that converts incomplete information about the process into an action. Ross's two-state model makes that decision precise: the process can be good or bad, the bad state persists until revision, and inspection reveals the current state. The observable state for decision making is a probability rather than the underlying process state. This setup is useful when quality is inferred from occasional inspection and actions must be chosen before the state is known. Ross proved structural results for discounted control in this model, including sufficient conditions for a policy with one inspection interval and for a policy with no inspection at all. Ross (1971)

The conditions in Theorem 3.7 use the model's optimal value itself. They are therefore structural tests for the shape of an optimal rule, rather than parameter-only design formulas. The preceding concavity, monotonicity and Lipschitz estimates explain which features of that value function support the tests. The mission records those estimates alongside the main result, so the target is a coherent part of the paper rather than an isolated inequality. Ross (1971), pp. 589–593

Setting

The belief $P\in[0,1]$ is the probability that the production process is in the bad state at the beginning of a period. A good process becomes bad during a period with probability $\pi\in[0,1]$ if it is not revised. A bad process remains bad. Thus producing without inspection changes the next belief to $T(P)=P+\pi-\pi P$. The discount factor is $\beta\in(0,1)$. Producing without inspection has cost $0$ in the good state and cost $C$ in the bad state, so its expected current cost is $CP$. Inspection costs $I$ in either state, and revision costs $R$ in either state. The standing order is $0<C<I<R$. The explicit $C>0$ records that $C$ is a cost and makes the quotient in Theorem 3.7 meaningful.

Write $V_\beta(P)$ for the discounted value starting from belief $P$. Inspection reveals the current state: the next belief is $\pi$ after observing a good process and $1$ after observing a bad one. Revision resets the next belief to $\pi$. The three current-plus-continuation costs are

$$\begin{aligned} q_{\mathrm P}(P)&=CP+\beta V_\beta(T(P)),\\ q_{\mathrm I}(P)&=I+\beta P V_\beta(1)+\beta(1-P)V_\beta(\pi),\\ q_{\mathrm R}(P)&=R+\beta V_\beta(\pi). \end{aligned}$$

The Bellman equation is $V_\beta(P)=\min\{q_{\mathrm P}(P),q_{\mathrm I}(P),q_{\mathrm R}(P)\}$. A stationary rule is $\beta$-optimal here when it chooses an action attaining this minimum at every admissible belief. This is the paper's decision rule criterion associated with equation (3). Ross (1971), p. 590, equation (3)

Formalization targets

The first target is the sufficient condition for an optimal three-region rule. Set $\Delta=V_\beta(1)-V_\beta(\pi)$. If

$$\frac{(1-\beta)(R+\beta V_\beta(\pi))}{C}\le\frac{R-I}{\beta\Delta},$$

there are thresholds $\pi\le P_1\le P_2$ such that an optimal rule produces for $P<P_1$, inspects for $P_1\le P<P_2$, and revises for $P\ge P_2$. The revise interval may be empty: if no admissible belief has revision as an optimal action, $P_2$ may exceed $1$. If revision is optimal somewhere, the conclusion includes $P_2\le1$. This is a repair to the printed bound in Theorem 3.7(a); the proof on p. 593 explicitly lets a missing threshold be infinite. Ross (1971), pp. 592–593, Theorem 3.7(a)

The second target gives an optimal no-inspection rule. If

$$I+\beta\Delta\ge\frac{C}{1-\beta(1-\pi)} \quad\text{or}\quad \frac{R-I}{\beta\Delta}\le\frac{R}{C}\bigl(1-\beta(1-\pi)\bigr),$$

then some $P_1\ge\pi$ gives an optimal rule that produces below $P_1$ and revises from $P_1$ onward. A threshold above $1$ is allowed and means that the rule produces throughout the admissible belief interval. Both alternatives in the source's condition are retained. Ross (1971), p. 592, Theorem 3.7(b)

Significance

The theorem identifies two kinds of simple stationary rule that can be optimal despite the value function depending on an unobserved process state. It says more than the existence of an optimal action at each belief: the selected actions can be arranged in belief intervals, and in the second regime inspection can be omitted entirely. These statements provide a compact description of decisions over the full continuum $P\in[0,1]$. Ross (1971), Theorem 3.7

The result was proved in the 1971 paper. This mission asks for machine-checked Lean proofs of its two repaired clauses, the value equation, and the stated shape estimates. The definitions and finite-horizon bound can also support later formalizations of related belief-state control models. No proof of this mission's draft theorem is claimed merely by compiling its statement.

Difficulty

The action costs have different shapes as functions of belief: inspection and revision give affine and constant expressions, while the production alternative includes the value at an updated belief. The apparent order of their pairwise crossings does not by itself establish that one selected rule attains the minimum at every belief. Equalities at a threshold also matter, since the rule must be optimal at the boundary points. The printed upper bound on the last threshold fails when revision never minimizes the Bellman equation; imposing it without qualification would make the formal target false.

Formalization scope

Lean represents a belief as a real number and restricts all claims to $[0,1]$. It defines $V^0=0$ and obtains $V^{n+1}$ by taking the minimum of the three action costs with continuation $V^n$, exactly as in equation (4). The value $V_\beta$ is the limit of these iterates; convergence and boundedness are part of the equation (3) milestone. This prevents an arbitrary function satisfying a convenient fixed-point hypothesis from replacing the value the paper studies. The rule types are total real-to-action functions, while optimality is checked for every admissible belief, including $P=1$ and both thresholds.

The paper's general Lemma 2.1 is represented by its scalar two-state instance. The finite-horizon Lipschitz bound and its limiting corollary use $P_1,P_2\in[0,1]$. The last quotient in Corollary 3.6 divides by $\pi$, so that second inequality is stated under $\pi>0$; the first inequality, and the main theorem, cover $\pi=0$. If $\pi=1$, then $\Delta=0$. Lean's real division gives a zero quotient in that case; the two implications in Theorem 3.7 remain valid under this convention. The development needs reusable results about convergence of discounted value iteration, concavity and monotonicity on an interval, and elementary estimates for affine belief updates. Contributions establishing those results or proving either sufficient-condition clause are within scope.

Selected references

• Sheldon M. Ross, Quality Control under Markovian Deterioration, Management Science 17(9), Theory Series, 587–596, 1971. DOI: 10.1287/mnsc.17.9.587

Motivation

A production process can deteriorate without an operator seeing its current condition. Producing a unit, inspecting the process, and revising the process have different immediate costs and different effects on what can be known or controlled next period. The operator therefore needs a rule based on a belief about deterioration, rather than on the hidden physical state. Ross's two-state model asks when the simplest rule, producing every period without inspection, is actually optimal over an unlimited discounted horizon Ross 1971.

The question matters whenever an action has a cost now but may reduce future losses. Paying for inspection only supplies information; paying for revision restores a deteriorated process. The answer depends on the bad-state production cost, the deterioration probability, the revision charge, and the weight assigned to future periods. A comparison of immediate costs alone cannot settle whether revision is worthwhile. Ross's Theorem 3.4 gives an exact boundary between a regime where producing forever is optimal from every initial belief and a regime where revision is forced when deterioration is nearly certain Ross 1971, Theorem 3.4.

Setting

There are two underlying states: good and bad. The current state is hidden, and $P\in[0,1]$ is the probability that it is bad at the beginning of a period. Producing without inspection costs zero in the good state and $C$ in the bad state, so its expected immediate cost is $CP$. A good process becomes bad with probability $\pi$ in one period; a bad process remains bad until revision. Thus a period of production without inspection changes the belief to $T(P)=P+\pi-\pi P$. These are the conventions of the paper's Section 3 Ross 1971, p. 590.

The other actions are inspection, at cost $I$, and revision, at cost $R$. Inspection reveals the current state: the next belief is $1$ when the state was bad and $\pi$ when it was good. Revision returns the process to the good state before its next transition, so the next belief is $\pi$. The standing parameter conditions are $0<\beta<1$, $0\le\pi\le1$, and $0<C<I<R$; $\beta$ is the discount factor. The paper explicitly assumes $C<I<R$ and a discount factor in $(0,1)$. Positive $C$ states the intended positive bad-state cost and makes the threshold comparison meaningful Ross 1971, pp. 588, 590.

For a future-cost function $W$, the three Bellman alternatives at belief $P$ are $CP+\beta W(TP)$, $I+\beta P W(1)+\beta(1-P)W(\pi)$, and $R+\beta W(\pi)$. Their minimum defines one step of finite-horizon value iteration, beginning with $V^0=0$. The limit $V_\beta(P)$ is the optimal discounted cost. Write $R^0$ for the rule that always produces without inspection, and define its cost from the actual discounted series $\psi(P)=\sum_{n=0}^{\infty}\beta^n C T^nP$ Ross 1971, equations (3)–(5).

Formalization targets

The first target establishes that value iteration converges on $[0,1]$, gives a bounded solution to the two-state Bellman equation, and identifies that solution uniquely among bounded functions. The iterated update and Ross's equation (5) then evaluate the cost of $R^0$:

$$T^nP=1-(1-P)(1-\pi)^n,\qquad \psi(P)=\frac{C}{1-\beta}-\frac{C(1-P)}{1-\beta(1-\pi)}.$$

The sensitivity milestones retain the exact finite-horizon factor in Lemma 3.5 and the infinite-horizon bound in Corollary 3.6. In particular, for $P_1,P_2\in[0,1]$,

$$|V_\beta(P_1)-V_\beta(P_2)|\le \frac{C|P_1-P_2|}{1-\beta(1-\pi)}.$$

The mission goal is both clauses of Theorem 3.4. The always-produce rule is optimal from every initial belief exactly at and above the threshold

$$R\ge\frac{C}{1-\beta(1-\pi)}.$$

Below that threshold, revision is the unique minimizing action for beliefs sufficiently near $1$ from the left Ross 1971, pp. 591–592.

Significance

The theorem gives a parameter test for omitting both inspection and revision from an optimal policy in this model. Its second clause adds a local statement when that test fails: near certain deterioration, merely allowing revision as one optimal choice is insufficient; any optimal choice must revise. The sensitivity bounds quantify the effect of imperfect knowledge of the state and supply continuity of the value function used in the paper's treatment of that neighborhood Ross 1971, Theorem 3.4 and Corollary 3.6.

Ross proved these results in 1971. This mission asks for machine-checked proofs of the paper's exact statements in a concrete two-state discounted model. The reusable formal objects are the belief update, the three-action Bellman operator, finite-horizon values, and the always-produce cost series. The goal and milestones here are open formalization targets; their mathematical status as published theorems is distinct from their proof status in Lean.

Difficulty

The cost of always producing can be computed explicitly, but equality with the optimal value is a global assertion about all beliefs and all three available actions. A comparison at one belief does not certify optimality everywhere. The reverse implication also has to recover a parameter inequality from optimality of a policy, rather than from its immediate cost alone. The strict conclusion near $P=1$ requires control of the value as the belief varies; pointwise action comparison at $P=1$ does not itself establish an interval Ross 1971, pp. 591–592.

Formalization scope

The Lean model uses real parameters and a real belief restricted to $[0,1]$. It has three explicit actions and the exact right-hand sides of equation (3). Its value is the limit of iteration from $V^0=0$, so $V^1=\min\{CP,I,R\}$ matches the paper. Convergence, boundedness, and Bellman uniqueness are stated as a milestone. The always-produce cost is the infinite series of actual stage costs, with its closed form reserved for a separate milestone. Consequently, defining the cost by equation (5) cannot make that milestone true by definition.

The discounted-optimality claim for $R^0$ means $\psi(P)=V_\beta(P)$ for every $P\in[0,1]$. The phrase “every optimal policy revises” is represented by revision being strictly cheaper in the Bellman equation than both other actions; this expresses a unique minimizing action for a stationary decision at that belief. “Near $1$” means a one-sided neighborhood within $[0,1]$. The second inequality in Corollary 3.6 is stated only when $\pi>0$, because division by $\pi=0$ has a default value in Lean. The first inequality and Theorem 3.4 retain the $\pi=0$ case.

The development needs real series, limits, finite-horizon recursion, elementary inequalities, and bounded fixed-point reasoning. Proofs of the model-specific Bellman equation, cost identity, exact sensitivity bounds, and Theorem 3.4 are welcome. General tools for discounted Bellman operators or real-series identities would also be useful beyond this mission. No policy class is smuggled in as an arbitrary hypothesis: the value and the cost of $R^0$ are computed from the model data.

Selected references

• Sheldon M. Ross, Quality Control under Markovian Deterioration, Management Science 17(9), Theory Series, 587–596, 1971. DOI: 10.1287/mnsc.17.9.587.

Motivation

Scheduling independent jobs on unrelated parallel machines to minimize the makespan is one of the basic NP-hard problems of scheduling theory: each job has its own processing time on each machine, with no relation between machines, and the goal is to finish all jobs as early as possible. When the number of machines is part of the input, Lenstra, Shmoys and Tardos showed that no polynomial algorithm can come within a factor below 3/2 of the optimum unless P = NP. When the number of machines $m$ is a fixed constant, the picture is different: the problem admits a polynomial approximation scheme, a family of algorithms that reach any accuracy $1+\varepsilon$.

Such a scheme was already known. Horowitz and Sahni (1976) gave a fully polynomial approximation scheme for fixed $m$, but its space requirement grows like $(nm/\varepsilon)^m$. The second application of the Rounding Theorem in the 1987 report of Lenstra, Shmoys and Tardos is a scheme whose space is polynomial in the input size, in $m$, and in $\log(1/\varepsilon)$. This mission formalizes the approximation guarantee of that scheme (Theorem 3 of the report).

Timeline:

• 1976. Horowitz and Sahni, a fully polynomial approximation scheme for a fixed number of unrelated machines, with exponential space in $m$.
• 1985. Potts, a 2-approximation for unrelated machines whose running time is $m^{m-1}$ times a polynomial, based on LP rounding with enumeration.
• 1987. Lenstra, Shmoys and Tardos, the Rounding Theorem, a polynomial 2-approximation for arbitrary $m$, and, for fixed $m$, the scheme formalized here (FOCS 1987; journal version in Mathematical Programming 46, 1990).

Setting

There are $m$ machines and $n$ jobs. If job $j$ is scheduled on machine $i$ it takes $p_{ij}$ time units, a positive integer; $P=(p_{ij})$ is the processing-time matrix. A schedule $\sigma$ assigns every job to one machine. The load of machine $i$ is $\sum_{j:\sigma(j)=i} p_{ij}$, the makespan is the largest load, and $\mathrm{OPT}$ is the smallest makespan over all schedules.

Fix an integer deadline $d\ge0$ and an accuracy $\varepsilon>0$. Assigning job $j$ to machine $i$ is long if $p_{ij}>\varepsilon d$ and short otherwise. A schedule of long assignments $L$ is a partial assignment of jobs to machines using only long assignments; its long load on machine $i$ is $t_i$, and $L$ is admissible if $t_i\le d$ for every $i$.

For a threshold $t$ and deadlines $d_1,\dots,d_m$, the linear program (LP) of the Rounding Theorem has a variable $x_{ij}\ge0$ for every pair with $p_{ij}\le t$, the constraints $\sum_i x_{ij}=1$ for each job, and $\sum_j p_{ij}x_{ij}\le d_i$ for each machine. The residual LP of $(d,L)$ is (LP) for the jobs left unassigned by $L$, with $d_i=d-t_i$ and $t=\varepsilon d$.

The procedure $A_\varepsilon$, on input $d$, tries every admissible $L$; if the residual LP is feasible it takes a vertex $\tilde x$, rounds it to a 0-1 solution of the integer program (IP) of the Rounding Theorem, and combines the result with $L$. It answers 'no' if no residual LP is feasible. A $\rho$-relaxed decision procedure answers 'no' only when no schedule has makespan at most $d$, and otherwise returns a schedule of makespan at most $\rho d$. The binary search of Lemma 1 runs such a procedure on deadlines between $\lceil t/m\rceil$ and $t$, where $t$ is the makespan of the greedy schedule, and returns the best schedule found.

Formalization targets

Goal: Theorem 3

For every $m\ge1$, every positive integer matrix $P$, every $\varepsilon>0$, every LP solver $V$, the procedure $A_\varepsilon$ run with $V$ exists, and the binary search driven by any such procedure returns a schedule $\sigma$ with

$$\mathrm{makespan}(\sigma)\le(1+\varepsilon)\,\mathrm{OPT}.$$

Milestones (§3, p. 6)

1. Every machine in an admissible $L$ carries fewer than $1/\varepsilon$ long assignments, and for $n,m\ge1$

$$\#\{L\text{ admissible}\}<(n+1)^{m/\varepsilon}.$$

2. If some schedule has makespan at most $d$, its long part is admissible and its short part is a feasible solution of the residual LP.
3. If the short assignments take at most $d-t_i+\varepsilon d$ on machine $i$, the combined schedule has load at most $(1+\varepsilon)d$ on every machine.
4. $A_\varepsilon$ exists for every LP solver and is a $(1+\varepsilon)$-relaxed decision procedure.

Significance

Theorem 3 shows that for a fixed number of unrelated machines, the makespan can be approximated to any accuracy in polynomial time while keeping the memory polynomial in $\log(1/\varepsilon)$. It is an early instance of the pattern "enumerate the large items, solve an LP for the small ones, round", which recurs in later approximation schemes for scheduling and packing. Together with the 2-approximation of the same paper (mission 1 of this series) and the 3/2 hardness bound (mission 3), it delimits what is achievable for unrelated machines.

The theorem is proved in the paper; none of it is known to have a machine-checked proof. Formalizing it requires a precise account of the enumeration of long assignments, the residual LP, and the binary search, and it exercises the Rounding Theorem, which this series poses in mission 1, outside its original setting (with a non-integral threshold $t=\varepsilon d$).

Difficulty

The arithmetic of the scheme is short; the content lies in the Rounding Theorem, which turns a vertex of the residual LP into a 0-1 schedule exceeding each deadline by at most the threshold. The obvious argument, rounding an arbitrary feasible LP solution, fails: a non-vertex solution may split many jobs across many machines, and rounding them can overload a machine by far more than $t$. The bound depends on the structure of vertices of (LP), which an arbitrary feasible point does not have. A second difficulty is the count of milestone 1, which must be done with a real exponent $m/\varepsilon$ and a strict inequality.

Formalization scope

• Machines are Fin m, jobs Fin n, processing times a matrix P : Matrix (Fin m) (Fin n) ℕ with all entries positive. Load, makespan and optimal schedules are those of the published MatousekLP.Scheduling.Schedule, applied to the real cast of P.
• A vertex of an LP is a point of Set.extremePoints of its feasible region. Variables absent from the paper's (LP) are kept as matrix entries fixed to $0$, which leaves the vertices unchanged.
• The LP solver is a parameter (a vertex selector) and $A_\varepsilon$ is a predicate on procedures: each answer must extend an admissible schedule of long assignments, round the selected vertex within its support, and satisfy the (IP) load bound. The guarantee is proved for every such procedure. The output is thereby tied to what the algorithm computes, so the bound is not witnessed by an optimal schedule.
• The binary search is a definition: greedy start, $l=\lceil t/m\rceil$ (the paper's $t/m$ rounded up because makespans are integers), $d=\lfloor(u+l)/2\rfloor$, best stored schedule as output.
• Not formalized: that $m$ is fixed, the polynomial running time, and the space bound polynomial in $m$, $\log(1/\varepsilon)$ and the input size. The guarantee is stated for every $m\ge1$. The count $(n+1)^{m/\varepsilon}$ of milestone 1, on which the running-time claim rests, is formalized, with the real power Real.rpow.
• The constants are exact: $1+\varepsilon$, $(n+1)^{m/\varepsilon}$, $d-t_i+\varepsilon d$. Milestone 1 needs $n\ge1$ and $m\ge1$ for strictness.
• Theorem 1 (the Rounding Theorem) and Lemma 1 are milestones of mission 1 of this series and are not restated here.

Welcome contributions: a proof of the Rounding Theorem in the generality of real deadlines and thresholds, proofs of the counting bound, and lemmas on the binary search that are reusable for any relaxed decision procedure.

Selected references

• J.K. Lenstra, D.B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, CWI Report OS-R8714, Centre for Mathematics and Computer Science, Amsterdam, 1987 (the source; Theorem 3, p. 6). Journal version: Mathematical Programming 46 (1990) 259–271. https://doi.org/10.1007/BF01585745
• E. Horowitz, S. Sahni, Exact and approximate algorithms for scheduling nonidentical processors, Journal of the ACM 23 (1976) 317–327. https://doi.org/10.1145/321941.321951
• C.N. Potts, Analysis of a linear programming heuristic for scheduling unrelated parallel machines, Discrete Applied Mathematics 10 (1985) 155–164. https://doi.org/10.1016/0166-218X(85)90009-5
• D.S. Hochbaum, D.B. Shmoys, Using dual approximation algorithms for scheduling problems: theoretical and practical results, Journal of the ACM 34 (1987) 144–162. https://doi.org/10.1145/7531.7535

Motivation

A nonlinear program is rarely solved once. Its data are estimated, rounded, or varied on purpose in a parametric study, and an algorithm such as sequential quadratic programming replaces it at every iteration by a nearby linearised problem. Both uses need the same fact: near a solution, the Karush–Kuhn–Tucker (KKT) system should have exactly one solution for every small perturbation, and that solution should move Lipschitz-continuously with the perturbation. For problems with equality constraints only, or with strict complementary slackness, the classical implicit-function theorem gives this, as in Fiacco's sensitivity analysis (Fiacco 1976, reference [4] of the paper). Without strict complementarity the KKT system is not a smooth equation, and the classical theorem does not apply.

S. M. Robinson's paper Strongly regular generalized equations, Math. Oper. Res. 5 (1980) 43–62 introduced strong regularity to handle exactly this case. §2 of the paper proves an implicit-function theorem for generalized equations, §3 characterises strong regularity of linear generalized equations through a Schur complement, and §4, the subject of this mission, applies both to nonlinear programming. Its Theorem 4.1 identifies the conditions under which the KKT system is strongly regular. These conditions (strong second-order sufficiency and linearly independent binding gradients) became standard hypotheses in the stability theory of nonlinear programs and in the local convergence analysis of Newton-type methods.

Setting

Let $\Omega\subseteq\mathbb R^n$ be open and let $\theta:\Omega\to\mathbb R$, $g:\Omega\to\mathbb R^p$, $h:\Omega\to\mathbb R^q$ be Fréchet differentiable. The program is

$$\text{minimize } \theta(x)\quad\text{subject to}\quad g(x)\le0,\ h(x)=0.\qquad(4.1)$$

The Lagrangian is $\mathcal L(x,u,v)=\theta(x)+\langle u,g(x)\rangle+\langle v,h(x)\rangle$, and $\mathcal L'$ is its gradient in $x$.

For a set $C$ and a point $z$, the normal-cone operator $\partial\psi_C(z)$ is the set of vectors $y$ with $\langle y,c-z\rangle\le0$ for all $c\in C$ when $z\in C$, and the empty set when $z\notin C$. The KKT conditions of (4.1) are the generalized equation

$$0\in F(x,u,v)+\partial\psi_{\mathbb R^n\times\mathbb R^p_+\times\mathbb R^q}(x,u,v),\qquad F(x,u,v)=\big(\mathcal L'(x,u,v),\,-g(x),\,-h(x)\big).\qquad(4.3)$$

Its middle block says $g(x)\le0$, $u\ge0$ and $\langle u,g(x)\rangle=0$.

A generalized equation $0\in F(z)+\partial\psi_C(z)$ is strongly regular at a solution $z_0$ (DEFINITION, p. 45) if its linearisation $T(z)=F(z_0)+F'(z_0)(z-z_0)+\partial\psi_C(z)$ satisfies the following. There are neighbourhoods $U$ of $0$ and $V$ of $z_0$ and a constant $\lambda$ such that, for every $y\in U$, the inclusion $y\in T(z)$ has exactly one solution $z=s(y)$ in $V$, and $s$ is $\lambda$-Lipschitz on $U$.

At a solution $(x_0,u_0,v_0)$ the inequality constraints split into three groups:

• $g^+$, with $g_i(x_0)=0$ and $u_{0,i}>0$;
• $g^0$, the weakly active ones, with $g_i(x_0)=0=u_{0,i}$;
• $g^-$, with $g_i(x_0)<0$.

Write $\mathcal L''=\mathcal L''(x_0,u_0,v_0)$ for the Hessian of the Lagrangian in $x$, $H=h'(x_0)$, $G^+=g^{+\prime}(x_0)$ and $G^0=g^{0\prime}(x_0)$. A square matrix is a P-matrix if all its principal minors are positive.

Formalization targets

Goal: Theorem 4.1 (p. 56)

Assume $\theta,g,h$ are twice differentiable at $x_0$ and $(x_0,u_0,v_0)$ solves (4.3). Assume also:

• (a′) strong second-order sufficiency: $\langle y,\mathcal L''y\rangle>0$ for all $y\ne0$ with $G^+y=0$ and $Hy=0$;
• (b) linear independence: the matrix $\begin{bmatrix}G^+\\G^0\\H\end{bmatrix}$ has full row rank.

Then

$$\text{(4.3) is strongly regular at }(x_0,u_0,v_0).$$

The Lipschitz constant is not fixed; the goal asserts that one exists.

Milestones

1. The matrix $K=\begin{bmatrix}\mathcal L''&H^T&G^{+T}\\-H&0&0\\-G^+&0&0\end{bmatrix}$ of (4.5) is nonsingular.
2. The equations (4.8) define $V,A,B$ uniquely, and the Schur complement $S=[G^0\ 0\ 0]\,K^{-1}\,[G^0\ 0\ 0]^T$ of (4.6) satisfies $S=G^0V=V^T\mathcal L''V$, so $S$ is symmetric.
3. A symmetric matrix is a P-matrix if and only if it is positive definite.
4. $S$ is positive definite.
5. The §4 criterion (p. 55): (4.3) is strongly regular at $(x_0,u_0,v_0)$ if and only if $K$ is nonsingular and $S$ is a P-matrix.

A further item formalizes the example (4.9)–(4.10) on pp. 56–57: a linear generalized equation in $\mathbb R^4$ whose unique solution satisfies the ordinary second-order sufficient condition and (b), yet is not strongly regular.

Significance

Strong regularity is the hypothesis of Robinson's implicit-function theorem (Theorem 2.1 of the paper). Theorem 4.1 therefore yields, for a parametrised nonlinear program, a locally unique and Lipschitz-continuous KKT point together with its multipliers, without strict complementary slackness. The same property underlies the local quadratic convergence of Josephy–Newton and SQP methods, and the criterion of milestone 5 is the form in which it is usually checked. The example of (4.10) shows that the ordinary second-order sufficient condition is not enough; the weakly active constraints have to be dropped from the cone on which $\mathcal L''$ must be positive.

All statements are proved in the paper. None of them, nor the notion of strong regularity, has a machine-checked proof on this platform. The matrix milestones (1–4) are self-contained linear algebra and can be proved independently. Milestone 3 for arbitrary symmetric matrices is a variant of Sylvester's criterion, which Mathlib does not currently state. Milestone 5 rests on §3 and the appendix of the paper (the Schur-complement criterion and the reduction of a linear generalized equation over a polyhedral set), which are the subjects of the companion missions II and III of this series.

Difficulty

The obvious argument would apply the classical implicit-function theorem to the active KKT equations. It fails because of the weakly active constraints. Near $(x_0,u_0,v_0)$ a constraint with $g_i(x_0)=0=u_{0,i}$ can become active or inactive under arbitrarily small perturbations, so the solution map is piecewise smooth, not smooth. Uniqueness has to hold across all the pieces simultaneously, which is a combinatorial condition: the P-matrix property of a Schur complement, not the nonsingularity of a single Jacobian. Example (4.10) shows that the natural guess (nonsingularity of every piece, guaranteed by ordinary second-order sufficiency) is insufficient: three distinct KKT points can coalesce at the origin.

The analytic part is also not routine. Strong regularity concerns the linearised problem with an arbitrary small perturbation on the right-hand side, including perturbations of the complementarity block. The criterion needs the reduction of §3 and the appendix, which localises the polyhedral set $\mathbb R^n\times\mathbb R^p_+\times\mathbb R^q$ around the solution.

Formalization scope

• Spaces. Points of $\mathbb R^n$ are EuclideanSpace ℝ (Fin n). The triple $(x,u,v)$ lives in EuclideanSpace ℝ (Fin n ⊕ (Fin p ⊕ Fin q)), the Euclidean $\mathbb R^{n+p+q}$, so the normal cone uses the standard inner product. A product type, which carries the sup norm and no inner product, is deliberately not used.
• Normal cone. The operator includes the clause $z\in C$, so it is empty off $C$.
• Strong regularity. It is stated on the linearisation data, with a real Lipschitz constant $\lambda$, and requires existence, uniqueness in $V$ and the Lipschitz bound. Strong regularity at a point bundles a Fréchet derivative of $F$ there.
• Twice differentiable at $x_0$. This is encoded as $\theta$, $g_i$, $h_j$ differentiable on the open set $\Omega$ (the standing assumption of (4.1)), together with differentiability at $x_0$ of their gradients. It is not $C^2$ on $\Omega$, and symmetry of $\mathcal L''$ is not assumed; it follows.
• Matrix conventions. Positive definite means $\langle w,Mw\rangle>0$ for $w\ne0$, without symmetry. P-matrix quantifies over all nonempty principal index sets. The Schur complement is used only together with nonsingularity of (4.5), because Mathlib's inverse of a singular matrix is $0$.
• What must not be formalized. Replacing (a′) by the ordinary second-order sufficient condition, or restricting (b) to $G^+$ and $H$, gives a false or a different theorem. The milestones state exactly which constraints enter each condition: (a′) uses $G^+$ and $H$, and (b) uses $G^+$, $G^0$ and $H$. A formalization that drops the weakly active constraints from (b), or assumes strict complementarity, trivializes the goal to the classical implicit-function theorem.
• Infrastructure. A complete development needs the normal cone of a product of orthants, block-matrix inversion and Schur-complement identities, Sylvester-type criteria for symmetric matrices, and the reduction of a linear generalized equation over a polyhedral set to its reduced form. The linear-algebra milestones are reusable beyond this mission. Proofs of any milestone, and of the general P-matrix/positive-definite equivalence, are welcome.

Selected references

• S. M. Robinson, Strongly regular generalized equations, Mathematics of Operations Research 5(1) (1980) 43–62. https://doi.org/10.1287/moor.5.1.43
• A. V. Fiacco and G. P. McCormick, Nonlinear Programming: Sequential Unconstrained Minimization Techniques, Wiley, 1968 (reference [3] of the paper; second-order sufficient condition, Chapter 2).
• A. V. Fiacco, Sensitivity analysis for nonlinear programming using penalty methods, Mathematical Programming 10 (1976) 287–311 (reference [4] of the paper). https://doi.org/10.1007/BF01580379
• R. W. Cottle, Manifestations of the Schur complement, Linear Algebra and its Applications 8 (1974) 189–211 (reference [1] of the paper). https://doi.org/10.1016/0024-3795(74)90055-4
• A. L. Dontchev and R. T. Rockafellar, Implicit Functions and Solution Mappings, 2nd ed., Springer, 2014 (modern account of strong regularity). https://doi.org/10.1007/978-1-4939-1037-3