All missions

Motivation

Many problems in optimization reduce to finding a zero of a maximally monotone operator: minimizing a closed proper convex function (its subdifferential is maximally monotone), finding a saddle point of a convex–concave function, and solving monotone variational inequalities. The basic algorithm for this problem is the proximal point method of Martinet (1970) and Rockafellar (1976), which repeatedly applies the resolvent of the operator. The augmented Lagrangian method, the proximal method of multipliers, the Douglas–Rachford splitting method, ADMM and the primal–dual hybrid gradient method are all instances of it, so any speed-up of the proximal point method transfers to these widely used algorithms.

For convex minimization, Güler (1992) accelerated the proximal point method in the style of Nesterov, improving the rate of the function value from $O(1/i)$ to $O(1/i^2)$. For general maximally monotone operators no function value exists, and the natural measure of progress is the fixed-point residual $\|x_{i}-y_{i-1}\|$, the distance moved by one resolvent step. Gu and Yang (2020) showed that the plain proximal point method has the exact worst-case rate $O(1/i)$ for the squared residual. Relaxed and inertial variants had been studied, but none guaranteed an accelerated rate for this measure. Kim (arXiv:1905.05149, Math. Program. 2021) found one using the performance estimation problem (PEP) of Drori and Teboulle (2014): a new accelerated proximal point method whose squared fixed-point residual is at most $R^2/i^2$.

Setting

Let $\mathcal H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$. A set-valued operator $M:\mathcal H\to2^{\mathcal H}$ assigns a subset $Mx\subseteq\mathcal H$ to every point $x$. It is monotone if $\langle x-y,u-v\rangle\ge0$ whenever $u\in Mx$ and $v\in My$, and maximally monotone if moreover no monotone operator has a graph that properly contains the graph of $M$. The class of maximally monotone operators is $\mathcal M(\mathcal H)$, and $X_*(M)=\{x:0\in Mx\}$ is the set of zeros.

For a step size $\lambda>0$, the resolvent $J_{\lambda M}=(I+\lambda M)^{-1}$ maps $y$ to the unique $x$ with $y\in x+\lambda Mx$. It is single-valued for monotone $M$ and defined on all of $\mathcal H$ for maximally monotone $M$.

The general proximal point method with step coefficients $h=\{h_{i,k}\}$ starts at $y_0$ and iterates

$$x_{i+1}=J_{\lambda M}(y_i),\qquad y_{i+1}=y_i+\sum_{k=0}^{i}h_{i+1,k+1}(x_{k+1}-y_k).$$

Kim's proposed accelerated proximal point method starts at $x_0=y_0=y_{-1}$ and iterates

$$x_{i+1}=J_{\lambda M}(y_i),\qquad y_{i+1}=x_{i+1}+\frac{i}{i+2}(x_{i+1}-x_i)-\frac{i}{i+2}(x_i-y_{i-1}).$$

The coefficients (25) are $h_{i,k}=-\frac{2k}{i(i+1)}$ for $k<i$ and $h_{i,i}=\frac{2i}{i+1}$.

The PEP of Section 3 bounds the worst case of $\|x_N-y_{N-1}\|^2/R^2$ over all $M\in\mathcal M(\mathcal H)$ and all starts with $\|y_0-x_*\|\le R$. A semidefinite relaxation leads to the dual problem (D): minimize $c$ over nonnegative $a_2,\dots,a_N,b_N,c$ such that $\sum_{i=2}^Na_iA_{i-1,i}(h)+b_NB_N(h)+cC-u_Nu_N^\top\succeq0$. The matrices are explicit symmetric $(N+1)\times(N+1)$ matrices built from $h$ and the canonical basis $u_1,\dots,u_{N+1}$. Its optimal value is $\mathcal B_D(h)$.

Formalization targets

Goal: Theorem 4.1

For every $M\in\mathcal M(\mathcal H)$, every $\lambda>0$, every run of the proposed method, and every $x_*\in X_*(M)$ with $\|x_0-x_*\|\le R$ for a constant $R>0$,

$$\|x_i-y_{i-1}\|^2\le\frac{R^2}{i^2}\qquad\text{for every }i\ge1.$$

The constant is the paper's, and nothing is left unfixed.

Milestones

1. Lemma 4.1. For every $N\ge1$, $h$ from (25) with $a_i=\frac{2(i-1)i}{N^2}$, $b_N=\frac2N$, $c=\frac1{N^2}$ is feasible for (D) and for (HD) $=\min_h\mathcal B_D(h)$.
2. Section 3, (D). For any $h$ and any feasible point of (D), $\frac1{R^2}\|x_N-y_{N-1}\|^2\le c$ for every run of the general method with $\|y_0-x_*\|\le R$.
3. Eq. (28). With $h$ from (25), $\frac1{R^2}\|x_N-y_{N-1}\|^2\le\mathcal B_D(h)\le\frac1{N^2}$ for every $N\ge1$.
4. Proposition 4.1. The general method with (25) and the proposed method generate identical sequences from the same initial point.

Significance

Theorem 4.1 gives the first $O(1/i^2)$ rate for the fixed-point residual of a proximal point method on general maximally monotone operators. The rate uses no strong monotonicity, no smoothness, and no finite dimension. Because the proximal point method underlies the proximal method of multipliers, PDHG, Douglas–Rachford splitting and ADMM, the paper derives accelerated versions of each (Section 6). The same analysis also accelerates the forward method for cocoercive operators (Section 7). Later work related the method to the Halpern iteration (Lieder 2021) and showed that its rate is optimal among a broad class of fixed-point methods up to a constant (Park and Ryu 2022).

The result is proved in the paper, and to our knowledge no machine-checked proof exists. Formalizing it produces a verified chain of four results: an explicit semidefinite certificate (Lemma 4.1), the weak-duality step from an SDP certificate to an algorithmic bound, the resulting rate for the general method, and the algebraic identity between two recursions (Proposition 4.1). It also produces reusable definitions of monotone and maximally monotone set-valued operators on a real Hilbert space, which Mathlib does not have.

Difficulty

