Operations Research

Motivation

The least-squares (LS) problem $\min_x \|Ax - b\|$ assumes that the data $A \in \mathbb{R}^{n\times m}$, $b \in \mathbb{R}^n$ are exact. In applications they rarely are: they come from measurements, from linearizations, or from models with neglected dynamics. A classical response is sensitivity analysis or regularization (Tikhonov), where a weight trades the size of the solution against the fit, and the choice of that weight is left to the user. El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl. 18(4), 1997) take a deterministic view instead: the true data lie in a known ball around $(A, b)$, and the solution should minimize the residual it can be forced to have in the worst case over that ball. The paper shows that this robust least-squares (RLS) problem is solvable exactly, in the unstructured case by a second-order cone program (SOCP). The same worst-case idea, applied to regression, underlies the later equivalence between robustness and regularization (Xu, Caramanis and Mannor, 2009) and is a standard entry point to robust optimization (Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization, 2009).

This mission formalizes the first main result of the paper, Theorem 3.1: the worst-case residual has a closed form, its minimizer is unique, and minimizing it is an SOCP.

Setting

Vectors carry the Euclidean norm $\|v\| = (\sum_i v_i^2)^{1/2}$. For a matrix $X$, $\|X\|_F = (\sum_{i,j} X_{ij}^2)^{1/2}$ is the Frobenius norm and $\|X\|$ the largest singular value, i.e. the smallest $c \ge 0$ with $\|Xv\| \le c\|v\|$ for all $v$.

Fix $A \in \mathbb{R}^{n\times m}$ and $b \in \mathbb{R}^n$. A perturbation is a pair $\Delta A \in \mathbb{R}^{n\times m}$, $\Delta b \in \mathbb{R}^n$, collected in the augmented matrix $\Delta = [\Delta A\ \Delta b] \in \mathbb{R}^{n\times(m+1)}$. For a bound $\rho \ge 0$ and $x \in \mathbb{R}^m$, the worst-case residual is (paper, eq. (1))

and $x$ is an RLS solution if it minimizes $r(A,b,\rho,\cdot)$. The bound constrains the augmented matrix jointly, not $\Delta A$ and $\Delta b$ separately. The paper normalizes $\rho = 1$ and writes $r(A,b,x) = r(A,b,1,x)$. Finally, $[x;1] \in \mathbb{R}^{m+1}$ denotes $x$ stacked over $1$. In the Lean development these are RobustLS.Unstructured.eucNorm, frobNorm, specNorm, augment, stackOne, worstCaseResidual A b ρ x, its largest-singular-value variant worstCaseResidualSpec, and the SOCP constraint predicate SocpFeasible A b x λ τ.

Formalization targets

Goal: Theorem 3.1 (p. 1040)

For $n \ge 1$, every $A$, $b$:

the problem $\min_{x \in \mathbb{R}^m} r(A,b,x)$ has exactly one solution $x_{\mathrm{RLS}}$, and it is the SOCP

in the sense that $r(A,b,x)$ is the least $\lambda$ for which some $\tau$ makes $(x,\lambda,\tau)$ feasible.

Milestones

1. Eq. (16). Every perturbation with $\|[\Delta A\ \Delta b]\|_F \le 1$ has residual at most $\|Ax-b\| + \sqrt{\|x\|^2+1}$.
2. The worst-case perturbation. For a unit vector $u$ aligned with $Ax - b$ (arbitrary if $Ax = b$), the rank-one matrix $\Delta = u[x^T\ {-1}]/\sqrt{\|x\|^2+1}$ has $\|\Delta\|_F = \|\Delta\| = 1$ and attains the bound.
3. Spectral norm. The worst case over the larger ball $\|[\Delta A\ \Delta b]\| \le 1$ is the same value.
4. Strict convexity. $x \mapsto r(A,b,x)$ is strictly convex on $\mathbb{R}^m$.
5. The SOCP (15). For every $x$, $r(A,b,x)$ is the optimal $\lambda$ of (15) with $x$ fixed, and $x$ is an RLS solution exactly when it is the $x$-part of an optimal solution of (15).

Significance

The closed form replaces a maximization over a matrix ball of dimension $n(m+1)$ by two Euclidean norms. It shows that the RLS objective is the LS residual plus a penalty $\sqrt{\|x\|^2+1}$ that does not depend on $A$ or $b$, which is the starting point for the paper's Theorem 3.2 (the RLS solution is a Tikhonov-regularized LS solution with a data-dependent weight) and its analysis of continuity and conditioning. The SOCP formulation places the problem in the class solved by interior-point methods, at a cost the paper compares with one singular value decomposition of $A$. The spectral-norm statement says the worst case does not depend on which of the two standard matrix norms bounds the perturbation.

