All missions

Motivation

Paging is the problem of managing a two-level memory: a cache holds $k$ of the $n$ pages a program uses, every request must find its page in the cache, and a request to a page outside the cache (a page fault) forces the algorithm to bring the page in and evict another. An on-line algorithm chooses what to evict without seeing future requests. Sleator and Tarjan (CACM 1985) measured on-line paging algorithms against the optimal off-line algorithm, which knows the whole request sequence, and showed that no deterministic on-line algorithm can be within a factor smaller than $k$ of it.

Randomization changes that picture. Fiat, Karp, Luby, McGeoch, Sleator and Young (J. Algorithms 1991; arXiv:cs/0205038) gave a randomized algorithm, the marking algorithm, whose expected number of faults is within $2H_k$ of the optimum, where $H_k = 1 + \tfrac12 + \dots + \tfrac1k \approx \ln k$. This mission formalizes the other half of their paper's picture: no randomized paging algorithm can do better than $H_k$. The bound says that the logarithmic behaviour is not an artefact of one algorithm but a property of the problem.

Timeline:

• 1985 — Sleator and Tarjan: deterministic paging algorithms have competitive factor at least $k$; LRU and FIFO achieve $k$.
• 1988 — Karlin, Manasse, Rudolph and Sleator (Algorithmica 3, 1988) introduce the term competitive; Manasse, McGeoch and Sleator (STOC 1988; J. Algorithms 1990) extend it to randomized algorithms and pose the $k$-server problem, of which paging is the uniform-metric case.
• 1991 — Fiat et al.: the marking algorithm is $2H_k$-competitive, and no randomized algorithm is better than $H_k$-competitive (Theorem 4 and Corollary 5 of the paper). Raghavan gave an alternative proof of the lower bound through Yao's minimax principle.
• 1991 — McGeoch and Sleator give an $H_k$-competitive randomized paging algorithm (Algorithmica 6, 1991), so the lower bound is tight.

Setting

Let $M$ be a set of $n$ vertices with the uniform metric: any two distinct vertices are at distance $1$. A configuration of $k$ servers is a map $C : \{1,\dots,k\} \to M$; server $s$ sits at $C(s)$, and a vertex is covered when some server sits on it. A request sequence $\sigma$ is a finite list of vertices. A deterministic on-line algorithm assigns to every prefix of requests the configuration after serving it, in such a way that the vertex just requested is covered; its cost on $\sigma$ is the total distance travelled by its servers, which on the uniform metric is the number of server moves. Paging with $k$ cache slots and $n$ pages is exactly this $k$-server problem on $n$ uniform vertices.

The optimal off-line cost $\mathrm{OPT}_{C_0}(\sigma)$ is the least cost of any schedule of configurations that starts at $C_0$ and covers each request of $\sigma$ in turn.

A randomized on-line algorithm $A$ is a probability space $(\Omega,\mu)$ of coin outcomes together with a deterministic on-line algorithm $A_\omega$ for each outcome $\omega$. Its expected cost $C_A(\sigma)$ is the average of the cost of $A_\omega$ on $\sigma$ over $\omega$. The request sequence is fixed in advance and does not depend on the coins (an oblivious adversary). Following the paper, $A$ is $c$-competitive from the initial configuration $C_0$ if there is a constant $a$ such that

$$C_A(\sigma) \;\le\; c \cdot \mathrm{OPT}_{C_0}(\sigma) + a \qquad \text{for every request sequence } \sigma .$$

For the lower-bound argument, the probability vector $p=(p_i)_{i\in M}$ after a prefix $\sigma$ has $p_i$ equal to the probability, over $\omega$, that vertex $i$ is not covered by $A_\omega$ after serving $\sigma$. A set $S$ of marked vertices and the number $u = n - |S|$ of unmarked vertices are bookkeeping of the adversary, updated as the marking algorithm would update them.

Formalization targets

Goal: Corollary 5

For $1 \le k \le n-1$, every randomized on-line algorithm $A$ with $k$ servers on $n$ uniform vertices, every initial configuration $C_0$ and every real $c$,

$$c < H_k \;\Longrightarrow\; A \text{ is not } c\text{-competitive from } C_0 .$$

Theorem 4 (milestone)

The case $k = n-1$: no randomized algorithm for the uniform $(n-1)$-server problem on $n$ vertices is $c$-competitive with $c < H_{n-1}$.

Claims of the proof of Theorem 4 (milestones)

With $p$ the probability vector, $S$ the marked set, $P = \sum_{i\in S} p_i$ and $u = n - |S|$:

$$\sum_i p_i = 1 \quad(\text{servers on distinct vertices}),\qquad C_A(\sigma\,i) \ge C_A(\sigma) + p_i,$$ $$P = 0 \Rightarrow \exists\, i\notin S,\ p_i \ge \tfrac1u, \qquad P > \epsilon > 0 \Rightarrow \max_{j\in S} p_j \ge \tfrac{\epsilon}{|S|} > 0,$$ $$p_j = \max_{j'\notin S} p_{j'} \Rightarrow p_j \ge \tfrac{1-P}{u}, \qquad P \le \epsilon \Rightarrow \epsilon + p_j \ge \epsilon + \tfrac{1-P}{u} \ge \epsilon + \tfrac{1-\epsilon}{u} \ge \tfrac1u .$$

Significance

The result. Together with the marking algorithm's $2H_k$ upper bound, the corollary pins the randomized competitive ratio of paging to $\Theta(\log k)$, an exponential improvement over the deterministic ratio $k$ that no randomized algorithm can push below $H_k$. For $k = n-1$ the marking algorithm itself is $H_{n-1}$-competitive, so Theorem 4 makes it optimal there. The $H_k$ bound is the benchmark every later randomized paging algorithm is measured against, including the $H_k$-competitive algorithm of McGeoch and Sleator, and it is the uniform-metric base case of the randomized $k$-server conjecture.

Formalizing it. The theorem is proved and classical; no machine-checked proof is known to exist. The platform already has the deterministic bound (KServer.uniform_not_competitive_below_k, ratio $k$) and a formal Yao averaging principle for randomized $k$-server algorithms (KServer.randomized_yao_averaging), but no randomized paging lower bound. This mission produces the first formal $H_k$ lower bound, stated against the published randomized $k$-server model, and a formal version of the paper's adversary argument. Either route — the paper's adaptive construction of a nemesis sequence from the probability vector, or Raghavan's distributional argument through Yao's principle — is welcome.

Difficulty

The adversary may not look at the coins, yet it must build one fixed sequence against which the expected cost is high in every phase. Requesting an uncovered vertex is not available, since which vertex is uncovered depends on the coins; requesting the vertex with the largest uncovered probability gives only $1/n$ per request and loses the harmonic sum. Lifting the per-phase bound to the asymptotic statement also requires handling the additive constant $a$, the initial configuration of the off-line algorithm, and, for Corollary 5, the reduction from $n$ vertices to $k+1$ of them for an algorithm that may still place servers on the others.

Formalization scope

The Lean development reuses the published definitions KServer_model (configurations Fin k → M, deterministic on-line algorithms as functions of the request prefix, offlineCost) and KServer_randomized (RandomizedAlgorithm: a probability measure on coin outcomes, a deterministic algorithm per outcome, measurable costs; expCost as a lower Lebesgue integral in $[0,\infty]$; IsCompetitiveFrom C₀ c: every drawn algorithm starts at $C_0$ and there is one constant $a$, fixed before the sequence, with expCost σ ≤ ENNReal.ofReal (c * offlineCost C₀ σ + a)). The clamp at $0$ in ENNReal.ofReal only weakens the property the goal refutes. The vertex set is an abstract type $M$ with an equivalence Fin n ≃ M and the uniform metric as a hypothesis, never the line metric of Fin n. $H_k$ is Mathlib's harmonic k cast to $\mathbb R$. The goal quantifies over every algorithm and every initial configuration, with no laziness or distinct-positions assumption, and over every real $c < H_k$, including $c \le 0$.

