The OR Formalization Drive

Motivation

A firm that will receive or deliver a quantity of a commodity, currency or security at a future date carries price risk until that date. When the asset itself cannot be traded in the meantime, the standard instrument for reducing that risk is a futures contract on a correlated asset: the firm takes a position in futures and adjusts it over time, and the gains or losses of the futures position offset part of the movement of its commitment. Choosing that position is the hedging problem. The classical answer, the minimum-variance hedge ratio, is a static one-period rule. Duffie and Richardson (Ann. Appl. Probab. 1991) solved the dynamic version in continuous time with a quadratic criterion: minimize the expected squared deviation of terminal wealth from a target. Their explicit feedback solution became a reference point for the later literature on mean-variance hedging in incomplete markets (Schweizer, Gouriéroux–Laurent–Pham, and others), where the same quadratic criterion is studied under general semimartingale prices.

Setting

Fix a horizon $T>0$ and a probability space $(\Omega,\mathcal F,P)$ carrying a two-dimensional standard Brownian motion $(B,\varepsilon)$ with its filtration $\mathbb F$. Let $\mu,\sigma,m,v,\rho$ be bounded measurable functions on $[0,T]$, with $|v|$ bounded away from zero and $\rho_t\in[-1,1]$. The Brownian motion $\xi_t=\int_0^t\rho_s\,dB_s+\int_0^t\sqrt{1-\rho_s^2}\,d\varepsilon_s$ has instantaneous correlation $\rho$ with $B$. The committed asset $S$ and the futures price $F$ follow

$$dS_t=\mu_tS_t\,dt+\sigma_tS_t\,dB_t,\qquad dF_t=m_tF_t\,dt+v_tF_t\,d\xi_t,\qquad S_0,F_0>0.$$

The hedger is committed to $k$ units of $S$ at time $T$. A trading strategy is a progressively measurable process $\theta$ (the futures position) with $E\int_0^T\theta_t^2F_t^2\,dt<\infty$; $\Theta$ denotes the set of them. Its futures gain is the stochastic integral $G(\theta)_t=\int_0^t\theta_s\,dF_s$, and the terminal wealth is $W(\theta)=kS_T+G(\theta)_T$. Given a target level $L\in\mathbb R$, problem (3) is

$$\min_{\theta\in\Theta}E\big[(W(\theta)-L)^2\big].$$

With $\gamma_t=m_t\sigma_t\rho_t/v_t-\mu_t$, the tracking process is $Z_t=k\exp(-\int_t^T\gamma_s\,ds)S_t$, so that $Z_T=kS_T$, and the feedback map is

$$\Phi(G^*_t)=\frac1{F_t}\Big[\frac{m_t}{v_t^2}(L-Z_t-G^*_t)-\frac{\sigma_t\rho_t}{v_t}Z_t\Big],$$

where $G^*$ solves $dG^*_t=\Phi(G^*_t)\,dF_t$, $G^*_0=0$. The strategy $\varphi=\Phi(G^*)$ depends only on the gains realized so far and the current price $S_t$.

Formalization targets

Goal: Proposition 1

$$\varphi_t=\Phi(G^*_t)\ \text{ solves }\ \min_{\theta\in\Theta}E\big[(kS_T+G(\theta)_T-L)^2\big]$$

for every commitment $k$, every target $L$ and every solution $G^*$ of (10). No constant is hard-coded: the statement is the paper's for arbitrary coefficients satisfying the standing hypotheses.

Milestones

1. Lemma 1: $\varphi\in\Theta$ is optimal iff $E[(L-kS_T-G(\varphi)_T)\,G(\theta)_T]=0$ for every $\theta\in\Theta$.
2. Existence (§3.3): equation (10) has a solution with $G^*_t\in L^2(P)$.
3. Itô dynamics of $Z$: $dZ_t=(\gamma_t+\mu_t)Z_t\,dt+\sigma_tZ_t\,dB_t$.
4. Moment equations for $E(Z_tG_t)$, $E(G^*_tG_t)$ and $E(G_t)$, with $G=G(\theta)$.
5. Lemma 2: $H_t=E[(L-Z_t-G^*_t)G(\theta)_t]$ satisfies $\dot H_t=-(m_t^2/v_t^2)H_t$.
6. The solution of (13): $H_t=H_0\exp(-\int_0^tm_s^2/v_s^2\,ds)$.

Two further items, not milestones, formalize §4: Lemma 3 (a solution of (3) is mean-variance efficient) and §4.1 (maximizing the quadratic utility $E[W-cW^2]$, $c>0$, is problem (3) with $L=1/(2c)$).

Significance

Proposition 1 gives the optimal dynamic hedge in closed feedback form for every target level at once. Varying $L$ traces out the whole mean-variance frontier of terminal wealth (Lemma 3), and the choice $L=1/(2c)$ solves the quadratic-utility problem (§4.1); the minimum-variance hedge of §4.3 of the paper is obtained by optimizing over $L$. The result is also an instance of a general pattern: a quadratic hedging problem in an incomplete market reduces to an $L^2$ projection onto the space of attainable gains, and the projection is computed by a linear SDE.

The result is proved in the paper, in six pages. No machine-checked version of it, or of any continuous-time hedging result, exists on the platform. A formalization requires Itô's formula for products of Itô processes, the zero-mean property of square-integrable stochastic integrals, Fubini's theorem for moments, and existence for a linear SDE with an Itô-process forcing term; each of these is reusable well beyond this paper.

Difficulty

The projection step (Lemma 1) is Hilbert-space geometry and the final ODE step is Grönwall. The difficulty lies in between: the orthogonality $E[(L-kS_T-G^*_T)G(\theta)_T]=0$ must be verified against every trading strategy $\theta$, about which only $E\int_0^T\theta_t^2F_t^2\,dt<\infty$ is known. A computation that treats $\theta$ as bounded, continuous or simple does not suffice. Making the paper's moment computations rigorous requires controlling the integrability of products such as $Z_t\theta_tF_t$ and $G^*_tG(\theta)_t$, proving that the stochastic-integral parts of Itô's product rule are true martingales rather than local martingales, and differentiating expectations in time when the coefficients are only measurable, so that derivatives exist only almost everywhere.

Formalization scope

The stochastic layer is the published definition file Peng1990_SMP_Stochastic (the $L^2$ Itô integral and Itô processes on $\mathbb R_{\ge0}$ time), imported, not redefined. The mission commits to the following conventions.

• $(B,\varepsilon)$ is one $\mathbb R^2$-valued standard Brownian motion; $B$ is coordinate 0, $\varepsilon$ coordinate 1, and $d\xi$ is expanded as $\rho\,dB+\sqrt{1-\rho^2}\,d\varepsilon$.
• The filtration is the natural filtration of $(B,\varepsilon)$, not its augmentation, and trading strategies are progressively measurable instead of predictable. Neither change alters the space of terminal gains.
• Gains are relations: a gain process is any version of the Itô integral, and every statement quantifies over all versions.
• The objective $E[(W-L)^2]$ and variances take values in $[0,\infty]$, so a non-square-integrable wealth cannot be optimal through a junk value $0$; inner products carry explicit integrability.
• $\rho_t\in[-1,1]$ (§3.1), not $[0,1]$ (§2). The sign of $v$ is free; only $|v|\ge\delta>0$ is assumed.
• "$\Phi(G^*)$ defined by (9)–(11)" means: for every solution of (10), where a solution includes that $\Phi(G^*)$ is a trading strategy. The paper takes this membership for granted.
• Lemma 2 and the moment equations are stated in integral form ($H_t=H_0-\int_0^t(m^2/v^2)H\,ds$), which is the paper's "for almost every $t$" derivative together with absolute continuity; continuity of the coefficients is not assumed.
• The display for $dZ$ in the proof of Lemma 2 omits $dt$; the drift is $(\gamma_t+\mu_t)Z_t\,dt$.
• In §4.1, $c>0$ is assumed explicitly.