The obvious approach would be a Lyapunov (potential) function argument, but the paper does not give one. The rate comes out of a semidefinite program. Lemma 4.1 asks for positive semidefiniteness of an $(N+1)\times(N+1)$ matrix whose entries are double sums over $h$, uniformly in $N$. The passage from the dual certificate back to the iterates happens in an arbitrary, possibly infinite-dimensional Hilbert space, where each constraint matrix corresponds to a monotonicity inequality between iterates, so matrix positivity has to be turned into an inequality between inner products in $\mathcal H$. The PEP is a relaxation that discards constraints, so only weak duality is available, and a rate that holds only for $\dim\mathcal H\ge N+1$ (Lemma 3.1) is not what is asked. Proposition 4.1 is a two-level induction with index bookkeeping at $i=0,1$.

Formalization scope

$\mathcal H$ is any real Hilbert space (NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace), with no finite-dimensional specialization. An operator is M : H → Set H. Maximal monotonicity says that every monotone A with M x ⊆ A x for all x equals M.

The resolvent step is relational: $x_{i+1}=J_{\lambda M}(y_i)$ is encoded as $\lambda^{-1}(y_i-x_{i+1})\in Mx_{i+1}$. For monotone $M$ and $\lambda>0$ this determines $x_{i+1}$ uniquely, and for maximally monotone $M$ such an $x_{i+1}$ exists for every $y_i$ (Minty's theorem). No function-valued resolvent with junk values off its domain is used. Sequences are indexed by ℕ. The paper's $y_{-1}=y_0$ is y (0 - 1) = y 0 under natural-number subtraction. The general method has no $x_0$, so its initial-distance condition is on $y_0$, as in (17). The step size $\lambda$ is written lam.

PEP matrices are Matrix (Fin (N+1)) (Fin (N+1)) ℝ, with a 1-based basis basisVec N i $=u_i$. $\mathcal B_D(h)$ is the infimum of the feasible values of $c$ computed in EReal, so an infeasible $h$ gets the value $+\infty$ as in the paper; Eq. (28) compares it with the real bounds cast to EReal.

A formalization in which the iterate predicate cannot be satisfied, the residual is $\|x_i-x_{i-1}\|$, the correction term is dropped or has the wrong sign, the initial point is decoupled ($x_0\ne y_0$), or $M$ is only monotone on finitely many points, would state a different theorem, and none is used here.

Useful infrastructure includes a Minty-type existence lemma, uniqueness of the resolvent, and a lemma turning a positive semidefinite certificate into an inequality between inner products in $\mathcal H$ (via Matrix.PosSemidef and Gram matrices). These are reusable for PEP-based rates of other first-order methods. Proofs of any milestone, and of the goal by other routes, are welcome.

Selected references

• D. Kim, Accelerated proximal point method for maximally monotone operators, Math. Program. 190 (2021) 57–87; arXiv:1905.05149v4. https://arxiv.org/abs/1905.05149
• R. T. Rockafellar, Monotone operators and the proximal point algorithm, SIAM J. Control Optim. 14 (1976) 877–898. https://doi.org/10.1137/0314056
• O. Güler, New proximal point algorithms for convex minimization, SIAM J. Optim. 2 (1992) 649–664. https://doi.org/10.1137/0802032
• Y. Drori, M. Teboulle, Performance of first-order methods for smooth convex minimization: a novel approach, Math. Program. 145 (2014) 451–482. https://doi.org/10.1007/s10107-013-0653-0
• G. Gu, J. Yang, Tight sublinear convergence rate of the proximal point algorithm for maximal monotone inclusion problems, SIAM J. Optim. 30 (2020) 1905–1921. https://doi.org/10.1137/19M1299049
• F. Lieder, On the convergence rate of the Halpern-iteration, Optim. Lett. 15 (2021) 405–418. https://doi.org/10.1007/s11590-020-01617-9
• J. Park, E. K. Ryu, Exact optimal accelerated complexity for fixed-point iterations, ICML 2022; arXiv:2201.11413. https://arxiv.org/abs/2201.11413
• H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5

Motivation

A process on a shared-memory multiprocessor that finds a lock held must decide what to do while it waits. It can spin, repeatedly testing the lock and occupying its processor, or it can block, giving the processor to another process and paying a fixed context-switch cost $C$ to be descheduled and later restored. Spinning is cheap when the lock is released soon; blocking is cheap when the wait is long. The waiting time is not known in advance, so the choice has to be made on-line. This is the spin-block problem, studied by Karlin, Manasse, McGeoch and Owicki in Competitive Randomized Algorithms for Nonuniform Problems (Algorithmica 11, 1994, doi:10.1007/BF01189993), §4. Mathematically it is the continuous form of the ski-rental problem, and the same rent-or-buy structure recurs in power-down policies and in TCP acknowledgement (Karlin, Kenyon, Randall, STOC 2001).

Timeline:

• Karlin, Manasse, Rudolph and Sleator (1988, doi:10.1007/BF01762111) introduced competitive analysis of snoopy caching and showed that $2$ is the optimal deterministic factor there. The spin-block analogue is recorded in the 1994 paper (pp. 558–559): spinning for time $C$ and then blocking is $2$-competitive, and no deterministic algorithm does better.
• Karlin, Manasse, McGeoch and Owicki (SODA 1990; Algorithmica 1994) found the optimal randomized factors for snoopy caching and spin-block. For spin-block, Theorem 10 (p. 559) gives $e/(e-1)\approx1.582$ against an oblivious adversary. Theorem 9 (p. 559) shows that against an adaptive on-line adversary randomization does not help: the factor stays $2$.

Setting

Fix a context-switch cost $C>0$. A lock wait is described by its release time $\tau\ge0$. An algorithm handling the wait chooses a blocking time $b\in[0,\infty]$: it spins until time $b$ and then blocks ($b=\infty$: never block). The cost of the wait is

$$\mathrm{waitCost}_C(b,\tau)=\begin{cases}\tau,&\tau\le b,\\ b+C,&b<\tau,\end{cases}$$

so a lock released exactly at the blocking time costs $\tau$. The optimal off-line algorithm, which knows $\tau$, pays $\min(\tau,C)$.

An input is a finite sequence $\sigma=(\tau_0,\dots,\tau_{n-1})$ of lock waits. A deterministic on-line algorithm chooses the blocking time of wait $j$ as a function of $\tau_0,\dots,\tau_{j-1}$, the release times it has already observed. Its cost $C_A(\sigma)$ is the sum of the wait costs, and the off-line cost is $C_{opt}(\sigma)=\sum_j\min(\tau_j,C)$.

A randomized on-line algorithm is a probability distribution over deterministic on-line algorithms: a probability space $(I,\mu)$ and a deterministic algorithm $A_i$ for each $i\in I$, with $i\mapsto C_{A_i}(\sigma)$ measurable for every $\sigma$. Its expected cost is $\mathbf{E}C_A(\sigma)=\int C_{A_i}(\sigma)\,d\mu(i)$. Following §1 of the paper, $A$ is $c$-competitive against an oblivious adversary if there is a constant $a$ with

$$\mathbf{E}C_A(\sigma)\le c\cdot C_{opt}(\sigma)+a\qquad\text{for every input }\sigma .$$

The adversary is oblivious: it fixes $\sigma$ before the algorithm's random choices are made.

The paper's algorithm blocks at a random time with cumulative distribution

$$\pi(t)=\begin{cases}\dfrac{e^{t/C}-1}{e-1},&0\le t\le C,\\[1ex] 1,&t>C,\end{cases}$$

where $\pi(t)$ is the probability of blocking before time $t$.

Formalization targets

Goal: Theorem 10 (p. 559)

For every $C>0$:

$$\Big(\forall A\ \forall c,\ A\ \text{is } c\text{-competitive}\ \Rightarrow\ c\ge\tfrac{e}{e-1}\Big)\quad\text{and}\quad\exists A,\ A\ \text{is } \tfrac{e}{e-1}\text{-competitive}.$$

Milestones

1. Expected cost of one wait (§4.1, p. 560). For a blocking time with law $\nu$ and release time $\tau$,

$$\mathbf{E}\,\mathrm{waitCost}_C(b,\tau)=\pi(\tau)\,C+\int_0^\tau(1-\pi(t))\,dt,\qquad \pi(t)=\nu\{b<t\}.$$

2. The ratio of the paper's distribution (§4.1, p. 560). With the $\pi$ above, for all $\tau\ge0$,

$$\pi(\tau)\,C+\int_0^\tau(1-\pi(t))\,dt\le\tfrac{e}{e-1}\min(\tau,C).$$

3. Theorem 10, first claim: the lower bound $c\ge e/(e-1)$ for every $c$-competitive randomized algorithm.
4. Theorem 10, second claim: existence of an $e/(e-1)$-competitive randomized algorithm.

Significance

Theorem 10 settles the randomized competitive ratio of the continuous ski-rental problem: $e/(e-1)$ is achievable and cannot be improved by any on-line algorithm, randomized or not, against an oblivious adversary. The same constant is the limit of the paper's snoopy-caching ratios $e_p/(e_p-1)$ as the block size grows, and it recurs in randomized rent-or-buy problems and in on-line primal-dual analyses.

The result is proved in the literature, and the mission's work is to formalize it. The platform has related material but not this statement: Primal-Dual Online Algorithms I: Fractional Ski Rental proves a deterministic, fractional, discrete-day bound (PrimalDualOnline.SkiRental.fractional_competitive), which is a different model and contains no lower bound. A complete formalization produces a reusable model of randomized on-line algorithms with history-dependent decisions and an exact lower bound for them.

Difficulty

The upper bound per lock wait is an explicit computation. The difficulty lies elsewhere. First, the on-line algorithm is allowed to adapt to the release times of all previous waits, so a bound for a single wait does not by itself bound a sequence: the randomized algorithm must be assembled so that each wait is handled with the right blocking law, whatever happened before. Second, the lower bound is a statement about every randomized algorithm and must survive the additive constant $a$: a single hard lock wait proves nothing, because $a$ absorbs any bounded loss. It has to be shown that on long sequences of waits every algorithm loses a factor $e/(e-1)$ on average. The natural first idea, to exhibit one bad release time for each algorithm, fails for randomized algorithms facing an oblivious adversary.

Formalization scope

All objects live in the namespace NonuniformCompetitive.SpinBlock. Release times are ℝ≥0, blocking times ℝ≥0∞, wait costs ℝ≥0∞, and the off-line cost is real. Committed conventions:

• $C>0$ is a hypothesis of every theorem (the paper's "some large cost $C$"); at $C=0$ blocking at once is free and the lower bound fails.
• A tie $b=\tau$ costs $\tau$; this matches "$\pi(t)$ is the probability that the algorithm blocks sometime before time $t$".
• Inputs are finite sequences of lock waits and competitiveness carries the additive constant $a$ of §1 (p. 543). A formalization with a single wait and no additive constant would be a different, easier lower bound and is ruled out.
• The on-line algorithm sees the release times of earlier waits (the information used by the paper's adaptive algorithms, p. 561). This enlarges the class of algorithms: it strengthens the lower bound and does not affect the upper bound.
• A randomized algorithm is a mixed strategy whose cost on each fixed input is measurable in the random outcome; the expected cost is a lower Lebesgue integral. Without measurability the lower integral would not be the expectation and the upper bound would become easier than the paper's.
• Milestone 1 is stated for every blocking law, not only for the paper's $\pi$. Milestone 2 keeps the paper's inequality, although equality holds.

Infrastructure a complete development needs: Lebesgue integrals of functions of a random variable (the layer-cake formula), interval integrals of the exponential, the construction of a probability measure on $[0,\infty]$ with a prescribed continuous distribution function, and a Yao-type averaging argument over finitely supported input distributions for the lower bound. The model of randomized on-line algorithms with history-dependent decisions is reusable for other rent-or-buy problems. Contributions welcome: proofs of the milestones, and intermediate lemmas such as the discretised lower bound for a fixed step $C/p$.

Selected references

• A. R. Karlin, M. S. Manasse, L. A. McGeoch, S. Owicki, Competitive Randomized Algorithms for Nonuniform Problems, Algorithmica 11 (1994), 542–571. doi:10.1007/BF01189993
• A. R. Karlin, M. S. Manasse, L. Rudolph, D. D. Sleator, Competitive Snoopy Caching, Algorithmica 3 (1988), 79–119. doi:10.1007/BF01762111
• A. Borodin, R. El-Yaniv, Online Computation and Competitive Analysis, Cambridge University Press, 1998.
• A. R. Karlin, C. Kenyon, D. Randall, Dynamic TCP Acknowledgement and Other Stories about e/(e−1), STOC 2001, 502–509. doi:10.1145/380752.380845
• N. Buchbinder, J. Naor, The Design of Competitive Online Algorithms via a Primal–Dual Approach, Foundations and Trends in Theoretical Computer Science 3 (2009). doi:10.1561/0400000024

Why the endpoint behaviour of Sturm–Liouville operators matters

A quantum particle on a line or half-line, and the radial part of a particle in a spherically symmetric potential, are described by a Sturm–Liouville expression

$$\tau f = \frac{1}{r}\big(-(pf')' + qf\big)$$

on an interval $I = (a, b)$. The expression alone does not define a Hamiltonian: a self-adjoint operator needs a domain, and on a general interval the choice of domain is a choice of boundary conditions at $a$ and $b$. Whether a boundary condition is needed at all depends on the behaviour of $\tau$ near the endpoint. H. Weyl settled this in 1910 (Math. Ann. 68, 220–269) with his limit circle / limit point dichotomy: at each endpoint either all solutions of $\tau u = z u$ are square integrable near it and a boundary condition must be imposed, or they are not and no condition is possible. This mission formalizes Sections 9.1–9.2 of G. Teschl, Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), which develop the theory for coefficients that are only locally integrable, and culminate in Theorem 9.9, the Weyl alternative.

Setting

Let $-\infty \le a < b \le \infty$ and $I = (a,b)$. The coefficients satisfy: $p^{-1} \in L^1_{loc}(I)$ with $p > 0$; $q \in L^1_{loc}(I)$ real-valued; $r \in L^1_{loc}(I)$ with $r > 0$. The Hilbert space is $L^2(I, r\,dx)$ with $\langle f, g\rangle = \int_a^b f^* g\, r\,dx$.

A function $f$ is locally absolutely continuous, $f \in AC_{loc}(I)$, if it is an indefinite integral of a locally integrable function on $I$. The equation $\tau f = g$ means that $f$ and its quasi-derivative $pf'$ both lie in $AC_{loc}(I)$ and $-(pf')' + qf = rg$ almost everywhere. A solution of $(\tau - z)u = 0$, $z \in \mathbb{C}$, is a complex-valued $u$ with $\tau u = z u$ in this sense. The maximal domain is

$$\mathfrak{D}(\tau) = \{ f \in L^2(I, r\,dx) \mid f, pf' \in AC_{loc}(I),\ \tau f \in L^2(I, r\,dx) \}.$$

The modified Wronskian is $W_x(f_1, f_2) = f_1(x)(pf_2')(x) - (pf_1')(x) f_2(x)$, with no complex conjugation, and $W_a(f_1, f_2) = \lim_{x \to a} W_x(f_1, f_2)$, $W_b$ likewise.

$\tau$ is limit circle (l.c.) at $a$ if there is a $v \in \mathfrak{D}(\tau)$ with $W_a(v^*, v) = 0$ and $W_a(v, f) \ne 0$ for some $f \in \mathfrak{D}(\tau)$; otherwise it is limit point (l.p.) at $a$. The same holds at $b$. A function $u$ is square integrable near $a$ if $\int_a^c |u|^2 r\,dx < \infty$ for some $c \in I$.

Formalization targets

Goal: the Weyl alternative (Theorem 9.9)

For every Sturm–Liouville expression as above,

$$\tau \text{ is l.c. at } a \iff \text{for one } z_0 \in \mathbb{C}, \text{ all solutions of } (\tau - z_0)u = 0 \text{ are square integrable near } a,$$

and if $\tau$ is l.c. at $a$, then for every $z \in \mathbb{C}$ all solutions of $(\tau - z)u = 0$ are square integrable near $a$. The same two statements hold at $b$.

Milestones

1. Theorem 9.1. For $rg \in L^1_{loc}(I)$, $c \in I$, $\alpha, \beta \in \mathbb{C}$, the problem $(\tau - z) f = g$, $f(c) = \alpha$, $(pf')(c) = \beta$ has a unique solution, entire in $z$.
2. Lemma 9.2. If $u_1, u_2$ solve $(\tau - z)u = 0$ with $W(u_1, u_2) = 1$, every solution of $(\tau - z)f = g$ is given by the variation-of-constants formula (9.10).
3. Eq. (9.7). For $f, g \in \mathfrak{D}(\tau)$ the limits $W_a(g^*, f)$, $W_b(g^*, f)$ exist and $\langle g, \tau f\rangle = W_a(g^*, f) - W_b(g^*, f) + \langle \tau g, f\rangle$ (the printed $W_b - W_a$ has the wrong sign for the Wronskian (9.5)).
4. Lemma 9.5. If $v \in \mathfrak{D}(\tau)$, $W_a(v^*, v) = 0$ and $W_a(v^*, \hat f) \ne 0$ for some $\hat f \in \mathfrak{D}(\tau)$, then $W_a(v, f) = 0 \Leftrightarrow W_a(v, f^*) = 0$, and $W_a(v, f) = W_a(v, g) = 0 \Rightarrow W_a(g^*, f) = 0$.
5. Theorem 9.6. The operator $Af = \tau f$ on $\mathfrak{D}(A) = \{ f \in \mathfrak{D}(\tau) \mid W_a(v, f) = 0 \text{ if l.c. at } a,\ W_b(w, f) = 0 \text{ if l.c. at } b\}$ is self-adjoint, and the set $\mathfrak{D}_1$ of (9.21) is a core.
6. Lemma 9.7. For $z \in \rho(A)$ there are solutions $u_a$, $u_b$ of $(\tau - z)u = 0$, square integrable near $a$ resp. $b$ and satisfying the boundary condition there, and $(A - z)^{-1}$ is the integral operator with the Green function (9.28).

Significance

The Weyl alternative turns a question about operators into a question about an ordinary differential equation. Whether a Schrödinger operator $-d^2/dx^2 + q$ on a half-line needs a boundary condition at infinity, or whether $-\Delta + V$ with a radial potential is essentially self-adjoint on smooth functions, reduces to checking square integrability of solutions for a single value of $z$. Combined with Theorem 9.6 it classifies the self-adjoint realizations with separated boundary conditions: none at an l.p. endpoint, a one-parameter family at an l.c. endpoint. The Green function of Lemma 9.7 is the starting point of the spectral theory of one-dimensional Schrödinger operators: Weyl–Titchmarsh $m$-functions, spectral transformations, and oscillation theory in the rest of Teschl's Chapter 9.

The results are classical and proved in many textbooks. The formal content is new: Mathlib has unbounded operators (LinearPMap) and their adjoints, but no Sturm–Liouville theory, no quasi-derivatives, no ODE existence theorem for measurable, locally integrable coefficients (its Picard–Lindelöf theorem needs Lipschitz right-hand sides), and no self-adjoint realizations of differential operators on general intervals.

Difficulty

The definition of limit circle refers only to $\mathfrak{D}(\tau)$ and boundary limits of Wronskians, while the conclusion is about all solutions of an ODE for all $z \in \mathbb{C}$. The two sides are linked only through self-adjoint operators: the passage from boundary Wronskians to square integrable solutions goes through the resolvent of a self-adjoint realization, which exists only for $z \in \rho(A)$, and so only for nonreal $z$ in general. Extending the conclusion to real $z$, where no resolvent is available, needs an argument of a different kind. On the ODE side, the coefficients are only locally integrable, so solutions are merely locally absolutely continuous, equations hold only almost everywhere, and every boundary quantity is a limit whose existence must itself be established.

Formalization scope

• Interval and coefficients. The structure SLData bundles $a, b \in$ EReal with $a < b$ (infinite endpoints allowed), $p, q, r : \mathbb{R} \to \mathbb{R}$, and the standing hypotheses (i)–(iii) of p. 181; $p, r > 0$ pointwise on $I$. $L^2(I, r\,dx)$ is Lp ℂ 2 for the measure $r\,dx$ on $I$.
• Regularity. $AC_{loc}(I)$ is encoded by its integral characterization. The quasi-derivative $pf'$ is the continuous function $f^{[1]} \in AC_{loc}(I)$ with $f(y) - f(x) = \int_x^y f^{[1]}/p$, chosen by Classical.choose (it is unique on $I$). $\tau f = g$ is $(pf')(y) - (pf')(x) = \int_x^y (qf - rg)$ with a local integrability clause. No smoothness of the coefficients and no $C^2$ solutions are assumed.
• Boundary Wronskians $W_a$, $W_b$ are Filter.limUnder along $x \to a$, $x \to b$ inside $I$. They are used only on $\mathfrak{D}(\tau)$, where milestone (9.7) states that the limits exist. In Lemma 9.7, where $u_a$ need not lie in $\mathfrak{D}(\tau)$, the boundary condition is stated as a convergence.
• Operators. Operators in $L^2(I, r\,dx)$ are LinearPMaps; self-adjointness is Mathlib's IsSelfAdjoint. Theorem 9.6 asserts that an operator with graph $\{(f, \tau f) \mid f \in \mathfrak{D}(A)\}$ exists (i.e. is well defined) and is self-adjoint. $\rho(A)$ and $(A - z)^{-1}$ follow Teschl (2.66): a bounded two-sided inverse of $A - z$. No projection-valued measure or functional calculus is used.
• Corrections to the printed text. Lemma 9.7 says "a solution $u_a$ of $(\tau - z)u = g$"; the proof and (9.28) need $(\tau - z)u = 0$, which is what is stated. The condition at an endpoint in (9.21) is imposed only where $\tau$ is l.c., as in (9.20). The second line of (9.10) is stated for quasi-derivatives. The boundary term of (9.7) is printed as $W_b(g^*, f) - W_a(g^*, f)$; integration by parts with (9.5) gives $W_a(g^*, f) - W_b(g^*, f)$ (check: $p = r = 1$, $q = 0$ on $(0,1)$, $f = x^2$, $g = 1$), and the corrected identity is stated.
• Ruling out trivialization. Limit circle is the Wronskian notion of p. 187, never "all solutions are square integrable", which would make the goal circular. The goal has no hypothesis beyond the standing assumptions on $p, q, r$.

A complete development needs a Carathéodory-type existence theorem for linear first-order systems with $L^1_{loc}$ coefficients, the Lagrange identity with its boundary limits, Lemma 9.3 (a linear-algebra fact about functionals) and the computation of the closure and adjoint of the minimal operator (Lemma 9.4). The ODE layer and the $L^2(I, r\,dx)$ operator layer can be reused for the Weyl–Titchmarsh theory, oscillation theory (Sec. 9.7) and one-particle Schrödinger operators (Ch. 10). Contributions that build them as general lemmas are welcome.

Selected references

• G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, AMS Graduate Studies in Mathematics 99, 2009, Sections 9.1–9.2. https://doi.org/10.1090/gsm/099
• H. Weyl, "Über gewöhnliche Differentialgleichungen mit Singularitäten und die zugehörigen Entwicklungen willkürlicher Funktionen", Math. Ann. 68 (1910), 220–269. https://doi.org/10.1007/BF01474161
• J. Weidmann, Spectral Theory of Ordinary Differential Operators, Lecture Notes in Mathematics 1258, Springer, 1987. https://doi.org/10.1007/BFb0077960
• A. Zettl, Sturm–Liouville Theory, Mathematical Surveys and Monographs 121, AMS, 2005. https://doi.org/10.1090/surv/121

Motivation

Approximate policy iteration and policy gradient methods are the two classical families of reinforcement learning algorithms that work with approximate, sampled information instead of an exact model. Kakade and Langford (ICML 2002) observed that neither family answers three basic questions: is there a performance measure that is guaranteed to improve at every step, how hard is it to verify that an update improves it, and what performance is reached after a reasonable number of updates. Greedy approximate policy iteration can make the policy worse when the value estimates are slightly wrong at a few states, and policy gradient methods can stall on plateaus where estimating the gradient needs an enormous number of samples.

Their answer is conservative policy iteration: instead of jumping to a greedy policy, move only a controlled fraction of the way toward it, with a step size chosen from an estimate of how much the greedy policy helps. The paper proves that this update improves a restart-distribution performance measure monotonically, terminates after a number of iterations that depends only on the reward range and the target accuracy, and stops at a policy that the greedy oracle can no longer improve by much. The idea is the direct ancestor of trust-region and proximal policy optimization methods (TRPO, Schulman et al. 2015; PPO, Schulman et al. 2017), whose improvement bounds are refinements of the paper's Theorem 4.1.

Setting

A finite Markov decision process has a finite nonempty set of states $S$, a finite nonempty set of actions $A$, transition probabilities $P(s';s,a)$ (for each state $s$ and action $a$, a probability distribution over next states $s'$), a reward function $\mathcal R : S\times A\to[0,R]$ with $R>0$, and a discount factor $0\le\gamma<1$. A stochastic policy $\pi(a;s)$ gives, for each state $s$, a probability distribution over actions.

The normalized value of $\pi$ from $s$ is $V_\pi(s) = (1-\gamma)E[\sum_{t\ge0}\gamma^t\mathcal R(s_t,a_t)\mid\pi,s]$, where $s_0=s$, $a_t\sim\pi(\cdot\,;s_t)$, $s_{t+1}\sim P(\cdot\,;s_t,a_t)$; it lies in $[0,R]$. The state-action value is $Q_\pi(s,a) = (1-\gamma)\mathcal R(s,a)+\gamma E_{s'\sim P(s';s,a)}[V_\pi(s')]$ and the advantage is $A_\pi(s,a) = Q_\pi(s,a)-V_\pi(s)\in[-R,R]$.

For a state distribution $\mu$ (a restart distribution), the discounted future state distribution is $d_{\pi,\mu}(s) = (1-\gamma)\sum_{t\ge0}\gamma^t\Pr(s_t=s;\pi,\mu)$ (eq. (2.1)), and the performance measure is $\eta_\mu(\pi) = E_{s\sim\mu}[V_\pi(s)]$.

The policy advantage of a policy $\pi'$ with respect to $\pi$ and $\mu$ is

$$\mathbb A_{\pi,\mu}(\pi') = E_{s\sim d_{\pi,\mu}}\big[E_{a\sim\pi'(a;s)}[A_\pi(s,a)]\big],$$

and $\mathrm{OPT}(\mathbb A_{\pi,\mu}) = \max_{\pi'}\mathbb A_{\pi,\mu}(\pi')$. The conservative update (4.1) is $\pi_{new} = (1-\alpha)\pi+\alpha\pi'$ with $\alpha\in[0,1]$. An $\varepsilon$-greedy policy chooser $G_\varepsilon$ (Definition 4.3) returns, for every policy $\pi$, a policy $\pi'$ with $\mathbb A_{\pi,\mu}(\pi')\ge\mathrm{OPT}(\mathbb A_{\pi,\mu})-\varepsilon$.

Conservative policy iteration (§5) starts from any policy and repeats: call $G_\varepsilon(\pi,\mu)$ to get $\pi'$; form an $\frac\varepsilon3$-accurate estimate $\hat{\mathbb A}$ of $\mathbb A_{\pi,\mu}(\pi')$ from $\mu$-restarts; if $\hat{\mathbb A}<\frac{2\varepsilon}3$, stop and return $\pi$; otherwise apply (4.1) with $\alpha = \frac{(1-\gamma)(\hat{\mathbb A}-\varepsilon/3)}{4R}$ and repeat.

Formalization targets

Goal: Theorem 4.4 (p. 5)

With probability at least $1-\delta$, conservative policy iteration (i) strictly improves $\eta_\mu$ with every policy update, (ii) stops after at most $72R^2/\varepsilon^2$ policy updates, and (iii) returns a policy $\pi$ with

$$\mathrm{OPT}(\mathbb A_{\pi,\mu}) < 2\varepsilon.$$

The estimation step is represented by its guarantee: each reached loop's estimate fails to be $\frac\varepsilon3$-accurate with probability at most $\delta/(N+1)$, $N=\lfloor72R^2/\varepsilon^2\rfloor$.

Milestones

Lemma 6.1 (p. 6), the performance difference identity:

$$\eta_\mu(\tilde\pi)-\eta_\mu(\pi) = \frac1{1-\gamma}E_{(a,s)\sim\tilde\pi d_{\tilde\pi,\mu}}[A_\pi(s,a)].$$

Theorem 4.1 (p. 4), with $\varepsilon=\max_s|E_{a\sim\pi'(a;s)}[A_\pi(s,a)]|$ and all $\alpha\in[0,1]$:

$$\eta_\mu(\pi_{new})-\eta_\mu(\pi)\ge\frac{\alpha}{1-\gamma}\Big(\mathbb A-\frac{2\alpha\gamma\varepsilon}{1-\gamma(1-\alpha)}\Big).$$

Corollary 4.2 (p. 5): if $\mathbb A\ge0$, the step size $\alpha=\frac{(1-\gamma)\mathbb A}{4R}$ gives

$$\eta_\mu(\pi_{new})-\eta_\mu(\pi)\ge\frac{\mathbb A^2}{8R}.$$

Significance

Theorem 4.4 is the first guarantee of its kind for approximate reinforcement learning: the number of iterations is bounded by $72R^2/\varepsilon^2$, independent of the number of states and of the restart distribution, and every iteration provably helps. Lemma 6.1 is the standard performance difference lemma, used throughout the analysis of policy optimization, including natural policy gradient and trust-region methods; Theorem 4.1 is the prototype of the "surrogate objective minus a penalty" bound that TRPO refines.

These results are proved in the paper. As far as a search of the platform shows, none is formalized: the platform's finite-horizon performance difference lemma (Foster and Rakhlin's Lemma 13) is a different statement, for episodic problems with non-stationary policies. This mission produces machine-checked versions of the discounted performance difference identity, the conservative improvement bound with its exact constants, and the high-probability termination and quality guarantee of the algorithm, all on top of an explicit infinite-horizon model rather than an assumed Bellman equation.

Difficulty

The obvious argument for the improvement bound expands $\eta_\mu(\pi_{new})$ to first order in $\alpha$; that only gives $\frac{\alpha}{1-\gamma}\mathbb A+O(\alpha^2)$ with an unspecified constant, which cannot fix a step size. The exact bound needs control of how far the state distribution of the mixed policy drifts from that of the old policy, uniformly in time, and the performance difference identity is only useful once the states are weighted by the new policy's distribution. On the formal side, $V_\pi$ and $d_{\pi,\mu}$ are infinite discounted series, so summability, exchanges of sums and the identities $\sum_s d_{\pi,\mu}(s)=1$ and $\sum_a\pi(a;s)A_\pi(s,a)=0$ must all be established from the definitions. For Theorem 4.4, the algorithm is a random process whose policies depend on all earlier estimates; the argument has to be made pathwise on the event that every reached loop is accurate, together with a union bound over the loops that can be reached.

Formalization scope

Policies are functions π : S → A → ℝ with π s a the paper's $\pi(a;s)$, and P s a s' is $P(s';s,a)$; both are constrained by the published predicates IsPolicy and IsTransitionKernel. $V_\pi$ is $(1-\gamma)$ times the published series PolicyValue, so values are normalized as in the paper. $\mathrm{OPT}$ is a real supremum over all stochastic policies; the set is nonempty and bounded, and the maximum is attained. Every theorem carries the standing assumptions of §2: finite nonempty $S$ and $A$, a transition kernel, rewards in $[0,R]$ with $R>0$, $0\le\gamma<1$, and a state distribution $\mu$. In Corollary 4.2, $R$ is any upper bound on the rewards rather than necessarily the attained maximum.

In Theorem 4.4 the run is formalized pathwise, driven by arbitrary real random estimates on a probability space; the conclusion bounds the probability of the failure event by $\delta$. Two deviations from the printed statement are disclosed. First, (ii) is stated for policy updates: the proof bounds updates, and the algorithm calls $G_\varepsilon$ once more than it updates, so "at most $72R^2/\varepsilon^2$ calls" is off by one. Second, the per-loop failure budget is $\delta/(N+1)$, which covers the $N+1$ loops that may be reached. The Hoeffding estimate (5.1) is not formalized: as printed it concerns the $\frac\varepsilon6$-biased target, and its role is taken by the accuracy hypothesis. The step size is clipped at $1$, which never binds when the estimate is accurate. No trivializing reading is available: the accuracy hypothesis is satisfied by a perfect estimator and a $0$-greedy chooser exists, so the theorem is not vacuous, and strict improvement at every update is required, not merely nonnegative change.

Pages are PDF pages; the paper has no printed page numbers.

A complete development needs summability and algebra of discounted occupation measures, the performance difference identity, and a union bound over the loops of a random process; the first two are reusable for any discounted policy-optimization result. Proofs of the milestones in any order are welcome.

Selected references

• S. Kakade and J. Langford, Approximately Optimal Approximate Reinforcement Learning, Proceedings of the 19th International Conference on Machine Learning (ICML), 2002. https://dl.acm.org/doi/10.5555/645531.656005
• J. Schulman, S. Levine, P. Moritz, M. Jordan, P. Abbeel, Trust Region Policy Optimization, ICML 2015. https://arxiv.org/abs/1502.05477
• J. Schulman, F. Wolski, P. Dhariwal, A. Radford, O. Klimov, Proximal Policy Optimization Algorithms, 2017. https://arxiv.org/abs/1707.06347
• D. J. Foster and A. Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making, 2023. https://arxiv.org/abs/2312.16730

Motivation

A two-machine flow shop is the simplest multi-stage production system: every job visits machine 1 and then machine 2, each machine works on one job at a time, and the goal is to finish all jobs as early as possible. S. M. Johnson's 1954 paper (Naval Research Logistics Quarterly 1(1):61–68, doi:10.1002/nav.3800010110) answered this question, posed by R. Bellman, with an exact rule, now called Johnson's rule. It is one of the first exact results in machine scheduling. In the three-field notation of Graham, Lawler, Lenstra and Rinnooy Kan (1979) the problem is written $F2\,\|\,C_{\max}$. The rule is the standard polynomial case against which the NP-hardness of the three-machine flow shop (Garey, Johnson and Sethi 1976) is contrasted, and it is still used inside heuristics for larger shops.

Timeline:

• 1954. Johnson proves the two-machine rule and a three-machine special case (the latter is the second mission of this series).
• 1976. Garey, Johnson and Sethi prove that the three-machine flow shop is NP-hard in the strong sense, so the two-machine case marks the boundary of tractability.

Setting

There are $n$ items $i = 1, \dots, n$. Item $i$ needs $A_i > 0$ units of time on machine 1 and then $B_i > 0$ units on machine 2. Each time is setup time plus work time, and the times are otherwise arbitrary. A schedule assigns start times $s^1_i$ and $s^2_i$. It is feasible when all start times are nonnegative, the intervals $[s^1_i, s^1_i + A_i]$ of distinct items do not overlap on machine 1, the intervals $[s^2_i, s^2_i + B_i]$ do not overlap on machine 2, and $s^1_i + A_i \le s^2_i$ for every item. The total elapsed time $T(s) = \max_i (s^2_i + B_i)$ is the time at which the last item leaves machine 2.

An order is a permutation $\sigma$, where $\sigma(k)$ is the item in position $k$. The as-soon-as-possible schedule $a_\sigma$ of an order processes the items in the order $\sigma$ on both machines, with no delay on machine 1. Each item starts on machine 2 as soon as it has left machine 1 and machine 2 is free.

Relation (II). Item $i$ is definitely preferred to item $j$ when

$$\min(A_i, B_j) < \min(A_j, B_i),$$

and the two items are indifferent when equality holds. An order is consistent with all the definite preferences when no item is definitely preferred to an item placed earlier.

For an order $\sigma$ the paper uses the quantities

$$K_u = \sum_{l \le u} A_{\sigma(l)} - \sum_{l < u} B_{\sigma(l)}, \qquad F(\sigma) = \max_u K_u .$$

Formalization targets

Goal: Theorem 1 (p. 63)

For positive $A, B$:

$$\exists\, \sigma \text{ consistent with (II)}, \qquad\text{and}\qquad \forall\, \sigma \text{ consistent with (II)},\ \forall\, s \text{ feasible}:\quad a_\sigma \text{ is feasible and } T(a_\sigma) \le T(s).$$

The comparison is against every feasible schedule, including those whose two machines follow different orders.

Milestones

1. Lemma 1 (p. 61). Every feasible schedule can be replaced, at no greater total elapsed time, by a feasible schedule that follows one common order on both machines.
2. As soon as possible (p. 62). For a fixed common order, $a_\sigma$ is feasible and minimizes $T$ among the feasible schedules that follow $\sigma$.
3. Closed form (p. 62). $T(a_\sigma) = \sum_i B_i + F(\sigma)$, i.e. the total idle time of machine 2 is $\max_u K_u$.
4. Adjacent interchange (p. 63). Interchanging the items in positions $j, j+1$ leaves every other $K_u$ unchanged. Moreover, $\max(K_j, K_{j+1}) < \max(K'_j, K'_{j+1})$ holds if and only if (II) holds for the pair.
5. Interchanges do not increase $F$ (p. 63). If the pair in positions $j, j+1$ satisfies (II) non-strictly, then $F(\sigma) \le F(\sigma')$.
6. Lemma 2 (p. 64). Relation (II) is transitive, except when the middle item is indifferent to both others.
7. Worked example (p. 65). For $A = (4,4,30,6,2)$ and $B = (5,1,4,30,3)$, the order $(5,1,4,3,2)$ takes 47 units with 4 units of idle time. The reversed order takes 78 units, and every order takes between 47 and 78 units.

Significance

The theorem reduces an optimization over a continuum of start-time vectors, and over $n!$ orders, to sorting with respect to a pairwise relation. The paper's working rule computes an optimal order in $O(n \log n)$ time. The two-machine rule is the building block of Johnson's three-machine result, of the Campbell–Dudek–Smith heuristic for $m$ machines, and of lower bounds in branch-and-bound methods for flow shops. The closed form $T(a_\sigma) = \sum_i B_i + \max_u K_u$ reappears across flow-shop theory as a longest-path formula.

The result is classical and proved. This mission contributes a machine-checked proof in Lean 4 against Mathlib. As far as a search of the platform shows, no formal statement of the flow-shop model or of Johnson's rule exists there. The mission also fixes a reusable Lean model of a two-machine schedule: start times, feasibility, total elapsed time and the as-soon-as-possible schedule of an order.

Difficulty

The paper's argument leaves two steps informal, and a formal proof must supply both. First, Lemma 1 is justified by a picture and the phrase "successive interchanges". The page does not show that each interchange keeps the schedule feasible and does not delay the last completion on machine 2, and this is where most of the modelling work sits. Second, relation (II) is not a strict weak order when there are ties, so the obvious sorting argument fails. Consistency on adjacent pairs does not imply optimality: the items $(A, B) = (5,2), (1,1), (2,5)$, in that order, satisfy (II) non-strictly on both adjacent pairs, yet take 13 units against an optimum of 10. Lemma 2's exception is exactly this case.

Formalization scope

Items are Fin n (0-based) and times are real numbers. Positivity $A_i > 0$, $B_i > 0$ is a hypothesis of the goal and of Lemma 1, the as-soon-as-possible step and the closed form, as on p. 61. Lemma 2 and the interchange statements are pure min/sum algebra and carry no positivity. An order is σ : Equiv.Perm (Fin n) with σ k the item in position k. Interchanging positions $j, j+1$ is σ * Equiv.swap j (j+1). The total elapsed time is Finset.univ.fold max 0 of the machine-2 completion times, so it is $0$ when $n = 0$. $K_u$ is indexed by 0-based positions (Lean's $K_u$ is the paper's $K_{u+1}$), and $F$ requires $n \ge 1$.

Conventions made explicit or corrected:

• "Consistent with all the definite preferences" is imposed on all pairs of positions $k < l$ as the non-strict inequality $\min(A_{\sigma(k)}, B_{\sigma(l)}) \le \min(A_{\sigma(l)}, B_{\sigma(k)})$. The goal also asserts that such an order exists, so its main clause is not vacuous.
• The display of $K'_u$ on p. 63 prints the upper limit $u$ on the $B'$-sum. The definition of $K_u$ on p. 62 and the reduction of (I) to (II) require $u-1$, and the formalization uses $u-1$.
• Lemma 2 keeps the page's exception (item 2 indifferent to both items); without it the statement is false.

Measuring the objective by $F(\sigma)$, or comparing only against schedules that follow one common order, would drop Lemma 1 and change the theorem. The goal compares against every feasible start-time schedule. The working rule of p. 64 (a procedure) is not formalized.

Proofs of any milestone are welcome, as are further lemmas about the as-soon-as-possible schedule and a formalization of the working rule. The schedule definitions are the basis for the three-machine mission of this series.

Selected references

• S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1):61–68, 1954. doi:10.1002/nav.3800010110
• M. R. Garey, D. S. Johnson, R. Sethi, The complexity of flowshop and jobshop scheduling, Mathematics of Operations Research 1(2):117–129, 1976. doi:10.1287/moor.1.2.117
• R. L. Graham, E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5:287–326, 1979. doi:10.1016/S0167-5060(08)70356-X
• H. G. Campbell, R. A. Dudek, M. L. Smith, A heuristic algorithm for the n job, m machine sequencing problem, Management Science 16(10):B630–B637, 1970. doi:10.1287/mnsc.16.10.B630