A formalization in which competitiveness is vacuous (a model with no algorithms, or a cost that is always infinite), in which the adversary may choose the sequence after seeing the coins, or which fixes $c$ or the additive constant, would be a different statement and is ruled out by the published definitions used here.

The probability vector is the one new definition, uncoveredProb A σ i. Milestones about it assume the uncovered events measurable, the standing convention that $p_i$ is a probability; the model itself only guarantees measurable costs. The milestone $\sum_i p_i = 1$ assumes the $n-1$ servers occupy distinct vertices, as in the paper; in general $\sum_i p_i \ge 1$. The arithmetic milestones are stated for an arbitrary probability vector on a finite set. Reusable pieces: the probability vector and the cost lemma apply to any randomized $k$-server algorithm on a uniform metric, and a restriction lemma (from $n$ vertices to $k+1$) would serve other paging lower bounds.

Selected references

• A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive Paging Algorithms, J. Algorithms 12(4):685–699, 1991. https://doi.org/10.1016/0196-6774(91)90041-V ; preprint arXiv:cs/0205038v1 (cited version). https://arxiv.org/abs/cs/0205038
• D. D. Sleator, R. E. Tarjan, Amortized Efficiency of List Update and Paging Rules, Comm. ACM 28(2):202–208, 1985. https://doi.org/10.1145/2786.2793
• M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive Algorithms for Server Problems, J. Algorithms 11(2):208–230, 1990. https://doi.org/10.1016/0196-6774(90)90003-W
• L. A. McGeoch, D. D. Sleator, A Strongly Competitive Randomized Paging Algorithm, Algorithmica 6:816–825, 1991.
• P. Raghavan, Lecture Notes on Randomized Algorithms, IBM Research Report, Yorktown Heights, 1990 (the alternative proof of the lower bound, pp. 118–119).

Motivation

Paging is the problem of managing a two-level memory: a fast cache holding $k$ pages and a slow memory holding the rest. When a requested page is not in the cache (a page fault), it must be brought in and, if the cache is full, some page must be evicted. An on-line paging algorithm decides which page to evict without knowing future requests. Sleator and Tarjan (CACM 1985) compared on-line algorithms with the optimal off-line algorithm on every request sequence and showed that the best deterministic algorithms (LRU, FIFO) lose a factor of exactly $k$, and that no deterministic on-line algorithm does better.

Randomization changes this picture. Fiat, Karp, Luby, McGeoch, Sleator and Young (J. Algorithms 1991; arXiv:cs/0205038) showed that the randomized marking algorithm is $2H_k$-competitive, where $H_k=1+\tfrac12+\dots+\tfrac1k$, and that no randomized algorithm is better than $H_k$-competitive. For $k<n-1$ the marking algorithm does not reach $H_k$, already for $k=2$ and $n=4$. For two servers the same paper gives a different algorithm, EATR ("end after twice requested"), and proves it $3/2$-competitive. Since $H_2=3/2$, EATR is strongly competitive for $k=2$: no randomized algorithm has a smaller competitive factor. This mission formalizes that result.

Timeline:

• 1985: Sleator and Tarjan, deterministic paging: factor $k$, and $k$ is optimal.
• 1988: Karlin, Manasse, Rudolph and Sleator introduce the term competitive (Algorithmica 3:79–119); Manasse, McGeoch and Sleator formulate the $k$-server problem and extend competitiveness to randomized algorithms (J. Algorithms 1990).
• 1991: Fiat et al.: the marking algorithm is $2H_k$-competitive, the lower bound $H_k$, and EATR is $3/2$-competitive for $k=2$.
• 1991: McGeoch and Sleator give an $H_k$-competitive algorithm for every $k$ (Algorithmica 6, 1991; reference [12] of the paper).

Setting

The uniform $2$-server problem has a finite set $M$ of $n\ge 2$ vertices, any two distinct vertices at distance $1$, and two servers. A request sequence $\sigma=\sigma(0),\sigma(1),\dots$ is a list of vertices; each request must be covered by a server when it is served, and the cost is the number of server moves. This is paging with a cache of two pages: vertices are pages and the covered vertices are the cache.

A deterministic algorithm $B$ has a cost $C_B(\sigma)$; a randomized algorithm $A$ has an expected cost $C_A(\sigma)$, averaged over its random choices. $A$ is $c$-competitive if there is a constant $a$ such that for every request sequence $\sigma$ and every deterministic algorithm $B$ (on-line or off-line),

$$C_A(\sigma)\le c\cdot C_B(\sigma)+a.$$

Algorithm EATR. The servers start on the vertices $1$ and $2$. The algorithm divides $\sigma$ into phases; the first phase starts at the first request to a vertex other than $1$ and $2$. Let $P$ be the set of vertices occupied by the servers at the end of the previous phase ($\{1,2\}$ before the first phase). During a phase, a vertex is clean if it is not in $P$ and has not been requested during this phase; a vertex is stale if it is neither clean nor the most recently requested vertex $\ell$. EATR keeps one server on $\ell$ and the other uniformly at random on the stale set. When a stale vertex $r$ is requested, the servers are placed on $\ell$ and $r$ and the phase ends; the next phase starts at the next request to a vertex not covered by a server. Requests between phases, and repeated requests to $\ell$, move nothing.

For a phase, $l$ denotes the number of clean vertices requested in it. For a deterministic algorithm $A$, $d$ and $d'$ denote the numbers of $A$'s servers that do not coincide with any of EATR's servers at the beginning and at the end of the phase. An algorithm is lazy if it moves no server on a request to a covered vertex and exactly one server on a request to an uncovered one.

Formalization targets

Goal: Theorem 3

With $\mathrm{OPT}(\sigma)$ the optimal off-line cost of serving $\sigma$ from the servers' starting position $(1,2)$, there is a constant $c$ such that for all $\sigma$

$$C_{\mathrm{EATR}}(\sigma)\le \tfrac32\,\mathrm{OPT}(\sigma)+c.$$

The constant $c$ is left free; the factor $3/2$ is the paper's and is optimal.

Milestones, in the order of the proof

1. Laziness (p. 4): every deterministic algorithm is dominated by a lazy one (a published theorem, reused).
2. Adversary bound for structured phases (p. 5): in a complete EATR phase with $l$ clean requests, a lazy $A$ pays at least $l-d+d'$.
3. Stale set before the terminating request (p. 6): it has $l+1$ elements, each covered with probability $1/(l+1)$.
4. Expected cost of a phase to EATR (p. 6): exactly $l+\frac{l}{l+1}$.
5. Per-phase ratio (p. 6): EATR's expected phase cost is at most $\tfrac32(C_A+d-d')$, since $\frac{l+l/(l+1)}{l}=1+\frac{1}{l+1}\le\frac32$.

Significance

The result. Theorem 3 settles the randomized competitive ratio of paging with two cache slots: combined with the paper's lower bound $H_k$ (Corollary 5, the subject of a companion mission), the optimal factor for $k=2$ is exactly $3/2$, against $2$ for every deterministic algorithm. The general case was settled later by McGeoch and Sleator's $H_k$-competitive partitioning algorithm, which is considerably more complicated.

