The OR Formalization Drive

Motivation

Queueing control problems (admission control, routing, service-rate selection, flow control) are naturally posed as Markov decision chains with a denumerably infinite state space, such as the number of customers in a buffer, and are usually judged by their long-run average cost per unit time. When the state space is finite, Chapter 6 of Sennott's book shows that an average cost optimal stationary policy always exists. On a countable state space this fails: Section 7.1 of the book gives examples in which no average cost optimal policy exists, and one in which no stationary policy comes within a given distance of the minimum average cost. The question addressed by this mission is under which verifiable conditions on the discounted value functions a countable-state model has a constant minimum average cost and an optimal stationary policy.

Timeline, following the book's bibliographic notes (p. 163). The book names Taylor (1965) and Derman (1966) as earlier pivotal work and Ross (1968), and his 1983 textbook, as the direct predecessor. Sennott (1989, Operations Research 37) weakened Ross's assumptions to cover models with unbounded costs, and proved the main result of Section 7.2; the (SEN) assumptions of Chapter 7 are the cleaner version of Sennott (1993). Cavazos-Cadena (1991) gave the example, adapted as Example 7.3.1 of the book, showing that under these assumptions the optimality inequality can be strict. The weaker (H*) assumptions of Section 7.7 appear, in a slightly different form, in Sennott (1995). Part (iv) of Theorem 7.2.3 is new in the book.

Setting

A Markov decision chain (MDC) $\Delta$ has a countable state space $S$, for each state $i$ a finite nonempty action set $A_i$, a nonnegative finite cost $C(i,a)$, and transition probabilities $P_{ij}(a)$ with $\sum_j P_{ij}(a) = 1$. A policy $\theta$ chooses the action at time $n$ at random according to a distribution that may depend on the whole history $(X_0, A_0, \dots, X_n)$; a stationary policy $f$ always chooses $f(i) \in A_i$ in state $i$.

For an initial state $i$, the $n$-horizon cost is $v_{\theta,n}(i) = \sum_{t=0}^{n-1} E_\theta[C(X_t,A_t) \mid X_0 = i]$, the average cost is $J_\theta(i) = \limsup_{n} v_{\theta,n}(i)/n$, and the minimum average cost is $J(i) = \inf_\theta J_\theta(i)$ over all policies. A policy is average cost optimal if $J_\theta \equiv J$. For $\alpha \in (0,1)$ the discounted value function is $V_\alpha(i) = \inf_\theta \sum_{t \ge 0} \alpha^t E_\theta[C(X_t,A_t) \mid X_0 = i]$. All these quantities lie in $[0,\infty]$.

Fix a distinguished state $z$ and put $h_\alpha(i) = V_\alpha(i) - V_\alpha(z)$. The (SEN) assumptions are:

• (SEN1) $(1-\alpha)V_\alpha(z)$ is bounded for $\alpha \in (0,1)$;
• (SEN2) there is a nonnegative finite function $M$ with $h_\alpha(i) \le M(i)$ for all $i$ and $\alpha$;
• (SEN3) there is a nonnegative finite constant $L$ with $-L \le h_\alpha(i)$ for all $i$ and $\alpha$.

A limit function $h$ is a pointwise limit of $h_{\beta_n}$ along some sequence $\beta_n \to 1^-$. If $f_\alpha$ is a stationary policy realizing the discount optimality equation $V_\alpha(i) = \min_a \{C(i,a) + \alpha\sum_j P_{ij}(a)V_\alpha(j)\}$, a limit point $f$ is a stationary policy with $f_{\beta_n}(i) = f(i)$ for large $n$, for each $i$, along some $\beta_n \to 1^-$.

Formalization targets

Goal: Theorem 7.2.3

Under (SEN), there is a finite constant $J = \lim_{\alpha\to1^-}(1-\alpha)V_\alpha(i)$ independent of $i$; limit functions exist, satisfy $-L \le h \le M$ and the average cost optimality inequality (ACOI)

$$J + h(i) \ge \min_{a \in A_i}\Big\{C(i,a) + \sum_j P_{ij}(a)h(j)\Big\}, \qquad i \in S;$$

every stationary policy realizing the minimum is average cost optimal with $J_e \equiv J$ and $E_e[h(X_n)]/n \to 0$; every limit point of discount optimal stationary policies is average cost optimal and satisfies the corresponding inequality for an associated limit function; and the average cost of any optimal policy is a limit, not only a limit supremum.

Milestones

• Proposition 7.1.1: finitely many initial transitions with finite cost do not change $J_\theta$.
• Lemma 7.2.1: a bounded-below solution $(J,h)$ of the ACOI inequality for a stationary $e$ gives $J_e \le J$.
• Proposition B.6: a sequence of functions squeezed between $-L$ and $M$ on a countable set has a pointwise convergent subsequence.
• Proposition 7.2.4: (SEN) does not depend on the choice of $z$.
• Proposition 7.7.1: (SEN) $\Rightarrow$ (H*) $\Rightarrow$ (H).
• Proposition 7.7.2: the conclusions of Theorem 7.2.3 hold under (H), with a state-dependent lower bound $L(i)$.

Significance

Theorem 7.2.3 is the existence theorem the rest of Chapter 7 builds on (p. 128): the ACOE results of Section 7.4, the (BOR) and (CAV) sufficient conditions of Section 7.5, and the worked queueing models of Section 7.6 all work under (SEN) and invoke it. It justifies computing an average cost optimal policy for a queueing model as a limit of discount optimal policies, and it shows that the minimum average cost is the Abelian limit of the normalized discounted value.

The results are proved in the book and in Sennott (1989, 1993, 1995), but none of them has a machine-checked proof: Mathlib has no Markov decision processes, and the platform's average cost results concern finite state spaces or Borel models with different assumptions. The formalization produces a general-policy, countable-state MDC development with extended-real values, reusable by the later missions of this series.

Difficulty

On a finite state space the relative value functions are bounded and the Abelian limit $(1-\alpha)V_\alpha$ can be controlled directly. Here $h_\alpha$ is bounded above only by a function $M$ that may be unbounded, so passing to the limit in the discounted optimality equation $\sum_j P_{ij}(a)h_\alpha(j)$ cannot use dominated convergence, and in general only an inequality survives in the limit; Example 7.3.1 shows that the inequality in the ACOI can be strict. Showing that a policy realizing the ACOI is optimal requires control of $E_e[h(X_n)]/n$ for a function $h$ that is unbounded above, and part (iv) requires comparing the limit inferior and limit superior of Cesàro averages for an arbitrary, possibly history-dependent optimal policy.

Formalization scope

The state space is any countable type ([Countable S]); actions form a type with finite nonempty Finset action sets; costs are ℝ≥0; transition probabilities, costs over time and value functions are ℝ≥0∞. Policies are general: randomized and history dependent, with histories encoded as finite state and action sequences and the process law built by an explicit recursive product. Finite horizon costs have terminal cost $0$, as the chapter prescribes.

The relative value $h_\alpha(i) = V_\alpha(i) - V_\alpha(z)$ is computed in EReal, never through a truncated real subtraction: a state with $V_\alpha(i) = \infty$ gives $h_\alpha(i) = +\infty$, so (SEN2) cannot hold through a junk value, and (SEN1) is a bound by a finite constant that itself forces $V_\alpha(z) < \infty$. Sums $\sum_j P_{ij}(a)h(j)$ and expectations $E[h(X_n)]$ of real functions are extended reals, computed as positive part minus negative part; they are never Bochner integrals and never default to $0$ when not summable. The limit $\alpha \to 1^-$ is the filter 𝓝[<] 1. Limit functions and limit points follow Definition 7.2.2 literally, over arbitrary sequences $\alpha_n \to 1^-$ in $(0,1)$, and the (SEN), (H), (H*) sets are predicates carrying their witnesses $M$ and $L$.