The result is proved in the paper; the proof is short. To the best of the planning survey (September 2026), no machine-checked proof exists, and Prove2Me has no statement about worst-case residuals or robust least squares. The mission produces a verified closed form that later missions of this series (Tikhonov form of the solution, structured and linear-fractional perturbations) and any formalization of robust regression can import.

Difficulty

The upper bound alone does not give the theorem: the statement is an equality, and the equality needs an explicit maximizer. The paper's printed maximizer is wrong by a sign: with $[x^T\ 1]$ in place of $[x^T\ {-1}]$ the perturbation does not attain the bound (for $A = 0$, $x = 0$, $b = e_1$ it gives residual $0$ instead of $2$), so a transcription of the printed proof fails. Two further points are silent in the paper. The operator norm of a rank-one matrix has to be computed from the definition of the largest singular value. Uniqueness of the minimizer needs existence first, which follows from growth of $r$ at infinity and is not stated. Working with the sSup definition of the worst case requires showing the set of residuals is bounded, which is milestone 1.

Formalization scope

• Dimensions are Fin n, Fin m; $A$ is Matrix (Fin n) (Fin m) ℝ, $b$ and $x$ are functions Fin n → ℝ, Fin m → ℝ. The augmented matrix $[\Delta A\ \Delta b]$ is indexed by Fin m ⊕ Unit, and so is $[x;1]$.
• Vector norms are the Euclidean norm written as $\sqrt{\sum_i v_i^2}$ (eucNorm), never Mathlib's ‖·‖ on Fin n → ℝ, which is the sup norm. The Frobenius norm and the largest singular value are explicit definitions (frobNorm, specNorm); specNorm is the infimum of admissible operator constants.
• The maximum in (1) is sSup of the set of attained residuals. For $\rho \ge 0$ the set is nonempty and bounded, so this is the true maximum; milestones 1 and 2 state the bound and the attaining perturbation directly, so no statement relies on the value of sSup on an unbounded set.
• The paper's normalization $\rho = 1$ is kept; general $\rho > 0$ follows from the scaling $\phi(A,b,\rho) = \rho\,\phi(A/\rho,b/\rho,1)$ the paper records on p. 1039 and is not a target.
• The goal assumes $n \ge 1$. For $n = 0$ the only perturbation is the empty matrix, the worst case is $0$, and the closed form fails; the paper's setting ($Ax \simeq b$ with data $b \in \mathbb{R}^n$) has $n \ge 1$. Milestones 3–5 carry the same hypothesis.
• Milestone 2 states the corrected perturbation $[x^T\ {-1}]$; the printed $[x^T\ 1]$ is false.
• A trivializing formalization — an upper bound in place of the equality, a worst case over $\Delta A$ and $\Delta b$ bounded separately, or uniqueness among critical points only — is ruled out: the goal is the equality for the jointly bounded augmented matrix and ∃! of a global minimizer over all of $\mathbb{R}^m$.

Contributions welcome: lemmas on Frobenius and operator norms of rank-one matrices, the inequality $\|Mz\| \le \|M\|_F\|z\|$ in this explicit setting, and strict convexity of $x \mapsto \sqrt{\|x\|^2+1}$; these are reusable beyond the mission.

Selected references

• L. El Ghaoui and H. Lebret, Robust Solutions to Least-Squares Problems with Uncertain Data, SIAM Journal on Matrix Analysis and Applications 18(4):1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
• A. Ben-Tal, L. El Ghaoui and A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
• H. Xu, C. Caramanis and S. Mannor, Robust Regression and Lasso, Journal of Machine Learning Research 10:1485–1510, 2009 (IEEE Trans. Inf. Theory 56(7), 2010). https://jmlr.org/papers/v10/xu09b.html
• M. S. Lobo, L. Vandenberghe, S. Boyd and H. Lebret, Applications of Second-Order Cone Programming, Linear Algebra and its Applications 284:193–228, 1998. https://doi.org/10.1016/S0024-3795(98)10032-0

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

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$,

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|$:

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),

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$

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

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

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

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

Formalization targets

Goal: Proposition 5.4

For every $\gamma>0$:

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

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

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

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.