Formalizing it. The result has been proved since 1991; no machine-checked proof of it is on the platform (a search for EATR, randomized paging and two-server results on 2026-09-26 found only deterministic $k$-server theorems). The mission produces a formal model of a randomized on-line algorithm as a probability distribution over states evolving with the request sequence, a formal treatment of the phase decomposition and of the telescoping amortization that relates expected on-line cost to the optimal off-line cost, and a first strongly competitive randomized paging result on the platform, alongside the deterministic $k$-server results already there.

Difficulty

The per-phase computations are short. The main difficulty is the global accounting. The adversary's cost in a phase is bounded only in amortized form, $l-d+d'$, where $d$ and $d'$ compare the adversary's servers with EATR's at the phase boundaries; the bound becomes a statement about $\mathrm{OPT}$ only after the $d$ and $d'$ terms telescope across phases. This needs care with the requests that lie outside every phase (before the first phase, between phases, and in an unfinished last phase), during which the adversary may move. A further difficulty is that the off-line optimum ranges over arbitrary schedules, which may move several servers on one request, while the phase bound is proved for lazy on-line algorithms: the reduction from one to the other must be made explicit. Finally, the uniform law of the stale server is an invariant of a Markov chain on states that must be tracked through the whole phase.

Formalization scope

The vertices are an abstract metric space $M$ with an enumeration $e:\mathrm{Fin}\,n\simeq M$, $2\le n$, and the hypothesis that distinct points are at distance $1$; the metric of $\mathrm{Fin}\,n$ is not used. The starting vertices $1,2$ are $e(0),e(1)$. $\mathrm{OPT}$ is KServer.offlineCost of the published KServer model: the infimum of total movement over all schedules serving $\sigma$ from $(e(0),e(1))$. Comparing with this infimum covers every deterministic $B$ starting from EATR's position; a $B$ starting elsewhere differs by at most $2$, which the constant absorbs. The constant is quantified before $\sigma$.

EATR is a PMF over states: a deterministic record (the set $P$, whether a phase is in progress, the last requested vertex, the vertices requested in the phase) and the random position of the second server. Its expected cost is the expected number of server moves, summed over the requests. The paper fixes only that the second server is uniform on the stale set; when a clean request enlarges the stale set, the formalization moves one server by a fixed coupling that keeps the law uniform, and this choice is stated in the definition. A formalization that defines EATR's expected cost by the closed formula of the proof, or that restricts $\sigma$ to complete phases, would make the goal a different statement; neither is done here. The pre-phase prefix and an unfinished last phase belong to $\sigma$ and are covered by the constant.