A development that bounds only $h_\alpha$ as a free function, rather than the one built from the infimum over all policies, or that quantifies only over stationary policies in $J(i)$, proves a different and weaker theorem and does not count.

Needed infrastructure: the law of the controlled process under a general policy, monotone and Fatou-type limit interchanges for countable sums, the Abelian inequality $\limsup(1-\alpha)\sum\alpha^t c_t \le \limsup \frac1n\sum_{t<n}c_t$ (Proposition 6.1.1 of the book), and the existence and optimality of discount optimal stationary policies (Theorem 4.1.4). The MDC layer and these two results are shared with other missions of the series; contributions to them are welcome.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Chapter 7 (pp. 127–166) and Appendix B. https://doi.org/10.1002/9780470317037
• L. I. Sennott, Average cost optimal stationary policies in infinite state Markov decision processes with unbounded costs, Operations Research 37 (1989) 626–633. https://doi.org/10.1287/opre.37.4.626
• L. I. Sennott, The average cost optimality equation and critical number policies, Probability in the Engineering and Informational Sciences 7 (1993). (Cited in the book's bibliography, p. 321.)
• L. I. Sennott, Another set of conditions for average optimality in Markov control processes, Systems & Control Letters 24 (1995) 147–151. (Cited in the book's bibliography.)
• R. Cavazos-Cadena, A counterexample on the optimality equation in Markov decision chains with the average cost criterion, Systems & Control Letters 16 (1991) 387–392. (Cited in the book's bibliography.)
• S. M. Ross, Non-discounted denumerable Markovian decision models, Annals of Mathematical Statistics 39 (1968) 412–423. (Cited in the book's bibliography.)
• H. M. Taylor, Markovian sequential replacement processes, Annals of Mathematical Statistics 36 (1965) 1677–1694. (Cited in the book's bibliography.)
• E. A. Feinberg and Y. Liang, On the optimality equation for average cost Markov decision processes and its validity for inventory control; formalized on Prove2Me in the mission of the same name (Borel state spaces, a different model).

Motivation

Queueing control problems (admission control, routing, service rate selection) are naturally modelled as Markov decision chains with a countably infinite state space and unbounded costs, for instance a holding cost that grows with the queue length. For such models the long-run average cost criterion is often the relevant one, and the central question is whether an optimal stationary policy exists and can be computed from an average cost optimality equation (ACOE). Chapter 7 of Linn I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, doi:10.1002/9780470317037) develops a verifiable set of conditions, the (SEN) assumptions, under which an average cost optimality inequality (ACOI) holds and yields an optimal stationary policy. The inequality may be strict (Example 7.3.1), and an optimal policy may induce a Markov chain without positive recurrent states.

Sections 7.4 and 7.5 answer two practical questions: when is the ACOI in fact an equation, and how can (SEN) be checked in a concrete model? The answer culminates in the (BOR) assumptions, which require only one well-behaved stationary policy and the finiteness of a set of low-cost states.

According to the book's bibliographic notes (p. 163): the (BOR) assumptions modify a line of development due to Borkar (SIAM J. Control Optim. 22, 1984, and 27, 1989; monograph 1991) and are weaker than his original conditions; the proof that (BOR) implies (SEN) is from Cavazos-Cadena and Sennott (Oper. Res. Letters 11, 1992), and the version of (BOR) used here is from Sennott (Prob. Eng. Inform. Sci. 7, 1993). Proposition 7.5.5 and the (CAV*) assumptions go back to Cavazos-Cadena (Kybernetika 25, 1989); Proposition 7.5.3 and Corollary 7.5.4 to Sennott (Oper. Res. 37, 1989).

Setting

A Markov decision chain consists of a countable state space $S$, finite nonempty action sets $A_i$, nonnegative finite costs $C(i,a)$ and transition probabilities $P_{ij}(a)$. A policy $\theta$ may use the whole history and randomize. For $\alpha\in(0,1)$ the discount value function is $V_\alpha(i)=\inf_\theta V_{\theta,\alpha}(i)$, the infimum of $\sum_t\alpha^tE_\theta[C(X_t,A_t)\mid X_0=i]$; the average cost of $\theta$ is $J_\theta(i)=\limsup_n\frac1nE_\theta[\sum_{t<n}C(X_t,A_t)\mid X_0=i]$ and the minimum average cost is $J(i)=\inf_\theta J_\theta(i)$. All of these lie in $[0,\infty]$.

For a distinguished state $z$ the relative value is $h_\alpha(i)=V_\alpha(i)-V_\alpha(z)$. The (SEN) assumptions are: (SEN1) $(1-\alpha)V_\alpha(z)$ is bounded on $(0,1)$; (SEN2) $h_\alpha\le M$ for a finite function $M\ge0$; (SEN3) $h_\alpha\ge-L$ for a finite constant $L\ge0$. Under (SEN), $J=\lim_{\alpha\to1^-}(1-\alpha)V_\alpha(i)$ is a finite constant, and a limit function $h$ is a pointwise limit of $h_{\beta_n}$ along some $\beta_n\to1^-$. The ACOI and ACOE read

$$J+h(i)\ \ge\ (\text{resp. }=)\ \min_{a\in A_i}\Big\{C(i,a)+\sum_jP_{ij}(a)h(j)\Big\},\qquad i\in S.$$

For a nonempty set $G$ the first passage time is $T=\min\{n\ge1:X_n\in G\}$. The class $\Re(i,G)$ consists of the policies that, from $i$, enter $G$ with probability one in finite expected time $m_{iG}(\theta)$; $\Re^*(i,G)$ adds a finite expected first passage cost $c_{iG}(\theta)=E_\theta[\sum_{t<T}C(X_t,A_t)]$. A (randomized) stationary policy $d$ is $z$ standard if the Markov chain it induces has $m_{iz}<\infty$ and $c_{iz}<\infty$ for every $i$; it then has a single positive recurrent class $R_d\ni z$ and a finite constant average cost $J_d$.

Formalization targets

Goal: Theorem 7.5.6

Assume (BOR): (BOR1) a $z$ standard policy $d$ exists; (BOR2) for some $\varepsilon>0$ the set $D=\{i: C(i,a)\le J_d+\varepsilon\text{ for some }a\}$ is finite; (BOR3) every $i\in D-R_d$ can be reached from $z$ by some $\theta_i\in\Re^*(z,i)$. Then (SEN) holds and every limit function satisfies the ACOE; every average cost optimal stationary policy $e$ has a positive recurrent state in

$$D(e)=\{i: C(i,e)\le J+\varepsilon\},$$

at most $|D(e)|$ positive recurrent classes and no null recurrent class; and a policy realizing the minimum in the ACOE satisfies $e\in\Re^*(i,D(e)\cap R(e))$ for every $i$.

Milestones

• Lemma 7.4.1: $h_\alpha(i)\le c_{iz}(\theta_i)$ for $\theta_i\in\Re^*(i,z)$, hence (SEN2).
• Lemma 7.4.2: $h(i)\le c_{iG}(\theta)-Jm_{iG}(\theta)+E_\theta[h(X_T)]$ for $\theta\in\Re(i,G)$ under an integrability condition.
• Theorem 7.4.3: four sufficient conditions for equality in the ACOI at a state.
• Lemma 7.5.2: $J_d=(1-\alpha)\sum_{i\in R}\pi_i(d)V_{d,\alpha}(i)$ for a $z$ standard $d$.
• Proposition 7.5.3: a $z$ standard policy gives (SEN1–2).
• Corollary 7.5.4: on $S=\{0,1,\dots\}$, increasing $V_\alpha$ plus a $0$ standard policy gives (SEN), with nonnegative increasing limit functions.
• Proposition 7.5.5: an optimal stationary policy has a positive recurrent state of cost at most $J+\varepsilon$, reachable from $i$, when (7.33) holds.
• Corollaries 7.5.9 and 7.5.10: the (CAV) and (CAV*) conditions imply (BOR).

Significance

Theorem 7.5.6 reduces the verification of the ACOE for a queueing model to three checks that do not involve the discount value function: exhibit one stationary policy with finite mean return times and costs to a fixed state (typically a stable "serve at maximal rate" policy), check that low costs occur on a finite set (automatic when the holding cost grows without bound, Corollaries 7.5.9–7.5.10), and check reachability of finitely many states. Its conclusions go beyond existence: optimal stationary policies induce chains with positive recurrent classes located in a known finite set, and ACOE-realizing policies reach them in finite expected time and cost. This is what makes value iteration and approximating-sequence methods in later chapters of the book applicable to these models.

The results are proved in the book. The present mission produces machine-checked statements of the first passage calculus for general (history-dependent, randomized) policies, of (SEN) and limit functions, and of the chain of implications from (CAV*) to the ACOE. No machine-checked version of these statements is known.

Difficulty

The obvious approach to the ACOE is to pass to the limit $\alpha\to1^-$ in the discount optimality equation. Exchanging this limit with $\sum_jP_{ij}(a)h_\alpha(j)$ requires a dominating function, and (SEN2) only gives a pointwise bound $M$ whose expectation may be infinite; Fatou's lemma then yields only the inequality. Obtaining equality requires tracking first passages to sets and showing that the discrepancy $\Phi$ vanishes along them, which in turn needs finiteness of $c_{iG}$ that is not assumed but has to be derived. On the recurrence side, the average cost criterion is a limit superior of Cesàro averages over a countable state space, and mass can escape to infinity; the finiteness of the set $D$ is what prevents an optimal policy from spending its time in transient or null recurrent states, and turning that into positive recurrence requires the renewal-type identities of Appendix C.

Formalization scope

States form a countable type $S$; action sets are nonempty Finsets; costs are in ℝ≥0; transition probabilities are ℝ≥0∞-valued with row sums one on admissible actions. Policies are general: a history is a state sequence and an action sequence, and all probabilities and expectations (hitting probabilities, $m_{iG}$, $c_{iG}$, $P_\theta(X_T=j)$, $Q^{(n)}_{ij}$) are computed from the history probabilities of the process. $V_\alpha$, $J_\theta$, $m_{iG}$ and $c_{iG}$ take values in $[0,\infty]$; $m_{iG}=\infty$ when $G$ is missed with positive probability; the first passage time satisfies $T\ge1$. $h_\alpha$ and $\sum_jP_{ij}(a)h(j)$ are in the extended reals, with the book's convention that a function bounded below has an expectation in $(-\infty,+\infty]$. Limit functions are real valued. Positive recurrence, communicating classes and steady state probabilities $\pi_j=(m_{jj})^{-1}$ are the notions for the chain induced by a (randomized) stationary policy. $J_d$ is the average cost of $d$ from $z$.

A formalization in which the ACOE is asserted for some convenient function instead of every limit function, or in which $|D(e)|$ is a natural-number cardinality that vanishes on infinite sets, would trivialize part of the goal; the statements quantify over all limit functions and use Set.encard.

A complete development needs: history-dependent policies and their path laws on countable spaces; first passage decompositions (strong Markov property at $T$); Abelian limits of $\sum_t\alpha^tP(T=t)$; Fatou and dominated convergence for series; and the renewal reward theorem for positive recurrent classes (Appendix C of the book). The first passage and Markov chain layer is reusable beyond this mission. Proofs of individual milestones, and sharper statements of the Appendix C facts they use, are welcome.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999. doi:10.1002/9780470317037
• V. S. Borkar, "On minimum cost per unit time control of Markov chains", SIAM J. Control Optim. 22 (1984), 965–978.
• V. S. Borkar, "Control of Markov chains with long-run average cost criterion: the dynamic programming equations", SIAM J. Control Optim. 27 (1989), 642–657.
• V. S. Borkar, Topics in Controlled Markov Chains, Pitman Research Notes in Mathematics 240, Longman, 1991.
• R. Cavazos-Cadena, "Weak conditions for the existence of optimal stationary policies in average Markov decision chains with unbounded costs", Kybernetika 25 (1989), 145–156.
• R. Cavazos-Cadena and L. I. Sennott, "Comparing recent assumptions for the existence of average optimal stationary policies", Oper. Res. Letters 11 (1992), 33–37.
• L. I. Sennott, "The average cost optimality equation and critical number policies", Prob. Eng. Inform. Sci. 7 (1993).
• L. I. Sennott, "Average cost optimal stationary policies in infinite state Markov decision processes with unbounded costs", Operations Research 37 (1989), 626–633. doi:10.1287/opre.37.4.626
• K. L. Chung, Markov Chains with Stationary Transition Probabilities, 2nd ed., Springer, 1967.

Motivation

The subgradient method minimizes a convex function $f$ on $\mathbb{R}^n$ that need not be differentiable, by stepping against an arbitrary subgradient. With stepsizes $h_k \to 0$, $\sum h_k = \infty$ it converges (Shor, Theorem 2.2), but in general only slowly: no stepsize rule that ignores the structure of $f$ gives a geometric rate. Section 2.3 of N. Z. Shor's Minimization Methods for Non-Differentiable Functions (Springer 1985) identifies geometric conditions on $f$ under which a simple geometric stepsize rule does give linear convergence — convergence with the speed of a geometric progression — and computes the rate explicitly.

The results are the origin of what is now studied as sharpness or error-bound conditions for nonsmooth optimization. Their practical content is that nonsmooth problems whose level sets are not too elongated near the minimum (piecewise-linear functions, maxima of finitely many well-conditioned pieces, positive definite quadratics) can be solved by the subgradient method at a linear rate, with a stepsize rule that needs only one or two scalar parameters.

Timeline. Shor proposed the subgradient method in 1962. The book presents the geometric stepsize rule under an angle condition (Theorem 2.7) and its level-surface form (Theorem 2.8), and attributes the block-halving rule of Theorem 2.9 to its reference [94]. Goffin (Math. Programming 13, 1977) gave the sharp rate in terms of a condition number of the level sets. The book compares the quadratic case with L. V. Kantorovich's rate for steepest descent.

Setting

Let $E_n$ be the $n$-dimensional Euclidean space with inner product $(x, y)$ and $f : E_n \to \mathbb{R}$ convex. A vector $g$ is a subgradient of $f$ at $x$ if $f(y) - f(x) \ge (g, y - x)$ for all $y$; $g_f(x)$ denotes an arbitrary subgradient at $x$, chosen once for each $x$. Let $M^*$ be the set of minimum points of $f$, assumed nonempty; for $x \in E_n$, $x^*(x)$ is the point of $M^*$ nearest to $x$.

Given a starting point $x_0$ and positive stepsizes $h_1, h_2, \dots$, the normalized subgradient method is

$$x_{k+1} = x_k - h_{k+1}\frac{g_f(x_k)}{\|g_f(x_k)\|}, \qquad k = 0, 1, 2, \dots,$$

stopped when $g_f(x_k) = 0$ (then $x_k \in M^*$).

Two shape conditions are used. The angle condition (2.12) with angle $0 \le \varphi < \pi/2$ asks that every subgradient make an angle at most $\varphi$ with the direction to the nearest minimum point:

$$(g_f(x), x - x^*(x)) \ge \cos\varphi\,\|g_f(x)\|\,\|x - x^*(x)\|.$$

The level-surface ratio condition (2.20), for a function with unique minimum point $x^*$, asks that on a ball $Y$ around $x^*$ any two points $x, z$ on a common level surface $f(x) = f(z) \ne f(x^*)$ satisfy $\|x - x^*\| \le \sigma\|z - x^*\|$.

Formalization targets

Goal: Theorem 2.8 (p. 32)

If $f$ has a unique minimum point $x^*$, $\sigma \ge \sqrt2$, $h_1 \ge \|x_0 - x^*\|/\sigma$, and (2.20) holds on $Y = \{y : \|y - x^*\| \le \sigma h_1\}$, then with $h_{k+1} = h_k\sqrt{\sigma^2-1}/\sigma$

$$\|x_k - x^*\| \le h_{k+1}\,\sigma, \qquad k = 0, 1, 2, \dots$$

Milestones

1. Theorem 2.7 (pp. 30–31): under (2.12) and the geometric rule $h_{k+1} = h_k r(\varphi)$ with $r(\varphi) = \sin\varphi$ for $\varphi \ge \pi/4$ and $r(\varphi) = 1/(2\cos\varphi)$ for $\varphi < \pi/4$,

$$\|x_k - x^*(x_k)\| \le h_{k+1}/\cos\varphi \quad\text{resp.}\quad 2h_{k+1}\cos\varphi .$$

2. Remark after Theorem 2.7 (p. 32): the same conclusion when (2.12) holds only at the iterates.
3. Inequality (2.22) (p. 33): (2.20) on $Y$ implies $(g, x - x^*) \ge \sigma^{-1}\|g\|\,\|x - x^*\|$ for every $x \in Y$ and every subgradient $g$ at $x$.
4. Example (p. 33): for $A$ symmetric positive definite with extreme eigenvalues $\lambda \le \mu$,

$$\min_{x \ne 0}\frac{(Ax, x)}{\|Ax\|\,\|x\|} = \frac{2\sqrt{\lambda\mu}}{\lambda + \mu},$$

attained at $x = \sqrt{\mu/(\lambda+\mu)}\,s_1 + \sqrt{\lambda/(\lambda+\mu)}\,s_2$. 5. Theorem 2.9 (p. 34): under the assumptions of Theorem 2.8 with $\sigma \ge 2$, the rule $h_{k+1} = h_0 2^{-[(k+1)/N]}$ with $N \ge 3\sigma^2 + 1$ gives $\|x_k - x^*\| \le 2\sigma h_{k+1}$.

Significance

The results. Theorem 2.7 shows that the subgradient method, often dismissed as sublinear, converges linearly once the geometry of $f$ is controlled and the stepsizes decrease geometrically at the right ratio; the rate $r(\varphi)$ depends only on the angle. Theorem 2.8 restates the hypothesis in terms of the shape of level surfaces, a condition that can be checked for concrete functions, and gives rate $\sqrt{\sigma^2-1}/\sigma$. The Example computes the angle for positive definite quadratics, yielding rate $(\varrho - 1)/(\varrho + 1)$ with $\varrho = \mu/\lambda$ the condition number — the same rate as steepest descent with exact line search in Kantorovich's analysis, obtained with less storage. Theorem 2.9 removes the need to know $\sigma$ exactly in the stepsize ratio.

Formalizing them. All five results are proved in the book; none is formalized, and no linear-rate result for a nonsmooth first-order method is on the platform. The formalization pins the constants (2.13)–(2.19), the stepsize indexing, and the treatment of the stopped iteration; the Example is a Kantorovich-type inequality for symmetric operators that is reusable beyond this mission.

Difficulty

The obvious one-step estimate $\|x_{k+1} - x^*\|^2 = \|x_k - x^*\|^2 - 2h_{k+1}(g, x_k - x^*)/\|g\| + h_{k+1}^2$ alone does not contract: the step length is fixed in advance and does not shrink with the distance, so a step may overshoot the minimum. The rate argument has to track the ratio between the current distance and the current stepsize, and the admissible ratio of stepsizes is dictated by the worst case of this quadratic in the distance; in the two regimes $\varphi \ge \pi/4$ and $\varphi < \pi/4$ the worst case sits at different ends. For Theorem 2.8, the shape condition is only assumed on the ball $Y$, so the iterates must be shown to stay in $Y$, and the passage from level surfaces to subgradients needs the distance from $x^*$ to a level surface, which is not a quantity the iteration computes. Theorem 2.9's constant stepsize blocks are not monotone in distance at all, and the count $3\sigma^2 + 1$ must be matched against a worst-case phase.

Formalization scope

The space $E_n$ is EuclideanSpace ℝ (Fin n); $f$ is real-valued and ConvexOn ℝ Set.univ. A subgradient selection is an arbitrary function g with g x a subgradient at every x, quantified universally. Stepsizes are h : ℕ → ℝ with h (k+1) used at step k; the recursions $h_{k+1} = h_k r$ are imposed for $k \ge 1$, $h_1$ being the chosen initial step (the book's "$k = 0, 1, 2, \dots$" in Theorem 2.8 is read this way). The iteration stops at $g_f(x_k) = 0$ by an explicit branch that repeats $x_k$, never through $x/0 = 0$; the bounds are asserted for every $k$, which implies the book's "either the method stops or …" form. $x^*(x)$ is a definition (the nearest point of the set of minima), and the set of minima is assumed nonempty. Unique minimum is stated as $M^* = \{x^*\}$. The ball $Y$ is closed, and (2.20) is assumed only for pairs in $Y$ with a common value different from $f(x^*)$. In (2.16) the ratio is $1/(2\cos\varphi)$, as the proof requires, where the page prints "1/2 cos φ". In Theorem 2.9, "the assumptions of Theorem 2.8" are taken with $h_1 = h_0$, which fixes $h_0 \ge \|x_0 - x^*\|/\sigma$ and $Y$ of radius $\sigma h_0$. In the Example, the extreme eigenvalues are pinned by $\lambda\|x\|^2 \le (Ax,x) \le \mu\|x\|^2$ together with unit eigenvectors, and the minimum is stated with IsLeast.

A statement in which the stepsizes or the bound constants could be chosen after the iterates, or in which the shape condition quantified over an empty set of pairs, would be trivially true; here every constant is fixed by the hypotheses before the sequence is generated, and the conditions are the book's.

Needed infrastructure: the subgradient inequality, continuity of convex functions on $\mathbb{R}^n$, nearest points of closed convex sets, and elementary trigonometry. The nearest-point map and the stepsize ratio are defined within the mission; the subgradient inequality, the set of minima and the iteration come from the series' shared definitions. Contributions welcome: proofs of the milestones, and a reusable Kantorovich-type cosine bound for symmetric positive definite operators.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer 1985, §2.3, pp. 30–36. https://doi.org/10.1007/978-3-642-82118-9
• J.-L. Goffin, On convergence rates of subgradient optimization methods, Mathematical Programming 13 (1977) 329–347. https://doi.org/10.1007/BF01584346
• L. V. Kantorovich, Functional analysis and applied mathematics, Uspekhi Mat. Nauk 3 (1948) 89–185 (steepest descent rate for quadratics, cited by Shor as [45]).

Motivation

The subgradient method for a convex function $f$ moves from $x_k$ against a subgradient $g_f(x_k)$, and everything hinges on the step length. Divergent-series stepsizes guarantee convergence but are slow and need no information about $f$. When the optimal value $f^*$, or any level $c$ that is known to be attainable, is available, B. T. Polyak proposed in 1969 the step

$$x_{k+1} = x_k - \frac{\gamma\,[f(x_k) - c]}{\|g_f(x_k)\|^2}\, g_f(x_k),$$

which uses the current gap $f(x_k) - c$ to scale the move. This Polyak stepsize is still the reference adaptive rule in nonsmooth convex optimization, in the solution of convex feasibility problems, and in the Lagrangian relaxation heuristics of integer programming (Held–Wolfe–Crowder, Camerini–Fratta–Maffioli), where it is known under the name "relaxation step".

Section 2.4 of N. Z. Shor's Minimization Methods for Non-Differentiable Functions (Springer 1985) places Polyak's rule in the framework of Fejér-type approximations developed by I. I. Eremin: an iteration whose map strictly decreases the distance to every point of a target set. It then proves convergence of the rule, linear rates under growth conditions, its behaviour when the level is set too low, and a property of the conjugate-subgradient direction of Camerini, Fratta and Maffioli (1975).

Timeline:

• 1965–1969: Eremin introduces Fejér mappings for systems of convex inequalities.
• 1969: Polyak, Minimization of unsmooth functionals, proposes the step with the known optimal value and proves convergence and a linear rate under a sharp-minimum condition.
• 1975: Camerini, Fratta and Maffioli combine the Polyak step with a conjugate direction for Lagrangian relaxation.
• 1985: Shor's book collects these results in Section 2.4 (Theorems 2.10–2.16).

Setting

$E_n$ is the $n$-dimensional Euclidean space with inner product $(x, y)$ and norm $\|x\|$. A vector $g$ is a subgradient of $f : E_n \to \mathbb{R}$ at $x_0$ if $f(x) - f(x_0) \ge (g, x - x_0)$ for all $x$. A subgradient selection is a map $g_f$ with $g_f(x)$ a subgradient at every $x$; nothing else is assumed about it, in particular not continuity.

For a nonempty set $M \subseteq E_n$, a map $\varphi : E_n \to E_n$ is $M$-Fejér if $\varphi(y) = y$ and $\|\varphi(x) - y\| < \|x - y\|$ for all $y \in M$ and $x \notin M$.

For a convex $f$ with $f^* = \inf f$ and a level $c \ge f^*$, let $M(c) = \{x : f(x) \le c\}$. Polyak's method (2.32) is the iteration $x_{k+1} = \varphi_c(x_k)$ with the map displayed above for $x \notin M(c)$ and $\varphi_c(y) = y$ on $M(c)$; the factor $\gamma$ is fixed in $(0, 2)$.

The conjugate-subgradient procedure (2.38), for a convex $f$ with minimum point $x^*$ and $f^* = f(x^*)$, is

$$x_{k+1} = x_k - h_k s_k, \quad h_k = \frac{[f(x_k) - f^*]\gamma_k}{\|s_k\|^2}, \qquad s_0 = g_f(x_0),\quad s_k = g_f(x_k) + \beta_k s_{k-1}.$$

Formalization targets

Goal: Theorem 2.11

If $0 < \gamma < 2$ and $M(c) \neq \emptyset$, then for any $x_0 \in E_n$

$$\exists k^* : x_{k^*} \in M(c) \qquad \text{or} \qquad \lim_{k \to \infty} x_k \text{ exists and lies in } M(c).$$

The goal fixes no constant and no rate; it asserts only that the method finds a point of the level set, in finite time or in the limit.

Milestones

1. Theorem 2.10. Iterates of a continuous $M$-Fejér map converge to a point of $M$.
2. Inequality (2.33). For $x_k \notin M(c)$ and $y \in M(c)$,

$$\|x_{k+1} - y\|^2 \le \|x_k - y\|^2 - \gamma(2-\gamma)\frac{[f(x_k) - c]^2}{\|g_f(x_k)\|^2} < \|x_k - y\|^2 .$$

3. Theorem 2.12. Under $f(x) - f^* \ge m\|x - x^*\|^2$ and an $L$-Lipschitz gradient near $x^*$, with $c = f^*$: $\|x_k - x^*\| \le q^k \|x_0 - x^*\|$, $q = (1 - \gamma(2-\gamma)m^2/L^2)^{1/2} < 1$.
4. Theorem 2.13. Under the sharp-minimum condition $f(x) - f(x^*) \ge m\|x - x^*\|$ and subgradients bounded by $L$ near $x^*$, with $c = f(x^*)$: $\|x_{k+1} - x^*\| \le q\|x_k - x^*\|$.
5. Theorem 2.14. If $\min \psi = d > 0$ and the method runs with $c = 0$, then $\lim_k \min_{0 \le i \le k} \psi(x_i) \le 2d/(2-\gamma)$.
6. Theorem 2.15. For (2.38) with $0 < \gamma_k \le 1$, $\beta_k \ge 0$: $(x_k - x^*, s_k) \ge (x_k - x^*, g_f(x_k))$.
7. Theorem 2.16. With the Camerini–Fratta–Maffioli coefficient $\beta_k$ and $0 \le \alpha_k \le 2$: $(x_k - x^*, s_k)/\|s_k\| \ge (x_k - x^*, g_f(x_k))/\|g_f(x_k)\|$.

Significance

Theorem 2.11 is the convergence guarantee of the most widely used adaptive step rule for nonsmooth convex problems. With $c = f^*$ it yields a minimizer; with $c > f^*$ it solves the convex inequality $f(x) \le c$, and applied to $\psi = \max_i f_i^+$ it solves consistent systems of convex inequalities. The linear rates of Theorems 2.12–2.13 are the prototype of the "sharpness implies linear convergence" results of modern first-order methods, and Theorem 2.14 quantifies the loss when the level is underestimated, which is the situation of every practical variant that estimates $f^*$ on the fly. Theorems 2.15–2.16 are the justification of the conjugate-subgradient directions used in Lagrangian relaxation.

All results are classical and proved on paper. None of them is formalized on Prove2Me: the platform has a smooth, strongly convex Polyak gradient-descent bound (a different theorem) and Fejér-monotonicity statements for polyhedral relaxation methods, but no Polyak subgradient step, no $M$-Fejér map and no conjugate-subgradient procedure. The mission produces machine-checked versions of the whole section, with the page's misprints corrected where the proof and the statement disagree.

Difficulty

The obvious argument for the goal is to observe that $\varphi_c$ is $M(c)$-Fejér, by (2.33), and invoke Theorem 2.10. That argument fails: Theorem 2.10 needs a continuous map, and $\varphi_c$ depends on an arbitrary subgradient selection, which is discontinuous wherever $f$ is not differentiable. The book says so explicitly. Fejér monotonicity gives boundedness and a limit of each distance $\|x_k - y\|$, but convergence of the whole sequence to a single point of $M(c)$, and the fact that an accumulation point cannot lie outside $M(c)$, have to be obtained without continuity of the map.

For Theorem 2.14 the level $c = 0$ lies strictly below the minimum, so $M(0) = \emptyset$, the target set of the iteration as run is empty, no Fejér property is available for it, and the theorem controls only the best value found, not the iterates.

Formalization scope

• $E_n$ is EuclideanSpace ℝ (Fin n); $f$ is real-valued on all of $E_n$ and ConvexOn ℝ Set.univ f.
• The subgradient selection is universally quantified; no theorem assumes continuity of it.
• Iterations are sequences x : ℕ → E_n with the recursion as a hypothesis; the first term is arbitrary.
• Polyak's step map is defined piecewise: it returns $x$ on $M(c)$ (as the book sets $\varphi_c(y) = y$) and at $g_f(x) = 0$. No statement relies on Lean's convention $x/0 = 0$. The same holds for $h_k$ when $s_k = 0$.
• $M(c) \neq \emptyset$ is a hypothesis of the goal: the book's proof picks $y \in M(c)$, and for $c = f^*$ not attained the conclusion is false (for $f = e^x$, $c = 0$, the method moves by $\gamma$ each step and diverges).
• "$\lim x_k \in M(c)$" is the existence of a limit in $M(c)$, not a statement about cluster points.
• $\gamma \in (0, 2)$ is stated in every theorem on Polyak's method; the book fixes this range at Theorem 2.11.
• Theorem 2.12's "strongly convex" is used through its displayed growth condition only; the statement is made for convex $f$ satisfying it, with $L > 0$ and $q$ computed with Real.sqrt.
• Theorem 2.13 assumes the bound $\|g\| \le L$ on subgradients in the ball, which is what the proof uses; a Lipschitz constant on the closed ball alone does not give it, and the printed statement fails without it.
• Theorem 2.14 is stated with "$\le 2d/(2-\gamma)$"; the printed "$=$" is false in general.
• Theorem 2.16's inequality is stated at indices where $s_k \neq 0$ and $g_f(x_k) \neq 0$.

A formalization in which $M(c)$ may be empty, the selection is assumed continuous, or the step divides by zero through Lean's conventions would be a different theorem; these are ruled out above.

Needed infrastructure: Fejér monotone sequences in finite dimensions (bounded, with convergent distances), the subgradient inequality, and the fact that a zero subgradient characterizes a minimum. These are reusable for every subgradient-type method. Contributions of general lemmas on Fejér-monotone sequences are welcome.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, §2.4, pp. 36–42. https://doi.org/10.1007/978-3-642-82118-9
• B. T. Polyak, Minimization of unsmooth functionals, USSR Computational Mathematics and Mathematical Physics 9(3), 1969, 14–29. https://doi.org/10.1016/0041-5553(69)90061-5
• I. I. Eremin, The relaxation method of solving systems of inequalities with convex functions on the left-hand side, Soviet Mathematics Doklady 6, 1965, 219–222.
• P. M. Camerini, L. Fratta, F. Maffioli, On improving relaxation methods by modified gradient techniques, Mathematical Programming Study 3, 1975, 26–34.

Motivation

Many optimization problems in operations research are posed on an expectation: a two-stage or multistage stochastic program minimizes $f(x) = E\,F(x,\xi)$, where $F(\cdot,\xi)$ is convex but nonsmooth and the expectation cannot be computed exactly. What can be computed is a stochastic subgradient, a random vector whose mean is a subgradient of $f$. The stochastic subgradient method replaces the exact subgradient in the classical method by such a random vector. It was introduced by Yu. M. Ermoliev and N. Z. Shor in 1968 and developed by Ermoliev, Nurminski and others into a standard tool of stochastic programming; the same scheme, under the name stochastic (sub)gradient descent, underlies most of large-scale machine learning.

This mission formalizes Section 2.6 of N. Z. Shor, Minimization Methods for Non-Differentiable Functions (Springer 1985): the almost-sure convergence theorem for the stochastic subgradient method (Theorem 2.19), together with two deterministic results of the same section on perturbed and restarted variants of the subgradient method (Theorems 2.18 and 2.20).

Timeline, as recorded in the book:

• 1968, Ermoliev and Shor: the notion of a stochastic subgradient, introduced for a random search method for two-stage stochastic programs; the convergence theorem reproduced as Theorem 2.19.
• 1972, Bazhenov: convergence of a subgradient method with restarts for almost differentiable (in general nonconvex) functions, Theorem 2.18.
• 1976, Shepilov: stability of the subgradient method with respect to errors in the point where the subgradient is computed, Theorem 2.20.

Setting

$E_n$ is $n$-dimensional Euclidean space with inner product $(x,y)$. A vector $g$ is a subgradient of $f : E_n \to \mathbb{R}$ at $x_0$ if $f(x) - f(x_0) \ge (g, x - x_0)$ for all $x$; $M^*$ is the set of minimum points of $f$.

Stochastic subgradient method. Fix a probability space $(\Omega, \mathcal F, P)$ with a filtration $(\mathcal F_k)_{k \ge 0}$, a deterministic starting point $x_0$, stepsize rules $h_k : E_n \to \mathbb{R}$ and random vectors $g_k : \Omega \to E_n$. The iterates are

$$x_{k+1} = x_k - h_k(x_k)\, g_k, \qquad k = 0,1,\dots$$

In the book's notation $g_k = g_\omega(x_k)$: a random vector whose expectation, given the state at step $k$, is a subgradient of $f$ at $x_k$. In the Lean development the iterates are stochIter h G x₀ k ω.

Perturbed subgradient method (Shepilov). Given a subgradient selection $g_f$, points $\tilde x_k$ with $\|\tilde x_k - x_k\| \le \delta_k$, and steps $h_k > 0$: $x_{k+1} = x_k - h_k\, g_f(\tilde x_k)/\|g_f(\tilde x_k)\|$.

Restarted method (Bazhenov). For a function $f$ that is almost differentiable (Lipschitz on bounded sets, differentiable almost everywhere, with gradient continuous where it exists) and a selection $g_f(x)$ of almost-gradients (limit points of gradients at nearby points of differentiability), with $S_r = \{x : \|x - x^*\| \le r\}$: take the normalized step $\bar x_{k+1} = x_k - h_k\, g_f(x_k)/\|g_f(x_k)\|$ and restart from $x_0$ whenever $\bar x_{k+1}$ leaves $S_r$ (resetIter).

Formalization targets

Goal: Theorem 2.19 (p. 46)

Let $f$ be convex with a unique minimum point $x^*$. Suppose $E\{g_k \mid \mathcal F_k\}$ is a subgradient of $f$ at $x_k$, $E\{\|g_k\|^2 \mid \mathcal F_k\} \le c$, and almost surely $h_k(x_k) > 0$, $\sum_k h_k(x_k) = +\infty$, $\sum_k h_k^2(x_k) < \infty$. Then

$$P\Big(\lim_{k\to\infty} \|x_k - x^*\| = 0\Big) = 1 .$$

Milestones

1. Eq. (2.42), the conditional one-step inequality

$$E\{\|x_{k+1} - x^*\|^2 \mid \mathcal F_k\} \le \|x_k - x^*\|^2 + c\,h_k^2(x_k).$$

2. Proof of Theorem 2.19, pp. 46–47: with probability one $\|x_k - x^*\|^2$ converges to a finite limit (no divergence condition on the steps).
3. Theorem 2.20 (Shepilov): under $\delta_k \to 0$, $\sum h_k\delta_k < \infty$, $\sum h_k^2 < \infty$, $\sum h_k = \infty$, the perturbed method converges to a point of $M^*$.
4. Theorem 2.18 (Bazhenov): if $f(x^*) = \min_{S_r} f$ and $\inf_{S_r\setminus S_\varepsilon} (g_f(x), x - x^*) > 0$ for every $0 < \varepsilon < r$, the restarted method with $h_k \to 0$, $\sum h_k = \infty$ converges to $x^*$ from any $x_0 \in S_r$.

Significance

Theorem 2.19 is the basic justification of stochastic subgradient methods: without computing $f$ or any exact subgradient, the method reaches the minimizer with probability one, under stepsize conditions that are met by $h_k = 1/(k+1)$. It is the nonsmooth convex counterpart of the Robbins–Monro theorem and the prototype of the almost-sure convergence results for stochastic quasi-gradient methods used in stochastic programming. Theorem 2.20 shows that the deterministic method tolerates summable errors in the point where the subgradient is evaluated, which is what allows subgradients to be approximated by finite differences (Section 1.3). Theorem 2.18 extends the convergence of the normalized method to local minima of a class of nonconvex functions.

All four results are proved in the literature. To the best of the platform search (September 2026), none is machine-checked: the platform has almost-sure convergence theorems for smooth stochastic approximation under ODE-type hypotheses (Borkar–Meyn) and in-expectation bounds for stochastic gradient descent, neither of which covers this recursion. A formal proof of the goal would give a reusable almost-sure convergence argument for nonsmooth stochastic methods on top of Mathlib's martingale theory.

Difficulty

The deterministic proof of convergence of the subgradient method compares $\|x_{k+1}-x^*\|^2$ with $\|x_k - x^*\|^2$ along the whole trajectory. With random directions this comparison holds only in conditional expectation, and the term $h_k(g_k - E\{g_k\mid\mathcal F_k\}, x_k - x^*)$ is not controlled pathwise. Taking expectations of the one-step inequality and summing gives only bounds on $E\|x_k - x^*\|^2$, which do not yield almost-sure convergence. Moreover the stepsize $h_k(x_k)$ depends on the random iterate, so the conditions $\sum h_k^2(x_k) < \infty$ and $\sum h_k(x_k) = \infty$ hold only almost surely, not uniformly, and the iterates need not be square-integrable. Identifying the almost-sure limit as $0$ requires using the uniqueness of the minimizer to bound $(E\{g_k\mid\mathcal F_k\}, x_k - x^*)$ away from zero outside a neighbourhood of $x^*$.

In Theorems 2.18 and 2.20 the difficulty is that the distance to $x^*$ is not monotone: steps taken near the solution, or with a perturbed subgradient, can increase it, and a restart can move the iterate far away.

Formalization scope

• $E_n$ is EuclideanSpace ℝ (Fin n); $f$ is real-valued (finite everywhere); convexity is ConvexOn ℝ Set.univ f; uniqueness of $x^*$ is a separate hypothesis.
• Probabilistic model. The book assumes the distribution of $g_\omega(x_k)$ is determined by $x_k$ and independent of the past, and remarks this is inessential. The formalization uses a filtration: $g_k$ is $\mathcal F_{k+1}$-measurable, each $h_k$ is Borel measurable, $x_0$ is deterministic, and the hypotheses are on conditional expectations given $\mathcal F_k$. This contains the book's model.
• Condition (iii) is printed as $E\|g_\omega(x_k)\|^2 \le c$; the proof uses the conditional bound in (2.42), and the formalization assumes the conditional bound $E\{\|g_k\|^2\mid\mathcal F_k\} \le c$ almost surely.
• Every expectation carries an integrability hypothesis ($g_k$ and $\|g_k\|^2$ integrable), so no conditional expectation defaults to Lean's junk value $0$. The one-step milestone assumes $\|x_k - x^*\|^2$ integrable and a bounded stepsize rule at that step, and concludes integrability of $\|x_{k+1}-x^*\|^2$.
• Conditions (i)–(ii) on the random stepsizes are required almost surely. "With probability one $\lim\|x_k - x^*\| = 0$" is ∀ᵐ ω ∂μ, Tendsto (fun k => ‖x k ω - x*‖) atTop (𝓝 0).
• Division by zero. In Theorems 2.18 and 2.20 the normalized step is undefined when the subgradient vanishes; the formalization skips the step (the iterate is repeated) by an explicit branch, not through Lean's convention $x/0 = 0$. When the subgradient never vanishes the sequences are exactly the book's.
• The printed display (2.42) has $x_k$ where $x_{k+1}$ is meant on its left-hand side; the corrected inequality is stated.
• A trivializing formalization, for instance dropping the integrability hypotheses so that the conditional expectations vanish, or quantifying the stepsize conditions so that they cannot hold, is excluded by the hypotheses above; the hypotheses are satisfiable (deterministic subgradients of $f(x) = \|x\|$ with $h_k = 1/(k+1)$).
• Mathlib supplies conditional expectation (MeasureTheory.condExp), filtrations, and almost-sure convergence of $L^1$-bounded (sub/super)martingales; the supermartingale convergence theorem the book cites from Doob is used from Mathlib, not restated. A Robbins–Siegmund-type lemma for nonnegative almost-supermartingales would be the natural reusable contribution. The almost-differentiability and subgradient definitions duplicate drafts of other missions in this series.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, Section 2.6, pp. 44–47. https://doi.org/10.1007/978-3-642-82118-9
• Yu. M. Ermoliev and N. Z. Shor, A random search method for two-stage problems of stochastic programming and its generalization, Kibernetika (Kiev), no. 1, 90–92, 1968.
• L. G. Bazhenov, On the conditions for convergence of methods for minimizing almost differentiable functions, Kibernetika (Kiev), no. 4, 71–72, 1972.
• M. A. Shepilov, On a method of generalized gradient for finding the absolute minimum of a convex function, Kibernetika (Kiev), no. 4, 52–57, 1976.
• Yu. M. Ermoliev, Methods of Stochastic Programming, Nauka, Moscow, 1976.
• H. Robbins and D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics, Academic Press, 1971, pp. 233–257. https://doi.org/10.1016/B978-0-12-604550-5.50015-8
• J. L. Doob, Stochastic Processes, Wiley, New York, 1953 (supermartingale convergence theorem).

Motivation

Solving a square system of nonlinear equations $\psi_i(x) = 0$, $i = 1, \dots, n$, $x \in \mathbb{R}^n$, is one of the oldest tasks of numerical analysis. It appears whenever optimality conditions, equilibrium conditions or discretized differential equations have to be solved. N. Z. Shor's Minimization Methods for Non-Differentiable Functions (Springer 1985, translated by K. C. Kiwiel and A. Ruszczyński) treats such a system as the nonsmooth minimization problem

$$\min_{x \in E_n} f(x), \qquad f(x) = \max_{1 \le i \le n} |\psi_i(x)|,$$

whose optimal value is $0$ exactly when the system is consistent. Section 3.5 of the book applies the subgradient method with space dilation to this problem. At each iteration that method needs the gradient of one of the $\psi_i$, not all $n$ of them. Taking the dilation coefficient to its extreme value ($\beta = 0$) turns the method into a gradient orthogonalization method. The book shows that this method converges at a quadratic rate near a regular solution, like Newton's method, although it never forms or factorizes the Jacobian.

This mission is the eighth in a series formalizing Shor's book. It covers Sections 3.5–3.6 (printed pp. 62–71).

Setting

$E_n$ is the $n$-dimensional Euclidean space with inner product $(x, y)$ and norm $\|x\|$. The data are functions $\psi_1, \dots, \psi_n : E_n \to \mathbb{R}$ with gradients $g_{\psi_i}(x)$, and the max-residual function is $f(x) = \max_i |\psi_i(x)|$ (3.24). The Jacobian is the matrix $J(x) = \{\partial\psi_i/\partial t_j\}_{i,j=1}^n$ of partial derivatives with respect to the coordinates $x = \{t_1, \dots, t_n\}$.

An almost-gradient of a function $f$ at $x_0$ is an accumulation point of a sequence of gradients $\nabla f(x_k)$, where $x_k \to x_0$ and $f$ is differentiable at every $x_k$ (p. 18).

The regular case (p. 63) is the situation in which $f^* = \min f = 0$ is attained at a point $x^*$, the $\psi_i$ are continuously differentiable near $x^*$, and $J(x^*)$ is nonsingular.

The gradient orthogonalization method (3.27) runs in stages of $n$ steps. A stage starting at $x_0$ produces $x_1, \dots, x_n$ as follows. At step $k+1$, $0 \le k < n$, the gradient $g_{\psi_{k+1}}(x_k)$ is projected on the subspace orthogonal to the gradients $g_{\psi_1}(x_0), \dots, g_{\psi_k}(x_{k-1})$ used earlier in the stage. Call the result $\varphi_{k+1}$. The step is

$$x_{k+1} = x_k - \frac{\psi_{k+1}(x_k)}{\|\varphi_{k+1}\|^2}\, \varphi_{k+1}.$$

For $k = 0$ there is nothing to project, so $\varphi_1 = g_{\psi_1}(x_0)$. The next stage starts at $x_n$.

Formalization targets

Goal: Theorem 3.9, one stage squares the error

Let $x^* = 0$ solve the system, let the $\psi_i$ be continuously differentiable with gradients Lipschitz with constant $L$ on a ball $S_\delta = \{x : \|x\| < \delta\}$ (3.28), and let $g_{\psi_1}(0), \dots, g_{\psi_n}(0)$ be linearly independent. Then there exist $\varepsilon > 0$ and $c > 0$ such that every stage with $\|x_0\| \le \varepsilon$ satisfies

$$\|x_n\| \le c\, \|x_0\|^2 .$$

Milestones inside the proof

The proof of Theorem 3.9 passes through these displayed results, stated here in attack order:

• Eq. (3.29): near the solution, the orthogonalized gradients satisfy $\|\varphi_{k+1}\| > b > 0$, with $b$ uniform over stages.
• Eq. (3.33): after step $k+1$, $|\psi_{k+1}(x_{k+1})| \le (L/b^2)\, \psi_{k+1}^2(x_k)$.
• Lemma 3.1: a step of length $h$ in a unit direction orthogonal to $g_{\psi_i}(x_1)$ changes $\psi_i$ by at most $L h (h + \|x_1 - x_2\|)$.
• Eqs. (3.36)–(3.37): within a stage, $\max_k \|x_k\| \le c_1 \|x_0\|$, and at the end point $f(x_n) \ge c_2 \|x_n\|$.

Companion result: Theorem 3.8

In the regular case, for every $\delta > 0$ there is a neighborhood of $x^*$ in which every almost-gradient satisfies

$$(1-\delta) f(x) \le (g_f(x), x - x^*) \le (1+\delta) f(x).$$

Significance

Theorem 3.9 says that a method which evaluates one equation and one gradient per step, and never solves a linear system, has the local quadratic rate of Newton's method on a regular system. The stages combine: once one stage starts close enough to the solution, the errors of later stages satisfy $\|x_0^{(r+1)}\| \le c\|x_0^{(r)}\|^2$. Theorem 3.8 describes the geometry of $f$ near a regular solution. The ratio of $(g_f(x), x - x^*)$ to $f(x)$ tends to $1$, which is what allows the dilation parameters of the book's Theorem 3.3 to approach their extreme values near the solution. Both results connect the nonsmooth space-dilation methods of Chapter 3 to classical Newton-type theory.

All results of this mission are proved in the book. None of them has, to our knowledge, a machine-checked proof: the platform has local quadratic convergence results for cubic-regularized Newton, proximal Newton and semismooth Newton, but not for this method. The work is formalizing Shor's proof. This includes building the Gram-determinant argument behind (3.29) and the second-order estimates, which are reusable for other projection-based solvers of Kaczmarz type.

Difficulty

A naive argument analyses each step as a Newton step for one equation and stops there. That shows each equation $\psi_{k+1}$ is small right after its own step, but the theorem needs all equations to be small at the end of the stage. Later steps move the point and can undo the progress on earlier equations. The step directions are orthogonal to the earlier gradients, but those gradients were taken at earlier points, not at the current one. Controlling this drift needs Lemma 3.1 together with the bound (3.36), which says that the whole stage stays within a multiple of $\|x_0\|$.

A second difficulty is that the method is only defined near the solution. The step divides by $\|\varphi_{k+1}\|^2$, and a uniform positive lower bound on these norms comes from the nonvanishing of a Gram determinant evaluated at $n$ different points. The final passage from small residuals to a small error needs the growth bound (3.37), which uses the nonsingularity of the Jacobian once more.

Formalization scope

• Representation. $E_n$ is EuclideanSpace ℝ (Fin n). The equations are a family ψ : Fin n → E_n → ℝ indexed from $0$, so ψ k is the book's $\psi_{k+1}$. Gradients are Mathlib's gradient, and $S_\delta$ is the open ball Metric.ball 0 δ. Continuous differentiability is ContDiff ℝ 1; in Theorem 3.8 it is ContDiffOn ℝ 1 on a neighborhood of $x^*$.
• The stage. A stage is a predicate IsOrthStage ψ x on a sequence $x : \mathbb{N} \to E_n$, which fixes $x_1, \dots, x_n$ from $x_0$. The projection is starProjection onto the orthogonal complement of the span of the earlier gradients.
• Corrected misprint. The printed Step 1, (3.27a), divides by $\|g_{\psi_1}(x_0)\|$ rather than its square. The formalization uses the square, which is what (3.27b) and the proof's (3.31)–(3.33) require at $k = 0$.
• Division by zero. The book gives no rule for $\varphi_{k+1} = 0$; Lean's $t/0 = 0$ would leave the point unchanged. All statements apply the method only near the solution, where (3.29) bounds $\|\varphi_{k+1}\|$ away from zero.
• Quantifier order. In Theorem 3.9 and in (3.29), (3.36)–(3.37), the constants ($\varepsilon$, $c$, $\delta'$, $b$, $\varepsilon_0$, $c_1$, $c_2$) are existentials placed before the stage. They depend only on the data $\psi, \delta, L$. A statement with $c$ chosen after $x_0$ would be trivial, with $c = \|x_n\|/\|x_0\|^2$, and is ruled out.
• Nonsingularity. In Theorem 3.9 it is the linear independence of $g_{\psi_i}(0)$, the book's primary hypothesis. In Theorem 3.8 it is $\det J(x^*) \ne 0$, with $J$ defined by coordinate partial derivatives.
• Almost-gradients. They are quantified universally: Theorem 3.8 holds for every almost-gradient, not for one chosen one.

Not formalized: Theorem 3.10 (pp. 70–71), the $n$-step quadratic convergence of the $\beta = 0$ r-algorithm with resetting. Its directional minimization rule is not pinned down on the page. The algorithm says "determined by minimizing", while the proof uses "the smallest positive root" of a stationarity equation. A contribution that fixes this rule and states the theorem is welcome as a follow-up.

Contributions of any of the five milestones are welcome independently. The Gram-determinant lower bound (3.29) and Lemma 3.1 are general facts about orthogonalization and Lipschitz gradients, and are useful beyond this mission.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, §§3.5–3.6, pp. 62–71. https://doi.org/10.1007/978-3-642-82118-9
• J. M. Ortega and W. C. Rheinboldt, Iterative Solution of Nonlinear Equations in Several Variables, Academic Press, 1970. https://doi.org/10.1137/1.9780898719468