Operations Research

Motivation

Firms that can buy the same item from two suppliers, a cheap slow one and a fast expensive one, face the dual-sourcing inventory problem: how much to order from each source in every period when demand is random and unmet demand is backlogged. Global sourcing (offshore regular supply plus a near-shore express supply) is the standard example (Allon and Van Mieghem 2010). When the two lead times differ by more than one period, the optimal policy depends on the whole pipeline of outstanding orders. No simple optimal policy is known, and dynamic programming is intractable for long lead times.

The tailored base-surge (TBS) policy orders a constant amount from the slow source and uses the fast source to bring the expedited inventory position up to a fixed level. It is simple, and it is used in practice. Janakiraman, Seshadri and Sheopuri (JSS, Management Science 2015) showed that its best parameters solve a convex program that does not depend on the regular lead time, and they conjectured, with numerical support, that TBS is near-optimal when that lead time is long.

Timeline:

• Karlin and Scarf (1958), Scarf (1960): structure of optimal single-source backlog policies with a lead time.
• Sheopuri, Janakiraman and Seshadri (2010): reduction of dual-sourcing policies to the truncated regular pipeline and the expedited inventory position (Lemma 1 here).
• Allon and Van Mieghem (2010): the TBS policy, with conjectures and numerical evidence.
• JSS (2015): the TBS cost formula and a convex program for its parameters.
• Xin and Goldberg (2018): proof of the conjecture with an explicit rate (Management Science 64(1), 2018). This mission formalizes that result.

Setting

Let $D$ be a nonnegative random variable with finite mean $\mathbb E[D]$ that is not almost surely constant. Demands $D_1, D_2, \dots$ are i.i.d. copies of $D$. The regular source has lead time $L$, the express source has lead time $L_0 \ge 0$, and $L > L_0 + 1$. In period $t$ the controller orders $q^R_t \ge 0$ and $q^E_t \ge 0$; then $q^R_{t-L} + q^E_{t-L_0}$ arrives and $D_t$ is realized, so the on-hand inventory evolves as $I_{t+1} = I_t + q^R_{t-L} + q^E_{t-L_0} - D_t$ and may be negative. Initially nothing is on order and $I_1 = -\sum_{i=1}^{\hat G} D'_{-i}$, where the $D'_{-i}$ are further i.i.d. copies of $D$ and $\mathbb P(\hat G = k) = 2^{-k}$, $k \ge 1$.

The per-period cost is $c\,q^E_{t-L_0} + G(I_{t+1})$ with $G(y) = h y^+ + b y^-$, where $b, h > 0$ and $c > 0$ is the express premium (the regular unit cost is normalized to $0$). An admissible policy $\pi \in \Pi$ chooses the two orders in period $t$ as deterministic measurable functions of $(q^R_{t-L}, \dots, q^R_{t-1}, q^E_{t-L_0}, \dots, q^E_{t-1}, I_t)$. Its long-run average cost is

$$C(\pi) = \limsup_{T\to\infty}\frac1T\sum_{t=L_0+1}^T \mathbb E[C^\pi_t], \qquad \mathrm{OPT}(L) = \inf_{\pi\in\Pi}C(\pi).$$

With the expedited inventory position $\hat I_t = I_t + \sum_{k=t-L_0}^{t-1}q^E_k + \sum_{k=t-L}^{t-L+L_0}q^R_k$, the TBS policy $\pi_{r,S}$ orders $q^R_t = r$ and $q^E_t = \max(0, S - \hat I_t)$. A best TBS pair $(r^*, S^*)$ minimizes $C(\pi_{r,S})$ over $0 \le r \le \mathbb E[D]$ and $S \in \mathbb R$ (first in $r$ through $F^\infty(r) = \inf_S C(\pi_{r,S})$, then in $S$).

The constants $\epsilon_0$ and $Y_0$ are explicit functionals of the law of $D$ and of $L_0, b, h, c$. They are built from $g = \inf_x\mathbb E[G(x - \sum_{i=1}^{L_0+1}D'_i)]$, $U = c\,\mathbb E[D] + \mathbb E[G(-\sum_{i=1}^{L_0+1}D'_i)]$, $p_0 = \mathbb P(D < \mathbb E[D])$, the mean absolute deviation $\eta_0$, and the large-deviation quantities $\gamma_\epsilon, \vartheta_\epsilon$ of $\phi_\epsilon(\theta) = e^{\theta(\mathbb E[D]-\epsilon)}\mathbb E[e^{-\theta D}]$ (p. 441).

Formalization targets

Goal: Theorem 1 (p. 441)

For all $L_0 \ge 0$, $\epsilon \in (0,1)$ and $L > \epsilon_0^{-2} + Y_0\epsilon^{-2}$,

$$\frac{C(\pi_{r^*,S^*})}{\mathrm{OPT}(L)} < 1 + \epsilon.$$

The threshold does not depend on $L$, so the statement gives an explicit, inverse-polynomial rate. Its limit form $C(\pi_{r^*,S^*})/\mathrm{OPT}(L) \to 1$ is Corollary 1 of the paper.

Milestones

In the order the proof uses them:

• the bound $g \le \mathrm{OPT}(L) \le U$;
• Lemma 1, the reduction to $\hat\Pi$ (quoted from Sheopuri et al.);
• Eq. (3), the TBS cost formula $C(\pi_{r,S}) = c(\mathbb E[D]-r) + \mathbb E[G(I^r_\infty + S - \sum_{i=1}^{L_0+1}D'_i)]$ (quoted from JSS);
• Theorem 2, the existence of a stationary-like vector $(\chi^{*,L}, q^{*,L}, \mathcal I^{*,L})$ with $r_L = \mathbb E[\chi^{*,L}_1]$;
• Corollary 2 and Lemma 2, the lower bound $\mathrm{OPT}(L) \ge c(\mathbb E[D]-r_L) + (1-\alpha)V^{L-L_0}_\alpha(r_L,-\infty)$ through a discounted single-source problem;
• Lemma 3, the Bellman equation and structure of that problem (quoted from JSS and Scarf 1960);
• Lemma 4 (8) and (9), and Corollary 3, the passage to the infinite horizon and to base-stock policies;
• Lemma 5, the random-walk maxima $M^r_k$ (proof omitted in the paper);
• Lemmas 8–9 and Corollary 4: $r_L < \mathbb E[D] - \epsilon_0$ once $L > \epsilon_0^{-2} + L_0 + 1$.

Significance

The theorem shows that one of the simplest dual-sourcing heuristics is asymptotically optimal as the regular lead time grows. This is the regime where exact dynamic programming is hopeless. The best TBS parameters come from a convex program independent of $L$, so the result yields an algorithm whose running time does not grow with $L$ and whose optimality gap is bounded explicitly for every finite $L$. It extends the lower-bounding technique of Xin and Goldberg's lost-sales work (Operations Research 2016) from a static to a dynamic relaxation.

Formalization adds the following. To the best of available knowledge, none of the objects involved (average-cost inventory control with backlog, TBS policies, Lindley-type maxima of random walks with their Spitzer identity) exists in Mathlib or on the platform. The paper's proof defers several ingredients to the literature or omits them: Lemma 1, Eq. (3), Lemma 3, and the details of Lemmas 5 and 7. A complete formal proof must supply them. The result is proved on paper but not formalized anywhere.

Difficulty

An optimal dual-sourcing policy need not be stationary, its induced Markov chain need not have a stationary distribution, and the inventory is unbounded below. The natural argument would compare the optimal policy's steady state with the TBS steady state, and it fails at its first step. Theorem 2 replaces the steady state by a vector with a few distributional properties, built from time averages. That construction, and the independence structure it must carry, is the central technical step. The conditional Jensen step then leads to a single-source problem with possibly negative demand, where textbook interchange-of-limits theorems do not apply directly. Finally, bounding $r_L$ away from $\mathbb E[D]$ requires a quantitative lower bound on the growth of random-walk maxima under only a first-moment assumption.

Formalization scope

Conventions of the Lean development (namespace XinGoldbergTBS.Asymptotic):

• The law of $D$ is a probability measure on $\mathbb R$ with no mass on $(-\infty,0)$, finite mean, and no atom of mass $1$. The paper's "strictly positive (possibly infinite) variance" is read as "not almost surely constant".
• $c_R = 0$, $b > 0$, $h > 0$, $c > 0$, and $L, L_0$ are natural numbers. The paper's standing assumption $L > L_0 + 1$ is a hypothesis wherever the paper states it; in Theorem 1 it follows from the threshold.
• Costs, expectations, $C(\pi)$, $\mathrm{OPT}(L)$, $V^n_\alpha$ and $V^\infty_\alpha$ take values in $[0,\infty]$, so infinite costs are never truncated. The ratio in Theorem 1 is stated as $C(\pi_{r^*,S^*}) < (1+\epsilon)\mathrm{OPT}(L)$, which is equivalent because $0 < g \le \mathrm{OPT}(L) \le U < \infty$.
• $\Pi$ is exactly the paper's class: deterministic, time-dependent, measurable, nonnegative orders that depend on the pipeline and inventory. It is neither restricted to stationary policies nor enlarged to randomized ones. TBS policies are members, so $C(\pi_{r,S}) \ge \mathrm{OPT}(L)$ by construction.
• $\vartheta_\epsilon \in [0,\infty]$ is the supremum of the minimizers of $\phi_\epsilon$ on $[0,\infty)$, and it is $\infty$ if the infimum is not attained; $1/\infty = 0$.
• The existence of a best TBS pair is asserted in the paper via JSS. The goal therefore also asserts that some TBS policy with $0 \le r \le \mathbb E[D]$ meets the bound, so it cannot hold vacuously when no minimizer exists.
• $r_L$ belongs to a witness of Theorem 2, and the results that use it hold for every witness.
• The single-source class $\bar\Pi$ ("feasible nonanticipative policies, as typically defined") is read as nonnegative orders that are measurable functions of past demands. In Lemma 3 "increasing" is read as nondecreasing, and convexity in $x$ includes finiteness.
• The paper states Eq. (3) without a range for $r$; it is stated here for $0 \le r \le \mathbb E[D]$, the TBS parameters over which the paper optimizes. At $r = \mathbb E[D]$ both sides are $+\infty$. In Lemma 8, the range's upper end is $+\infty$ when $\epsilon = 0$.
• Differences such as $V^\infty_\alpha - V^n_\alpha$ and $M^r_\infty - M^r_n$ are stated additively, and the negative terms of (9) and Corollary 3 are moved to the other side.

Lemma 1, Eq. (3) and Lemma 3 are results the paper quotes from Sheopuri et al. (2010), JSS and Scarf (1960). Proposition 1 (conditional-expectation form of the bound) is not included.

A trivializing formalization is ruled out: $\mathrm{OPT}(L)$ ranges over the full admissible class, the constants are definitions rather than hypotheses, and the goal includes an existence clause.

Reusable beyond this mission: average-cost inventory models with lead times, discounted single-source backlog value functions, and Spitzer-type identities for random-walk maxima. Contributions to any milestone are welcome.

Selected references

• L. Xin and D. A. Goldberg, Asymptotic Optimality of Tailored Base-Surge Policies in Dual-Sourcing Inventory Systems, Management Science 64(1):437–452, 2018. https://doi.org/10.1287/mnsc.2016.2607
• G. Janakiraman, S. Seshadri and A. Sheopuri, Analysis of Tailored Base-Surge Policies in Dual Sourcing Inventory Systems, Management Science 61(7):1547–1561, 2015.
• G. Allon and J. A. Van Mieghem, Global Dual Sourcing: Tailored Base-Surge Allocation to Near- and Offshore Production, Management Science 56(1):110–124, 2010.
• A. Sheopuri, G. Janakiraman and S. Seshadri, New Policies for the Stochastic Inventory Control Problem with Two Supply Sources, Operations Research 58(3):734–745, 2010.
• H. Scarf, The Optimality of (s, S) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960, pp. 196–202.
• L. Xin and D. A. Goldberg, Optimality Gap of Constant-Order Policies Decays Exponentially in the Lead Time for Lost Sales Models, Operations Research 64(6):1556–1565, 2016.

Motivation

A Markovian decision process (Howard, 1960) models a controller who, in each of finitely many states, picks a decision, earns a reward and moves to a random next state according to known transition probabilities. In applications (inventory control, equipment replacement, quality control) those probabilities are estimated, not known. Satia and Lave (Operations Research 21(3), 1973) treat the uncertainty in two ways: a game-theoretic formulation, in which each unknown row only lies in a given set, and a Bayesian formulation, going back to Silver (1963) and Martin (1967), in which the controller holds a prior on the unknown matrix and learns from observed transitions.

The Bayesian problem is the natural one but its state includes the whole prior, so it cannot be solved exactly beyond small cases. The paper's contribution in the Bayesian part is a pair of computable bounds on the Bayesian optimal return in terms of the two game-theoretic values (max-max and max-min). This mission formalizes those bounds and the chain of facts they rest on.

Setting

There are $N$ states $i$ and, in state $i$, a finite nonempty set $K_i$ of decisions. A transition $i \to j$ under decision $k$ earns $r^k_{ij}$ and rewards are discounted by $\beta$, $0 \le \beta < 1$. The row $p_i^k = (p^k_{ij})_j$ of transition probabilities is unknown; it is known to lie in a closed convex nonempty set $S_i^k$ of probability vectors, and $S = \{P : p_i^k \in S_i^k \text{ for all } i, k\}$.

A prior $g$ is a probability distribution on matrices $P = (p_i^k)$ whose rows are all probability vectors. Its means are $\bar p^k_{ij} = E(p^k_{ij})$. After a transition $l \to j$ under decision $m$ the prior is replaced by the Bayes transformation $T^m_{lj} g(P) = C\,p^m_{lj}\,g(P)$ (Eq. (8)), with $C$ the normalizing constant. The Bayesian optimal return $f(i,g)$ solves the recursion

$$f(i, g) = \max_{k \in K_i} \Big\{ \sum_j \bar p^k_{ij} r^k_{ij} + \beta \sum_j \bar p^k_{ij} f(j, T^k_{ij} g) \Big\}. \qquad (10)$$

The max-max and max-min values $V^+$, $V^-$ solve

$$V_i^\pm = \max_{k \in K_i} \operatorname*{max/min}_{p_i^k \in S_i^k} \Big\{ \sum_j p^k_{ij} r^k_{ij} + \beta \sum_j p^k_{ij} V_j^\pm \Big\},$$

with max for $V^+$ and min for $V^-$. Finally $\alpha = \operatorname{prob}(P \in S \mid g)$, the prior probability that the true matrix lies in $S$.

The Lean development lives in the namespace SatiaLave.Bayes: UncertainMDP, IsPrior, pbar, bayes, SolvesEq10, SolvesVplus, SolvesVminus, alpha, rmax, rmin, policyValue.

Formalization targets

Goal: Propositions 9 and 10

For every bounded solution $f$ of (10), all solutions $V^+$, $V^-$, every prior $g$ and every state $i$,

$$\alpha V_i^- + (1-\alpha)\min_{i,j,k}\frac{r^k_{ij}}{1-\beta} \;\le\; f(i,g) \;\le\; \alpha V_i^+ + (1-\alpha)\max_{i,j,k}\frac{r^k_{ij}}{1-\beta},$$

together with the existence of $f$, $V^+$ and $V^-$. Both halves are the paper's printed statements.

Milestones

1. Proposition 6 (Martin): (9)/(10) has a unique bounded solution (unique at priors).
2. No learning (p. 733): at a point-mass prior $\delta_P$, $f(\cdot,\delta_P)$ solves the optimality equations of the process with known $P$.
3. Proposition 8: $f(i,g)$ is convex in $g$.
4. Jensen step (proof of Proposition 9): $f(i,g) \le \int f(i,\delta_P)\,dg(P)$.
5. Policy step (proof of Proposition 10): $f(i,g) \ge \int [q + \beta P^A q + \beta^2 [P^A]^2 q + \cdots]_i\,dg(P)$ for every pure stationary policy $A$.

Significance

The result. The bounds sandwich an intractable quantity between two quantities computable by finite algorithms (the max-max and max-min policy-iteration procedures of the same paper), weighted by a single prior probability $\alpha$. When the prior concentrates on $S$ ($\alpha \to 1$) the bounds become $V_i^- \le f(i,g) \le V_i^+$: the Bayesian return lies between the pessimistic and optimistic robust values. They are the upper and lower bounds on the return that the paper's implicit-enumeration method (the decision tree of its Fig. 2 and Proposition 12) uses to compare decisions. The Jensen step is a value-of-information inequality (Bayesian optimal return is at most the expected full-information optimal return), which recurs throughout Bayesian control and bandit theory.

Formalizing it. The results are proved on paper (Propositions 6 and 8 by reference to Martin's book and Satia's thesis, Propositions 9 and 10 in the text); none is machine-checked. The mission produces a Lean model of Bayes-adaptive Markov decision processes with priors as measures, the Bayes transformation and its fixed-point recursion, and the link between the Bayesian and the robust (rectangular) formulations. Martin's existence-uniqueness theorem and the convexity of the Bayesian value are reusable for any Bayes-adaptive model.

Difficulty

The prior space is infinite-dimensional and not a vector space, so the recursion (10) lives on a space of measures, and the usual finite-state arguments do not apply verbatim. Proposition 8 gives convexity only along finite mixtures, while the proof of Proposition 9 applies Jensen's inequality to the integral mixture $g = \int \delta_P\,dg(P)$ of point masses; bridging the two, or proving the value-of-information inequality directly, is the central step. The paper also restricts the point masses to $x_i^k \in S_i^k$, which cannot represent a prior with mass outside $S$; the formal statement integrates over every transition matrix, as the next line of the paper's display requires. Measurability of $P \mapsto f(i,\delta_P)$ is not automatic, since $f$ is only characterized by a functional equation.

Formalization scope

• States are a nonempty Fintype S; decisions a dependent family D i of nonempty finite types. A matrix is P : (i : S) → D i → S → ℝ with the product Borel $\sigma$-algebra.
• Priors are measures: a probability measure giving full mass to matrices whose rows are probability vectors. This generalizes the paper's densities $g(P)$ and includes the point masses $a_x$ its proof uses.
• Bayes transformation at $\bar p = 0$: the normalizing constant does not exist; bayes then returns $g$. That posterior is always multiplied by $\bar p = 0$ in (10), so the choice is immaterial.
• Readings of informal words. "The problem reduces to a Markovian decision process" = at a point-mass prior, fixed by every Bayes transformation, $f$ solves the known-$P$ optimality equations. "Convex in $g$" = convex along mixtures of priors. "Unique set of bounded functions" = two bounded solutions agree at every prior (values at non-priors are unconstrained). "Satisfy (9)" is formalized as (10), which the paper derives from (9) by linearity of $E$. $\max_{P\in S}$/$\min_{P\in S}$ in $V^\pm$ is taken over the row $p_i^k \in S_i^k$ (the only row that enters; $S$ is a product), as ⨆/⨅ over a nonempty bounded set. "Obviously $f(i,g)\ge V_i^A$" is stated for every pure stationary policy $A$, not only a max-min optimal one. The policy return is the componentwise series $\sum_n \beta^n (P^A)^n q$.
• Added hypotheses, not printed: $0 \le \beta < 1$; $S_i^k \ne \emptyset$; $N \ge 1$. Printed and kept: $S_i^k$ closed and convex.
• $f$, $V^+$, $V^-$ are quantified as solutions of their equations; $\alpha$ is computed from $g$, never a free parameter; $\max_{i,j,k}[r^k_{ij}/(1-\beta)]$ ranges over all states $i,j$ and $k \in K_i$. Integrability of the integrands in milestones 4 and 5 is part of their conclusions.
• Trivializations ruled out. A free $\alpha \in [0,1]$, or $f$ defined off priors, would make the goal false or vacuous; the goal also asserts that bounded $f$ and $V^\pm$ exist, so its universal part is not vacuous.
• Not in scope: Proposition 7 (matrix-beta conjugacy, which needs a Dirichlet distribution), Propositions 11–13 and the numerical example.

Welcome contributions: the Banach fixed-point argument for (10) on bounded functions of priors; lemmas that bayes maps priors to priors and that point masses are fixed; continuity of the known-$P$ optimal value in $P$; a general Jensen inequality for functions convex along mixtures of probability measures.

Selected references

• J. K. Satia and R. E. Lave, Jr., Markovian Decision Processes with Uncertain Transition Probabilities, Operations Research 21(3), 728–740, 1973. https://doi.org/10.1287/opre.21.3.728
• J. J. Martin, Bayesian Decision Problems and Markov Chains, Wiley, New York, 1967.
• E. A. Silver, Markovian Decision Processes with Uncertain Transition Probabilities or Rewards, Interim Technical Report No. 1, Operations Research Center, Massachusetts Institute of Technology, August 1963.
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• J. K. Satia, Markovian Decision Process with Uncertain Transition Matrices or/and Probabilistic Observation of States, Ph.D. dissertation, Stanford University, 1968.

Motivation

Many problems in optimization and equilibrium modelling reduce to a system of equations $F(x) = 0$ whose map $F : \mathbb R^n \to \mathbb R^n$ is Lipschitz but not differentiable: reformulations of nonlinear complementarity problems through the componentwise minimum or the Fischer–Burmeister function, Karush–Kuhn–Tucker systems of constrained programs, and gradients of augmented Lagrangians all have kinks. Newton's method, $x^{k+1} = x^k - F'(x^k)^{-1}F(x^k)$, is the standard fast local solver for smooth systems, but it needs a derivative at every iterate.

Qi and Sun (Math. Programming 58, 1993) replaced the Jacobian by an arbitrary element of Clarke's generalized Jacobian and showed that the resulting method converges locally superlinearly under a regularity condition they called semismoothness, extending Mifflin's notion for functionals (Mifflin, SIAM J. Control Optim. 15, 1977) to vector-valued maps. This theorem is the foundation of the family of semismooth Newton methods used in complementarity, variational inequalities and PDE-constrained optimization.

Timeline. Robinson (1988) and Pang (Math. OR 15, 1990) studied Newton methods built on B-derivatives, with convergence proved under a strong Fréchet derivative at the solution; Kummer (1988) gave an abstract framework for Newton methods for nonsmooth equations; Qi and Sun (1993) proved local superlinear convergence for the generalized-Jacobian iteration under semismoothness and nonsingularity of $\partial F(x^*)$, with order $1+p$ under $p$-order semismoothness.

Setting

Let $F : \mathbb R^n \to \mathbb R^m$ be locally Lipschitz. By Rademacher's theorem $F$ is differentiable on a set $D_F$ of full measure; write $JF(y)$ for the Jacobian at $y \in D_F$. The generalized Jacobian is

$$\partial F(x) = \mathrm{co}\Big\{\lim_{i\to\infty} JF(x_i) : x_i \to x,\ x_i \in D_F\Big\},$$

the convex hull of all limits of Jacobians along sequences of differentiability points converging to $x$. The one-sided directional derivative is $F'(x;h) = \lim_{t\downarrow 0}(F(x+th)-F(x))/t$.

$F$ is semismooth at $x$ if it is Lipschitz near $x$ and, for every $h$, the limit of $Vh'$ over $V \in \partial F(x+th')$, $h' \to h$, $t \downarrow 0$ exists. For $0 < p \le 1$, $F$ is $p$-order semismooth at $x$ if in addition $Vh - F'(x;h) = O(\|h\|^{1+p})$ for $V \in \partial F(x+h)$, $h \to 0$.

For $m = n$, the nonsmooth Newton method is

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

where any element of $\partial F(x^k)$ may be chosen at each step. A run is a pair of sequences $(x^k)$, $(V_k)$ with $V_k \in \partial F(x^k)$ and $V_k(x^{k+1}-x^k) = -F(x^k)$ for all $k$. A root $x^*$ ($F(x^*) = 0$) is regular when every $V \in \partial F(x^*)$ is nonsingular.

Formalization targets

Goal: Theorem 3.2, local superlinear convergence

Let $F$ be locally Lipschitz, $F(x^*) = 0$, $F$ semismooth at $x^*$, and every $V \in \partial F(x^*)$ nonsingular. Then there is $\delta > 0$ such that every $V \in \partial F(y)$ with $\|y - x^*\| < \delta$ is nonsingular, a Newton step from such a $y$ stays within $\delta$ of $x^*$, and every run with $\|x^0 - x^*\| < \delta$ satisfies

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

The goal asserts only the shape of the convergence (superlinear) and fixes no constants.

Stronger: Theorem 3.2, order $1 + p$

If moreover $F$ is $p$-order semismooth at $x^*$, $0 < p \le 1$, there are $\delta > 0$ and $C$ with

$$\|x^{k+1} - x^*\| \le C\|x^k - x^*\|^{1+p}$$

for every run started within $\delta$ of $x^*$.

Milestones

The milestones follow the paper's route: Proposition 2.1 (the limit in the definition of semismoothness is the directional derivative), Lemma 2.2 (Lipschitz continuity of $F'(x;\cdot)$ and its realisation by an element of $\partial F(x)$), Theorem 2.3 (semismoothness is equivalent to $Vh - F'(x;h) = o(\|h\|)$ and to the corresponding condition at differentiability points), the Remark's expansion (2.17), Proposition 3.1 (uniform invertibility near a regular point), the order-$(1+p)$ sentence of Theorem 3.2, and Corollary 2.5 (strong Fréchet differentiability implies semismoothness).

Significance

The theorem gives a locally superlinearly convergent method for Lipschitz equations with no smoothness beyond semismoothness at the root. Convex, smooth and subsmooth functions are semismooth, as are sums and scalar products of semismooth functions (the paper, citing Mifflin), and later work showed that the complementarity and KKT reformulations on which semismooth Newton solvers are built are semismooth as well; the order-$(1+p)$ variant gives local quadratic convergence for strongly semismooth maps. Mission II of this series treats the paper's global convergence theorem on a ball, and Mission III the semismoothness of augmented Lagrangian gradients, which supplies the application.

The results are proved in the paper. No machine-checked version of the generalized Jacobian, of semismoothness or of the nonsmooth Newton method is known to exist in Mathlib or on this platform; the platform's formalized Newton results concern one-dimensional $C^2$ functions (MetodosNumericos.newton_local_convergence) and smooth convex minimization. A complete development would provide the first formal library for Clarke's generalized Jacobian and semismooth maps.

Difficulty

The classical Newton proof compares $F(x^k)$ with its linearization $JF(x^*)(x^k - x^*)$ and uses continuity of the Jacobian at $x^*$. Here neither is available: $F$ need not be differentiable at $x^*$ or at any iterate, the element $V_k$ is chosen arbitrarily from a set, and $V_k$ need not be close to any fixed linear map. The comparison has to go through the directional derivative $F'(x^*; \cdot)$, which is only positively homogeneous, not linear. The analytic content therefore sits in Section 2: showing that semismoothness, defined through a limit over a set-valued map, controls $Vh - F'(x;h)$ uniformly in the direction, and that $F(x+h) - F(x) - F'(x;h)$ is small. Both rest on Clarke's mean-value inclusion and on compactness and upper semicontinuity of $\partial F$, none of which is in Mathlib. The superlinear rate also requires a uniform bound on $\|V^{-1}\|$ in a whole neighbourhood, not just at $x^*$.

Formalization scope

Everything lives in the namespace NonsmoothNewton.Local. Section 2 results are stated for maps between finite-dimensional real normed spaces $E \to G$ (the paper's $\mathbb R^n \to \mathbb R^m$ is the Euclidean instance); Section 3 results use EuclideanSpace ℝ (Fin n). Conventions fixed by the Lean statements:

• $JF$ is fderiv; the generalized Jacobian is the convex hull (no closure) of limits of fderiv along sequences $x_i \to x$ of differentiability points.
• $F'(x;h)$ is the one-sided limit over $t \downarrow 0$, never the two-sided lineDeriv; its value is a limUnder, used only where existence is a hypothesis or a consequence.
• Nonsingular means IsUnit in the ring of continuous linear endomorphisms; $\|V^{-1}\| \le C$ is a two-sided inverse of operator norm at most $C$.
• A run of (3.2) is encoded by the linear equation $V_k(x^{k+1} - x^k) = -F(x^k)$ with $V_k \in \partial F(x^k)$; all choices of $V_k$ are quantified, and $\delta$ is chosen before the run.
• Pinned asymptotics. The goal's rate is the proof's display (3.3), stated as IsLittleO along atTop; the printed Theorem 3.2 states only well-definedness and convergence. "Order $1+p$" is pinned as $\|x^{k+1}-x^*\| \le C\|x^k-x^*\|^{1+p}$ with $\delta$ and $C$ uniform over runs. Every $o(\|h\|)$ in (2.8), (2.9) and (2.17) is its $\varepsilon$–$\delta$ form with a non-strict inequality $\le \varepsilon\|h\|$, and every $O(\|h\|^{1+p})$ is an explicit constant and radius.
• The standing assumptions "$F$ locally Lipschitzian" of Sections 2 and 3 are hypotheses of every statement.
• The strong Fréchet derivative of Corollary 2.5 is Mathlib's HasStrictFDerivAt, which corrects the misprint $F(x)$ for $F(z)$ in the paper's display (2.16).

A trivializing formalization is ruled out: the update is not written with a junk inverse (which would make a singular step "well defined"), the generalized Jacobian is the paper's nonempty set rather than one that could be empty, and the theorem quantifies over every run rather than asserting that some run converges.

A complete development needs Clarke's mean-value inclusion (2.2), compactness and upper semicontinuity of $\partial F$ for locally Lipschitz maps (via Rademacher's theorem, available in Mathlib), and perturbation bounds for inverses of linear maps. The generalized-Jacobian and semismoothness layer is reusable beyond this mission, in particular for Missions II and III of this series. Contributions of proofs of any milestone, and of general lemmas about $\partial F$, are welcome.

Selected references

• L. Qi, J. Sun, A nonsmooth version of Newton's method, Mathematical Programming 58 (1993) 353–367. https://doi.org/10.1007/BF01581275
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983 (SIAM reprint 1990). https://doi.org/10.1137/1.9781611971309
• R. Mifflin, Semismooth and semiconvex functions in constrained optimization, SIAM Journal on Control and Optimization 15 (1977) 959–972. https://doi.org/10.1137/0315061
• J.-S. Pang, Newton's method for B-differentiable equations, Mathematics of Operations Research 15 (1990) 311–341. https://doi.org/10.1287/moor.15.2.311
• J. M. Ortega, W. C. Rheinboldt, Iterative Solution of Nonlinear Equations in Several Variables, Academic Press, 1970 (SIAM reprint 2000). https://doi.org/10.1137/1.9780898719468

Motivation

Connecting a set of terminals by a network of direct links of least total length is one of the oldest problems of combinatorial optimization. R. C. Prim's 1957 paper in the Bell System Technical Journal (DOI) was motivated by the rate structure for Bell System leased-line services, in which the charge for connecting a set of terminals depends on the length of a shortest network connecting them. The paper states two local construction principles, P1 and P2, and shows that any sequence of their applications produces a shortest network, first for points in the plane and then for arbitrary connected labelled graphs with arbitrary real edge lengths. The paper's §V specialization of the principles, growing a single fragment, is what is now called Prim's algorithm, and its §IV statement is the form of the minimum spanning tree theorem used throughout network design, clustering and approximation algorithms.

Timeline. O. Borůvka (1926) solved the problem for an electrical network in Moravia; V. Jarník (1930) gave the single-fragment procedure; J. B. Kruskal (1956, Proc. AMS 7, 48–50) proved that adding globally shortest links avoiding cycles yields a shortest spanning tree; Prim (1957) gave the more permissive principles P1 and P2, which contain both the Jarník procedure and Kruskal's rule as special orders of application; E. W. Dijkstra (1959) rediscovered the single-fragment procedure.

Setting

Let $V$ be a finite set of $N$ terminals and $G$ a simple graph on $V$, the labelled graph whose edges are the possible links. Each edge $e$ carries a real length $w(e)$; lengths may be negative, zero, or tie. For a finite set $F$ of links, $H(F)$ denotes the graph on $V$ whose edges are the links of $F$.

• A spanning subtree of $G$ is a set $F$ of edges of $G$ such that $H(F)$ is a tree on $V$. Its length is $\ell_w(F) = \sum_{e \in F} w(e)$.
• A shortest spanning subtree (SSS) is a spanning subtree of least length among all spanning subtrees of $G$. Prim's dictionary is "shortest connection network (SCN) ↔ shortest spanning subtree (SSS)". $L(G,w)$ denotes that least length.
• Given the links $F$ made so far, the connected components of $H(F)$ are the isolated terminals (one terminal) and isolated fragments (two or more terminals).
• Principle 1: any isolated terminal $t$ can be connected to a nearest neighbor, a $G$-neighbor $n$ with $w(\{t,n\}) \le w(\{t,m\})$ for all $G$-neighbors $m$ of $t$.
• Principle 2: any isolated fragment $C$ can be connected to a nearest neighbor $n \notin C$ by a shortest available link $\{u,n\}$, $u \in C$; equivalently $\{u,n\}$ is a shortest edge of $G$ with one end in $C$ and the other outside.
• A construction is a sequence of links $e_0, e_1, \dots$, each an application of P1 or P2 with respect to the links before it. It is complete when it has $N-1$ links.

Only edges of $G$ are possible links; in Prim's distance table a missing edge has length $\infty$.

Formalization targets

Goal (§IV, p. 1396)

For every finite connected graph $G$ and every $w$,

$$\Bigl(\exists\ \text{a complete construction}\Bigr) \ \wedge\ \Bigl(\forall\ \text{complete constructions } e_0,\dots,e_{N-2}:\ \{e_0,\dots,e_{N-2}\} \text{ is a SSS of } G\Bigr).$$

This is the sentence "P1 and P2 will provide a SSS for any connected labelled graph with any set of real edge lengths." It fixes nothing about the order of applications, the component chosen, or the tie-breaking.

Milestones

1. Counting (§II, p. 1392): after any construction with $k$ links, $H(F)$ is acyclic with $N-k$ components; a complete construction is a spanning subtree; a construction with fewer than $N-1$ links can be extended.
2. Necessary Condition 1 (p. 1392): every terminal of a SSS is linked in it to at least one nearest neighbor.
3. Necessary Condition 2 (p. 1392): every fragment $S$ of a SSS, $\emptyset \ne S \ne V$, is linked in it to a nearest neighbor by a shortest available link.
4. Distinct lengths (§III, p. 1393): if the edge lengths are pairwise distinct, every link of every construction belongs to every SSS.
5. Continuity (§III, p. 1394): $w \mapsto L(G,w)$ is continuous.

Significance

The goal is the correctness theorem of a whole family of greedy minimum spanning tree procedures at once: Jarník–Prim (one growing fragment), Kruskal (globally shortest link first) and Borůvka-style interleavings all produce sequences of P1/P2 applications. Because lengths are arbitrary reals, it also covers maximum spanning trees by a sign change (p. 1397) and graphs that are not complete.

The result is classical and fully proved in the literature. What this mission adds is a machine-checked statement in exactly Prim's generality. Mathlib has spanning trees of connected graphs (SimpleGraph.Connected.exists_isTree_le) and the edge count of trees, but no minimum spanning tree theory. Existing Prove2Me items on minimum spanning trees are either restricted to complete graphs with distance matrices or state a cut property in existence form at a single vertex; none states Prim's principles or his necessary conditions.

Difficulty

The obvious argument, "each link P1 or P2 adds belongs to the shortest network", uses a unique shortest network, and that fails with ties: when two links tie, a P1/P2 link need not lie in a given SSS. Prim's own treatment of ties (§III) is an informal perturbation argument; the formal statement must hold for every tie-breaking choice made during a construction, not only for a generic perturbed instance. Negative lengths remove the easy reading "shortest connected spanning subgraph": the minimum must range over trees only. The statements also involve the component structure of $H(F)$ as it changes during a construction, and tree paths in an arbitrary, not necessarily complete, graph.

Formalization scope

Namespace ShortestConnection.Principles, Mathlib SimpleGraph. Conventions:

• $V$ is a Fintype with decidable equality; $G$ is a SimpleGraph V (at most one link per pair, no loops, which is Prim's setting). Lengths are w : Sym2 V → ℝ; only values on edges of $G$ matter.
• Link sets are Finset (Sym2 V); linkGraph F is SimpleGraph.fromEdgeSet F. A spanning subtree requires ↑F ⊆ G.edgeSet and (linkGraph F).IsTree.
• An isolated fragment is a whole connected component of linkGraph F; the P2 condition is a single inequality against every $G$-edge leaving it, which is equivalent to "nearest neighbor and shortest link" in Prim's sense.
• A construction is a List (Sym2 V) checked entrywise against l.take i; complete means length Fintype.card V - 1 (natural subtraction, used only for nonempty $V$).
• $L$ is sInf of the lengths of spanning subtrees; continuity is in the product topology.

Implicit hypotheses made explicit: $G$ connected (hence $V \ne \emptyset$) wherever an SSS or a complete construction is involved; at least two terminals for Necessary Condition 1; $S$ nonempty and $S \ne V$ for Necessary Condition 2; pairwise distinct edge lengths only in milestone 4, as in the paper's temporary assumption.

The goal's existence clause rules out a vacuous formalization in which no complete construction exists; the step predicates are defined from lengths and components only, never through shortest spanning subtrees, and they are not restricted to one growing fragment or to the globally shortest link.

Needed infrastructure: tree exchange (adding an edge to a spanning tree creates one cycle; removing any other cycle edge yields a spanning tree), component counts under edge addition, and minima of finitely many continuous functions. The exchange and counting lemmas are reusable for any matroid-greedy or spanning-tree mission. Contributions of intermediate lemmas, and proofs of the milestones in any order, are welcome.

Selected references

• R. C. Prim, Shortest Connection Networks And Some Generalizations, Bell System Technical Journal 36 (1957), 1389–1401. https://doi.org/10.1002/j.1538-7305.1957.tb01515.x
• J. B. Kruskal, On the shortest spanning subtree of a graph and the traveling salesman problem, Proceedings of the AMS 7 (1956), 48–50. https://doi.org/10.1090/S0002-9939-1956-0078686-7
• V. Jarník, O jistém problému minimálním, Práce Moravské Přírodovědecké Společnosti 6 (1930), 57–63.
• O. Borůvka, O jistém problému minimálním, Práce Moravské Přírodovědecké Společnosti 3 (1926), 37–58.
• R. L. Graham, P. Hell, On the history of the minimum spanning tree problem, Annals of the History of Computing 7 (1985), 43–57. https://doi.org/10.1109/MAHC.1985.10011

Motivation

Quasi-Newton methods minimize a smooth function $f$ on $\mathbb{R}^n$ by moving along $d_k = -H_k g_k$, where $g_k$ is the gradient and $H_k$ is an approximation of the inverse Hessian built from observed gradient differences. The BFGS update is the most widely used way of building $H_k$, but it stores a dense $n \times n$ matrix, which is prohibitive for large $n$.

Nocedal's 1980 paper (Math. Comp. 35, 773–782) proposed keeping only the last $m$ correction pairs and rebuilding the matrix from a simple initial matrix $H_0$ at every step. The resulting method, called SQN in the paper, is now known as L-BFGS, and it is the default large-scale unconstrained optimizer in many numerical libraries and in machine learning. The paper's main theoretical claim is that this truncation does not destroy the finite termination of BFGS on quadratics.

Timeline:

• 1970: Broyden, Fletcher, Goldfarb and Shanno introduce the BFGS update (references [1] and [5] of the paper).
• 1977: Nazareth relates BFGS to conjugate gradients (Argonne Tech. Memo 282, reference [7]); his form of preconditioned conjugate gradients is the one the paper uses.
• 1977–1978: Shanno studies the memoryless BFGS update, the case $m = 1$ (reference [11]; journal version Math. Oper. Res. 3, 1978).
• 1980: Nocedal defines the special BFGS matrices and the SQN method and states that on quadratics with exact line searches SQN is identical to preconditioned conjugate gradients, hence has quadratic termination.
• 1989: Liu and Nocedal (Math. Programming 45) study the method, now called L-BFGS, for large-scale problems.
• 1998: Kolda, O'Leary and Nazareth (SIAM J. Optim. 8) treat limited-memory and update-skipping BFGS variants with exact line searches on quadratics.

Setting

Let $A$ be a symmetric positive definite $n \times n$ matrix and $b \in \mathbb{R}^n$, and let $f(x) = \tfrac12 x^T A x + b^T x$, a strictly convex quadratic with gradient $g(x) = Ax + b$ and unique minimizer $x^\ast = -A^{-1} b$.

Exact line search. Along a direction $d \neq 0$ from $x$, the step $\alpha = -g(x)^T d / d^T A d$ minimizes $f(x + \alpha d)$.

BFGS update. For a pair $(s, y)$ with $\rho = 1/y^T s$ and $v = I - \rho y s^T$, the BFGS update of $H$ is

$$\bar H = v^T H v + \rho s s^T .$$

Special BFGS matrices. Fix $H_0$ symmetric positive definite and a number $m \ge 1$ of stored corrections. Given pairs $(s_j, y_j)$, the special matrix $H_K$ is $H_0$ updated by the pairs $j = K - \min(K, m), \dots, K-1$, oldest first (the paper's (4)–(5)). Only the $m$ most recent pairs enter, and the matrix is rebuilt from $H_0$.

SQN. Starting from $x_0$, with $g_i = g(x_i)$:

$$d_i = -H_i g_i, \qquad x_{i+1} = x_i + \alpha_i d_i, \qquad s_i = x_{i+1} - x_i,\quad y_i = g_{i+1} - g_i,$$

with $\alpha_i$ the exact step and $H_{i+1}$ the special matrix built from the last $\min(i+1, m)$ pairs.

PCG with fixed preconditioner $H_0$. $d_0 = -H_0 g_0$, $x_{i+1} = x_i + \alpha_i d_i$, $d_{i+1} = -H_0 g_{i+1} + \beta_{i+1} d_i$ with $\beta_{i+1} = y_i^T H_0 g_{i+1} / y_i^T d_i$.

Formalization targets

Goal: quadratic termination of SQN

For every $n$, every symmetric positive definite $A$ and $H_0$, every $b$, $x_0$ and every $m \ge 1$,

$$\exists\, k \le n : \quad A x_k + b = 0 ,$$

where $x_k$ are the SQN iterates. The statement fixes no constant beyond the dimension bound $n$.

Milestones

1. Property (a): the special matrices are positive definite whenever $y_i^T s_i > 0$ for all $i$.
2. Eq. (7): along conjugate steps, $v_i y_i = 0$ and $v_i y_j = y_j$ for $i > j$.
3. Eq. (6): along conjugate steps, $H_k y_j = s_j$ for the $m$ most recent $j$ (when $k > m$).
4. Eq. (10): the special matrix equals $m$ sum-form BFGS corrections applied to $H_0$.
5. Eq. (15): the PCG directions satisfy $d_i^T y_j = 0$ for $i \neq j$.
6. Eq. (16): $g_i^T H_0 g_j = 0$ for $i \neq j$ and $g_i^T d_j = 0$ for $j < i$.
7. The PCG with fixed preconditioner $H_0$ reaches the minimizer in at most $n$ steps.
8. SQN and this PCG produce identical iterates and directions at every step.

Significance

The result shows that storing only $m$ correction pairs costs nothing on quadratics: for any $m \ge 1$, SQN terminates in at most $n$ steps, like full BFGS and conjugate gradients. It explains why L-BFGS with small $m$ is competitive, and it is the model case for later analyses of limited-memory methods (their linear convergence on uniformly convex functions, and their relation to Krylov methods). Property (b) is the reason one expects efficiency to grow with $m$: the matrix satisfies the secant equation on the $m$ most recent directions.

The claims are classical and generally accepted, but the paper argues them in a few lines ("it is straightforward to show"), deferring the PCG facts (15)–(16) to a reference. No machine-checked proof of the termination of BFGS, L-BFGS or preconditioned conjugate gradients is known to this mission. A formalization would provide a verified model of L-BFGS on quadratics and a reusable development of conjugate-direction methods with a preconditioner.

Difficulty

The obvious route, "SQN is BFGS and BFGS terminates", fails: SQN discards old corrections, so the classical BFGS argument (hereditary secant conditions on all past directions) does not apply once more than $m$ steps have been taken. The paper asserts the identity of SQN with preconditioned conjugate gradients in one sentence ("using a similar argument as for the SCG"), and the PCG relations it relies on are quoted from a technical report. The other difficulty is bookkeeping: the window of stored pairs shifts, the matrix is a nested product, and the runs must remain meaningful after the minimizer is reached.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, $x^T y$ is dotProduct, and $s y^T$ is Matrix.vecMulVec. Symmetric positive definiteness is Matrix.PosDef. Indices are 0-based, as in the paper. The exact line search is the closed-form step $-g^T d / d^T A d$. The iterations have no stopping rule: once the gradient vanishes the direction and step are zero and the iterate stays at the minimizer (Lean's $0/0 = 0$). Past that point the zero pair stored by SQN leaves the BFGS step unchanged. The hypotheses are exactly the paper's: $A \succ 0$, $H_0 \succ 0$, $m \ge 1$ and exact line searches. $H_0$ need not be diagonal.

Two misprints are corrected and flagged in the items: the denominator of $\beta$ in (13) is $y_{i-1}^T d_{i-1}$ (as in (12) and p. 778), and the second relation of (16) is stated for $j < i$ (as used on p. 778), since it fails for $i < j$.

Ruled out: SQN is defined through its own matrices (4)–(5), rebuilt from $H_0$ and the last $m$ pairs. It is not defined through the PCG recurrence, not by one BFGS update of the previous matrix, and not with a stop rule that returns $-A^{-1}b$. The standing assumption $y_k^T s_k > 0$ is not a hypothesis of any statement about a run (it fails after termination and would make the goal vacuous). With $m = 0$ SQN is steepest descent and the goal is false, so $m \ge 1$ is required.

Needed infrastructure: algebra of rank-one updates and of Matrix.PosDef under congruence, conjugate-direction lemmas for quadratics, and the fact that $n+1$ mutually $H_0$-orthogonal vectors in $\mathbb{R}^n$ include a zero vector. The PCG results (milestones 5–7) are reusable beyond this mission. Proofs of any milestone, or of the goal directly, are welcome.

Selected references

• J. Nocedal, Updating Quasi-Newton Matrices with Limited Storage, Mathematics of Computation 35(151), 1980, 773–782. https://doi.org/10.1090/s0025-5718-1980-0572855-7
• D. F. Shanno, Conjugate gradient methods with inexact searches, Mathematics of Operations Research 3(3), 1978, 244–256. https://doi.org/10.1287/moor.3.3.244
• L. Nazareth, A Relationship Between the BFGS and Conjugate Gradient Algorithms, ANL-AMD Tech. Memo 282 (rev.), Argonne National Laboratory, 1977 (reference [7] of Nocedal 1980; no online copy located).
• T. G. Kolda, D. P. O'Leary, L. Nazareth, BFGS with update skipping and varying memory, SIAM Journal on Optimization 8(4), 1998, 1060–1083. https://doi.org/10.1137/S1052623496306450
• D. C. Liu, J. Nocedal, On the limited memory BFGS method for large scale optimization, Mathematical Programming 45, 1989, 503–528. https://doi.org/10.1007/BF01589116

Motivation

Newton's method is the standard second-order algorithm for unconstrained minimization, but without safeguards it has no global guarantee: far from a minimizer the Newton step can increase the objective, and at a point where the Hessian is indefinite the step can head for a saddle point or a maximum. The usual repairs (line search, trust regions, Levenberg–Marquardt damping) come with convergence proofs, but for nonconvex objectives those proofs typically give no rate at all, or only the rate of the gradient method.

Nesterov and Polyak (Math. Program. 108 (2006) 177–205) proposed to regularize the second-order Taylor model of the objective with a cubic term and to take as the next iterate a global minimizer of the regularized model. They showed that the resulting method has a global worst-case rate of convergence to points satisfying the second-order necessary conditions, for every objective with a Lipschitz continuous Hessian and without any convexity. That rate, $O(k^{-2/3})$ for the gradient norm, is better than the $O(k^{-1/2})$ of the gradient method. It became the reference point for the complexity theory of nonconvex second-order optimization: adaptive variants (Cartis, Gould and Toint, Math. Program. 127 (2011) 245–295) and lower bounds showing that $O(\epsilon^{-3/2})$ iterations are optimal among second-order methods (Carmon, Duchi, Hinder and Sidford, Math. Program. 184 (2020) 71–120) are stated against it.

This mission formalizes the general convergence result of that paper, Theorem 1 of Section 3, together with the properties of the cubic step from Section 2 on which it rests.

Setting

Let $F \subseteq \mathbb{R}^n$ be a closed convex set with nonempty interior, and let $f$ be twice differentiable on $F$ with gradient $f'(x)$ and Hessian $f''(x)$. A starting point $x_0 \in \operatorname{int} F$ is fixed, and $F$ is assumed to contain the level set $\mathcal{L}(f(x_0)) = \{x \in \mathbb{R}^n : f(x) \le f(x_0)\}$ in its interior. Assumption 1: the Hessian is Lipschitz continuous on $F$ in the spectral norm, $\|f''(x) - f''(y)\| \le L\|x - y\|$ for all $x, y \in F$, with $L > 0$.

For a parameter $M > 0$ the cubic model of $f$ at $x$ is

$$m_{M,x}(y) = \langle f'(x), y - x\rangle + \tfrac12 \langle f''(x)(y - x), y - x\rangle + \tfrac{M}{6}\|y - x\|^3 .$$

The cubic-regularized Newton step $T_M(x)$ is any global minimizer of $m_{M,x}$ over $\mathbb{R}^n$; it exists because the model is continuous and coercive. Write $r_M(x) = \|x - T_M(x)\|$ and $\bar f_M(x) = f(x) + \min_y m_{M,x}(y)$.

The cubic regularization of Newton method (3.3) fixes $L_0 \in (0, L]$, starts at $x_0$ and, for $k \ge 0$, chooses $M_k \in [L_0, 2L]$ such that $f(T_{M_k}(x_k)) \le \bar f_{M_k}(x_k)$, then sets $x_{k+1} = T_{M_k}(x_k)$. The choice $M_k = L$ always passes the test.

Write $\lambda_n(A)$ for the smallest eigenvalue of a symmetric matrix $A$. The measure of local optimality is

$$\mu_M(x) = \max\Big\{ \sqrt{\tfrac{2}{L + M}\,\|f'(x)\|},\ -\tfrac{2}{2L + M}\,\lambda_n(f''(x)) \Big\}.$$

It is nonnegative and vanishes exactly when $f'(x) = 0$ and $f''(x) \succeq 0$.

Formalization targets

Goal: Theorem 1, inequality (3.4)

If $f(x) \ge f^*$ for all $x \in F$, then every run of method (3.3) satisfies, for every $k \ge 1$,

$$\min_{1 \le i \le k} \mu_L(x_i) \le \frac{8}{3}\cdot\left(\frac{3\,(f(x_0) - f^*)}{2k\cdot L_0}\right)^{1/3}.$$

The constant $8/3$ and the exponent $1/3$ are the paper's; the statement holds for every admissible choice of the parameters $M_k$ and of the global minimizers $x_{k+1}$.

Milestones, in attack order

1. Lemma 1 (2.2): $\|f'(y) - f'(x) - f''(x)(y - x)\| \le \tfrac12 L\|y - x\|^2$ on $F$.
2. Eq. (2.5): $f'(x) + f''(x)(T - x) + \tfrac12 M\|T - x\|(T - x) = 0$ for $T = T_M(x)$.
3. Proposition 1 (2.7): $f''(x) + \tfrac12 M r_M(x) I \succeq 0$.
4. Lemma 2 (2.8): $\langle f'(x), x - T_M(x)\rangle \ge 0$ when $f(x) \le f(x_0)$.
5. Lemma 4 (2.11): $f(x) - \bar f_M(x) \ge \tfrac{M}{12} r_M(x)^3$.
6. Lemma 4 (2.12): for $M \ge L$, $T_M(x) \in F$ and $f(T_M(x)) \le \bar f_M(x)$.
7. Lemma 3 (2.9): $\|f'(T_M(x))\| \le \tfrac12(L + M) r_M(x)^2$ when $T_M(x) \in F$.
8. Lemma 5: $\mu_M(T_M(x)) \le r_M(x)$.
9. Theorem 1, first claim: $\sum_{i \ge 0} r_{M_i}(x_i)^3 \le \tfrac{12}{L_0}(f(x_0) - f^*)$.
10. Theorem 1, second claim: $\lim_{i\to\infty} \mu_L(x_i) = 0$.

Significance

Inequality (3.4) is a global, dimension-free complexity bound for reaching approximate second-order stationarity. It controls both the gradient norm, $\min_{1\le i\le k}\|f'(x_i)\| = O(k^{-2/3})$, and the most negative curvature, $\max\{0, -\lambda_n(f''(x_i))\} = O(k^{-1/3})$, along the best iterate, from a single scalar potential $f(x_0) - f^*$. The second claim of Theorem 1 gives the asymptotic counterpart: every limit point satisfies the second-order necessary conditions. Section 4 of the paper derives its faster rates for star-convex and gradient-dominated functions from the same Section 2 lemmas.

The result is proved on paper and widely cited; to our knowledge no machine-checked proof of it or of the Section 2 lemmas exists. A formalization adds a checked statement of the method with its exact constants, and reusable facts about global minimizers of cubic models (Proposition 1 in particular) that the companion missions on star-convex, gradient-dominated and locally quadratic convergence also rely on.

Difficulty

Most steps are short inequalities, but two are not. Proposition 1 is a statement about a global minimizer of a nonconvex function: the first- and second-order conditions of a local minimizer give only $f''(x) + \tfrac12 M r I + \tfrac{M}{2r}(T - x)(T - x)^\top \succeq 0$, which is weaker. The natural first attempt, "take the second-order optimality condition of the model at $T$", therefore fails. The paper proves it in Section 5.1 through a one-dimensional dual characterization of the minimizer.

The second is Lemma 2's second claim, used for (2.12): showing that $T_M(x)$ stays in $F$ requires a boundary argument along the segment from $x$ to $T_M(x)$, since the Taylor bounds are only available inside $F$. The remaining work is calculus in $\mathbb{R}^n$: the integral form of Taylor's theorem for the gradient under a Lipschitz Hessian, and eigenvalue perturbation for the second entry of $\mu$.

Formalization scope

The space is EuclideanSpace ℝ (Fin n) for arbitrary n : ℕ. The gradient and Hessian are maps g and H with HasGradientAt f (g x) x and HasFDerivAt g (H x) x at every x ∈ F. At boundary points of $F$ this asks for two-sided derivatives, a mild strengthening of "twice differentiable on $F$". The Lipschitz condition uses the operator norm, which is the spectral norm. $T_M(x)$ is represented by the predicate IsCubicStep (global minimizer of cubicModel), and every lemma is stated for every such minimizer. The run predicate IsCubicNewtonRun is 0-based. It writes $\bar f_{M_k}(x_k)$ as $f(x_k)$ plus the model value at $x_{k+1}$, which is the minimum because $x_{k+1}$ attains it. $\lambda_n$ is lamMin, the Rayleigh-quotient infimum over the unit sphere, which equals the smallest eigenvalue for the (symmetric) Hessian. The lower bound $f^*$ is required on $F$ only. The minimum over $1 \le i \le k$ is written as the existence of an index attaining the bound.

A stationary point of the cubic model is not an admissible step, and the run must keep the test $M_k \in [L_0, 2L]$ and the acceptance test. Replacing the step by any point with $f(x_{k+1}) \le f(x_k)$ makes the goal false, and dropping the square root in $\mu_M$ makes Lemma 5 false. The statements rule out all three. Lemma 5 carries the hypothesis $T_M(x) \in F$, which its printed proof uses and which holds at every iterate.

A complete development needs the Taylor bounds (2.2)–(2.3) for vector-valued derivatives on convex sets, and first- and second-order optimality for the cubic model. It also needs a proof of Proposition 1 (Section 5.1 or any other correct argument) and eigenvalue perturbation via Rayleigh quotients. The cubic-model lemmas and Proposition 1 are reusable across the whole series. Proofs of any milestone, alternative proofs of Proposition 1, and general Mathlib-level lemmas about Rayleigh quotients are welcome.

Selected references

• Yu. Nesterov and B. T. Polyak, Cubic regularization of Newton method and its global performance, Mathematical Programming, Ser. A 108 (2006) 177–205. https://doi.org/10.1007/s10107-006-0706-8
• C. Cartis, N. I. M. Gould and Ph. L. Toint, Adaptive cubic regularisation methods for unconstrained optimization. Part I: motivation, convergence and numerical results, Mathematical Programming 127 (2011) 245–295. https://doi.org/10.1007/s10107-009-0286-5
• Y. Carmon, J. C. Duchi, O. Hinder and A. Sidford, Lower bounds for finding stationary points I, Mathematical Programming 184 (2020) 71–120. https://doi.org/10.1007/s10107-019-01406-y
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9