Proposition 1 would hold vacuously if equation (10) had no solution; the existence milestone rules this out and must be proved, not assumed. Contributions are welcome on Itô's product formula and the martingale property of Itô integrals in the Peng framework, on the existence of solutions of linear SDEs, and on the Grönwall-type uniqueness for (13).

Selected references

• D. Duffie, H. R. Richardson, Mean-Variance Hedging in Continuous Time, The Annals of Applied Probability 1(1) (1991) 1–15. https://doi.org/10.1214/aoap/1177005978
• S. Peng, A General Stochastic Maximum Principle for Optimal Control Problems, SIAM J. Control Optim. 28(4) (1990) 966–979. https://doi.org/10.1137/0328054
• P. Protter, Stochastic Integration and Differential Equations, Springer, 1990. https://doi.org/10.1007/978-3-662-02619-9
• D. G. Luenberger, Optimization by Vector Space Methods, Wiley, 1969.
• M. Schweizer, Mean-Variance Hedging for General Claims, The Annals of Applied Probability 2(1) (1992) 171–179. https://doi.org/10.1214/aoap/1177005776

Motivation

Reflected Brownian motion on the orthant is the diffusion that arises as the heavy-traffic limit of open networks of queues. In a $K$-station network the scaled queue-length vector lives in the nonnegative orthant $\mathbb R^K_+$; in the interior it moves like a Brownian motion, and when a station empties the process is pushed back into the orthant in a direction determined by the routing of customers between stations. Harrison (1978) obtained such a limit for two queues in tandem, and Reiman (Open Queueing Networks in Heavy Traffic, Math. Oper. Res. 9 (1984)) showed that general $K$-station open networks lead exactly to the class of processes studied here.

Classical constructions of reflected diffusions (Stroock and Varadhan 1971, Watanabe 1971) require a smooth boundary and a reflection direction varying continuously on it. The orthant has corners and the reflection direction jumps between faces, so those results do not apply. Harrison and Reiman (Reflected Brownian Motion on an Orthant, Ann. Probab. 9 (1981)) construct the process pathwise, following Skorokhod's one-dimensional approach, and derive its Markov property from the construction. The process has since become the standard object in the diffusion approximation of queueing networks.

Setting

Fix a positive integer $K$. Vectors in $\mathbb R^K$ are row vectors, indexed by $j=1,\dots,K$. Let $A$ be a $K\times K$ covariance matrix (symmetric, nonnegative definite), $b\in\mathbb R^K$ a drift vector, and $Q=(q_{ij})$ a nonnegative $K\times K$ matrix with zeros on the diagonal and spectral radius strictly less than one. $S=\mathbb R^K_+$ is the nonnegative orthant.

Let $C$ be the space of continuous paths $x:[0,\infty)\to\mathbb R^K$ with the topology of uniform convergence on compact intervals, and $C_S$ the paths with $x(0)\in S$. For $x\in C_S$, the Skorokhod problem asks for $y,z\in C$ with, for every $j$,

$$z_j(t)=x_j(t)+y_j(t)-\sum_{i=1}^K q_{ij}\,y_i(t),\qquad z_j(t)\ge 0,\qquad t\ge0, \tag{5–6}$$

$y_j$ nondecreasing with $y_j(0)=0$ (7), and $y_j$ increasing only at times $t$ where $z_j(t)=0$ (8). In matrix form, $z=x+y(I-Q)$. Theorem 1 of the paper shows there is exactly one such pair, written $y=\psi(x)$, $z=\phi(x)$.

The process is obtained by feeding a Brownian path into this map. On a probability space $(\Omega,\mathcal F,P)$ let $X$ be a $K$-dimensional Brownian motion with covariance matrix $A$, drift $b$ and $X(0)\in S$ almost surely, with $X(0)$ independent of the increments of $X$. Let $\mathcal F_t=\mathcal F(X(s);0\le s\le t)$. Set $Y=\psi(X)$ and $Z=\phi(X)$ where $X\in C_S$, and $Y=Z=0$ on the exceptional null set. $Z$ is reflected Brownian motion on $S$ with reflection matrix $I-Q$.

Formalization targets

Goal: Corollary 1

There is a family $(\kappa_t)$ of Markov transition kernels on $\mathbb R^K$, depending only on $(Q,A,b)$, such that for every such $X$, $Y$, $Z$:

$$\text{(a)}\quad Y(t),\ Z(t)\ \text{are } \mathcal F_t\text{-measurable},\ t\ge0;$$ $$\text{(b)}\quad (Y,Z)\ \text{satisfies (1)–(4) a.s., and any pair satisfying (1)–(4) a.s. equals } (Y,Z) \text{ a.s.};$$ $$\text{(c)}\quad P\big[Z(s+t)\in B \mid \mathcal F_s\big]=\kappa_t\big(Z(s),B\big)\ \text{a.s.},\qquad s,t\ge0,\ B \text{ Borel}.$$

Here (1)–(4) are (5)–(8) for the paths of $X$, $Y$, $Z$. The kernel is chosen before the probability space and the initial law, which is what "stationary transition probabilities" means.

Milestones

The milestones follow the proof of Theorem 1 on pp. 304–305:

1. a positive diagonal $\Lambda$ with $\|\Lambda^{-1}Q\Lambda\|<1$ (Veinott scaling);
2. (5)–(8) are invariant under $(Q,x,y,z)\mapsto(\Lambda^{-1}Q\Lambda,x\Lambda,y\Lambda,z\Lambda)$;
3. the key observation that (5)–(8) are equivalent to $y\in C_0$, the fixed-point equation $y=\pi(y)$ with $\pi(y)(t)=\sup_{0\le s\le t}[y(s)Q-x(s)]^+$, and $z=x+y(I-Q)$;
4. the contraction $\|\pi(y)-\pi(y')\|\le\alpha\|y-y'\|$ on $[0,T]$;
5. convergence of the Picard iterates $y^{n+1}=\pi(y^n)$, $y^0\equiv0$;
6. the Lipschitz bound $\|\psi(x)-\psi(x')\|\le\|x-x'\|/(1-\alpha)$;
7. Theorem 1 itself: existence and uniqueness, non-anticipation (9), continuity (10);
8. the regeneration property (11): with $x^*(t)=z(T)+x(T+t)-x(T)$, $y^*(t)=y(T+t)-y(T)$, $z^*(t)=z(T+t)$, one has $y^*=\psi(x^*)$, $z^*=\phi(x^*)$.

Milestone 7 is the platform theorem Reiman84.QueueLength.lemma_1, posed as an open target by an earlier mission (Reiman 1984 cites it as its Lemma 1). It is referenced here and not posed again.

Significance

Corollary 1 is what makes $Z$ a usable stochastic process: adaptedness and almost-sure uniqueness say $Z$ is determined by the driving Brownian motion in a non-anticipating way, and the Markov property with time-homogeneous kernels is the starting point for the change-of-variable formula of §3, for generators, for stationary distributions, and for the heavy-traffic limit theorems in which $Z$ appears as the limit. The pathwise map $\phi$ and its Lipschitz continuity are reused throughout queueing theory: the continuous-mapping argument for heavy-traffic limits rests on exactly the continuity (10) established here.

The results are classical, with complete published proofs. None of them has a machine-checked proof. Mathlib has the measure-theoretic layer (kernels, conditional expectation, independence) but no reflection maps, no construction of multidimensional Brownian motion with drift, and no Markov-process theory in continuous time. This mission provides a formal statement of the pathwise reflection theory and its probabilistic consequence on which such a development can build.

Difficulty

The pathwise part is a contraction argument, but the contraction is not in the original norm: the map $y\mapsto yQ$ need not be a contraction for any standard norm when only the spectral radius of $Q$ is below one. The proof first changes coordinates by a positive diagonal matrix, and the right norm must be matched to the row-vector convention. The fixed-point characterization also has to be shown equivalent to the complementarity condition (8), which is where the zero diagonal of $Q$ enters.

For Corollary 1, the difficulty is measure-theoretic. Adaptedness requires measurability of a path functional with respect to the uncompleted natural filtration, which uses (9) and (10) and the fact that continuous paths are determined by countably many coordinates. The Markov property requires the regeneration identity (11) together with independence of the post-$s$ increments of $X$ from $\mathcal F_s$, and a kernel that is jointly measurable and independent of the initial law. Conditioning on $\mathcal F_s$ alone, without identifying the future as a fixed functional of $Z(s)$ and an independent Brownian motion, does not give a kernel that is the same for all $s$.

Formalization scope

• $\mathbb R^K$ is Fin K → ℝ (paper index $j$ = Lean index $j-1$), with $K\ge1$; row vector times matrix is Matrix.vecMul. Paths are functions ℝ → Fin K → ℝ; only times $t\ge0$ are constrained.
• Spectral radius $<1$ is rendered as $Q^m\to0$, the rendering of Reiman84.QueueLength.lemma_1. $A$ is PosSemidef.
• (5)–(8) are the published Reiman84.QueueLength.IsReflectionPair; (8) reads "$y_j$ is constant on every interval $[s,t]\subseteq[0,\infty)$ on which $z_j>0$". $C_S$ is IsCPlus; uniform convergence on compacts is UocTendsto; Brownian motion from $0$ with drift and covariance is IsDriftedBM.
• The norm on $C[0,T]$ is $\sup_{0\le t\le T}\|y(t)\|_\infty$. The suprema in $\pi$ and in the norm are real suprema, honest only for continuous paths, and every statement using them assumes continuity.
• The paper's $\|P\|$ is printed as the maximal row sum. Under the row-vector convention the contraction, Picard and Lipschitz steps need the maximal column sum; with the printed reading the contraction inequality is false (a nilpotent $3\times3$ counterexample is recorded in those items). Veinott scaling is stated as printed; applying it to $Q^\top$ gives the column version.
• The Brownian motion is $X=X_0+\xi$ with $\xi$ a drifted Brownian motion from $0$ and $X_0\ge0$ a.s. independent of the whole process $\xi$. $\mathcal F_t$ is the uncompleted σ-algebra generated by $X(s)$, $0\le s\le t$.
• $Y$ and $Z$ enter Corollary 1 as hypotheses: a solution of (5)–(8) on $\{X\in C_S\}$, zero elsewhere. That such processes exist is the existence part of Theorem 1, the referenced open item.
• The kernel family is quantified before the probability space, so it cannot depend on $s$, on $\Omega$ or on the law of $X(0)$. A version of (c) with a kernel depending on these, with the completed or full σ-algebra in place of $\mathcal F_s$, or with one-dimensional marginals only, is a different and weaker statement and is ruled out.

Out of scope: Theorem 2 (the change-of-variable formula, which needs stochastic integration), the necessity of spectral radius $<1$, and §§3–4. Useful contributions beyond the milestones include a construction of multidimensional Brownian motion with drift in Mathlib, the Skorokhod map as a function on $C_S$, and general lemmas on measurability of continuous path functionals.

Selected references

• J. M. Harrison and M. I. Reiman, Reflected Brownian Motion on an Orthant, Annals of Probability 9(2), 302–308, 1981. https://doi.org/10.1214/aop/1176994471
• M. I. Reiman, Open Queueing Networks in Heavy Traffic, Mathematics of Operations Research 9(3), 441–458, 1984. https://doi.org/10.1287/moor.9.3.441
• A. F. Veinott, Jr., Discrete Dynamic Programming with Sensitive Discount Optimality Criteria, Annals of Mathematical Statistics 40(5), 1635–1660, 1969. https://doi.org/10.1214/aoms/1177697379
• A. V. Skorokhod, Stochastic Equations for Diffusion Processes in a Bounded Region, Theory of Probability and Its Applications 6(3), 264–274, 1961. https://doi.org/10.1137/1106035
• D. W. Stroock and S. R. S. Varadhan, Diffusion Processes with Boundary Conditions, Communications on Pure and Applied Mathematics 24, 147–225, 1971. https://doi.org/10.1002/cpa.3160240206

Motivation

The ellipsoid method decides questions about a convex set $K \subseteq \mathbb{R}^n$ by maintaining an ellipsoid that contains the relevant part of $K$ and shrinking it step by step. Introduced for convex minimization by Yudin and Nemirovskii and by Shor in the 1970s, it became famous in 1979 when Khachiyan used it to show that linear programming is solvable in polynomial time. Grötschel, Lovász and Schrijver (Combinatorica 1 (1981)) observed that the method never needs an explicit description of $K$: it only needs, for a query point $y$, either a confirmation that $y$ is (nearly) in $K$ or a hyperplane (nearly) separating $y$ from $K$. From this they derived that optimization and separation are polynomially equivalent for convex bodies, which in turn gives polynomial algorithms for problems with exponentially many constraints: matroid intersection, submodular function minimization, and the stable set problem in perfect graphs.

The engine of all of these applications is a single quantitative statement, Theorem (2.4) of the paper: with a weak separation oracle and with all numbers rounded to a fixed number of binary digits, a prescribed number $N$ of ellipsoid steps produces an $\varepsilon$-optimal point.

Timeline. 1976–1977: Yudin–Nemirovskii and Shor, the method for convex programming. 1979: Khachiyan, polynomial-time linear programming. 1981: Gács–Lovász publish a complete proof of Khachiyan's result with the explicit rounded update; Grötschel–Lovász–Schrijver state and prove the weak-oracle version, Theorem (2.4), and its combinatorial consequences; Bland–Goldfarb–Todd survey the method (Oper. Res. 29 (1981)). 1988: the monograph of Grötschel, Lovász and Schrijver (Springer) gives the full theory of weak oracles.

Setting

All norms are Euclidean: $\|v\| = \sqrt{v^{\mathsf T}v}$, and for a symmetric matrix $\|A\|$ is the largest absolute eigenvalue. $S(a_0,\rho)$ is the closed Euclidean ball of radius $\rho$ about $a_0$, and $S(K,\delta)$ the set of points within distance $\delta$ of $K$.

A convex body $(K, a_0, r, R)$ consists of a compact convex $K\subseteq\mathbb{R}^n$, $n\ge 2$, and $0<r\le R$ with

$$S(a_0,r)\subseteq K\subseteq S(a_0,R).$$

A weak separation oracle with precision $\delta>0$ answers a query $y$ either with "$y\in S(K,\delta)$", or with a vector $d$, $\|d\|\ge 1$, such that $d^{\mathsf T}x\le d^{\mathsf T}y+\delta$ for all $x\in K$.

Given an objective $c$ and an accuracy $\varepsilon>0$ (with $\varepsilon<r$ and $\|c\|\ge 1$), set

$$N = 4n^2\left\lceil \log\frac{2R^2\|c\|}{r\varepsilon}\right\rceil,\qquad \delta = \frac{R^2\,4^{-N}}{300n},\qquad p = 5N .$$

Start from $x_0=a_0$, $A_0=R^2I$. At step $k$ query the oracle at $x_k$. If it answers "feasible", $k$ is a feasible index and $a=c$; otherwise $a=-d$. Put $b_k = A_ka/\sqrt{a^{\mathsf T}A_ka}$ and

$$x_k^* = x_k+\frac{1}{n+1}b_k,\qquad A_k^* = \frac{2n^2+3}{2n^2}\Bigl(A_k-\frac{2}{n+1}b_kb_k^{\mathsf T}\Bigr),$$

and obtain $x_{k+1}$, $A_{k+1}$ by rounding $x_k^*$, $A_k^*$ to $p$ binary digits, keeping $A_{k+1}$ symmetric. The ellipsoids are $E_k=\{x : (x-x_k)^{\mathsf T}A_k^{-1}(x-x_k)\le 1\}$, and $K_k$ is the set of points of $K$ whose objective value is at least that of every feasible centre found before step $k$.

In Lean, IsRoundedRun K c a₀ R δ p N x A feas a d records exactly these conditions, Kk is $K_k$, and $E_k$ is the published LinearOptimization.ellipsoid (x k) (A k).

Formalization targets

Goal: Theorem (2.4)

If $j<N$ is a feasible index whose centre is best among the feasible centres, $c^{\mathsf T}x_j=\max\{c^{\mathsf T}x_k : k<N \text{ feasible}\}$, then

$$c^{\mathsf T}x_j \ \ge\ \max_{x\in K} c^{\mathsf T}x - \varepsilon .$$

The statement is for every run, i.e. for every sequence of valid oracle answers and every admissible rounding.

Milestones, in attack order

1. (13): the explicit inverse $(A_k^*)^{-1}=\frac{2n^2}{2n^2+3}\bigl(A_k^{-1}+\frac{2}{n-1}\frac{aa^{\mathsf T}}{a^{\mathsf T}A_ka}\bigr)$, and $A_k^*\succ 0$.
2. Lemma (2.1): $A_0,\dots,A_N$ are positive definite, $\|x_k\|\le\|a_0\|+R2^k$, $\|A_k\|\le R^22^k$, $\|A_k^{-1}\|\le R^{-2}4^k$.
3. Lemma (2.2): $\mu(E_{k+1}) < e^{-1/(5n)}\mu(E_k)$.
4. Lemma (2.3): $K_k\subseteq E_k$ for $k=0,\dots,N$.
5. (32): $\mu(K_N)\le\mu(E_N)\le e^{-N/(4n)}\mu(E_0)=e^{-N/(4n)}R^nV_n$.
6. (34): the piece above the level $t$ of the cone with base the $r$-disc through $x_0$ orthogonal to $c$ and apex $y\in K$ has volume $\frac{V_{n-1}r^{n-1}(\zeta-c^{\mathsf T}x_0)}{n\|c\|}\bigl(\frac{\zeta-t}{\zeta-c^{\mathsf T}x_0}\bigr)^n$, which bounds $\mu(\{z\in K: c^{\mathsf T}z\ge t\})$ from below.

Significance

Theorem (2.4) turns any weak separation procedure for a convex body into a weak optimization procedure, with a number of oracle calls and a numerical precision polynomial in $n$, $\log R$, $\log(1/r)$, $\log\|c\|$ and $\log(1/\varepsilon)$. This is the "only if" half of the paper's Theorem (3.1), and through it the source of the polynomial algorithms of Chapters 4–6 of the paper and of the 1988 monograph. Its rounding analysis is what makes the method an algorithm on finite-precision numbers rather than an argument about exact real arithmetic.

The result is proved, and has been for over forty years. What this mission adds is a machine-checked proof of the rounded, weak-oracle version, including the error analysis that the paper compresses into "rounding errors can be estimated similarly". Related items already on the platform formalize exact-arithmetic ellipsoid methods: Bertsimas–Tsitsiklis's central-cut method for polyhedra (LinearOptimization.ellipsoid_method_correct, proved) and Bubeck's version for convex minimization with a first-order oracle (arXiv:1405.4980). Neither has a weak oracle, the inflated factor $(2n^2+3)/(2n^2)$, or rounding.

Difficulty

For the exact update with factor $n^2/(n^2-1)$ and an exact separating hyperplane through the centre, containment and volume decrease are a classical computation. Here three perturbations interact. The cut is shifted by $\delta$, so the retained half-ellipsoid is slightly larger than a half. The rounded matrix differs from $A_k^*$ by up to $n2^{-p}$ in norm, which could destroy positive definiteness if the smallest eigenvalue were not controlled from below, and Lemma (2.1)'s bound $R^24^{-k}$ is what controls it. The containment $K_{k+1}\subseteq E_{k+1}$ must absorb both errors, and it is the inflation factor $(2n^2+3)/(2n^2)$, chosen larger than the optimal one, that leaves room. The paper bounds the remainder term in (29) only by "similar methods"; making that bound explicit is the bulk of the work. The final step also needs the volume rate $e^{-N/(4n)}$ in (32), which is sharper than iterating Lemma (2.2) and requires the exact per-step volume ratio of the inflated update.

Formalization scope

$\mathbb{R}^n$ is Fin n → ℝ with Lebesgue measure. Since Lean's norm on Fin n → ℝ is the sup norm, the Euclidean norm is written out (euclNorm), and the bounds $\|A_k\|\le R^22^k$, $\|A_k^{-1}\|\le R^{-2}4^k$ are stated as quadratic-form (eigenvalue) bounds. $N$ uses the natural logarithm and the integer ceiling.

The runs generalize the page in three ways, each of which makes the theorems stronger: the oracle's answers are any answers valid for its specification; rounding is any symmetric value within $2^{-p}$ entrywise; and data are real rather than rational.

The page's standing assumptions $\varepsilon<r$, $\|c\|\ge1$, $n\ge2$ (p. 173) are hypotheses. Two hypotheses are added, because the page's $N$, $\delta$ and $p$ are absolute numbers and the claims fail at extreme scales:

• $R\ge 1$ (Lemmas (2.1)–(2.3), (32), Theorem (2.4)): for $R=r=2^{-1000}$, $\varepsilon=r/2$, $n=2$, rounding can make $A_1=0$.
• $\varepsilon\le1$ (Lemma (2.3), (32), Theorem (2.4)): for $R=r=10^{13}$, $\varepsilon=0.99r$, $n=2$, $\delta>2r$, and a valid oracle can cut away all of $K$.

Neither is needed in (13) or (34).

A run predicate without the oracle clause would make Lemma (2.3) false, and one with exact equality instead of rounding would state a weaker theorem; the goal quantifies over every run, never over some run. Positive definiteness of the $A_k$ is a consequence (Lemma (2.1)), not a hypothesis: since Lean's inverse of a singular matrix is $0$, assuming it would hide the lemma's content.

Out of scope: the paper's polynomial-time claims (Theorem (3.1) and its consequences), the bit length of the numbers, and the rationality of inputs, since no oracle-machine model with bit complexity exists in Mathlib or on the platform.

Reusable infrastructure: volumes of ellipsoids and of cone pieces, Sherman–Morrison-type inverses, and perturbation bounds for positive definite matrices. Contributions of these as separate lemmas are welcome.

Selected references

• M. Grötschel, L. Lovász, A. Schrijver, The ellipsoid method and its consequences in combinatorial optimization, Combinatorica 1(2) (1981) 169–197. https://doi.org/10.1007/bf02579273
• P. Gács, L. Lovász, Khachiyan's algorithm for linear programming, Mathematical Programming Study 14 (1981) 61–68. https://doi.org/10.1007/BFb0120921
• L. G. Khachiyan, A polynomial algorithm in linear programming, Soviet Mathematics Doklady 20 (1979) 191–194 (English translation of the original article).
• R. G. Bland, D. Goldfarb, M. J. Todd, The ellipsoid method: a survey, Operations Research 29(6) (1981) 1039–1091. https://doi.org/10.1287/opre.29.6.1039
• M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. https://doi.org/10.1007/978-3-642-97881-4
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Ch. 8. Book record.
• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8 (2015). https://arxiv.org/abs/1405.4980

Motivation

The restricted shortest path problem asks for a shortest route between two points of a network subject to a budget on a second additive quantity, such as travel time, cost or risk. It appears as the pricing subproblem of column generation for crew scheduling and vehicle routing, in quality-of-service routing in communication networks, and in scheduling, where Hassin's own §7 uses it for a single-machine problem. The problem is NP-hard (Garey and Johnson, 1979), so exact polynomial algorithms are not expected, and the natural question is how well it can be approximated in polynomial time.

Timeline.

• 1966–1985. Practical exact methods and pseudopolynomial dynamic programs (Joksch 1966; Lawler 1976; Handler and Zang 1980; Aneja, Aggarwal and Nair 1983; Henig 1985).
• 1987. Warburton gives the first fully polynomial approximation scheme (FPAS) for this problem on acyclic graphs, based on rounding and scaling (Warburton, Oper. Res. 35, 1987).
• 1992. Hassin gives two faster FPASs: a rounding-and-scaling scheme driven by an approximate decision test (§3–§4), and a strongly polynomial scheme (§5–§6) (Hassin, Math. Oper. Res. 17, 1992).
• 2001. Lorenz and Raz give a simpler and faster scheme built on the same test-and-search pattern (Lorenz–Raz, Oper. Res. Lett. 28, 2001).

Hassin's combination of an approximate decision test with a geometric search on the bounds is the pattern later schemes for resource-constrained path problems refine, which is why his first scheme is the subject of this mission.

Setting

A directed graph has vertex set $\{1,\dots,n\}$, $n\ge 2$, and edge set $E$. Following the paper, the vertices are numbered so that every edge $(i,j)\in E$ has $i<j$; in particular the graph is acyclic. Each edge carries a positive integer length $c_{ij}$ and a positive integer transition time $t_{ij}$. A path $p=(v_0,\dots,v_m)$ has length $c(p)=\sum_r c_{v_{r-1}v_r}$ and transition time $t(p)=\sum_r t_{v_{r-1}v_r}$. For a nonnegative integer $T$, a $T$-path is a path from $1$ to $n$ with $t(p)\le T$, and $\mathrm{OPT}$ is the length of a shortest $T$-path.

Fix $0<\varepsilon<1$. For a real $V$, the rounded lengths are

$$\tilde c^V_{ij}=\Big\lfloor \frac{c_{ij}(n-1)}{V\varepsilon}\Big\rfloor .$$

Procedure TEST(V) deletes the edges with $c_{ij}>V$ and answers NO if, for some integer $c<(n-1)/\varepsilon$, some $1$–$n$ path in the remaining graph has transition time at most $T$ and rounded length at most $c$; otherwise it answers YES.

The Rounding Algorithm keeps bounds $(LB,UB)$ on OPT. Starting from initial bounds $(LB_0,UB_0)$, Step 1 repeats while $UB>2LB$: with $V=(LB\cdot UB)^{1/2}$ it sets $LB\leftarrow V$ if TEST(V) = YES and $UB\leftarrow V(1+\varepsilon)$ if TEST(V) = NO. Step 2 outputs a $T$-path that is shortest for the rounded lengths $\tilde c^{LB}_{ij}=\lfloor c_{ij}(n-1)/(\varepsilon LB)\rfloor$. The bounds after $k$ passes are written $(LB_k,UB_k)$.

Formalization targets

Goal: the approximation guarantee of the Rounding Algorithm

If $LB_0>0$ is a lower bound on the length of every $T$-path, $N$ is a stage at which $UB_N\le 2LB_N$, and $p$ is a Step 2 output at $LB_N$, then

$$c(p)\le (1+\varepsilon)\,c(q)\qquad\text{for every }T\text{-path }q,$$

that is, $c(p)\le(1+\varepsilon)\,\mathrm{OPT}$. The initial upper bound $UB_0$ is arbitrary.

Milestones (§3–§4)

1. Rounding error (§3, p. 38): with $\delta=V\varepsilon/(n-1)$, $0\le c_{ij}-\delta\tilde c^V_{ij}\le\delta$ for every edge, and $0\le c(p)-\delta\tilde c^V(p)\le V\varepsilon$ for every path.
2. TEST(V) = NO (§3, p. 38): some $T$-path has length $<V(1+\varepsilon)$, so $\mathrm{OPT}<V(1+\varepsilon)$.
3. TEST(V) = YES (§3, p. 38): every $T$-path has length $\ge V$, so $\mathrm{OPT}\ge V$.
4. Bound update (§4, p. 39): along the run, $LB_k>0$ and $LB_k$ is a lower bound on every $T$-path; if some $T$-path has length at most $UB_0$, some $T$-path has length at most $UB_k$.
5. Scaled-optimum error (§4, p. 39): a Step 2 output $p$ at any $LB>0$ satisfies $c(p)\le c(q)+\varepsilon LB$ for every $T$-path $q$.

Companion statements

• Termination when $(1+\varepsilon)^2<2$: some stage $N$ has $UB_N\le 2LB_N$; and an explicit instance with $\varepsilon=9/10$ on which Step 1 never stops.
• Initial bounds (Step 0, p. 39): every $1$–$n$ path has length between $1$ and the sum of the $n-1$ longest edge-lengths.
• Algorithms A and B (§2, pp. 37–38): their recursions compute $f_j(t)$ and $g_j(c)$, with $\mathrm{OPT}=f_n(T)=\min\{c\mid g_n(c)\le T\}$.

Significance

The guarantee makes the Rounding Algorithm a fully polynomial approximation scheme: combined with the paper's running-time analysis, a $(1+\varepsilon)$-approximate $T$-path is computed in time polynomial in the input size and $1/\varepsilon$. The two ingredients, an approximate decision test that answers "OPT $\ge V$" or "OPT $<V(1+\varepsilon)$", and a geometric search on the ratio $UB/LB$, are reused in later FPASs for constrained path, knapsack-type and scheduling problems; the milestones isolate them as separate statements.

The result has been proved since 1992 but, as far as a search of the platform and of Mathlib shows, none of it is machine-checked. This mission produces a checked version of the first scheme, stated for every stage at which the printed stopping test holds and every optimal Step 2 output. It also records, as a companion, that the printed Step 1 need not terminate when $\varepsilon>\sqrt2-1$, and proves termination under $(1+\varepsilon)^2<2$.

Difficulty

The arithmetic of each step is short; the difficulty is in the combinatorial facts the page uses without proof and in the bookkeeping of a run. The rounding error of a path is at most $V\varepsilon$ only because a $1$–$n$ path has at most $n-1$ edges, which follows from the numbering $i<j$ and must be derived for list-encoded paths. The YES case must cover $T$-paths through edges that TEST deleted, which the rounding argument does not see. The bound update needs both bounds to stay positive so that $(LB\cdot UB)^{1/2}$ is a meaningful test point, an invariant of the whole run rather than of one step. A tempting shortcut, assuming that LB is a lower bound on OPT at the stopping stage, would assume milestone 4; the goal assumes it only for $LB_0$.

Formalization scope

• Representation. Vertices are natural numbers; an instance is a structure with $n$, a finite edge set of pairs, and length and time functions, with a well-formedness predicate: $n\ge 2$, every edge $(i,j)$ has $1\le i<j\le n$, and lengths and times are positive. The requirement $n\ge2$ is not printed: a $1$–$n$ path and the divisions by $n-1$ presuppose it. Paths are nonempty vertex lists.
• Arithmetic. $n-1$ is taken in the reals; $\lfloor\cdot\rfloor$ is the natural-number floor of a nonnegative real; $(LB\cdot UB)^{1/2}$ is the real square root. Bounds and $\varepsilon$ are reals, $T$ is a natural number.
• OPT. OPT is never a number in the formal statements, because it is $\infty$ when no $T$-path exists. "OPT $\ge V$" is a bound on every $T$-path, "OPT $<V(1+\varepsilon)$" is the existence of a $T$-path, and the goal compares the output with every $T$-path. Algorithms A and B use values in $\mathbb N\cup\{\infty\}$.
• TEST(V) is defined by the answer the procedure reaches, not through Algorithm B's printed recursion, whose initial condition $g_j(0)=\infty$ is wrong for rounded lengths $0$; for $n\ge2$ and $\varepsilon<1$ the answers agree.
• The run is the iterate of one pass of Step 1; a stopped state is a fixed point. Step 2 outputs any $T$-path optimal for the rounded lengths, without pruning edges, as printed.
• Added hypothesis. The termination statement assumes $(1+\varepsilon)^2<2$, which the page does not state; without it the printed loop can run forever, and an explicit instance is included.
• Not a trivialization. The goal assumes nothing about TEST's correctness, the rounding error or the lower-bound invariant along the run, and the termination companion shows that its stopping hypothesis is reachable.
• Out of scope. The second, strongly polynomial scheme of §5–§6 is not included, because as printed its Partitioning Algorithm can report infeasibility on a feasible instance and formalizing it would require a corrected algorithm that is not the author's. All running-time claims, stated as $O(\cdot)$ bounds under an informal operation count, are also excluded, as are the $V'$ variant of the test points and the scheduling application of §7.
• Reusable parts. The list-based path layer with two additive weights, and the correctness of the pseudopolynomial recursions of Algorithms A and B, are independent of the approximation scheme. Contributions of proofs for any milestone or companion are welcome.

Selected references

• R. Hassin, Approximation schemes for the restricted shortest path problem, Mathematics of Operations Research 17(1):36–42, 1992. https://doi.org/10.1287/moor.17.1.36
• A. Warburton, Approximation of Pareto optima in multiple-objective, shortest-path problems, Operations Research 35(1):70–79, 1987. https://doi.org/10.1287/opre.35.1.70
• D. H. Lorenz and D. Raz, A simple efficient approximation scheme for the restricted shortest path problem, Operations Research Letters 28(5):213–219, 2001. https://doi.org/10.1016/S0167-6377(01)00069-4
• M. R. Garey and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.

Motivation

Reliability theory classifies life distributions by how they age. The IHRA class (increasing hazard rate average) is the smallest class of life distributions that contains the exponential distributions and is closed under forming coherent systems and taking limits in distribution (Birnbaum, Esary and Marshall 1966). It is therefore the natural class for the lifetime of a system built from components that wear out. A distribution belongs to it when its survival function $\bar F$ satisfies: $[\bar F(t)]^{1/t}$ is decreasing in $t > 0$.

Esary, Marshall and Proschan (Ann. Probability 1 (1973) 627–649) asked where such ageing comes from physically. Their answer is a shock model: a device receives shocks at the epochs of a Poisson process, each shock does random damage, and the device fails when the accumulated damage exceeds its capacity. The central result of their §4, formalized in this mission, is that this model always produces an IHRA life, whatever the damage distribution. In the authors' words, "the IHRA property has been obtained … as an implication of a natural physical model. The only hypothesis imposed upon $F$ is that it be the distribution of a nonnegative random variable." The paper is a standard reference of reliability theory and the source of the cumulative damage model used across maintenance and insurance applications.

Setting

Shocks arrive according to a Poisson process with rate $\lambda > 0$. Write $\bar P_k$ for the probability that the device survives the first $k$ shocks; then $1 \ge \bar P_0 \ge \bar P_1 \ge \dots \ge 0$ (display (2.2)). Conditioning on the number of shocks in $[0, t]$ gives the shock survival function (2.1):

$$\bar H(t) = \sum_{k=0}^{\infty} \bar P_k\, e^{-\lambda t}\frac{(\lambda t)^k}{k!}, \qquad t \ge 0,$$

with $\bar H(t) = 1$ for $t < 0$. The weights $K(k,t) = e^{-\lambda t}(\lambda t)^k/k!$ are the Poisson probabilities.

In the cumulative damage model the $i$th shock causes a damage $X_i \ge 0$, the damages are independent with common distribution function $F$ (so $F(z) = 0$ for $z < 0$), and the device survives $k$ shocks when $X_1 + \dots + X_k \le x$, for a fixed threshold $x$. Hence (4.1)

$$\bar P_k = F^{(k)}(x), \qquad k = 0, 1, \dots,$$

where $F^{(k)}$ is the $k$-fold convolution of $F$ and $F^{(0)}$ is degenerate at $0$. A distribution with survival function $\bar F$ is IHRA if $[\bar F(t)]^{1/t}$ is decreasing in $t > 0$; throughout, "decreasing" means non-increasing.

Formalization targets

Goal: Corollary 4.2, display (4.7)

For every distribution $F$ on $[0,\infty)$, every $\lambda > 0$ and every threshold $x$,

$$\bar H(t) = \sum_{k=0}^\infty e^{-\lambda t}\frac{(\lambda t)^k}{k!} F^{(k)}(x) \quad \text{is IHRA.}$$

This is the first of the three statements of Corollary 4.2; the second ((4.7a), independent damages $F_i$ that worsen with $i$) is an extra item of this mission, and the third ((4.7b), dependent damages satisfying (4.3)–(4.5)) belongs to mission III of this series.

Milestones

1. (2.6): $\bar H(t) \ge \bar H(0)e^{-\lambda t}$ for $t \ge 0$.
2. Theorem 3.1 (3.4) through the three claims of its proof (p. 633): if $1 = \bar P_0 \ge \bar P_1 \ge \dots$ and $\bar P_k^{1/k}$ is decreasing in $k \ge 1$, then $\bar P_k - \zeta^k$ ($0 \le \zeta \le 1$) has at most one sign change, from $+$ to $-$; this property passes to $\bar H(t) - e^{-(1-\zeta)\lambda t}$ on $t \ge 0$; hence $\bar H(t) - e^{-\theta t}$ has at most one sign change for every $\theta > 0$; and $H$ is IHRA.
3. Lemma 4.1: for $F$ on $[0,\infty)$, $[F^{(k)}(x)]^{1/k}$ is decreasing in $k = 1, 2, \dots$.

Further items

Lemma 4.1a and Corollary 4.2 (4.7a); Theorem 4.4 ($[F^{(k)}(x)]^{1/k}$ is constant in $k$ iff $F$ has no mass in $(0,x]$); Corollary 4.5 ((4.7) is exponential iff $F$ has no mass in $(0,x]$); Corollary 4.11 ($[P\{N(x) \ge k\}]^{1/k}$ is decreasing for the count $N(x)$ of an ordinary renewal process).

Significance

The goal turns a modelling assumption into a theorem: anyone who models failure as accumulated nonnegative damage under Poisson shocks obtains, without further checks, every consequence of IHRA proved in reliability theory, including the closure of the class under the formation of coherent systems. Theorem 3.1 (3.4) is reusable on its own: it reduces the IHRA property of any Poisson mixture to a discrete condition on the $\bar P_k$, and the same scheme drives the first passage result for wear processes (Theorem 4.10, mission III). Lemma 4.1, applied to renewal processes, gives Corollary 4.11, a statement about renewal counts with no shock model in sight.

All results are proved in the paper; none has a machine-checked proof that we know of. The Mathlib library has the Poisson distribution and the convolution of measures, but no reliability classes, no total positivity and no variation diminishing property. The mission's output is a formal proof of the paper's chain of results and, along the way, reusable statements about Poisson mixtures and convolution powers.

Difficulty

Two steps resist a direct argument. The first is the transfer from sequences to functions: knowing that $\bar P_k - \zeta^k$ changes sign at most once says nothing pointwise about the series $\sum_k(\bar P_k - \zeta^k)K(k,t)$. The paper invokes the variation diminishing property of the totally positive Poisson kernel (Karlin, Total Positivity, 1968), which is not in Mathlib. The second is Lemma 4.1, an inequality between convolution powers of an arbitrary law: no density, moments or continuity may be assumed, atoms at $0$ and at $x$ are allowed, so any argument through densities or Laplace transforms loses generality. A further subtlety is the passage from "one sign change of $\bar H(t) - e^{-\theta t}$ for every $\theta$" to the monotonicity of $[\bar H(t)]^{1/t}$, which needs care where $\bar H$ vanishes.

Formalization scope

• A distribution $F$ with $F(z) = 0$ for $z < 0$ is a probability measure $\mu$ on $\mathbb R$ with $\mu(-\infty,0) = 0$; nothing else is assumed. $F^{(k)}$ is the $k$-fold additive convolution of $\mu$ (Mathlib's Measure.conv) starting from the point mass at $0$, and $F^{(k)}(x)$ is the real number $F^{(k)}(-\infty,x]$.
• $\bar H$ is the series (2.1) as a function on $\mathbb R$, equal to $1$ on $t < 0$. It is never defined through a constructed random failure time, and IHRA is never encoded through a condition on the $\bar P_k$: the goal concludes that $[\bar H(t)]^{1/t}$ is decreasing on $t > 0$ for the series itself. This rules out the trivializing reading in which the goal unfolds to Lemma 4.1.
• Powers $[\bar H(t)]^{1/t}$ and $\bar P_k^{1/k}$ are real powers with exponent $1/t$, $1/k$ in $\mathbb R$.
• Hypotheses the paper leaves implicit and the Lean statements make explicit: $\lambda > 0$; $\bar P_k \ge 0$ (the $\bar P_k$ are probabilities); in Corollary 4.5, $x \ge 0$ (the threshold is a capacity), and "exponential" includes the degenerate rate $0$.
• Sign change statements about $\bar H$ hold on $t \ge 0$, where the series defines it.
• The threshold $x$ in the goal ranges over all reals, as printed.
• In Corollary 4.11 the renewal process is given by independent measurable interarrival times with common law $\mu$, and $N(x) = \#\{k \ge 1 : X_1 + \dots + X_k \le x\}$ takes values in $\{0, 1, \dots, \infty\}$.

A complete development needs: the variation diminishing property of the Poisson kernel (reusable for every Poisson mixture), monotonicity of $[F^{(k)}(x)]^{1/k}$ via convolution integrals, and elementary facts about real powers and sign changes. Proofs of any milestone or extra item, and general total positivity lemmas, are welcome.

Selected references

• J. D. Esary, A. W. Marshall and F. Proschan, Shock Models and Wear Processes, The Annals of Probability 1(4) (1973) 627–649. https://doi.org/10.1214/aop/1176996891
• Z. W. Birnbaum, J. D. Esary and A. W. Marshall, A Stochastic Characterization of Wear-Out for Components and Systems, The Annals of Mathematical Statistics 37 (1966) 816–825. https://doi.org/10.1214/aoms/1177699362
• S. Karlin, Total Positivity, Vol. I, Stanford University Press, 1968.
• R. E. Barlow and F. Proschan, Mathematical Theory of Reliability, Wiley, 1965. https://doi.org/10.1137/1.9781611971194

Motivation

Newton's method for a nonlinear system $F(x) = 0$, with $F:\mathbb R^n\to\mathbb R^n$, solves the linear system $F'(x_k)s_k = -F(x_k)$ at every step. For large systems that solve is itself iterative (a Krylov method such as GMRES), and it is stopped early. The resulting inexact Newton methods, introduced by Dembo, Eisenstat and Steihaug (SIAM J. Numer. Anal. 19 (1982)), accept any step with $\|F(x_k)+F'(x_k)s_k\|\le\eta_k\|F(x_k)\|$, where the forcing term $\eta_k\in[0,1)$ controls how accurately the linear system is solved. Their theory is local: it applies once the iterates are near a solution with invertible derivative.

Practical solvers (Newton–Krylov codes in large-scale simulation, nonlinear solver libraries such as PETSc's SNES and SUNDIALS' KINSOL) combine such inexact steps with a globalization, most often backtracking along the step. Eisenstat and Walker (SIAM J. Optim. 4 (1994)) gave the global convergence theory for this combination: what can be said about the iterates from an arbitrary starting point, with no assumption that a solution exists or that $F'$ is invertible anywhere.

Timeline. Dembo, Eisenstat and Steihaug (1982) proved local convergence of inexact Newton methods. Dembo and Steihaug (Math. Program. 26 (1983)) studied truncated Newton methods for unconstrained minimization. Brown and Saad (1990) studied globalized Newton–Krylov methods with line searches and model trust regions, under the inner-product norm. Eisenstat and Walker (1994) gave the general framework treated here, for an arbitrary norm. Their 1996 paper (SIAM J. Sci. Comput. 17) proposed the forcing-term choices that are now standard.

Setting

Let $E$ be $\mathbb R^n$ with an arbitrary norm $\|\cdot\|$, and let $F:E\to E$ be continuously differentiable with derivative $F'(x)$. A point $x_*$ is a limit point of $(x_k)$ if every ball $N_\delta(x_*)=\{y:\|y-x_*\|<\delta\}$ contains $x_k$ for infinitely many $k$.

Algorithm GIN (global inexact Newton method). Fix $t\in(0,1)$. At each $k$, find a level $\eta_k\in[0,1)$ and a step $s_k$ with

$$\|F(x_k)+F'(x_k)s_k\|\le\eta_k\|F(x_k)\| \quad (2.1),\qquad \|F(x_k+s_k)\|\le[1-t(1-\eta_k)]\,\|F(x_k)\| \quad (2.2),$$

and set $x_{k+1}=x_k+s_k$. Condition (2.1) says that $s_k$ reduces the norm of the local linear model by the factor $\eta_k$. Condition (2.2) asks that $\|F\|$ itself decrease by a fixed fraction $t$ of that predicted reduction.

Algorithm MR (minimum reduction method). Fix $\eta_{\max}\in[0,1)$ and $0<\theta_{\min}<\theta_{\max}<1$. At step $k$, choose $\bar\eta_k\in[0,\eta_{\max}]$ and a curve $\sigma_k$ with $\|F(x_k)+F'(x_k)\sigma_k(\eta)\|\le\eta\|F(x_k)\|$ for $\bar\eta_k\le\eta\le1$ (5.1). Start at $\eta_k=\bar\eta_k$. While (2.2) fails for $s_k=\sigma_k(\eta_k)$, replace $\eta_k$ by $1-\theta(1-\eta_k)$ for some $\theta\in[\theta_{\min},\theta_{\max}]$. Then set $x_{k+1}=x_k+\sigma_k(\eta_k)$.

Algorithm INB (inexact Newton backtracking). Choose $\bar\eta_k\in[0,\eta_{\max}]$ and an inexact Newton step $\bar s_k$ at level $\bar\eta_k$. While (2.2) fails, shorten the step, $s_k\leftarrow\theta s_k$, and raise the level, $\eta_k\leftarrow1-\theta(1-\eta_k)$. INB is MR with the backtracking curve $\sigma_k(\eta)=\frac{1-\eta}{1-\bar\eta_k}\bar s_k$ (6.1).

An algorithm does not break down if it produces an infinite sequence of iterates, in particular if every while-loop exits.

Formalization targets

Goal: Theorem 6.1 (global convergence of Algorithm INB)

If Algorithm INB does not break down and $x_*$ is a limit point of $(x_k)$ at which $F'(x_*)$ is invertible, then

$$F(x_*)=0,\qquad x_k\to x_*,\qquad s_k=\bar s_k\ \text{and}\ \eta_k=\bar\eta_k\ \text{for all sufficiently large }k.$$

The statement assumes no solution, bounded level set, Lipschitz derivative or particular norm. The last clause says that backtracking eventually stops, so the local rate is governed by the forcing terms $\bar\eta_k$.

Milestones

In attack order:

1. Lemmas 1.1 and 1.2. Continuity of $y\mapsto F'(y)^{-1}$ at an invertible point, and a uniform linearization error $\|F(z)-F(y)-F'(y)(z-y)\|\le\varepsilon\|z-y\|$ near $x$.
2. Theorem 3.3. If $F(x_k)\to0$, the steps satisfy (2.1) with a fixed $\eta$, and $\|F(x_k)\|$ is nonincreasing, then an invertible limit point is a zero and the limit.
3. Theorem 3.4. A GIN run with $\sum_k(1-\eta_k)=\infty$ has $F(x_k)\to0$, plus the conclusion of Theorem 3.3 at invertible limit points.
4. Theorem 3.5. A GIN run converges to a limit point near which $\|s_k\|\le\Gamma(1-\eta_k)\|F(x_k)\|$ (3.2).
5. Lemma 5.1. The while-loop terminates, with $1-\eta_k\ge\min\{1-\bar\eta_k,\theta_{\min}\delta/(\Gamma\|F(x_k)\|)\}$.
6. MR runs are GIN runs (§5).
7. Theorem 5.2 for MR. Under $\|\sigma_k(\eta)\|\le\Gamma(1-\eta)\|F(x_k)\|$ near a limit point $x_*$ (5.6): $F(x_*)=0$, $x_k\to x_*$, and $\eta_k=\bar\eta_k$ eventually.
8. INB runs are MR runs with the curve (6.1), and $s_k=\sigma_k(\eta_k)$ throughout the loop (§6).

Further items, which are not milestones: Corollary 6.2 (exact Newton with backtracking takes full Newton steps eventually), Theorem 5.2 for Algorithm TL, Lemma 3.1 (existence of acceptable GIN steps), and Proposition 2.1 (the Goldstein–Armijo alpha condition implies (2.2) in the Euclidean norm).

Significance

The result. Theorem 6.1 is the global convergence guarantee for the inexact Newton backtracking method that Newton–Krylov solvers implement. It separates three outcomes: the iterates diverge, they accumulate only at points where $F'$ is singular, or they converge to a solution with invertible derivative and eventually take the unmodified inexact Newton steps. In the third case the local theory of Dembo, Eisenstat and Steihaug applies from some iteration on, so the forcing terms alone set the convergence rate. Theorem 5.2 is the template: §§6–8 of the paper derive the convergence of backtracking, equality-curve and dogleg-type methods from it by verifying (5.6).

Formalizing it. The results are proved on paper and none of them has a machine-checked proof that we know of. The mission produces a library of algorithm-run predicates with explicit while-loops for inexact Newton methods. It also checks the paper's reduction chain (INB is a run of MR, MR is a run of GIN) and the global convergence theorems in an arbitrary finite-dimensional norm.

Difficulty

The obvious argument fails at both ends. Sufficient decrease (2.2) alone gives monotonicity of $\|F(x_k)\|$, but not convergence of the iterates. On the page, $F(x)=x^2-1$ admits sequences satisfying (2.2) with both $\pm1$ as limit points. Convergence of $\|F(x_k)\|$ to $0$ needs $\sum(1-\eta_k)=\infty$, and nothing in the algorithm states this. In Theorem 5.2 it has to be derived from the exit level of the while-loop, which depends on a neighbourhood of $x_*$ where the linearization error is uniformly controlled. A solver must combine a limit-point argument (only infinitely many iterates are near $x_*$, not all of them) with the loop's worst-case backtracking factor $\theta_{\min}$. The invertibility of $F'(x_*)$ enters only through the bound (5.6) for the backtracking curve, which must be established uniformly in $k$.

Formalization scope

• Space and norm. $E$ is a finite-dimensional real normed space ([NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]). This is exactly "$\mathbb R^n$ with an arbitrary norm". Fin n → ℝ (sup norm) and EuclideanSpace would each fix one norm. Only Proposition 2.1 assumes an inner product space, as the page does.
• Derivative. $F'$ is fderiv ℝ F, with ContDiff ℝ 1 F (the paper's standing assumption). Invertibility is ContinuousLinearMap.IsInvertible, and $F'(x)^{-1}$ is ContinuousLinearMap.inverse.
• Runs. An algorithm that does not break down is a predicate on infinite sequences (IsGINRun, IsMRRun, IsINBRun, plus IsTLRun, IsENBRun). The steps and levels the algorithm says to "find" or "choose" are data constrained only by the stated conditions. A while-loop is recorded by its number of passes $m_k$ and factors $\theta_{k,j}\in[\theta_{\min},\theta_{\max}]$. Every trial before the last fails the loop's test and the last one passes it. Termination is part of the run.
• Limit point is MapClusterPt xstar atTop x. "For all sufficiently large $k$" is ∀ᶠ k in atTop. The paper's "whenever $x_k$ is sufficiently near $x_*$ [and $k$ is sufficiently large]" is ∃ Γ, ∃ δ > 0, [∃ K,] ∀ k [≥ K], x k ∈ ball xstar δ → …. $\Gamma$ precedes $k$ ("independent of $k$"), and the "$k$ large" clause appears only in (3.2), where the page has it.
• Hypotheses as printed. Theorems 3.5 and 5.2 do not assume $F'(x_*)$ invertible. Theorem 5.2 does not assume $\sum(1-\eta_k)=\infty$. Lemma 5.1 is stated for one iteration of the loop shared by MR and TL, for every choice of factors.
• Trivializing readings ruled out. A run predicate without the "rejected" clause would allow needless backtracking, and one without the "accepted" clause would drop (2.2). Both clauses are present. A sorry-free check (F = id on $\mathbb R$) confirms that the INB, GIN and ENB run predicates and the goal's hypotheses are satisfiable, so the goal is not vacuous.
• Infrastructure. Continuity of operator inversion and uniform differentiability on neighbourhoods are in Mathlib. The run predicates and trial-level recursions are reusable for any line-search or backtracking analysis. Each milestone is stated independently; contributions in any order are welcome.

Selected references

• S. C. Eisenstat and H. F. Walker, Globally Convergent Inexact Newton Methods, SIAM J. Optim. 4(2) (1994) 393–422. https://doi.org/10.1137/0804022
• R. S. Dembo, S. C. Eisenstat and T. Steihaug, Inexact Newton Methods, SIAM J. Numer. Anal. 19(2) (1982) 400–408. https://doi.org/10.1137/0719025
• R. S. Dembo and T. Steihaug, Truncated-Newton algorithms for large-scale unconstrained optimization, Math. Program. 26 (1983) 190–212. https://doi.org/10.1007/BF02592055
• P. N. Brown and Y. Saad, Hybrid Krylov Methods for Nonlinear Systems of Equations, SIAM J. Sci. Stat. Comput. 11(3) (1990) 450–481. https://doi.org/10.1137/0911026
• S. C. Eisenstat and H. F. Walker, Choosing the Forcing Terms in an Inexact Newton Method, SIAM J. Sci. Comput. 17(1) (1996) 16–32. https://doi.org/10.1137/0917003
• J. E. Dennis and R. B. Schnabel, Numerical Methods for Unconstrained Optimization and Nonlinear Equations, SIAM Classics in Applied Mathematics 16 (1996). https://doi.org/10.1137/1.9781611971200