Needed infrastructure: finite probability distributions (Mathlib's PMF), the published KServer model and its laziness theorem, and bookkeeping lemmas on the deterministic phase record. The phase record and the amortization argument are reusable for the marking algorithm of the companion mission. Proofs of any milestone, and alternative decompositions of the goal, are welcome.

Selected references

• A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive Paging Algorithms, Journal of Algorithms 12(4):685–699, 1991. https://doi.org/10.1016/0196-6774(91)90041-V ; arXiv:cs/0205038v1, https://arxiv.org/abs/cs/0205038
• D. D. Sleator, R. E. Tarjan, Amortized Efficiency of List Update and Paging Rules, Communications of the ACM 28(2):202–208, 1985. https://doi.org/10.1145/2786.2793
• M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive Algorithms for Server Problems, Journal of Algorithms 11(2):208–230, 1990. https://doi.org/10.1016/0196-6774(90)90003-W
• L. A. McGeoch, D. D. Sleator, A Strongly Competitive Randomized Paging Algorithm, Algorithmica 6:816–825, 1991 (reference [12] of the paper).
• A. R. Karlin, M. S. Manasse, L. Rudolph, D. D. Sleator, Competitive Snoopy Caching, Algorithmica 3(1):79–119, 1988 (reference [9] of the paper).

Motivation

A risk measure assigns to a random financial position $X$ a capital requirement $\rho(X)$: the amount of cash that must be added to $X$ to make it acceptable. The axiomatic theory of convex risk measures (Föllmer–Schied 2002; Frittelli–Rosazza Gianin 2002) treats this number as computed with no information beyond the model. In practice a regulator or a risk manager revises the requirement as information arrives, so the requirement becomes a random variable measurable with respect to the information available at the time of measurement. Detlefsen and Scandolo (SFB 649 Discussion Paper 2005-006; published in Finance and Stochastics 9(4), 2005, doi:10.1007/s00780-005-0159-6) develop this conditional theory: axioms, a robust representation, and a treatment of dynamic risk measurement.

The entropic risk measure is the standard example of a convex risk measure that is not coherent. It is the capital requirement of an agent with exponential utility $u_\gamma(x)=1-e^{-\gamma x}$, and its penalty function in the robust representation is the relative entropy $\frac1\gamma H(Q\mid P)$ (Föllmer–Schied, Stochastic Finance, Example 4.60, as cited by the paper). Section 5 of the paper carries this example to the conditional setting and shows that its penalty is a conditional relative entropy. The same identity appears in dynamic entropic risk measures, exponential-utility indifference pricing and recursive utility, where one-period conditional entropic measures are composed over time.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$ and a sub-$\sigma$-algebra $\mathcal G\subseteq\mathcal F$, the information available at the time of measurement. $L^\infty$ is the space of essentially bounded random variables and $L^\infty_{\mathcal G}$ its $\mathcal G$-measurable part. All equalities and inequalities between random variables hold $P$-almost surely.

A conditional convex risk measure is a map $\rho:L^\infty\to L^\infty_{\mathcal G}$ that is translation invariant ($\rho(X+Z)=\rho(X)-Z$ for $Z\in L^\infty_{\mathcal G}$), monotone ($X\le Y\Rightarrow\rho(X)\ge\rho(Y)$), conditionally convex ($\rho(\Lambda X+(1-\Lambda)Y)\le\Lambda\rho(X)+(1-\Lambda)\rho(Y)$ for $\Lambda\in L^\infty_{\mathcal G}$, $0\le\Lambda\le1$), and satisfies $\rho(0)=0$.

The relevant probability models are

$$\mathcal P_{\mathcal G}=\{Q \text{ probability on } (\Omega,\mathcal F) : Q\ll P,\ Q(A)=P(A)\ \text{for all } A\in\mathcal G\}.$$

The essential supremum of a family $\mathcal X$ of $[-\infty,+\infty]$-valued random variables is the a.s. smallest random variable that dominates every member a.s.; the essential infimum is defined symmetrically. The minimal penalty of $\rho$ is

$$\alpha^*(Q)=\operatorname{ess.sup}_{X\in L^\infty}\{-E_Q(X\mid\mathcal G)-\rho(X)\},\qquad Q\in\mathcal P_{\mathcal G}.$$

For a risk aversion $\gamma>0$, the conditional entropic risk measure is

$$\rho_\gamma(X)=\frac1\gamma\log E_P\big(e^{-\gamma X}\mid\mathcal G\big),$$

the capital requirement for the acceptance set $A_\gamma=\{X\in L^\infty : E_P(e^{-\gamma X}\mid\mathcal G)\le1\}$. For $Q\in\mathcal P_{\mathcal G}$ with density $\varphi=dQ/dP$, the conditional relative entropy is

$$H_{\mathcal G}(Q\mid P)=E_P(\varphi\log\varphi\mid\mathcal G)\in[0,+\infty],\qquad 0\log0=0.$$

Formalization targets

Goal: Proposition 5.4

For every $\gamma>0$:

$$\rho_\gamma(X)=\operatorname{ess.sup}_{Q\in\mathcal P_{\mathcal G}}\Big\{-E_Q(X\mid\mathcal G)-\tfrac1\gamma H_{\mathcal G}(Q\mid P)\Big\}\quad(X\in L^\infty),\qquad \alpha^*(Q)=\tfrac1\gamma H_{\mathcal G}(Q\mid P)\quad(Q\in\mathcal P_{\mathcal G}).$$

The first identity is representability with the minimal penalty as the penalty; the second identifies that penalty.

Milestones

1. (Section 5, p. 12) $\rho_\gamma$ is a conditional convex risk measure.
2. (Section 5, p. 12) $\rho_\gamma(X)=\operatorname{ess.inf}\{Y\in L^\infty_{\mathcal G}: X+Y\in A_\gamma\}=\operatorname{ess.inf}\{Y\in L^\infty_{\mathcal G}: E_P(e^{-\gamma X}\mid\mathcal G)\le e^{\gamma Y}\}$.
3. (Proof of Proposition 5.4) $\rho_\gamma$ is continuous from above: $X_n\searrow X$ implies $\rho_\gamma(X_n)\nearrow\rho_\gamma(X)$.
4. (Section 5, p. 13) For $Q\in\mathcal P_{\mathcal G}$: $E_P(\varphi\mid\mathcal G)=1$ and $H_{\mathcal G}(Q\mid P)=E_Q(\log\varphi\mid\mathcal G)$.
5. (Proof of Proposition 5.4) $\alpha^*(Q)=\frac1\gamma\operatorname{ess.sup}_{Z\in L^\infty}\{E_Q(Z\mid\mathcal G)-\log E_P(e^Z\mid\mathcal G)\}$.
6. (Lemma 5.5) The conditional Donsker–Varadhan formula

$$\operatorname{ess.sup}_{Z\in L^\infty}\{E_Q(Z\mid\mathcal G)-\log E_P(e^Z\mid\mathcal G)\}=H_{\mathcal G}(Q\mid P),\qquad Q\in\mathcal P_{\mathcal G}.$$

Significance

The result gives the conditional entropic risk measure an explicit dual description: the capital requirement is a worst case over conditional models, each penalized by its conditional relative entropy. This duality is what makes entropic risk measures computable in dynamic settings. Recursive compositions of $\rho_\gamma$ over a filtration are time consistent, and their penalties add up by the chain rule for conditional relative entropy. Lemma 5.5 is also the conditional form of the Donsker–Varadhan (Gibbs) variational principle, which is used on its own in large deviations and in PAC-Bayesian bounds.

On status: the results are proved in the paper, and the unconditional versions are textbook material. Mathlib has unconditional Kullback–Leibler divergence, tilted measures, conditional Jensen's inequality and a $[0,+\infty]$-valued conditional expectation. As far as the platform search could establish, neither the conditional relative entropy nor the conditional Donsker–Varadhan formula nor any conditional risk measure has been formalized. This mission produces the first machine-checked conditional version, with $H_{\mathcal G}$ allowed to be infinite.

Difficulty

In the unconditional case both sides of Lemma 5.5 are numbers, and the supremum is a supremum over reals. Conditionally, both sides are random variables. The supremum over the uncountable family indexed by $L^\infty$ must be taken in the essential sense, and a pointwise supremum is neither measurable nor meaningful. The conditional relative entropy can be $+\infty$ on a set of positive probability. The integrand $\varphi\log\varphi$ need not be integrable, so the usual conditional expectation of $L^1$ is not available for it, and the "$\ge$" direction must reach an unbounded target through bounded test variables while controlling $\log E_P(e^{Z}\mid\mathcal G)$ at the same time. The ess.sup in the goal ranges over measures, not random variables, and each $E_Q(\cdot\mid\mathcal G)$ is a conditional expectation under a different measure. These are identified with $P$-a.s. objects through the condition $Q=P$ on $\mathcal G$.

Formalization scope

• $(\Omega,\mathcal F,P)$ is a probability space (IsProbabilityMeasure P), and $\mathcal G$ is m : MeasurableSpace Ω with hm : m ≤ mΩ. Payoffs are real functions with MemLp X ⊤ P. $L^\infty_{\mathcal G}$ membership is StronglyMeasurable[m] plus MemLp ⊤. Every (in)equality between random variables is $P$-a.e.
• $\mathcal P_{\mathcal G}$ is the subtype of probability measures $Q\ll P$ with $Q(A)=P(A)$ for all $A\in\mathcal G$. This is equality on $\mathcal G$, not equivalence of measures.
• $E_P(\cdot\mid\mathcal G)$ and $E_Q(\cdot\mid\mathcal G)$ on bounded variables are Mathlib's conditional expectations P[·|m] and Q[·|m]. Bounded variables are integrable under every $Q\ll P$, so no junk value arises.
• $\rho_\gamma$ is the paper's closed form $\frac1\gamma\log E_P(e^{-\gamma X}\mid\mathcal G)$. The ess.inf descriptions are a milestone, and no positivity hypothesis on $X$ is imposed.
• $\varphi$ is the real part of the Radon–Nikodym derivative Q.rnDeriv P. $H_{\mathcal G}(Q\mid P)$ and $E_Q(\log\varphi\mid\mathcal G)$ are generalized conditional expectations, $E(f^+\mid\mathcal G)-E(f^-\mid\mathcal G)$, built from Mathlib's $[0,+\infty]$-valued condLExp and valued in EReal. The negative parts are integrable, so $+\infty-(+\infty)$ never arises. In EReal, a real number minus $+\infty$ is $-\infty$, which is how a model with infinite entropy drops out of the supremum.
• Essential suprema and infima are predicates (IsEssSup, IsEssInf) on a candidate $P$-a.e. measurable EReal-valued function. The candidate must dominate every member a.s. and lie a.s. below every a.s. upper bound.
• Continuity from above means: a.s. monotone convergence $X_n\searrow X$ in $L^\infty$ implies a.s. monotone convergence $\rho(X_n)\nearrow\rho(X)$.
• $\gamma$ is a real constant with $\gamma>0$. The random risk aversion of Remark 5.6 is not formalized.
• Ruled out: defining $H_{\mathcal G}$ through the Bochner conditional expectation P[φ * log φ | m] (which returns $0$ when $\varphi\log\varphi$ is not integrable) or $\alpha^*$ through a pointwise supremum would make the goal false or vacuous, and so would stating it for an abstract convex risk measure in place of $\rho_\gamma$. The formalization uses the extended-valued $H_{\mathcal G}$, the essential supremum, and the explicit $\rho_\gamma$.
• The mission is self-contained. It redefines conditional convex risk measures, $\mathcal P_{\mathcal G}$ and the essential supremum in its own namespace CondConvexRisk.Entropic and does not assume the general representation theorem (Theorem 3.2). The generalized conditional expectation and the conditional Donsker–Varadhan formula are reusable beyond risk measures. Contributions are welcome on the ess.sup API (existence, upward-directed families), on conditional monotone convergence for condExp, and on the conditional Jensen step for $x\log x$.

Selected references

• S. Detlefsen, G. Scandolo, Conditional and Dynamic Convex Risk Measures, SFB 649 Discussion Paper 2005-006, Humboldt-Universität zu Berlin, 2005 (the version formalized; published in Finance and Stochastics 9(4), 2005, https://doi.org/10.1007/s00780-005-0159-6).
• H. Föllmer, A. Schied, Stochastic Finance: An Introduction in Discrete Time, de Gruyter, Berlin, 2002 (reference [8] of the paper).
• H. Föllmer, A. Schied, Convex measures of risk and trading constraints, Finance and Stochastics 6:429–447, 2002. https://doi.org/10.1007/s007800200072
• M. D. Donsker, S. R. S. Varadhan, Asymptotic evaluation of certain Markov process expectations for large time, III, Comm. Pure Appl. Math. 29:389–461, 1976. https://doi.org/10.1002/cpa.3160290405

Motivation

Gradient descent needs a step size, and the classical choices each ask for something the user may not have. A constant step $1/L$ needs the Lipschitz constant $L$ of the gradient, which is rarely known and often pessimistic. Backtracking needs repeated function evaluations. The exact line search needs a one-dimensional minimization at every iteration. Fatkhullin and Polyak (arXiv:2004.09875v2, SIAM J. Control Optim. 2021, doi:10.1137/20M1329858) proposed a step size for the static linear-quadratic regulator (their rule (4.8), §4.3, p. 11). In §6.1 they point out that the same rule applies to any smooth unconstrained problem $\min_{x\in\mathbb{R}^n} f(x)$. The rule divides the squared gradient norm by the Hessian quadratic form along the gradient. It needs one Hessian–vector product per iteration and neither $L$ nor the strong convexity constant $\mu$. In the paper's LQR experiment (§5, Figure 8, p. 13) the algorithm built on this step converges much faster than gradient descent with a constant step tuned at the first iterations.

The paper proves the method converges linearly for strongly convex functions (Theorem 6.1, p. 13). The proof takes one page (Appendix D.4, p. 19). This mission formalizes that theorem. It is the third mission of a series on this paper; the other two concern the LQR gradient method and gradient flow, and this one uses none of their control-theoretic objects.

Setting

Let $f:\mathbb{R}^n\to\mathbb{R}$ be twice differentiable, with gradient $\nabla f(x)$ and Hessian $\nabla^2 f(x)$. Three constants describe it.

• $f$ is $\mu$-strongly convex, $\mu>0$: $f(ax+by)\le af(x)+bf(y)-ab\,\frac{\mu}{2}\|x-y\|^2$ for all $x,y$ and $a,b\ge0$ with $a+b=1$.
• $\nabla f$ is Lipschitz with constant $L$: $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$.
• $\nabla^2 f$ is Lipschitz with constant $M$: $\|\nabla^2 f(x)-\nabla^2 f(y)\|\le M\|x-y\|$ in the operator norm.

Let $x_*$ be the global minimizer of $f$. The Hessian step size at a point $x$ is

$$\gamma(x)=\frac{\|\nabla f(x)\|^2}{\langle\nabla^2 f(x)\nabla f(x),\nabla f(x)\rangle},$$

the minimizer of the second-order Taylor model of $f$ along $-\nabla f(x)$. The method (6.1) runs

$$x_{j+1}=x_j-\gamma_j\nabla f(x_j),\qquad\gamma_j=\gamma(x_j),$$

from a starting point $x_0$. The damped method with factor $\sigma>0$ runs $x_{j+1}=x_j-\sigma\gamma_j\nabla f(x_j)$. For a quadratic $f(x)=\langle Hx,x\rangle$ the method (6.1) is steepest descent with exact line search.

Formalization targets

Goal: Theorem 6.1 (p. 13), both parts

Under the hypotheses above:

1. If $\delta>0$ and $M\sqrt{2L(f(x_0)-f(x_*))}\le3\mu^2(1-\delta)$ (condition (6.2)), the iterates of (6.1) satisfy

$$f(x_j)-f(x_*)\le\bigl(f(x_0)-f(x_*)\bigr)\Bigl(1-\frac{\mu\delta}{L}\Bigr)^j\quad\text{for all }j.\tag{6.3}$$

2. If $0<\sigma\le\mu/L$, the damped iterates from any $x_0$ satisfy

$$f(x_j)-f(x_*)\le\bigl(f(x_0)-f(x_*)\bigr)\Bigl(1-\frac{\mu\sigma}{L}\Bigr)^j\quad\text{for all }j.\tag{6.4}$$

The constants are the paper's, stated exactly.

Milestones (Appendix D.4, p. 19)

• Cubic Taylor bound (first display): $\bigl|f(x+y)-f(x)-\langle\nabla f(x),y\rangle-\frac12\langle\nabla^2 f(x)y,y\rangle\bigr|\le\frac M6\|y\|^3$.
• One-step inequality (third display): with $\varphi_j=f(x_j)$, $\varphi_{j+1}\le\varphi_j-\frac12\gamma_j\|\nabla f(x_j)\|^2\bigl(1-\frac{M\gamma_j^2}{3}\|\nabla f(x_j)\|\bigr)$.
• (D.1): $f(y)\le f(x)+\langle\nabla f(x),y-x\rangle+\frac{L}{2\mu}\langle\nabla^2 f(x)(y-x),y-x\rangle$.
• (D.2): one damped step gives $f(x_{j+1})\le f(x_j)-\frac{\sigma\gamma_j}{2}\|\nabla f(x_j)\|^2$.

Significance

Theorem 6.1 gives a rate for a step size computed from local second-order information alone. Part 1 says that near the minimizer the method converges at least as fast as gradient descent with step $\delta/L$, with no step-size parameter to tune. Part 2 gives convergence from every starting point, at the price of knowing a lower bound on $\mu/L$ for the damping. The same step appears in the paper's LQR method (rule (4.8)) and in gradient projection methods (p. 13, citing [37]), so the one-step inequalities are reusable beyond this theorem.

The result is proved in the paper. As of this writing none of it has a machine-checked proof. The formal work is the full development: the cubic Taylor bound from a Lipschitz second derivative on $\mathbb{R}^n$, the two one-step inequalities, and the inductions that give the rates.

Difficulty

The obvious argument for gradient descent uses the quadratic upper bound $f(y)\le f(x)+\langle\nabla f(x),y-x\rangle+\frac L2\|y-x\|^2$ and a step no larger than $2/L$. The Hessian step can be as large as $1/\mu$, far outside that range, so the quadratic bound in the Euclidean norm gives no decrease. Two different replacements are needed. For the undamped method, the cubic Taylor error must be controlled along the whole trajectory, and condition (6.2) is imposed only on $x_0$: the proof must show the gradient stays small enough at every later iterate. For the damped method, the upper bound must be measured in the local Hessian norm (D.1), which trades the step's size for the condition number $L/\mu$.

On the Lean side, Mathlib has Taylor's theorem in one variable. The cubic bound for a function on $\mathbb{R}^n$ with a Lipschitz Fréchet second derivative must be assembled from it or from the integral form along a segment. Mathlib has no ready-made link between strong convexity and a lower bound on the Hessian either.

Formalization scope

The space is EuclideanSpace ℝ (Fin n). The gradient is Mathlib's gradient f. The Hessian quadratic form $\langle\nabla^2 f(x)v,v\rangle$ is fderiv ℝ (fderiv ℝ f) x v v. Twice differentiability is differentiability of f and of fderiv ℝ f everywhere. The Lipschitz constant of the Hessian is in the operator norm of the bilinear map, not the Frobenius norm. Strong convexity is StrongConvexOn Set.univ μ f with 0 < μ; Mathlib's modulus is $\frac\mu2\|x-y\|^2$. $L$ and $M$ are real constants in the Lipschitz inequalities. The minimizer $x_*$ is a hypothesis ($f(x_*)\le f(y)$ for all $y$), not constructed.

Deviations from the page, all recorded in the items' Formalization Notes:

• The damping positivity $0<\sigma$ is added. It is implicit on the page.
• The damped claim is stated under the full hypotheses of Theorem 6.1, including the Lipschitz Hessian, although its proof does not use $M$.
• The one-step inequality for (6.1) is stated under the strong convexity of Theorem 6.1, which keeps $\gamma\ge0$. The gradient's Lipschitz constant is not assumed there.

At a stationary point the step is $0/0$; Lean evaluates it to $0$, so the method stays at the minimizer, and both rates remain true.

The iterates are those of the defined recursions (6.1) and its damped version. A statement about an arbitrary sequence satisfying a descent inequality would be a different, weaker theorem and does not discharge the goal. Condition (6.2) is imposed on $x_0$ only; a version assuming it at every iterate is also not the goal.

Contributions welcome: the multivariate cubic Taylor bound (reusable wherever a Lipschitz Hessian appears, e.g. in cubic regularization of Newton's method); the Hessian bounds $\mu I\preceq\nabla^2 f\preceq LI$ from strong convexity and a Lipschitz gradient; and the inequality $\frac12\|\nabla f(x)\|^2\le L(f(x)-f(x_*))$.

Selected references

• I. Fatkhullin, B. Polyak, Optimizing Static Linear Feedback: Gradient Method, arXiv:2004.09875v2, 2020; SIAM J. Control Optim. 59(5), 2021. https://arxiv.org/abs/2004.09875 · https://doi.org/10.1137/20M1329858
• Yu. Nesterov, B. T. Polyak, Cubic regularization of Newton method and its global performance, Math. Program. 108, 2006 (the cubic Taylor bound for Lipschitz Hessians). https://doi.org/10.1007/s10107-006-0706-8
• B. T. Polyak, Introduction to Optimization, Optimization Software, 1987 (gradient methods, strong convexity).

Motivation

The linear-quadratic regulator (LQR) is the basic problem of optimal control: steer a linear system $\dot x = Ax + Bu$ so as to minimize an integrated quadratic cost. When the full state is measured and the gain may be chosen freely, the optimal feedback is given by the algebraic Riccati equation (Kalman, 1960). In many applications only an output $y = Cx$ is measured, and the controller is restricted to a static feedback $u = -Ky$. For this output-feedback problem no Riccati-type characterization exists; the design problem is a non-convex optimization over the gain matrix $K$.

Direct optimization of the gain by gradient descent, known in the control literature since Levine and Athans (1970) and revived in reinforcement learning as policy gradient (Fazel, Ge, Kakade and Mesbahi, 2018, arXiv:1801.05039), is therefore of interest both to control engineers and to the learning community. Fatkhullin and Polyak (arXiv:2004.09875, SIAM J. Control Optim. 2021) give a self-contained analysis of the continuous-time problem: the cost is coercive on the set of stabilizing gains, smooth on sublevel sets, and, for state feedback, satisfies a gradient-domination (Łežanski–Polyak–Łojasiewicz) inequality. From these they derive convergence guarantees for the gradient method.

Setting

Fix real matrices $A\in\mathbb R^{n\times n}$, $B\in\mathbb R^{n\times m}$, $C\in\mathbb R^{r\times n}$ and weights $Q\in\mathbb R^{n\times n}$, $R\in\mathbb R^{m\times m}$, and an initial-state covariance $\Sigma\in\mathbb R^{n\times n}$. A gain is a matrix $K\in\mathbb R^{m\times r}$, and the closed-loop matrix is $A_K = A - BKC$. A square matrix is Hurwitz if all its complex eigenvalues have negative real part. The set of stabilizing gains is

$$\mathcal S = \{K\in\mathbb R^{m\times r} : A_K \text{ is Hurwitz}\}.$$

For $K\in\mathcal S$ let $X(K)$ be the unique solution of the Lyapunov equation

$$A_K^\top X + XA_K + C^\top K^\top RKC + Q = 0,$$

and define the cost $f(K)=\mathrm{Tr}\big(X(K)\Sigma\big)$, the expected integrated quadratic cost of the closed loop from a random initial state with covariance $\Sigma$. With $Y(K)$ the solution of $A_KY+YA_K^\top+\Sigma=0$, the gradient of $f$ in the Frobenius inner product is

$$\nabla f(K)=2\big(RKC-B^\top X(K)\big)Y(K)C^\top .$$

A known stabilizing gain $K_0\in\mathcal S$ is given, and $\mathcal S_0=\{K\in\mathcal S: f(K)\le f(K_0)\}$ is its sublevel set. The standing assumptions are $Q,R,\Sigma\succ0$, $\operatorname{rank}C=r$ and $B\neq0$. State feedback (SLQR) is the case $C=I$.

The gradient method with step sizes $\gamma_j$ is

$$K_{j+1}=K_j-\gamma_j\nabla f(K_j),\qquad j\ge0 .$$

A number $L>0$ is a smoothness constant if $\|\nabla f(K)-\nabla f(K')\|_F\le L\|K-K'\|_F$ for all $K,K'\in\mathcal S_0$.

Formalization targets

Goal: Theorem 4.2 for state feedback

For $C=I$, an optimal gain $K_*\in\mathcal S$, and any smoothness constant $L$:

1. if $0<\gamma_j\le 2/L$ for all $j$, then every $K_j\in\mathcal S_0$ and

$$f(K_{j+1})\le f(K_j)-\gamma_j\Big(1-\frac{L\gamma_j}{2}\Big)\|\nabla f(K_j)\|_F^2 ;$$

2. if $0<\varepsilon_1\le\gamma_j\le 2/L-\varepsilon_2$ with $\varepsilon_2>0$, then $\nabla f(K_j)\to0$,

$$\min_{0\le j\le k}\|\nabla f(K_j)\|_F^2\le\frac{f(K_0)}{c_1k}\quad(k\ge1),\qquad c_1=\frac{\varepsilon_1\varepsilon_2L}{2},$$

and there are $c\ge0$, $0\le q<1$ with $\|K_j-K_*\|_F\le c\,q^j$.

Milestones

In attack order:

• Appendix A lemmas. Trace duality of dual Lyapunov equations (Lemma A.1), the trace sandwich (Lemma A.4), and eigenvalue lower bounds for Lyapunov solutions (Lemma A.5).
• Coercivity and existence. Coercivity of $f$ with the lower bounds (3.1)–(3.2) (Lemma 3.8), boundedness of $\mathcal S_0$ (Corollary 3.9), and existence of a minimizer (Corollary 3.10).
• Smoothness. The gradient formula (Lemma 3.11) and existence of a smoothness constant on $\mathcal S_0$ (Theorem 3.15, qualitative form).
• Gradient domination for state feedback. Lemmas C.2, C.3 and C.1, and the LPL inequality with the explicit constant (3.11):

$$\tfrac12\|\nabla f(K)\|_F^2\ge\mu\big(f(K)-f(K_*)\big),\qquad K\in\mathcal S_0 \qquad\text{(Theorem 3.17)}.$$

• Theorem 4.2 for output feedback. Descent and stationarity, parts 1 and 2 without the linear rate, for general $C$.

Significance

The theorem shows that a plain first-order method, started from any stabilizing gain, never destabilizes the closed loop and decreases the cost monotonically, for output feedback as well as state feedback. For state feedback it converges globally and linearly to the optimal gain. The cost is non-convex, and its domain $\mathcal S$ is open, possibly non-convex and unbounded, so this does not follow from convex optimization theory. It is the continuous-time counterpart of the policy-gradient guarantees of Fazel et al. for discrete-time LQR, and it underlies model-free and data-driven variants of gain tuning.

The result is proved in the paper, but it has not been formalized. The formalization adds three things. It makes the invariance argument (the iterates stay in $\mathcal S_0$) explicit, and the paper describes that argument as the non-trivial part. It corrects the statements where the printed text is wrong (see below). It also produces a reusable library of Lyapunov-equation facts. Mathlib has no Lyapunov equation, no LQR cost and no Hurwitz stability theory, and the platform has no continuous-time LQR material. The nearest platform items treat discrete-time Riccati iteration (BertsekasDP.riccati_convergence_stability) and Polyak–Łojasiewicz rates on a whole normed space (ShiOptRates.pl_rate). Neither applies to a function defined only on a non-convex open subset.

Difficulty

The standard descent-lemma argument assumes $f$ is defined and $L$-smooth on the whole space. Here $f$ is defined only on $\mathcal S$, and it is not smooth on all of $\mathcal S$: it blows up at the boundary. A gradient step from a point of $\mathcal S_0$ could in principle jump out of $\mathcal S$, where the Lyapunov equation has no meaningful solution. The smoothness bound is available only inside $\mathcal S_0$, so the argument must show that the whole segment from $K_j$ to $K_{j+1}$ stays in $\mathcal S_0$ before the descent inequality can be used on it. That requires coercivity, compactness of $\mathcal S_0$ and an exit-time argument. For the linear rate, gradient domination has to be established on $\mathcal S_0$ with constants controlled by $f(K_0)$, and passing from function values to distances to $K_*$ needs that minimizer's structure. Gradient domination fails for output feedback (the paper's Example 3.4 has two disconnected components with different minima), so the linear rate is stated only for $C=I$.

Formalization scope

Matrices are Matrix (Fin p) (Fin q) ℝ. Hurwitz means every element of the complex spectrum has negative real part. $X(K)$, $Y(K)$ are "the unique solution of the Lyapunov equation, $0$ if there is none or several"; this junk value is never used, because every statement evaluates $f$ and $\nabla f$ only at gains proved or assumed to lie in $\mathcal S$. The iterates' membership in $\mathcal S_0$ is a conclusion of the goal, never a hypothesis; assuming it would delete the theorem's content. $\nabla f$ is defined by the formula (3.3), and Lemma 3.11 is the theorem that it is the gradient. $\|\cdot\|_F$ is $\sqrt{\sum M_{ij}^2}$, $\|\cdot\|$ is the spectral (operator) norm, and $\lambda_1,\lambda_n$ are the minimum and maximum eigenvalue of a symmetric matrix. State feedback is the instance $r=n$, $C=1$. In (4.6) the Frobenius norm replaces the paper's spectral norm, which is equivalent because $c$ is existential. The minimum over $0\le j\le k$ requires $k\ge1$.

Deviations from the printed text, each recorded in the item's Formalization Note:

• The smoothness constant. The explicit $L$ of (3.8) is false as printed (for $n=m=1$, $A=0$, $B=100$, $Q=100$, $R=10^{-3}$, $\Sigma=0.1$, $K_0=10^{-6}$, one has $f''(K_0)=2L$). The goal therefore takes $L$ as any Lipschitz constant of $\nabla f$ on $\mathcal S_0$, which is the paper's definition of $L$-smoothness (§3.6) and all that its proof uses. Theorem 3.15 enters only as "some such $L>0$ exists".
• Lemma C.1. It is stated with $\lambda_1^2(\Sigma)$ in the denominator, as its proof concludes and as (3.11) requires.
• Lemma A.5. It is stated for $A^\top X+XA+Q=0$; the printed $-Q$ admits no positive definite solution.
• The gain space. $\mathcal S\subseteq\mathbb R^{m\times r}$, where p. 3 prints $\mathbb R^{m\times n}$.

Not stated: Theorem 4.3 and Algorithm 4.1, Lemma 3.6, Lemmas 3.12–3.14, Corollary 3.16 and the explicit constant (3.8). Welcome contributions include a Lyapunov-equation library (existence, uniqueness, integral representation, positivity), continuity of the spectrum, and the exit-time argument, which is reusable for any descent method on a sublevel set of an open domain.

Selected references

• I. Fatkhullin, B. Polyak, Optimizing Static Linear Feedback: Gradient Method, SIAM J. Control Optim. 59(5), 2021; preprint arXiv:2004.09875v2. https://arxiv.org/abs/2004.09875
• M. Fazel, R. Ge, S. Kakade, M. Mesbahi, Global Convergence of Policy Gradient Methods for the Linear Quadratic Regulator, ICML 2018. https://arxiv.org/abs/1801.05039
• W. Levine, M. Athans, On the determination of the optimal constant output feedback gains for linear multivariable systems, IEEE Trans. Automat. Control 15(1), 1970. https://doi.org/10.1109/TAC.1970.1099363
• H. Karimi, J. Nutini, M. Schmidt, Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak–Łojasiewicz Condition, ECML PKDD 2016. https://arxiv.org/abs/1608.04636
• R. E. Kalman, Contributions to the theory of optimal control, Bol. Soc. Mat. Mexicana 5, 1960.

Motivation

The gradient projection method minimizes a continuously differentiable function over a closed convex set by alternating a gradient step with a projection back onto the set. It was proposed by Goldstein (1964) and by Levitin and Polyak (1966), and it is the basic step of many algorithms for bound constrained and linearly constrained optimization, including large-scale quadratic programming codes.

The classical convergence results either need a Lipschitz constant for the gradient to choose the step (Goldstein; Levitin–Polyak), or assume a bounded sequence of iterates and conclude only that limit points are stationary (Bertsekas, 1976, for the Armijo rule on a box; Dunn, 1981). Calamai and Moré (1987) introduced a general step-size rule that contains the Armijo procedure, and proved a convergence statement that needs no boundedness of the iterates: the projected gradients tend to zero. This statement is what later results on finite identification of the active constraints use as their hypothesis, so it is the natural entry point to the paper.

Setting

Let $E$ be a finite-dimensional real inner product space with norm $\|\cdot\|$, let $\Omega \subseteq E$ be nonempty, closed and convex, and let $f : E \to \mathbb R$ be continuously differentiable on $\Omega$, with gradient $\nabla f$ taken with respect to the inner product. The problem is

$$\min\{f(x) : x \in \Omega\}. \qquad (1.1)$$

• The projection into $\Omega$ is $P(x) = \operatorname{argmin}\{\|z - x\| : z \in \Omega\}$, the unique nearest point of $\Omega$ to $x$ (Eq. (1.3)).
• A point $x^* \in \Omega$ is stationary if $\langle \nabla f(x^*), x - x^* \rangle \ge 0$ for all $x \in \Omega$ (Eq. (1.5)).
• A direction $v$ is feasible at $x \in \Omega$ if $x + \tau v \in \Omega$ for all sufficiently small $\tau > 0$; the tangent cone $T(x)$ is the closure of the set of feasible directions.
• The projected gradient is $\nabla_\Omega f(x) = \operatorname{argmin}\{\|v + \nabla f(x)\| : v \in T(x)\}$ (Eq. (3.1)), the nearest point of $T(x)$ to $-\nabla f(x)$.

A run of the gradient projection method is a pair of sequences $(x_k)_{k\ge0}$, $(\alpha_k)_{k \ge 0}$ with $x_0 \in \Omega$, $\alpha_k > 0$ and $x_{k+1} = x_k(\alpha_k)$, where $x_k(\alpha) = P(x_k - \alpha \nabla f(x_k))$. For fixed constants $\gamma_1, \gamma_2 > 0$ and $\mu_1, \mu_2 \in (0,1)$, the steps satisfy the sufficient decrease condition

$$f(x_{k+1}) \le f(x_k) + \mu_1 \langle \nabla f(x_k), x_{k+1} - x_k\rangle \qquad (2.1)$$

and the condition that the step is not too small: either $\alpha_k \ge \gamma_1$, or $\alpha_k \ge \gamma_2 \bar\alpha_k > 0$ for some $\bar\alpha_k$ at which sufficient decrease fails,

$$f(x_k(\bar\alpha_k)) > f(x_k) + \mu_2 \langle \nabla f(x_k), x_k(\bar\alpha_k) - x_k \rangle. \qquad (2.2)\text{–}(2.3)$$

In Lean these objects are proj, projGrad and IsGradientProjectionRun in the namespace CalamaiMore.Convergence, together with the shared definitions tangentCone and IsStationaryPoint in CalamaiMore.Shared.

Formalization targets

Goal: Theorem 3.2

If, in addition, the steps are bounded, $\alpha_k \le \gamma_3$ for some constant $\gamma_3$ (3.2), $f$ is bounded below on $\Omega$, and $\nabla f$ is uniformly continuous on $\Omega$, then

$$\lim_{k \to \infty} \|\nabla_\Omega f(x_k)\| = 0.$$

No boundedness of $\{x_k\}$ is assumed, and no specific step rule beyond (2.1)–(2.3).

Milestones

1. Lemma 2.1: $P$ satisfies the variational inequality $\langle P(x) - x, z - P(x)\rangle \ge 0$ for $z \in \Omega$, is monotone (strictly when $P(y) \ne P(x)$) and nonexpansive.
2. Eqs. (2.4)–(2.5): $\langle \nabla f(x_k), x_k - x_k(\alpha)\rangle \ge \|x_k(\alpha) - x_k\|^2/\alpha$ for $\alpha > 0$, and its instance at $\alpha = \alpha_k$.
3. Lemma 2.2: $\alpha \mapsto \|P(x + \alpha d) - x\|/\alpha$ is nonincreasing on $(0, \infty)$.
4. Theorem 2.3: under the hypotheses of the goal without (3.2), $\|x_{k+1} - x_k\|/\alpha_k \to 0$.
5. Lemma 3.1: $-\langle \nabla f(x), \nabla_\Omega f(x) \rangle = \|\nabla_\Omega f(x)\|^2$; $\min\{\langle \nabla f(x), v\rangle : v \in T(x), \|v\| \le 1\} = -\|\nabla_\Omega f(x)\|$; and $x$ is stationary if and only if $\nabla_\Omega f(x) = 0$.
6. Theorem 2.4: if some subsequence $\{x_k : k \in K\}$ is bounded, $\|x_{k+1} - x_k\|/\alpha_k \to 0$ along $K$, and every limit point of $\{x_k\}$ is stationary.
7. Lemma 3.3: $x \mapsto \|\nabla_\Omega f(x)\|$ is lower semicontinuous on $\Omega$.
8. Theorem 3.4: with (3.2) and a bounded subsequence $\{x_k : k \in K\}$, $\|\nabla_\Omega f(x_{k+1})\| \to 0$ along $K$.

Significance

By Lemma 3.1, $\|\nabla_\Omega f(x)\|$ vanishes exactly at stationary points, so Theorem 3.2 says that the method approaches stationarity in a quantitative sense even when the iterates are unbounded. With Lemma 3.3 it gives that every limit point is stationary. For polyhedral $\Omega$ it is the hypothesis of the paper's Theorem 4.1: any sequence with $\nabla_\Omega f(x_k) \to 0$ converging to a nondegenerate point identifies the active constraints in finitely many iterations, which is the basis of active-set methods that switch between gradient projection steps and subspace minimization.

The results are proved in the paper. To our knowledge they have no machine-checked proof. This mission produces a formal account of the gradient projection method with a general step rule, a reusable projected gradient and tangent cone on a general finite-dimensional inner product space, and the standard projection estimates of §2, which are also the starting point of the paper's other two main results.

Difficulty

The obvious argument fails at two places. First, the continuity of $\nabla_\Omega f$ cannot be used: the map $x \mapsto \nabla_\Omega f(x)$ is not continuous, and $\|\nabla_\Omega f\|$ can be bounded away from zero in every neighborhood of a stationary point, because the tangent cone changes discontinuously at the boundary of $\Omega$. So $x_k \to x^*$ with $x^*$ stationary does not by itself force $\nabla_\Omega f(x_k) \to 0$, and here the iterates need not converge at all. Second, the steps $\alpha_k$ may tend to zero along a subsequence; the step rule gives information only through a trial step $\bar\alpha_k$, at a point other than $x_{k+1}$, and comparing the two projected steps is where the argument must work.

Formalization scope

The space is a type E with [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]; $\nabla f$ is Mathlib's gradient f. "Continuously differentiable on $\Omega$" is ∀ x ∈ Ω, DifferentiableAt ℝ f x together with ContinuousOn (gradient f) Ω. Bounded below is BddBelow (f '' Ω), uniform continuity is UniformContinuousOn (gradient f) Ω. Sequences are ℕ → E indexed from $0$; a subsequence is an infinite K : Set ℕ with limits along atTop ⊓ 𝓟 K; a limit point is a MapClusterPt. The projection and the projected gradient are total functions through a nearest-point map that returns $0$ when no nearest point exists; every theorem assumes $\Omega$ nonempty, closed and convex, and evaluates $\nabla_\Omega f$ only at points of $\Omega$, where the nearest point exists and is unique. The step rule is a predicate on the pair of sequences, so the theorems cover every rule satisfying (2.1)–(2.3); the auxiliary condition $\mu_1 \le \mu_2$, which the paper uses only to show that an admissible step exists, is not imposed.

The run predicate is satisfiable: for a constant $f$, the constant sequence $x_k = x_0 \in \Omega$ with $\alpha_k = \gamma_1$ is a run, so the goal is not vacuous. A formalization that states the goal for an arbitrary map in place of the projection, drops the bound $\alpha_k \le \gamma_3$, or replaces $\|\nabla_\Omega f(x_k)\|$ by $\|x_{k+1} - x_k\|/\alpha_k$ proves a different theorem and is not accepted.

Contributions welcome: the projection estimates (reusable for any projection-based method), existence and uniqueness of the projected gradient, the characterization of stationarity, and the two limit theorems.

Selected references

• P. H. Calamai, J. J. Moré, Projected gradient methods for linearly constrained problems, Mathematical Programming 39 (1987) 93–116. https://doi.org/10.1007/BF02592073
• A. A. Goldstein, Convex programming in Hilbert space, Bulletin of the AMS 70 (1964) 709–710. https://doi.org/10.1090/S0002-9904-1964-11178-2
• E. S. Levitin, B. T. Polyak, Constrained minimization methods, USSR Computational Mathematics and Mathematical Physics 6 (1966) 1–50. https://doi.org/10.1016/0041-5553(66)90114-5
• D. P. Bertsekas, On the Goldstein–Levitin–Polyak gradient projection method, IEEE Transactions on Automatic Control 21 (1976) 174–184. https://doi.org/10.1109/TAC.1976.1101194
• J. C. Dunn, Global and asymptotic convergence rate estimates for a class of projected gradient processes, SIAM Journal on Control and Optimization 19 (1981) 368–400. https://doi.org/10.1137/0319022
• E. M. Gafni, D. P. Bertsekas, Two-metric projection methods for constrained optimization, SIAM Journal on Control and Optimization 22 (1984) 936–964. https://doi.org/10.1137/0322061