Online Algorithms

The model

Fix $m \ge 1$ machines and $n$ jobs arriving one at a time in the order $0, \dots, n-1$. Job $i$ carries a whole vector of nonnegative loads $\tilde p(i,j)$, one per machine, with no assumed relationship between the entries — the same job may be cheap on one machine and unplaceable on another. This is the unrelated machines model. When job $i$ arrives its load vector becomes visible, and the algorithm must commit it to a single machine immediately and irrevocably, knowing nothing about the jobs still to come. A machine's load is the sum of $\tilde p(i,j)$ over the jobs assigned to it.

The setting formalized here is one normalized phase: loads are already scaled by a guessed makespan, so machine $j$ counts as eligible for job $i$ exactly when $\tilde p(i,j) \le 1$. The phase is allowed to give up rather than assign badly — it fails if an arriving job has no eligible machine, or if an internal weight grows past $1$.

The algorithm and the guarantee

The algorithm keeps a weight $x(j)$ per machine, initialized to $1/(2m)$. Job $i$ goes to the eligible machine $\ell$ minimizing $\tilde p(i,\ell)\, x(\ell)$; that machine's weight is then scaled by $1 + \tilde p(i,\ell)/2$, so a machine becomes exponentially unattractive as it fills. The weights are the primal variables of the covering LP

$$\min \sum_j x(j) + \sum_i z(i) \quad \text{s.t.} \quad \tilde p(i,j)\,x(j) + z(i) \ge 1 \ \text{ for every eligible pair } (i,j),$$

and each assignment raises one dual variable $y(i,\ell)$ to $1$. The guarantee follows from weak duality rather than a bespoke potential argument, which is the point of the primal-dual method.

The goal theorem states that if the dual admits a feasible solution putting unit total mass on every job — the certificate that the guessed makespan was large enough — then the phase does not fail, every job is assigned, and every machine ends with load

$$\sum_{i \,\text{assigned to}\, j} \tilde p(i,j) \ \le\ \frac{\ln(3m)}{\ln(3/2)}.$$

The source states this as $O(\log m)$; the explicit constant is what its proof yields.

Note that the load bound alone is not the theorem: it holds vacuously when the phase assigns nothing, and the milestones state it that way deliberately. The content is the conjunction of succeeded, assigns all, and the bound.

Scope

The doubling wrapper — guess a makespan, run a phase, double the guess and restart on failure — is what turns this phase into an $O(\log m)$-competitive online algorithm. It is outside this mission; the guarantee proved here is the conditional single-phase statement. The milestones break the argument into weak duality for finite LPs, the load bound, primal feasibility at each prefix, the primal objective identity, and the failure certificate.

Source

Niv Buchbinder and Joseph (Seffi) Naor, The Design of Competitive Online Algorithms via a Primal-Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3), 2009, Chapter 8, pp. 193–196 (Theorem 8.1). PDF · doi:10.1561/0400000024

Motivation

An online algorithm must commit to decisions before it knows the rest of its input, and it is judged by competitive analysis: the ratio between its cost and the cost of an optimal solution computed with full knowledge of the input. A recurring obstacle in this area is that each problem seems to need its own ad hoc potential-function argument. Buchbinder's thesis develops a single method that replaces those arguments — formulate the offline problem as a covering linear program, let the online algorithm raise the dual variables of its packing dual, and read the competitive ratio off the ratio between the primal and dual increments. The same recipe then yields algorithms for online set cover, weighted caching, ad-auction revenue, routing, and load balancing.

This mission formalizes the chapter where the method is introduced on its smallest example, the ski-rental problem. A customer needs skis for an unknown number of days: renting costs $1$ per day and buying costs $B$ once. The customer must decide, each morning, whether to rent again or buy, without knowing how many ski days remain. Despite its size the problem is the canonical rent-or-buy dilemma, and it has two classical tight results: a deterministic $2$-competitive algorithm, and a randomized algorithm whose competitive ratio tends to $e/(e-1)$, due to Karlin, Manasse, McGeoch and Owicki (1994). The primal-dual derivation of both is the content of Chapter 3.

Setting

An instance is a pair $(B, k)$: the purchase price $B$, a positive integer, and the number $k \ge 0$ of ski days, which the online algorithm does not know. An offline solution either buys at once, paying $B$, or rents on every day, paying $k$; so the offline optimum is

$$\mathrm{OPT}(B,k) \;=\; \min(B, k).$$

Chapter 3 casts this as a linear program (Figure 3.1, p. 18). The primal is a covering program with one buy variable $x$ and one rent variable $z_j$ per day $j$:

$$\text{minimize } \; B x + \sum_{j=1}^{k} z_j \quad \text{subject to} \quad x + z_j \ge 1 \ \text{ for each day } j.$$

Its dual is a packing program with one variable $y_j$ per day:

$$\text{maximize } \; \sum_{j=1}^{k} y_j \quad \text{subject to} \quad \sum_{j=1}^{k} y_j \le B, \qquad 0 \le y_j \le 1 .$$

The online structure enters in a single way: a new ski day appends a new covering constraint to the primal and a new variable to the dual, and previously raised primal variables may never be decreased. That monotonicity is what "previous decisions cannot be regretted" means formally.

The fractional primal-dual algorithm maintains $x$, initially $0$. On each new day, while $x < 1$ it sets $z_j \leftarrow 1 - x$, then raises

$$x \;\leftarrow\; x\left(1 + \tfrac{1}{B}\right) + \tfrac{1}{cB},$$

and sets $y_j \leftarrow 1$; once $x$ has reached $1$ it does nothing further. The free parameter $c$ is then pinned to the value that makes $x$ reach exactly $1$ after $B$ days,

$$c \;=\; \left(1 + \tfrac{1}{B}\right)^{B} - 1 .$$

Formalization targets

Goal — the fractional algorithm's competitive ratio at finite $B$

$$B\,x_k + \sum_{j=0}^{k-1} z_j \;\le\; \left(1 + \frac{1}{\left(1 + \frac{1}{B}\right)^{B} - 1}\right) \cdot \min(B, k) \qquad \text{for every } B \ge 1, \ k \ge 0 .$$

The coefficient is the exact finite-$B$ ratio $1 + 1/c$, left in closed form rather than replaced by a constant. This is deliberate: $\left(1+\frac1B\right)^B$ increases to $e$, so $c < e - 1$ and therefore $1 + 1/c > e/(e-1)$ for every finite $B$. A goal asserting $e/(e-1)$-competitiveness at finite $B$ would be false, and a goal asserting some rounded constant would be invalidated by any sharpening. The closed-form coefficient is the weakest statement that is stable under improvement.

Asymptotic companion — where $e/(e-1)$ actually lives

$$\lim_{B \to \infty} \left(1 + \frac{1}{\left(1 + \frac{1}{B}\right)^{B} - 1}\right) \;=\; \frac{e}{e-1} \;\approx\; 1.5819767 .$$

The classical constant is recorded here, as a limit of the coefficient sequence, and nowhere else.

Parallel target — the deterministic algorithm

$$\mathrm{detCost}(B,k) \;\le\; 2 \cdot \min(B,k), \qquad \mathrm{detCost}(B,k) = \begin{cases} k & k < B \\ 2B & k \ge B\end{cases}$$

Chapter 3's other result, independent of the fractional development.

Significance

The ski-rental bounds themselves are classical and tight, and nothing here is mathematically open. What the chapter contributes, and what this mission captures, is the derivation: it is the template instantiated by every later chapter of the thesis, so the artifacts built here — a covering/packing LP pair, its weak-duality instance, a monotone online variable with a closed-form growth law, and the primal-to-dual increment ratio as the source of the competitive factor — are the vocabulary in which the rest of the series will be stated.

On status: the mathematics is proved, published, and standard. It is not, to the best of a search of Mathlib at revision 0df444a, formalized — that revision contains no competitive-analysis or online-algorithm framework, no ski-rental development, and no general linear-programming weak-duality theorem. So the work this mission asks for is formalization of a known proof, not new mathematics, and the reusable output is infrastructure that does not currently exist in the library.

Difficulty

The offline problem is trivial, and a newcomer's first move — prove $\min(B,k)$ is the optimum and stop — solves the wrong problem. The content is entirely in the online constraint. Three specific places where the obvious argument stalls:

The optimum is never observed. The algorithm's cost must be compared against $\min(B,k)$ without $k$ being available to it. The comparison is routed through the dual instead: the dual objective the algorithm accumulates is a lower bound on every feasible primal solution, hence on the optimum, and the algorithm's own primal cost is a fixed multiple of that dual objective.

The growth law is piecewise. The update fires only while $x < 1$. Summing the per-day increments therefore does not telescope uniformly: days before $x$ reaches $1$ contribute $1 + 1/c$ each and later days contribute nothing, and the index at which the switch happens is exactly $B$ — which is a theorem about the recurrence, not an assumption.

The constant is forced, not chosen. $c = (1+1/B)^B - 1$ is not a free tuning parameter; it is the unique value for which the geometric sequence $x_j = \bigl((1+1/B)^j - 1\bigr)/c$ hits $1$ at $j = B$, which is in turn what makes the dual solution feasible ($\sum_j y_j \le B$). Dual feasibility and the choice of $c$ are the same fact.

Formalization scope

Conventions this development commits to. The purchase price is a natural number $B$ with $0 < B$, because Chapter 3 uses $B$ simultaneously as a price, as a day index ("buy skis on the $B$th day"), and as the exponent in $(1+1/B)^B$; costs are real numbers, with $B$ and $k$ coerced. Days are indexed from $0$, so day $j+1$ of the prose is index $j$, and Fin k indexes the $k$ days. Real division is total, so $1/0 = 0$; the hypothesis $0 < B$ is what keeps every reciprocal in the development genuine, and without it $c$ would evaluate to $0$ and the recurrence would collapse to the constant zero sequence. The algorithm's x < 1 guard is part of the formalized definition, not an informal aside: without it the cost would keep growing past day $B$.

A documented discrepancy in the source. The prose on p. 17 relaxes the integer program by letting $x$ and each $z_j$ range over $[0,1]$; Figure 3.1 on p. 18 prints only $x \ge 0$, $z_j \ge 0$. This mission takes the prose version, $0 \le x \le 1$ and $0 \le z_j \le 1$, as the canonical fractional program, and also records the nonnegativity-only region exactly as printed. Two separate theorems establish that both have least value $\min(B,k)$, so the discrepancy is resolved inside the mission rather than silently chosen. Solvers should note which of the two predicates a given statement uses.

Ruling out a trivializing formalization. The offline optimum is defined independently, as $\min(B,k)$, and is not derived from the algorithm's own behaviour; a separate theorem certifies that this value really is the least attainable objective value of the canonical program, so the goal cannot be satisfied by redefining the benchmark. The goal inequality is also tight — both sides are equal to $(1+1/c)$ times the number of days on which $x < 1$ — so it cannot be weakened into vacuity without becoming false.

Infrastructure, and what is reusable. The development needs only Mathlib big operators over Fin k, basic real analysis for the limit, and IsLeast. Two items are explicitly infrastructure rather than ski-rental content: the specialized weak-duality theorem for this covering/packing pair, and the Figure 3.1 optimum. Both are candidates for generalization by the later mission on Chapter 2's general linear-programming duality, and a solver who proves the general form there should expect this instance to be derivable from it rather than duplicated.

Out of scope here. The final paragraph of p. 19 rounds the fractional solution into a randomized algorithm by sampling a threshold $\alpha \in [0,1]$ uniformly and buying on the day whose increment of $x$ contains $\alpha$. That step needs a probability space and an expectation argument, and is deferred to the immediate follow-up mission, Primal-Dual Online Algorithms II: Randomized Rounding for Ski Rental. Contributions here should not anticipate it.

Selected references

• Niv Buchbinder, Designing Competitive Online Algorithms via a Primal-Dual Approach, PhD thesis, Tel Aviv University, 2008. Chapter 3, pp. 17–19. https://www.tau.ac.il/~nivb/download/phd-thsis.pdf
• Niv Buchbinder and Joseph (Seffi) Naor, The Design of Competitive Online Algorithms via a Primal-Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3), 2009. https://doi.org/10.1561/0400000024
• Anna R. Karlin, Mark S. Manasse, Lyle A. McGeoch and Susan Owicki, Competitive randomized algorithms for nonuniform problems, Algorithmica 11(6), 1994, 542–571. https://doi.org/10.1007/BF01294260
• Allan Borodin and Ran El-Yaniv, Online Computation and Competitive Analysis, Cambridge University Press, 1998.

Motivation

Almost every competitive online algorithm built by the primal-dual method rests on the same two facts about a pair of linear programs. The first is weak duality: any feasible solution of the dual is a lower bound on any feasible solution of the primal. The second is complementary slackness: if a feasible primal-dual pair satisfies a local, per-coordinate tightness condition, the pair is optimal — and if it satisfies that condition only up to factors $\alpha$ and $\beta$, the primal is within $\alpha\beta$ of optimal.

The second fact in its approximate form is the engine of the whole method. An online algorithm cannot compute an optimum; what it can do is maintain a primal solution and a dual solution side by side so that each new request preserves an approximate tightness invariant. The approximate complementary slackness theorem then converts that local invariant into a global competitive ratio, with no reference to the optimum at all. Chapter 2 of Buchbinder's thesis states it as the background result on which the rest of the work is built.

Setting

Fix finite index types $I$ (primal variables) and $J$ (primal constraints), a matrix $A : I \times J \to \mathbb{R}$, a cost vector $c : I \to \mathbb{R}$ and a right-hand side $b : J \to \mathbb{R}$. The covering primal and packing dual are

$$(P)\quad \min \sum_{i} c_i x_i \ \text{ s.t. } \ \sum_{i} A_{ij} x_i \ \ge\ b_j \ \ (\forall j), \qquad x \ge 0,$$ $$(D)\quad \max \sum_{j} b_j y_j \ \text{ s.t. } \ \sum_{j} A_{ij} y_j \ \le\ c_i \ \ (\forall i), \qquad y \ge 0.$$

Note the index convention: $A_{ij}$ carries the primal-variable index first, so the primal constraint indexed by $j$ sums over $i$ and the dual constraint indexed by $i$ sums over $j$.

Given $\alpha, \beta \ge 1$, the pair $(x,y)$ satisfies approximate complementary slackness when

• primal side: for every $i$ with $x_i > 0$, $\quad c_i/\alpha \ \le\ \sum_j A_{ij} y_j \ \le\ c_i$;
• dual side: for every $j$ with $y_j > 0$, $\quad b_j \ \le\ \sum_i A_{ij} x_i \ \le\ \beta\, b_j$.

Formalization targets

Goal — approximate complementary slackness

For a primal-feasible $x$, a dual-feasible $y$, and $\alpha,\beta \ge 1$ satisfying the two conditions above,

$$\sum_{i} c_i x_i \ \le\ \alpha\beta \sum_{j} b_j y_j .$$

Taking $\alpha = \beta = 1$ recovers exact complementary slackness and hence optimality of both members of the pair. The goal is stated with the source's hypotheses, including the two-sided bounds, rather than the weakest hypotheses that make the inequality go through; a separate item records the minimal-hypothesis strengthening.

Weak duality

$$\sum_j b_j y_j \ \le\ \sum_i c_i x_i \quad \text{for every feasible } x \text{ and } y,$$

with no nonnegativity assumption on $A$, $b$ or $c$ beyond feasibility itself.

Strong duality — imported, not reproved

Strong duality is not proved in this mission. The platform already carries LinearOptimization.lp_strong_duality, proved in this exact environment, for linear programs in Bertsimas–Tsitsiklis general form over Fin-indexed data. This mission's contribution is an adapter: from a primal optimum of $(P)$, produce a dual optimum of $(D)$ of equal value, for Fin-indexed instances. Reference items point at the imported theorem, its dual construction, and the dual-of-dual identity.

The biconditional — a dual optimum exists if and only if a primal optimum does — is deliberately left open. Weak duality does not derive the existence of a primal optimum from the existence of a dual one; the reverse implication needs strong duality applied to the dual program together with the dual-of-dual identity, and that reduction is not yet compiled. It is offered as a parallel target rather than claimed as established.

Significance

This mission is the foundation of the series. Every later mission — set cover, ski rental, and the online covering and packing problems that follow — states its approximation or competitiveness result as an instance of approximate complementary slackness. Formalizing it once, over arbitrary finite index types, is what makes the later missions short.

It also fills a real gap. Mathlib currently has no linear-programming duality: four separate attempts were closed unmerged. Approximate $(\alpha,\beta)$ complementary slackness appears not to be formalized in any public library, so the goal theorem is, as far as we can determine, first of its kind.

Difficulty

The goal is a summation argument, not a deep theorem: the work is in handling the per-coordinate case split on $x_i > 0$ versus $x_i = 0$ and in interchanging a double sum. Three mechanical milestones isolate exactly those steps. The strong-duality adapter is the hard item, because it must reconcile two different presentations of the same program — index types, matrix orientation, and bundling all differ between our definitions and the imported theorem's.

Formalization scope

Definitions cover §2.1 of the source. Four distinct notions of "the program has a finite optimum" are separated on purpose — attained optimum, nonempty feasible set, bounded objective, and the conjunction — because the source's informal word "bounded" conflates them. The definitions are stated over arbitrary finite index types; the strong-duality items are stated only for Fin, because that is the only index type for which the imported dependency path exists.

Selected references

• Niv Buchbinder, Designing Competitive Online Algorithms via a Primal-Dual Approach, PhD thesis, Tel Aviv University, 2008, §2.1, pp. 7–9. https://www.tau.ac.il/~nivb/download/phd-thsis.pdf
• Dimitris Bertsimas and John N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 — the general form used by the imported strong-duality theorem.

Motivation

Set cover is the standard worked example of the primal-dual method, and Chapter 2 of Buchbinder's thesis uses it that way: it is where the machinery of §2.1 is first turned on a concrete NP-hard problem. Two analyses appear. The greedy algorithm, analysed by dual fitting, buys the set with the best cost-per-newly-covered-element ratio and charges the price to the elements it covers; the resulting element prices form an infeasible dual that becomes feasible after scaling by $H_n$. The primal-dual algorithm instead raises the price of an uncovered element until some set's constraint goes tight, buys that set, and repeats; the resulting dual is feasible, and each bought set is paid for by elements of frequency at most $f$, giving an $f$-approximation.

Both analyses have the same shape, and it is the shape that matters for the rest of the series: the algorithm never sees the optimum. It maintains a dual solution, and the approximation ratio falls out of comparing the primal it built against the dual it accumulated.

Setting

An instance consists of a finite type $E$ of elements, a finite type $S$ indexing available sets, an assignment $s \mapsto A_s \subseteq E$, and a nonnegative cost $c : S \to \mathbb{R}$. Every element is assumed to lie in at least one available set; the source leaves this implicit, and without it no cover exists and the approximation statements are vacuous. The covering LP and its packing dual are

$$(P)\quad \min \sum_{s} c_s x_s \ \text{ s.t. } \sum_{s : e \in A_s} x_s \ \ge\ 1 \ \ (\forall e \in E), \quad x \ge 0,$$ $$(D)\quad \max \sum_{e} y_e \ \text{ s.t. } \sum_{e \in A_s} y_e \ \le\ c_s \ \ (\forall s \in S), \quad y \ge 0.$$

The frequency of an element is the number of sets containing it, and $f$ denotes the maximum frequency over all elements.

The two standing assumptions — nonnegative costs, and every element lying in some available set — are carried by a bundled SetCoverInstance, not passed as loose hypotheses. Every source-facing statement in the mission takes such an instance and reads those facts off its fields, so none of them can be instantiated at data violating either. The two indicator lemmas are the exceptions and are labelled as generalized assisting results: one has no cost function in scope at all, and the other's hypothesis that a given $C$ covers is strictly stronger than coverability of the family.

Costs are permitted to be zero and the ground type is permitted to be empty. No Nonempty E hypothesis appears anywhere; when $E$ is empty, $f = 0$ and the $f$-approximation bound reads $\mathrm{cost}(C) \le 0$, which the certificate's tightness clause forces to be $0 \le 0$ rather than anything false.

Formalization targets

The results are stated about certificates, not about executable algorithms. This is the central modelling decision of the mission and it is deliberate: the mathematical content of the source's proofs is entirely a statement about the invariants the output satisfies, and separating that from the question of whether a particular procedure produces such output keeps each half provable on its own.

A primal-dual certificate is a pair $(C, y)$ where $C \subseteq S$ covers $E$, $y$ is dual-feasible, and every $s \in C$ has a tight dual constraint, $\sum_{e \in A_s} y_e = c_s$.

Goal — the primal-dual $f$-approximation

For any primal-dual certificate $(C,y)$ and any fractional cover $x$,

$$\sum_{s \in C} c_s \ \le\ f \cdot \sum_{s \in S} c_s x_s .$$

Since this holds against every fractional cover, it holds in particular against an optimal one, so the cover $C$ costs at most $f$ times the fractional optimum and a fortiori at most $f$ times the integral optimum.

The double-counting step

The one substantive step of the goal is split out as its own target: for a primal-dual certificate,

$$\sum_{s \in C} c_s \ \le\ f \cdot \sum_{e \in E} y_e .$$

Tightness rewrites the cover's cost as a double sum over chosen sets and their elements; exchanging the order groups it by element, each charged at most $f$ times. With this and weak duality, the goal is two lines.

The greedy bound

A greedy certificate at ratio $\rho$ is a cover $C$ and a nonnegative $y$ with $\sum_{s \in C} c_s = \sum_{e} y_e$ and $\sum_{e \in A_s} y_e \le \rho\, c_s$ for every $s$. For such a certificate and any fractional cover $x$,

$$\sum_{s \in C} c_s \ \le\ \rho \cdot \sum_{s} c_s x_s .$$

Instantiating $\rho = H_n$ is what recovers the source's greedy guarantee; the harmonic bound itself is already in Mathlib.

Set-cover weak duality and LP attainment

Every dual packing is bounded by every fractional cover, $\sum_e y_e \le \sum_s c_s x_s$; the fractional optimum is at most the integral optimum; and both optima are attained, not merely bounded below. Attainment of the fractional optimum is a genuine linear-programming fact and is the hardest supporting item in the mission.

Significance

This is where the series first converts a dual-feasibility invariant into an approximation ratio on a concrete combinatorial problem, and the two certificate predicates are reused verbatim by the online covering missions later in the series. Set cover approximation has, as far as we can determine, no prior formalization in Mathlib or in any public Lean library: there is no set-cover problem statement, no greedy analysis, and no $f$-approximation result to build on.

Difficulty

The two certificate bounds are finite-summation arguments of moderate length — the work is in a double-counting step that reindexes a sum over chosen sets into a sum over elements, weighted by frequency. Attainment of the fractional optimum is different in kind: it needs a compactness or vertex argument about the covering polytope and is the item most likely to need real work. Zero-cost sets are permitted throughout, so any later algorithm definition that divides by a cost must handle that case explicitly.

Formalization scope

Definitions cover §2.2 of the source, excluding §2.2.2 (randomized rounding), which is deferred to a separate mission because its expected-cost and failure-probability analysis is measure-theoretic and shares no infrastructure with the deterministic results.

Two theorems are not in this mission: that the greedy algorithm produces a greedy certificate, and that the primal-dual algorithm produces a primal-dual certificate. Those require defining the algorithms and proving termination and coverage, and are planned as a second wave. Until that wave lands, the source's Theorems 2.4 and 2.6 should not be described as fully formalized — what this mission establishes is the certificate-to-ratio half of each.

Selected references

• Niv Buchbinder, Designing Competitive Online Algorithms via a Primal-Dual Approach, PhD thesis, Tel Aviv University, 2008, §2.2, pp. 10–14. https://www.tau.ac.il/~nivb/download/phd-thsis.pdf
• Vijay V. Vazirani, Approximation Algorithms, Springer, 2001, Chapters 2 and 15 — the standard treatment of the greedy and primal-dual set-cover analyses.

Motivation

Every guarantee in the preceding chapters assumes a fixed distribution and i.i.d. sampling. On-line learning drops both assumptions: an algorithm processes one example at a time, in an adversarial (worst-case) sequence, and is judged by regret against the best fixed comparator in hindsight rather than by generalization error. This chapter develops the theory for this setting — mistake bounds and regret bounds for prediction with expert advice, a margin-based mistake bound for the Perceptron — and then closes a conceptual gap: since on-line algorithms need no distributional assumption, can their guarantees be converted into ordinary distributional (batch) generalization guarantees when the data does happen to be i.i.d.? The on-line-to-batch conversion theorem answers yes, using nothing but an Azuma's-inequality martingale argument on the sequence of hypotheses the algorithm actually produces.

Setting

At round t, an on-line algorithm receives x_t, predicts ŷ_t, receives the true label y_t, and incurs loss L(ŷ_t,y_t); its regret R_T (Eq. 8.1) compares its cumulative loss to the best fixed action's in hindsight. §8.2 develops this for prediction with expert advice: the Halving algorithm (realizable case), Weighted Majority and its randomized version RWM (zero-one loss, Theorem 8.4's L_T ≤ log(N)/(1-β) + (2-β)L_T^min, proved by the chapter's recurring potential-function technique applied to W_t = ∑_i w_{t,i}), and the Exponential Weighted Average algorithm (convex losses). §8.3.1 analyzes the Perceptron, a linear classification algorithm whose margin-based mistake bound (Theorem 8.8, separable case; the non-separable Theorem 8.11, restated here, in terms of an arbitrary comparator v's hinge losses) depends only on the normalized margin, not the ambient dimension. §8.4 shows that averaging the hypotheses h_1,…,h_T an on-line algorithm produces while processing an i.i.d. sample S yields a hypothesis with controlled true risk: Lemma 8.14 bounds the average of the per-round risks R(h_t) by the average on-line loss via a martingale argument on V_t = R(h_t) - L(h_t(x_t),y_t), and Theorem 8.15 upgrades this, via the loss's convexity, to a bound on the risk of the averaged hypothesis (1/T)∑h_t.

Formalization targets

Theorem 8.4 (milestone). Fix β∈[1/2,1). For any T≥1: L_T ≤ log(N)/(1-β) + (2-β)L_T^min; for β=max{1/2,1-√(log(N)/T)}: L_T ≤ L_T^min + 2√(T log N).

Theorem 8.11 (milestone). M ≤ inf_{ρ>0,‖v‖₂≤1}[(r/ρ+√(r²/ρ²+4‖l_ρ‖₁))/2]², where l_ρ=(l_t)_{t∈I}, l_t=max{0,1-y_t(v·x_t)/ρ}.

Lemma 8.14 (milestone). For any δ>0, with probability at least 1-δ: (1/T)∑_tR(h_t) ≤ (1/T)∑_tL(h_t(x_t),y_t) + M√(2log(1/δ)/T).

Theorem 8.15 — the mission's goal (first inequality). Under Lemma 8.14's hypotheses, with L additionally convex in its first argument: for any δ>0, with probability at least 1-δ: R((1/T)∑_th_t) ≤ (1/T)∑_tL(h_t(x_t),y_t) + M√(2log(1/δ)/T).

Significance

Theorem 8.15 is the chapter's conceptual capstone: it is the only bridge in the whole book between the adversarial on-line-learning framework and the distributional PAC/statistical framework every other chapter develops, and its proof needs nothing beyond Lemma 8.14 plus convexity — no new machinery, just the right observation about the loss's structure. Theorem 8.4 is the chapter's cleanest instance of its recurring potential-function proof technique (reused, with variations, for Theorems 8.3, 8.6 and 8.7), and — checked against the platform's existing OnlineConvexOpt.Introduction.randomized_weighted_majority_mistake_bound (Hazan series) — a genuinely different result from what is already on the platform: that lemma bounds a mistake count with a (1+ε) multiplier, this bounds the RWM algorithm's own weighted-mixture loss with a 1/(1-β) term and a distinct optimal-β substitution, confirming BRIEF.md's assessment that the two are close but not interchangeable. Theorem 8.11 is the non-realizable generalization of the separable-case Perceptron bound (Theorem 8.8) that motivates soft-margin algorithms generally, expressed via an arbitrary comparator's hinge loss rather than assuming perfect separability. No prior art exists for the chapter's other content: GET /theorems?q=online%20to%20batch returns zero hits, and GET /theorems?q=perceptron returns only an unrelated neural-network topology result.

Difficulty

Theorem 8.4's proof (mirrored by Theorem 8.3's WM analogue) derives matching upper and lower bounds on the potential W_t, combines them via a logarithm, and substitutes a specific optimal β found by differentiating the resulting bound — a genuine two-step optimization argument, not a direct algebraic identity. Theorem 8.11's proof solves a quadratic inequality in √M after summing the hinge-loss-defining inequalities over the update set I and invoking the Cauchy-Schwarz step already used in Theorem 8.8's proof; keeping the inf over both ρ and v in the statement (not fixing them, per BRIEF.md's pitfall note) is what makes this a genuine bound rather than a bound for one arbitrary choice. Lemma 8.14's proof is an application of Azuma's inequality (the book's own Theorem D.7) to the martingale difference sequence V_t = R(h_t) - L(h_t(x_t),y_t), which requires h_t to be measurable with respect to the history strictly before round t — the on-line algorithm's hypothesis at round t must not depend on the pair drawn at that same round, per BRIEF.md's pitfall note. Theorem 8.15's step beyond Lemma 8.14 is the passage from the average of T individual risks to the risk of the averaged hypothesis, licensed by Jensen's inequality under the loss's convexity in its first argument — dropping convexity breaks exactly this step, not merely weakening a constant.

Formalization scope

GeneralizationError restates chunk 11-regression's Eq. (11.1) convention locally (Y := ℝ, consistent with that chunk's own harmless simplification), needed here since Theorem 8.15 requires averaging hypotheses into a single real-valued function. OnlineHypothesis A S t is formalized so that its type signature itself enforces history-adaptedness: the on-line algorithm A : (n:ℕ) → (Fin n → X × ℝ) → (X → ℝ) is a function of the prefix of the sample seen so far, and OnlineHypothesis A S t applies it only to S's first t pairs — this is what licenses Azuma's inequality's martingale-difference argument (the conditional-mean-zero property of V_t), per BRIEF.md's pitfall note. Revision (2026-09-19), correcting an earlier claim in this section: history-adaptedness does not by itself guard against GeneralizationError's Bochner integral silently junking to 0 for a non-measurable hypothesis (a distinct property — whether h_t, as a function of x, is Measurable — from whether h_t depends on round t's own draw). Moderation found this a live gap in both Lemma 8.14 and Theorem 8.15's drafted statements; both now carry an explicit hAmeas/hLmeas hypothesis in addition to the history-adapted type signature. RWM's w_{t,i}, W_t, p_{t,i}, L_t, L_T, L_{T,i}, L_T^min are modeled as their own recursively-defined algorithm state (mirroring, but never substituting into, chunk 07-boosting's AdaBoost pattern), matching this chapter's own loss-based (not mistake-count) quantities, per BRIEF.md's pitfall note distinguishing them from AdaBoost's and RWM-mistake variants. The Perceptron's w_t, update-index set I, and M = |I| are modeled the same way, using Eq. (8.23)'s equivalent sign-agreement update rule (the book's own reformulation of Figure 8.6's sgn-based rule). Theorem 8.11's inf_{ρ>0,‖v‖₂≤1} is a genuine nested restricted infimum (⨅ ρ ∈ Set.Ioi 0, ⨅ v ∈ Metric.closedBall 0 1, …), not a bound instantiated at fixed ρ, v, per BRIEF.md's explicit pitfall note. No numerical constant is altered from the book in any of the four theorems.

Not formalized: Theorems 8.1-8.3 (Halving and WM mistake bounds — the chapter's warm-up results, superseded in content by the more general RWM/EWA theorems that follow), Theorem 8.5 (a matching lower bound, a distinct impossibility result rather than an algorithm's guarantee), Theorems 8.6-8.7 (Exponential Weighted Average regret bounds — a third algorithm with its own potential-function proof, out of scope per BRIEF.md's restriction to §8.2's Halving/WM/RWM), Theorems 8.8-8.10 (the Perceptron's separable-case bound and its leave-one-out-based expected generalization bounds, both superseded in generality by Theorem 8.11 for this mission's purposes), Theorem 8.12 (Perceptron's L²-norm hinge-loss bound, the book's own note that it is implied by, and looser than, Theorem 8.11's L¹-norm bound), the dual/kernel Perceptron (an equivalent reformulation, not new generalization content), and Theorem 8.15's second displayed inequality (a regret-form corollary depending on the regret decomposition of the surrounding discussion, not drafted per BRIEF.md's own recommendation to commit to the first inequality as the goal). §8.3.2 (Winnow) and §8.5 (the game-theoretic connection) are out of scope per BRIEF.md's chapter restriction.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 8 (§8.2, §8.3.1, §8.4).
• N. Littlestone, M. K. Warmuth, "The weighted majority algorithm," Information and Computation 108(2), 1994 (WM/RWM's origin).
• F. Rosenblatt, "The perceptron: a probabilistic model for information storage and organization in the brain," Psychological Review 65(6), 1958 (the Perceptron algorithm).
• Y. Freund, R. E. Schapire, "Large margin classification using the perceptron algorithm," Machine Learning 37(3), 1999 (Theorem 8.11's hinge-loss mistake bound).

Motivation

Section 4 of this survey derives a simple randomized $O(\log m \log n)$-competitive algorithm for the online set-cover problem, by rounding the fractional solution the online packing-covering framework produces. An intriguing question the survey poses next: can the same guarantee be achieved deterministically? The standard tool for removing randomness, the method of conditional expectations, requires finding a pessimistic estimator — a potential function whose value the algorithm can track and whose behavior certifies the randomized algorithm's guarantee step by step. Chapter 5 constructs exactly this potential function for the weighted online set-cover problem, and shows that greedily minimizing it online reproduces the randomized algorithm's competitive ratio with no randomness at all. This mission formalizes that construction: the potential function itself (Lemma 5.1) and the correctness guarantee it buys (Theorem 5.2).

Setting

Fix a finite universe of elements $E$ and a finite family of sets $T$ with positive costs $c_s$, both known to the algorithm in advance (only which elements will actually need covering, and in what order, is unknown). A monotonically increasing assignment $w : T \to \mathbb{R}$ of fractional weights to sets is produced online by a fractional subroutine (any $O(\log m)$- competitive online fractional algorithm — the survey's own Section 4.2 supplies one). An element's weight is $w_e := \sum_{s \mid e \in s} w_s$. Given a target $\alpha \ge c(C_{OPT})$ (a guessed upper bound on the optimal integral cover's cost — the survey handles an unknown optimum by doubling this guess across phases, outside this chapter's own scope), the algorithm maintains a chosen cover $C \subseteq T$ and the potential

$$\Phi \;=\; \sum_{e \notin \bar C} n^{2w_e} \;+\; n \cdot \exp\!\Big(\tfrac{1}{2\alpha} \sum_{s} \big(c_s \chi_C(s) - 3 w_s c_s \log n\big)\Big),$$

where $n = |E|$ and $\chi_C$ is $C$'s characteristic function. Whenever a set $s$'s weight increases, the algorithm computes $\Phi$ both with and without adding $s$ to $C$ and chooses whichever keeps $\Phi$ from exceeding its value before the step (failing only if neither does, which Lemma 5.1 shows cannot happen when $\alpha \ge c(C_{OPT})$).

Formalization targets

Theorem 5.2 (goal, p. 139): given the invariant $\Phi < n^2$ that Lemma 5.1 maintains throughout a run, (i) every element of weight $\ge 1$ is covered, and (ii) the chosen cover costs at most $\alpha \cdot O(\log m \log n)$.

Lemma 5.1 (milestone, p. 137): the potential function never increases in expectation across a weight-augmenting step, under the algorithm's own randomized choice of whether to add the augmented set to the cover (the internal argument — via the method of conditional expectations — that certifies the deterministic algorithm's choice rule never fails).

Significance

This chapter answers, for the online set-cover problem specifically, a question that recurs throughout online algorithm design: when can a randomized guarantee be derandomized online? The potential-function technique here is the survey's own template for the answer (it recurs, per the chapter's Notes section, in the routing algorithm of Chapter 9 and the ad-auctions algorithm of Chapter 10, both formalized as separate missions in this series) — a self-contained, reusable instance of "derandomization via an explicit pessimistic estimator" in the online setting, distinct from the offline set-cover primal-dual and dual-fitting algorithms of this book's own Chapter 2, already on the platform (PrimalDualOnline.SetCover.*, checked below: a static instance with no arrival order and no potential function, a genuinely different model).

Difficulty

The central formalization challenge is that Lemma 5.1's own statement, "$\Phi_{end} \le \Phi_{start}$", denotes the potential's value in expectation under the algorithm's randomized choice — not a single deterministic before/after pair — since the lemma is proved via a probabilistic argument (adding $s$ to the cover with probability $1 - n^{-2\delta_s}$) whose role is purely internal to justifying the deterministic algorithm's rule (choose whichever of the two options controls $\Phi$). Stating the lemma as a bare inequality between two potential values, without the mixture, would either be false (the "add $s$" branch alone can increase $\Phi$) or would silently smuggle in the derandomized choice as a hypothesis rather than proving it is always available. This mission states the expectation explicitly as a probability-weighted average of the two branch potentials, matching the actual analytic content of the book's proof (equations 5.1-5.6) rather than its final one-line restatement.

Formalization scope

SetCoverInstance E T bundles elemSets : E → Finset T (the sets containing an element) and positive costs c. elementWeight and coveredBy are literal transcriptions of $w_e$ and "$e \in \bar C$". potential transcribes $\Phi$'s displayed formula verbatim, with n cast from Fintype.card E. potential_nonincreasing (Lemma 5.1) is the expectation inequality described above. algorithm_correctness (Theorem 5.2) takes the potential invariant Φ < n² as a hypothesis (the state Lemma 5.1, applied repeatedly from the initial value $\Phi < n^2$, is what the book's own proof shows every reachable state satisfies) together with an explicit ratio β standing for "the fractional solution is O(log m)-competitive" (∑ wₛcₛ ≤ βα) — the book imports this fact from Section 4 as a black-box subroutine rather than re-deriving a specific numeric constant in this chapter, and this mission does the same rather than re-deriving Chapter 4's own constant under the (different) $d \to m$ substitution the book's prose glosses over. The conclusion is then the fully explicit α · log n · (3β + 2), matching the book's own derivation (displayed inequality, p. 139-140) with O(log m) replaced by the parameter β. This correctly rules out the trivializing formalization in which the O(log m log n) bound is left as an unquantified existential constant, or in which Φ's invariant is assumed directly as an unmotivated free hypothesis rather than the fact Lemma 5.1 is what actually establishes. Reals throughout; Real.log, Real.exp, Real.rpow (via the ^ notation on reals) for the book's own log, exp and n^{2w_e}. Nothing here is reused from 04-framework (concurrent draft; per this series' own rule, drafts do not import drafts) even though this chapter's fractional subroutine is conceptually the same online covering framework — restated here only as the abstract ratio β, not as a Lean dependency. Welcome contributions: completing the two sorrys, and formalizing the doubling-across-phases wrapper (Section 5.1's "Obtaining a Deterministic Algorithm" discussion) that removes the need to know α ≥ c(C_OPT) in advance.

Selected references

• N. Buchbinder, J. Naor. The Design of Competitive Online Algorithms via a Primal-Dual Approach. Foundations and Trends in Theoretical Computer Science, 3(2-3):93-263, 2009. https://doi.org/10.1561/0400000024
• N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor. The online set cover problem. STOC 2003 / SIAM J. Comput. 39(2), 2009 (cited by this book's Chapter 5 Notes as [3]).

Motivation

The metrical task system (MTS) problem is one of the earliest and most general online models: a server occupies a state in a metric space, requests arrive with per-state service costs, and the server may change state (paying the metric's transition cost) before serving each request. On a general metric, competitive algorithms are hard to design directly. Chapter 6 shows that on a weighted star metric — the simplest genuinely non-uniform metric, a hub with leaves at varying distances — the online primal-dual framework of Chapter 4 becomes applicable, but only after a change of rules: the chapter defines a new MTS model, in which the server may change state only at the boundary of a "phase" (an interval during which its accumulated service cost reaches the state's own transition charge), and shows this new model is cost-equivalent, up to a constant factor, to the standard model. This equivalence is what licenses recasting the (new-model) problem as a covering linear program with the online primal-dual framework directly applicable — the chapter's actual algorithmic payoff (an unnumbered $O(\log N)$-competitive result, Section 6.2) rests entirely on it.

Setting

Fix a set of leaves $V$ (the book's finite $\{1,\dots,N\}$) of a weighted star, each leaf $i$ at distance $d'(i) \ge 0$ from the center. The chapter immediately collapses the full star metric to a single per-state transition charge $d(i) := 2d'(i)$, since on a star every transition $i \to j$ costs at most $d'(i) + d'(j)$, and charging the doubled source leaf's distance alone (never charging for arriving) upper-bounds every transition cost independent of destination. A standard-model solution is a finite sequence of runs, each specifying a state $s_i$ occupied and the service cost $w_i \ge 0$ accumulated while in that state, ending with a transition (cost $d(s_i)$) to the next run's state; its total cost is $\sum_i (w_i + d(s_i))$. A new-model solution is a finite sequence of phases, each specifying a state visited; a phase's cost is exactly $d(\text{state})$ regardless of how much service actually occurred during it (a state change is only permitted once a phase's accumulated service reaches the phase's own $d$-value), so the new model's total cost is $\sum_i d(s_i)$.

Formalization targets

Lemma 6.1 (goal, p. 144): any standard-model solution's runs $(s, w)$ transform into a new-model solution whose cost is at most $2 \cdot \sum_i (w_i + d(s_i))$; in particular $OPT_n(\bar\sigma) \le 2 \cdot OPT_o(\bar\sigma)$.

Lemma 6.2 (milestone, p. 145): any new-model solution's phases $(s, w)$, with each phase's actual service $w_i \le d(s_i)$, are simultaneously a legal standard-model solution (the same trajectory, recosted) whose standard-model cost is at most $2 \cdot \sum_i d(s_i)$.

Together (stated in the book but not separately numbered, hence not a formalization target here): a $c$-competitive algorithm in the new model implies a $4c$-competitive algorithm in the standard model.

Significance

This is a model-equivalence result, a distinct and recurring pattern in online algorithm design from the competitive-ratio bounds formalized elsewhere in this series: rather than analyzing an algorithm directly, the chapter first shows that solving an easier, more restricted version of the problem (state changes only at phase boundaries) loses only a constant factor, and only then designs an algorithm for the restricted version. The technique generalizes (the chapter's own Notes section places it in the context of Borodin et al.'s original MTS bounds, and of later work on hierarchically well-separated trees for general metrics), but this chapter gives its cleanest, self-contained instance: two short, tight (factor-2 each direction) transformations between two formally distinct online cost models. No prior formalization of metrical task systems on a weighted star, or of this new/standard model equivalence, was found on the platform as of 2026-09-20 (search below); the platform's existing KServer.* campaign formalizes a different online problem (uniform-metric $k$-server) with a different metric structure and is not adjacent substrate for this chapter's weighted-star MTS model.

Difficulty

The central obstacle is representing "a solution" at a level of abstraction faithful to the book's own proof without committing to a full continuous-time process model (states as functions of a real time variable, phases as recursively-defined stopping times, requests as an explicit arriving sequence) that neither lemma's own proof actually needs. Both proofs work entirely at the granularity of a solution's runs (standard model) or phases (new model) — finite sequences of (state, cost) data — never referencing continuous time except to justify that this decomposition exists. This mission formalizes both lemmas at exactly that granularity: a run/phase sequence indexed by Fin k, with costStandard/costNewPhases the book's own displayed cost formulas. Lemma 6.1's proof genuinely constructs a new object (the delayed-transition solution $S'$) and only bounds its cost, never gives $S'$ a closed form — formalized here as an existential over a per-segment cost witness w', bounded above and below exactly as the proof's own argument does (with the lower bound d(s i) ≤ w' i serving as the guard against the vacuous witness w' = 0, since without it the existential is trivially satisfiable and asserts nothing). Lemma 6.2's proof, by contrast, reuses the same trajectory in both models with no construction at all, formalized directly as a cost comparison between costStandard and costNewPhases applied to the identical (s, w) data.

Formalization scope

WeightedStar V bundles centerDist : V → ℝ (the book's $d'$) with non-negativity; WeightedStar.d is the collapsed charge $d(i) = 2d'(i)$. costStandard/costNewPhases are literal transcriptions of the two models' displayed cost formulas over a Fin k-indexed run/phase sequence. standard_to_new (Lemma 6.1) is the existential described above; new_to_standard (Lemma 6.2) is the direct cost comparison. Reals throughout; V is left a general Type* (not assumed Fintype) since neither lemma's own statement needs the chapter's finiteness assumption $|V|=N$ — that assumption only matters for the unnumbered $O(\log N)$-competitive claim of Section 6.2, out of scope per BRIEF.md's explicit instruction (no numbered theorem to formalize it against). This correctly rules out the trivializing formalization in which "new-model solution" is left as an unconstrained free variable satisfying only the conclusion's own inequality, or in which the star structure is dropped entirely in favor of an arbitrary metric (the chapter's own reduction to a per-state charge $d(i)$, rather than a full metric $d: V\times V\to\mathbb R$, is precisely what the star's structure licenses, and is preserved here via WeightedStar.d rather than a bare hypothesis-level function). Welcome contributions: completing the two sorrys (Lemma 6.1's needs an explicit construction of $S'$ and its per-segment cost bound; Lemma 6.2's is a short termwise algebraic argument), and formalizing the Section 6.2 covering-LP algorithm and its $O(\log N)$-competitive claim as a follow-on mission once it can be stated against a numbered result.

Selected references

• N. Buchbinder, J. Naor. The Design of Competitive Online Algorithms via a Primal-Dual Approach. Foundations and Trends in Theoretical Computer Science, 3(2-3):93-263, 2009. https://doi.org/10.1561/0400000024
• Bansal et al., reference [14] of this chapter's own bibliography (not independently verified by this mission), cited by the book as the source of the weighted-star MTS results this chapter presents ("The results in this chapter are based on the work of Bansal et al. [14]," p. 147).
• Borodin, Linial, Saks, reference [29] of this chapter's own bibliography (not independently verified by this mission), cited as the paper that originally formulated the standard MTS model and its tight $2N-1$ deterministic bound (p. 147).

Motivation

Caching is a two-level memory-management problem — the fast level (cache) can hold only $k$ items, and the algorithm must decide, online, which item to evict whenever the current request misses — that is normally analyzed through the competitive ratio of ad hoc marking or LRU-style rules. Buchbinder and Naor's survey [1] instead recasts weighted caching (non-uniform fetching costs) as an instance of the covering/packing linear program, and derives a fractional online algorithm through the same primal-dual recipe formalized in this series' 04-framework mission (Chapter 4), but for a genuinely different LP shape: the caching LP's right-hand side varies from constraint to constraint, unlike Chapter 4's uniform $b(j)=1$. This mission covers Sections 7.1-7.2 of Chapter 7, "Generalized Caching": the fractional weighted-caching algorithm and its $2(1+\ln k)$-competitive analysis. Sections 7.3-7.4, which further generalize to non-uniform page sizes (not just costs), are out of scope — a natural follow-on mission, not attempted here (see Formalization scope).

Setting

Fix a finite set $V$ of primal variables $x(p,j)$ — one per page $p$ and each of its eviction intervals between its $j$-th and $(j{+}1)$-th request — with fetching cost $c(p,j) = c_p \ge 1$ (the book's standing weighted-caching assumption), and a finite set $\mathrm{Time}$ of online constraints, one per request time $t$, revealed in the order enumerated by $\mathrm{Time}$. The eviction-charged LP formulation (the book charges for evicting pages rather than fetching them, an equivalent reformulation up to an additive constant independent of the request sequence) constrains, at each time $t$: $\sum_{v \in S(t)} x_v \ge \mathrm{rhs}(t)$, where $S(t)$ is the set of currently-active eviction variables for pages present until $t$ (excluding the page just requested) and $\mathrm{rhs}(t) = |B(t)| - k$ is the amount of cache space those pages must collectively vacate. The Lagrangian dual has a variable $y(t)$ per request time and a variable $z(p,j)$ per eviction interval, with dual constraint $\big(\sum_{t \mid v \in S(t)} y(t)\big) - z_v \le c_v$. As in Chapter 4, primal variables may only increase and the algorithm sees each constraint only upon its arrival.

The Fractional Caching algorithm (p. 153-154) sets each $x(p,j)$ to jump from $0$ to $1/k$ the first time its dual constraint tightens, then increases continuously according to an exponential function of the accumulated dual sum until it saturates at $1$ (at which point $z(p,j)$ begins absorbing further dual increase at the same rate, freezing $x(p,j)$). This is a genuinely different LP shape from Chapter 4's framework (non-uniform, time-varying right-hand side) reusing the same complementary-slackness design pattern as that chapter's Algorithm 3.

Formalization targets

Theorem 7.1 (the goal, p. 154), given the algorithm's final dual values $y \ge 0$, $z \ge 0$ and primal feasibility:

$$\Big(\forall v,\ \textstyle\sum_{t \mid v \in S(t)} y_t - z_v \le c_v(1+\ln k)\Big) \ \Longrightarrow\ \Big(\forall x''\text{ feasible},\ \textstyle\sum_v c_v x_v \le 2(1+\ln k)\sum_v c_v x''_v\Big),$$

i.e. the algorithm is $2(1+\ln k)$-competitive, with the constant taken verbatim from the book's own theorem statement (no $O(\cdot)$ instantiation needed here, unlike most goals in this series). The antecedent is itself Eq. (7.2) (p. 155), formalized as the milestone dual_near_feasible: the algorithm's dual solution, scaled down by $1+\ln k$, is feasible — the book's own intermediate step, derived from the fact that every cachingX value is capped at $1$.

Significance

Chapter 7 is the first chapter in this survey to apply the online primal-dual method to an LP whose right-hand side is not uniformly $1$ (unlike Chapters 4 and 5), demonstrating the method's reach beyond the "simplified" 0/1-coefficient covering LP that 04-framework formalizes. The $2(1+\ln k)$ fractional guarantee is also the analytical core of the chapter's randomized rounding result (Theorem 7.3, not part of this mission — see Formalization scope), which converts it into an actual $O(\log k)$-competitive randomized algorithm against an adaptive adversary, and of the chapter's further generalization to non-uniform page sizes (Theorem 7.5, Sections 7.3-7.4). No formal development of weighted or generalized caching was found on the platform as of 2026-09-20 (searches below); the existing KServer.* namespace formalizes a different, unweighted, uniform $k$-server model and shares no substrate with this mission. This mission is the first.

Difficulty

As with 04-framework's Algorithm 3, the central obstacle is characterizing an online process by its final output alone: cachingX is defined as the algorithm's own closed-form update rule (threshold-then-exponential, capped once $x(p,j)=1$), evaluated at the run's final accumulated dual values, rather than as an independently-constrained free variable — the latter would let $x$ and $y$ be chosen to satisfy the conclusion's inequalities directly, trivializing the claim that a specific online algorithm achieves this ratio. Establishing that the capped closed form is faithful (not merely an invented convention) requires the same monotonicity argument 04-framework's alg3X uses, adapted to this chapter's extra $z(p,j)$ term inside the exponent (present here; absent from Chapter 4's Algorithm 3). The proof's own structure — splitting the primal cost into a $0\to1/k$ contribution ($C_1$) bounded via complementary slackness and a $1/k\to1$ contribution ($C_2$) bounded via a derivative/telescoping argument over the continuous accumulation process (Eqs. (7.6)-(7.10), p. 155-157) — is, as in Chapter 4, a genuinely dynamic fact about the trajectory, not encoded as a hypothesis; the mission states the theorem faithfully and leaves the sorry for that argument, per this series' documented-simplification convention.

Formalization scope

CachingInstance V Time bundles S : Time → Finset V, rhs : Time → ℝ (unlike 04-framework's CoveringInstance, whose right-hand side is fixed at $1$ throughout), c : V → ℝ with hc_pos : ∀v, 1 ≤ c v (the book's own literal cp ≥ 1, not a strengthening), and k : ℕ with hk_pos : 0 < k. dualSum inst y v := ∑_{t \mid v \in S(t)} y_t, matching 04-framework's pattern. cachingX inst y z v is a noncomputable def: 0 before activation, otherwise min 1 ((1/k) exp((dualSum - z - c v)/c v)), so "the algorithm's output" is genuinely a function of its dual trajectory. Reals throughout; Real.log for the book's natural log $\ln$. Explicitly out of scope: Section 7.3's rounding apparatus (Theorem 7.3, the map from fractional to randomized-integral cache states) and Section 7.4's non-uniform-page-size generalization (Theorem 7.5) — both are natural follow-on missions building on this one's CachingInstance and cachingX, not attempted here per this chunk's own BRIEF.md, which flags Theorem 7.1 alone as "a complete, self-contained mission goal" when the rounding apparatus proves too heavy for a single pass. Welcome contributions: completing the two sorrys, and the Section 7.3-7.4 follow-on mission.

Selected references

• N. Buchbinder, J. Naor. The Design of Competitive Online Algorithms via a Primal-Dual Approach. Foundations and Trends in Theoretical Computer Science, 3(2-3):93-263, 2009. https://doi.org/10.1561/0400000024

Motivation

Network routing is one of the paradigmatic applications of the online primal-dual method: requests for bandwidth between a source and target arrive one at a time, and the algorithm must commit bandwidth to paths without knowing future requests. Chapter 4 already gave a simple (3, O(log n))-competitive routing algorithm as an illustration of the general framework. This chapter asks for something qualitatively stronger: a uni-criteria (1, O(log n))-competitive algorithm — one that routes the full optimal bandwidth (no loss on the throughput side at all), paying only in a bounded edge-capacity violation. The chapter shows this exact-throughput guarantee is achievable, and is moreover the key building block for several other routing objectives (fair routing, max-min fairness) built on top of it in Section 9.2 — a (1, O(log n))-competitive algorithm composes into those richer objectives in a way a merely constant-factor-lossy algorithm does not.

Setting

Fix a graph $G=(V,E)$, $|V|=n$, $|E|=m$, with integer edge capacities $u: E \to \mathbb{N}$. Routing requests $r_i$ arrive online, each demanding one unit of bandwidth between a source and target; in the splittable model (this chapter's comparison class), a request's bandwidth may be divided across multiple paths. A $(c_1,c_2)$-competitive algorithm routes at least $1/c_1$ of the maximum possible bandwidth while guaranteeing every edge's load (bandwidth allocated divided by capacity) is at most $c_2$. The chapter's generic algorithm (Section 9.1) maintains, for each of $O(\log n)$ copies $G_0,\dots,G_k$ of the graph (copy $j$ keeping only edges of capacity at least $m^j$, each capped at $\min(u(e), m^{j+2})$), a primal-dual pair matching Chapter 4's own routing LP (Fig. 9.1, identical to Fig. 4.2): a request is routed on the shortest path (by the copy's current primal edge-lengths $x(e,j)$) if that length is below $1$, multiplicatively updating $x(e,j)$ on the path's edges; otherwise, subject to a capacity-limited fallback rule, on an arbitrary feasible path.

Formalization targets

Theorem 9.2 (goal, p. 204): the algorithm is (1, O(log n))-competitive with respect to all splittable routing solutions — exact throughput (ratio 1), edge load at most O(log n).

Lemma 9.1 (milestone, p. 202-204): a single copy $G_j$'s own guarantee, which Theorem 9.2's proof composes across all copies: the algorithm accepts at least $M$ (the maximum splittable bandwidth achievable in $G_j$, out of the requests introduced to it) and incurs load $O(\log n)$ on every edge of $G_j$.

Significance

This is the survey's demonstration that the online primal-dual method, in its most basic form (a single accumulating dual sum driving a multiplicative primal update, exactly Chapter 4's framework), scales to a genuinely harder bicriterion objective once composed across a carefully constructed family of graph copies — the copies are what let the algorithm avoid ever needing to reason about which of the exponentially many $s_i$-$t_i$ paths to consider, reducing routing to a sequence of independent shortest-path computations. The chapter's own Section 9.2 builds a coordinate-wise-competitive fair-routing algorithm directly on top of Theorem 9.2 (not formalized here), and its Notes section places $(1, O(\log n))$-competitiveness as "a crucial non-trivial step" the chapter needed before those richer objectives became tractable at all. No prior formalization of online routing, splittable or otherwise, was found on the platform as of 2026-09-20 (search below).

Difficulty

This is the most algorithmically intricate chapter in this series: the algorithm processes each request against every one of $O(\log n)$ graph copies, each copy running its own instance of the Chapter-4-style primal-dual update, and Theorem 9.2's own proof composes Lemma 9.1's per-copy guarantee via a combinatorial backward induction (partitioning the offline-optimal solution's paths into groups by bottleneck capacity, and showing group by group that the algorithm's cumulative routed bandwidth across the top levels dominates the cumulative optimal bandwidth in those groups) together with a separate geometric argument bounding how many copies any single edge can meaningfully appear in. Fully modeling the copy construction, the request-routing process, and both composition arguments from first principles was judged to exceed this mission's time budget without sacrificing the faithfulness of what does get stated (per CAPTAIN_BRIEF.md rule 6). Instead: Lemma 9.1 is formalized via the two facts its own proof isolates as doing the real work — a weak-duality contradiction bound (stepB ≥ M − uMin) and the step-(1c) fallback's own greedy-fill rule for part (i); the multiplicative-update invariant x(e,j) ≤ 2 for part (ii), whose consequence — the exact constant 2 + 6·log₂n — is re-derived from scratch in this mission (the displayed equation this derivation depends on was garbled by the PDF's text extraction; it was confirmed against the actual typeset page image before drafting, see SELF_REVIEW.md). Theorem 9.2 then composes Lemma 9.1 across copies via two explicit, clearly-labeled hypotheses standing for the book's own backward-induction accounting and edge-multiplicity argument, respectively — genuine mathematical content this mission does not re-derive, named honestly as hypotheses rather than silently assumed away or approximated by a weaker statement.

Formalization scope

No shared data structure was introduced: every quantity in both theorems (bandwidths, capacities, loads) is a plain real-number hypothesis-level parameter, since neither theorem's own content needs a reusable instance record (unlike the packing/covering CoveringInstance of 04-framework, this chapter's per-copy quantities are consumed once each, not threaded through a family of algorithms). per_copy_guarantee (Lemma 9.1) takes the weak-duality bound, the step-(1c) fill rule, and the x(e,j)≤2 invariant as hypotheses and derives both parts of the lemma's conclusion by real algebra (a sign case-split for part (i); Real.logb/rpow manipulation for part (ii)). routing_competitive (Theorem 9.2) takes Lemma 9.1's guarantee (universally quantified over the copy index J, a general Fintype) plus the two composition hypotheses described above, and derives the bicriterion conclusion by summation, transitivity, and scaling. This correctly rules out the trivializing formalization in which the composition hypotheses are strengthened to directly assert the theorem's own conclusion (each is a strictly weaker, independently-motivated fact — the backward-induction accounting identity and the geometric edge-multiplicity bound — checked in MODERATION_NOTES.md against this exact failure mode). Reals throughout; Real.logb 2 for log₂. Welcome contributions: completing the two sorrys (Lemma 9.1's part (i) is short algebra; part (ii) needs Real.rpow/Real.logb lemmas; Theorem 9.2's is transitivity/summation once its hypotheses are in hand), and — the natural follow-on — formalizing the copy construction and the backward-induction/edge-multiplicity arguments hquota/hload_aggregation currently stand in for, which would upgrade them from hypotheses to theorems in their own right; Section 9.2's coordinate-wise-competitive fair-routing algorithm (Theorem 9.3) and the matching lower bound (Lemma 9.5) are further natural follow-ons.

Selected references

• N. Buchbinder, J. Naor. The Design of Competitive Online Algorithms via a Primal-Dual Approach. Foundations and Trends in Theoretical Computer Science, 3(2-3):93-263, 2009. https://doi.org/10.1561/0400000024

Motivation

The group Steiner tree problem generalizes the ordinary Steiner tree problem: given a rooted tree and several groups of vertices, find a minimum-cost subtree that connects at least one vertex of each group to the root. It is a canonical instance of the generalized-connectivity family this survey studies in Chapter 11 — a family that also contains the online set-cover problem (Chapter 5 of this series) as a special case. Buchbinder and Naor's chapter shows how to convert the celebrated offline randomized-rounding algorithm of Garg, Konjevod and Ravi [56] into an online one, by imitating its per-edge coupling structure one iteration at a time as the online fractional solution (obtained from this survey's own Chapter 4 framework) evolves. This mission formalizes that online rounding scheme's three defining probabilistic guarantees and the resulting competitive-ratio theorem.

Setting

Fix a rooted tree T = (V, E, r) with non-negative edge costs c : E → ℝ, and k groups g₁, …, g_k ⊆ V, each request (r, gᵢ) arriving online. An online covering algorithm (from Chapter 4's framework, applied to the LP relaxation of this connectivity problem) maintains a monotonically increasing fractional weight w : E → ℝ on the edges, reinterpreted so that wₑ is the maximum flow that can be routed through e to any vertex of its subtree — a technical substitution needed so weights are monotone non-increasing along any root-to-leaf path, the property the rounding algorithm requires. At the end of each iteration in which some weights are augmented from w to w' = w + δ, the rounding algorithm processes every edge e with δₑ > 0, in topological order starting from the root, and randomly decides whether to add it to a growing random edge-cover C ⊆ E: deterministically, if w'ₑ > 1; via a single coin flip, if e is incident to the root or its parent edge's inclusion in C is already certain; via a coin flip conditional on the parent edge already being in C, otherwise. Because a coin is only ever flipped for a child once its parent is (or is already known to be) in C, C always induces a connected subtree containing the root.

Formalization targets

Theorem 11.4 (the goal, p. 231): there is a randomized online algorithm for the group Steiner problem in trees with competitive ratio O(log²n log k), where n is the number of leaves. It is built by running T independent trials of the rounding scheme in parallel and taking the union of the resulting covers, for T chosen (this mission's own explicit derivation — the book gives only the narrative "we run O(log k log N) independent trials... using simple probabilistic analysis") so that every group fails to be covered with probability at most 1/(2k), while the union's expected cost stays at T · log(n) · OPT.

Three milestones, in attack order, each stated exactly as the book states it (p. 230-231), with the book's own caveat "we state the main lemmas and omit the proofs" preserved — no in-source proof exists for any of the three beyond the algorithm's own description, so each is left sorry with no invented proof strategy:

• Lemma 11.1: at the end of an iteration, ℙ[e ∈ C] = w'ₑ for every edge, and ℙ[e ∈ C] = 1 whenever wₑ > 1 already.
• Lemma 11.2: the expected cost of C is at most ∑_{e∈T} cₑ w'ₑ (linearity of expectation applied to Lemma 11.1).
• Lemma 11.3: for a group g of size at most N with total routable flow wg ≥ 1, the probability some vertex of g is covered is Ω(1/log N).

Significance

This is the survey's most involved application of the primal-dual framework: unlike Chapters 5, 9, 10 and 13, which round a single scalar decision per online step, the group Steiner algorithm must couple an entire iteration's worth of edge decisions so that the resulting random set stays a connected subtree — the coin-flip probabilities in the Algorithm box are exactly the minimal adjustment needed to keep marginal probabilities matching the fractional solution while preserving this connectivity invariant online. No formal development of the group Steiner problem (online or offline) was found on the platform as of 2026-09-20; this mission is the first.

Difficulty

Two distinct obstacles. First, faithfully representing "the probability that e ∈ C" for an online, coupled random process without assuming its proof: the mission represents the algorithm's random cover as an abstract finite probability distribution RandomCover E and states each lemma as an implication from the Algorithm box's three coupling rules (transcribed as hypotheses on marginal and conditional probabilities) to the claimed marginal or expected-value conclusion — capturing exactly what the book asserts without proof, rather than either assuming the conclusion trivially or constructing a full multi-iteration coupled process (which the source's own "we omit the proofs" indicates is genuinely nontrivial, citing [56]). Second, Theorem 11.4's own competitive ratio is stated in the book only asymptotically, with a purely narrative derivation ("we run O(log k log N) independent trials... we get a competitive ratio of O(log n log k log N)... probability at least 1 − 1/k") and no displayed formula anywhere in the chapter. Per this series' explicit-constants rule, this mission supplies its own explicit closed form for the number of trials T and the resulting bounds via a standard Chernoff/union-bound argument applied to Lemma 11.3's constant α; this derivation is the mission's own (documented below), not a transcription, since none exists in the source to transcribe.

Formalization scope

RandomCover E is a finite pmf p : Finset E → ℝ (Finset E itself finite since E is Fintype), with marg, condProb and expectedCost/probHits derived from it by ordinary Finset sums — no measure theory, since the sample space is always finite. RoundedTree E bundles parent : E → Option E (e(p)) and a non-negative cost. Lemma 11.3's wg (the flow routable to a group's vertices simultaneously) is left as hypothesis-supplied data rather than defined via an explicit max-flow formalization, which this mission's scope does not require (welcome contribution). Theorem 11.4's number of trials is the explicit closed form T = ⌈(log N · log(2k)) / α⌉, α the (existentially quantified, uniform) constant from Lemma 11.3; its coverage guarantee is 1 − 1/(2k) per group (this mission's own union-bound derivation), not the book's stated 1 − 1/k — the book reaches the stronger bound via an additional shortest-path fallback mechanism for any group the trials miss, which is out of scope here (welcome contribution, along with completing any of the four sorrys and formalizing Theorem 11.5's extension to general graphs via HST embedding, out of scope since it depends on an external embedding result not proved in this book).

Selected references

• N. Buchbinder, J. Naor. The Design of Competitive Online Algorithms via a Primal-Dual Approach. Foundations and Trends in Theoretical Computer Science, 3(2-3):93-263, 2009. https://doi.org/10.1561/0400000024
• N. Garg, G. Konjevod, R. Ravi. A polylogarithmic approximation algorithm for the group Steiner tree problem. Journal of Algorithms, 37(1):66-84, 2000 (cited as [56] in the survey).
• N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor. A general approach to online network optimization problems. ACM Transactions on Algorithms, 2(4):640-660, 2006 (cited as [4], the source of this chapter's results per the Notes, p. 231).

Motivation

The classical online allocation (AdWords) problem has a tight 1 - 1/e competitive ratio in general, achieved by the water-level algorithm and matched by a lower bound in which the number of buyers interested in each item can be as large as the total number of buyers. Buchbinder and Naor's Chapter 13 observes that in many realistic settings each item's interested-buyer set is much smaller than the total buyer population, and shows this structural fact — an explicit bound d on interested buyers per item — provably beats 1 - 1/e for every finite d, via a deliberately non-water-level algorithm. This mission formalizes that algorithm's competitive ratio and its matching lower bound.

Setting

A seller offers items to n buyers one at a time; buyer i has budget B(i) > 0. Each item j has a fixed price b(j) > 0 and a set S(j) of interested buyers with |S(j)| ≤ d. The fractional LP relaxation (Fig. 13.1) allocates y(i,j) ∈ [0,1] of item j to buyer i, subject to each item being sold at most once in total and each buyer's spending never exceeding budget; the seller's objective is to maximize total revenue ∑_j ∑_{i∈S(j)} b(j)y(i,j). Buyers are partitioned into d+1 levels by the fraction of budget spent so far (level k = spent between k/d and (k+1)/d); on each new item, the allocation algorithm splits it equally among the interested buyers in the lowest non-empty level, moving to the next level once that level's buyers are exhausted or saturated — deliberately not the naive "water-level" rule of splitting among the least-spent buyers, which the book shows cannot beat 1-1/e even for small d. The analysis tracks a piecewise-linear trade-off potential function f_d, built from a geometric sequence, that relates each buyer's level to their contribution to a feasible primal (covering) solution.

Formalization targets

Theorem 13.1 (the goal, p. 240): the allocation algorithm is C(d)-competitive, with the book's own explicit closed form C(d) = 1 - (d-1)/(d(1+1/(d-1))^{d-1}) — strictly better than 1 - 1/e for every finite d, approaching it as d → ∞ (Table 13.1). Formalized via the survey's standard weak-duality pattern (as in 04-framework's Theorem 4.3): given the algorithm's per-item primal/dual cost changes satisfying the book's core inequality ΔX(j) ≤ (1/C(d))ΔY(j) (established there by a potential-function case analysis, not reproduced here), the algorithm's realized profit is C(d)-competitive against any feasible comparison allocation.

Lemma 13.2 (milestone, p. 244): a matching lower bound, C(d) ≤ 1 - (k - kH(d) + ∑_{i=1}^k H(d-i))/d, where H is the harmonic number and k is the largest value with H(d) - H(d-k) ≤ 1.

Significance

This chapter is the survey's demonstration that a structural restriction invisible to the classical 1-1/e lower bound — a bound on demand concentration, not on budgets or prices — can be exploited algorithmically, and the exploiting algorithm is not the naive generalization of the water-level rule but a genuinely different level-based, "who's-behind" allocation rule. No formal development of the bounded allocation problem was found on the platform as of 2026-09-20; this mission is the first.

Difficulty

The chapter's own proof of Theorem 13.1 (p. 241-244) is a page-and-a-half case analysis on how an item's fractional allocation crosses level boundaries, bookkeeping the change in both the primal potential-function value and the dual profit through several sub-cases (an item fully absorbed by one level; an item that empties a level and continues into the next; a level exhausting every interested buyer's budget). This mission formalizes the resulting per-item inequality ΔX(j) ≤ (1/C(d))ΔY(j) as a hypothesis (the theorem's own headline claim, not a case-by-case re-derivation) rather than modeling the stateful, order-dependent level-allocation process itself — the same scope choice this series makes for Chapter 11's randomized rounding process, where the book similarly omits (there, entirely; here, gives but does not ask this mission to reproduce) the underlying case analysis. The potential function f_d and its connection to the algorithm's primal variable (allocX) are formalized precisely, since they are what the goal's proof and Lemma 13.2 both depend on structurally, even though the case analysis linking them to ΔX/ΔY is left as the theorem's sorry.

Formalization scope

AllocationInstance I J bundles the LP data of Fig. 13.1 (S, B, b, d ≥ 2, ∀j, |S(j)|≤d) — restated locally per this series' rule that concurrent drafts cannot import each other, even though the problem is a special case of Chapter 10's ad-auctions model (the two chapters' algorithms differ: Chapter 10's is proportional-to-remaining-budget, this chapter's is level-based). geomSeq/potential transcribe the geometric sequence a_t and the potential function f_d at its level grid points exactly (not extended to non-grid-point reals, since Theorem 13.1's and Lemma 13.2's own statements only need the grid values). allocX connects the potential function to the algorithm's primal variable via each buyer's final level t(i). packingFeasible/packingValue transcribe Fig. 13.1's dual/packing LP with a genuine two-index allocation y : I → J → ℝ (not collapsed to a single per-item variable, unlike Chapter 4's simpler 0/1-coefficient framework). harmonicNum is the ordinary harmonic number. The level-based algorithm's literal stateful per-item update rule (which buyers move between which levels, in what order, within a single item's allocation) is not modeled directly — a documented scope reduction (STATUS.md), not a substitution of the "water-level" algorithm the book explicitly warns against (this mission's theorem13_1 commits to neither algorithm's literal rule, only to the resulting invariant the book's own proof establishes for the level-based one). Welcome contributions: completing the two sorrys, and modeling the level-allocation process explicitly enough to derive hinvariant from first principles.

Selected references

• N. Buchbinder, J. Naor. The Design of Competitive Online Algorithms via a Primal-Dual Approach. Foundations and Trends in Theoretical Computer Science, 3(2-3):93-263, 2009. https://doi.org/10.1561/0400000024
• B. Kalyanasundaram, K. Pruhs. An optimal deterministic algorithm for online b-matching. Theoretical Computer Science, 233(1-2):319-325, 2000 (cited as [73], the 1-1/e lower bound).

Motivation

Chapter 4's framework (formalized in this series' 04-framework mission) solves the online covering-packing pair only in the restricted setting a(i,j) ∈ {0,1}, b(j) = 1 — every constraint is an unweighted "cover me with at least one of these" condition. Chapter 14 delivers the promise made at the very start of the survey (p. 115: "we show how to extend the ideas we present here to handle general (non-negative) values of a(i,j) and b(j)"): fully general non-negative coefficients, normalized so every constraint reads ∑_i a(i,j)x(i) ≥ 1. This mission formalizes both halves of that generalization — the packing scheme (Theorem 14.1, with a matching lower bound, Lemma 14.2, showing an extra additive term is unavoidable) and the covering scheme (Theorem 14.3, the goal).

Setting

Fix a finite set I of primal (covering) variables with positive costs c(i), and a finite set J of dual (packing) variables/covering constraints, with a(i,j) ≥ 0 for every pair (Fig. 14.1). The packing scheme (Section 14.1) is parameterized by a target competitive ratio B > 0: on each new dual variable y(j) and its coefficients a(i,j), the algorithm increases y(j) continuously and each x(i) by an explicit exponential increment function until the new primal constraint is satisfied, achieving B-competitiveness for the packing objective at the cost of an additive O(log(a_i(max)/a_i(min))) term (beyond the multiplicative O(log n)) in how much each dual constraint can be violated — qualitatively different from Chapter 4's purely multiplicative O(log d) bound, and Lemma 14.2 proves this additive term cannot be removed. The covering scheme (Section 14.2) instead works in phases: each phase assumes a doubling lower bound α(r) on OPT and "forgets" its primal/dual variables once the primal cost exceeds α(r), restarting with α(r+1) = 2α(r) — a structurally different mechanism from Chapter 4's direct algorithms, needed because with general coefficients a single monotone run can no longer be analyzed via one potential function alone.

Formalization targets

Theorem 14.3 (the goal, p. 253): for any B > 0, the phase-based covering scheme (each constraint normalized to ∑_i a(i,j)x(i) ≥ 1/B) is competitive with an explicit ratio 8 log(2n)/B, taken directly from the proof's own final displayed chain, 2α(r) ≤ 4α(r-1) ≤ (8 log(2n)/B) Y(r-1) ≤ (8 log(2n)/B) OPT (p. 253-254) — the theorem's own statement only gives O(log n/B), so this explicit constant is this mission's own instantiation from the proof, not an independent derivation and not a transcription of a displayed theorem-level formula (flagged, per this series' explicit-constants rule).

Two milestones, in attack order:

• Theorem 14.1 (p. 249): the packing scheme is B-competitive, and violates each dual constraint by at most the book's own exact displayed bound c(i)·2log(1 + n·a_i(max)/a_i(min))/B (Claim (3) — the exact constant the proof establishes, not the theorem headline's O(·) simplification).
• Lemma 14.2 (p. 251): a matching lower bound, on the book's own explicit single-constraint instance, showing the additive log(a(max)/a(min)) term of Theorem 14.1 is necessary.

Significance

This chapter is the survey's demonstration that the primal-dual framework's core technique survives its most natural generalization, at the price of an explicit extra term the chapter also proves is unavoidable — a tight characterization, not merely an upper bound. Every other online covering/packing chapter in this survey (set cover, routing, ad-auctions, bounded allocation) is technically a special case of this chapter's general model; Chapter 4's restricted framework is the pedagogical entry point, and this chapter is where the general theory actually lives. No formal development of the general packing-covering problem was found on the platform as of 2026-09-20; this mission is the first.

Difficulty

Two distinct obstacles, mirroring this chapter's own two schemes. First, Theorem 14.1's proof (p. 249-251) establishes its per-round primal/dual derivative inequality via a direct calculus argument (differentiating the explicit increment function) — formalized here as a hypothesis (hX_le_BY) standing for that calculation, not reproduced, since the goal is a faithful statement of the resulting competitive ratio, and the increment function's own exponential form is transcribed in the theorem's docstring but the differentiation itself is out of scope. Second, Theorem 14.3's phase-based mechanism is genuinely stateful across an unbounded number of phases (each phase resets its own primal/dual variables while the LP's actual variables retain the running maximum) — modeling this process explicitly is comparable in complexity to Chapter 13's level-based algorithm, and this mission makes the same scope choice: the mechanism's output (the resulting cost/profit relationship, hX_le_ratio) is taken as a hypothesis standing for the book's own Claims (1) and (3) combined, rather than constructed phase-by-phase.

Formalization scope

GeneralInstance I J bundles Fig. 14.1's fully general LP data (a(i,j) ≥ 0, c(i) > 0) — restated locally (not importing 04-framework's CoveringInstance) per this series' rule against cross-draft imports, even though this chapter is the direct generalization of that one. aMax/aMin are the per-variable (not per-instance) maximum and minimum-non-zero coefficients Theorem 14.1 needs. harmonicNum is restated locally (duplicated from 13-bounded-allocation's own definition, for the same no-cross-draft-import reason). Both goal-adjacent theorems use this series' weak-duality "competitive against any feasible comparison solution" pattern (04-framework, reused as a convention, not re-derived): Theorem 14.1 against any feasible packing comparison (matching that it concerns the packing side), Theorem 14.3 against any feasible covering comparison (matching the covering side). Welcome contributions: completing the three sorrys (Theorem 14.1's calculus argument, Theorem 14.3's phase-based mechanism constructed explicitly, and Lemma 14.2's direct summation argument, which is the most tractable of the three to actually prove), and formalizing the sanity check that both schemes reduce to Chapter 4's Algorithm 1/2/3 when a(i,j) ∈ {0,1}, b(j) = 1 (checked by hand in SELF_REVIEW.md, not as a Lean lemma).

Selected references

• N. Buchbinder, J. Naor. The Design of Competitive Online Algorithms via a Primal-Dual Approach. Foundations and Trends in Theoretical Computer Science, 3(2-3):93-263, 2009. https://doi.org/10.1561/0400000024

Motivation

A system that processes a stream of tasks can often be configured in several ways, and the configuration affects both the cost of the current task and the cost of switching before the next one: paging schemes, replicated files, server placements. When the future is unknown, the natural worst-case yardstick is competitive analysis, introduced by Sleator and Tarjan for list update and paging (Sleator–Tarjan 1985): an on-line strategy is compared with the optimal strategy that knows the whole input in advance.

Borodin, Linial and Saks (J. ACM 1992; conference version STOC 1987) proposed metrical task systems as a single model containing all such problems, and determined the exact deterministic competitive ratio of every such system. Their theorem is the starting point of the on-line-algorithms literature on metrical task systems, the $k$-server problem (Manasse–McGeoch–Sleator 1990) and their randomized variants.

Timeline. 1985: Sleator and Tarjan introduce competitive analysis for paging and list update. 1987: Borodin, Linial and Saks prove $w(S,d)=2n-1$ for every $n$-state metrical task system (journal version 1992). 1990: Manasse, McGeoch and Sleator extend the task-system model to restricted task sets and pose the $k$-server conjecture. The randomized ratio of the uniform task system, bounded in the same paper between $H(n)$ and $2H(n)$, is the subject of the companion mission.

Setting

A task system $(S,d)$ has a finite set $S$ of $n$ states and a transition-cost matrix $d$ with $d(i,i)=0$, $d(i,j)>0$ for $i\neq j$, and the triangle inequality $d(i,j)+d(j,k)\ge d(i,k)$. It is metrical if also $d(i,j)=d(j,i)$.

A task $T$ is a vector of nonnegative processing costs $T(s)$, $s\in S$. Given a task sequence $\mathbf T=T^1\cdots T^m$ and an initial state $s_0$, a schedule is a map $\sigma:\{0,\dots,m\}\to S$ with $\sigma(0)=s_0$; task $T^i$ is processed in state $\sigma(i)$, and the cost is

$$c(\mathbf T;\sigma)=\sum_{i=1}^m d(\sigma(i-1),\sigma(i))+\sum_{i=1}^m T^i(\sigma(i)).$$

The off-line optimum $c_0(\mathbf T)$ is the minimum over all schedules. An on-line algorithm $A$ chooses $\sigma(i)$ knowing only $s_0$ and $T^1,\dots,T^i$; its cost is $c_A(\mathbf T)$. For $w>0$, $A$ is $w$-competitive if there is a constant $K_w$ with $c_A(\mathbf T)\le w\,c_0(\mathbf T)+K_w$ for every finite task sequence. The competitive ratio of $A$ is $w(A)=\inf\{w: A\text{ is }w\text{-competitive}\}$, and the competitive ratio of the task system is $w(S,d)=\inf_A w(A)$.

For the upper bound the paper also uses continuous-time schedules, in which task $T^i$ occupies the interval $[i,i+1)$ and the scheduler may change state at any real time, paying $\int_i^{i+1}T^i(\sigma(t))\,dt$ for processing. For a general (possibly asymmetric) matrix $d$, the cycle offset ratio $\psi(d)$ is the maximum over closed walks $s_0,\dots,s_k=s_0$ of $\sum_i d(s_{i-1},s_i)\big/\sum_i d(s_i,s_{i-1})$; it equals $1$ when $d$ is symmetric.

Formalization targets

Goal: Theorem 1.1

For every metrical task system $(S,d)$ with $n$ states,

$$w(S,d)=2n-1 .$$

The value depends on $n$ only, not on the distances.

Milestones

• Lemma 2.1. If $c_0(T^1\cdots T^m)\to\infty$ along an infinite task sequence $\mathbf T$, then $w(A)\ge w_{\mathbf T}(A)=\limsup_m c_A/c_0$.
• Theorem 2.2. Against the cruel taskmaster $M(\varepsilon)$, which charges $\varepsilon$ in the state the algorithm currently occupies,

$$w_{\mathbf T(\varepsilon)}(A)\ge\frac{2n-1}{1+\varepsilon/\min_{i\neq j}d(i,j)} .$$

• Lemma 3.1. Every on-line continuous-time algorithm is matched, on every task sequence, by an on-line discrete-time algorithm.
• Lemmas 6.3, 6.4, 6.2. Properties of the functions $f_k$ that drive the algorithm $A^*_d$: $f_k(s)-f_k(s')\le d(s',s)$; the identity $2\sum_{s\ne s_k}f_k(s)+f_k(s_k)=C_{k-1}+\sum_{i\le k}d(s_i,s_{i-1})$; and $f_k\le h_k$, the off-line cost at the $k$-th transition time.
• Theorem 6.1 (= Theorem 1.2). For every task system, symmetric or not, $A^*_d$ has competitive ratio at most $(2n-1)\psi(d)$.

Significance

The theorem settles the deterministic competitive ratio of the whole class of metrical task systems: the lower bound says that no deterministic on-line strategy can beat $2n-1$ on any metric, and the upper bound supplies one algorithm that achieves it on every metric. For asymmetric costs the same algorithm gives $(2n-1)\psi(d)$. The $2n-1$ lower bound is also the benchmark against which restricted models, such as paging and the $k$-server problem, measure their improvements, and the randomized question it leaves open drove much of the later work on metrical task systems.

The result was proved in 1987 and is standard; to the best of our knowledge no machine-checked proof exists. A formal development would provide a reusable model of deterministic on-line algorithms and competitiveness (on-line maps from task prefixes, additive competitiveness, infima over algorithms), an adversary construction by mutual recursion with an arbitrary algorithm, and an exact treatment of continuous-time schedules with piecewise-constant task costs. These pieces are reusable for other competitive-analysis results.

Difficulty

The lower bound is not a single bad input: the adversary is built from the algorithm it plays against, so the hard task sequence exists only as a recursion interleaved with the algorithm's choices, and the bound must hold for every deterministic on-line map, including ones that behave erratically. Obtaining the exact constant $2n-1$, rather than some $\Omega(n)$ bound, requires a sharp estimate of the off-line cost of that sequence.

The upper bound needs an algorithm defined in continuous time, whose transition times are determined by accumulated processing costs; the budgets can be zero, so transitions can be instantaneous, and a formal cost must remain well defined before one knows that only finitely many transitions occur. Relating the off-line cost function at those times to the recursively defined $f_k$ (Lemma 6.2) requires reasoning about all continuous-time off-line schedules. Finally, the goal combines both directions through infima over all on-line algorithms, and the discretization of Lemma 3.1 must be composed with the continuous-time algorithm.

Formalization scope

States form a finite type S (Fintype, DecidableEq, Nonempty); the goal is stated for all $n\ge1$, where $n=1$ gives $w(S,d)=1$. Task costs are finite nonnegative reals; the paper also allows $+\infty$ entries, which are excluded (this affects neither bound). A task sequence is T : Fin m → S → ℝ, with T i the paper's $T^{i+1}$, and a schedule is σ : Fin (m+1) → S. An on-line algorithm is a map sending $(s_0,[T^1,\dots,T^i])$ to $\sigma(i)$, so on-line behaviour is built into the type. Competitiveness is written additively, $c_A\le w\,c_0+K$, with $K$ independent of the task sequence and of $s_0$.

The competitive ratio competitiveRatio d is the real infimum of the set of all $w$ for which some on-line algorithm is $w$-competitive. It is not defined as an infimum of per-algorithm real infima: a non-competitive algorithm has $W_A=\emptyset$, whose real infimum is $0$, and that would drag $w(S,d)$ to $0$ for every system. Since the goal's value $2n-1$ is at least $1$ while the empty set's real infimum is $0$, the goal cannot hold vacuously.

Continuous-time algorithms are given as lists of $(\text{state},\text{length})$ pieces per unit interval; processing integrals are exact finite sums. The algorithm $A^*_d$ minimizes over states different from the current one, as its proof requires (the printed rule ranges over all states, and would stall); ties are left arbitrary. Its budgets may be $0$, its entry times are Option ℝ, and its cost is a sum in $[0,\infty]$, so that Theorem 6.1 itself asserts that only finitely many transitions occur. The ratio $\psi(d)$ excludes closed walks that never move, and Theorems 2.2 and 6.1 require $n\ge2$, where $\min_{i\ne j}d(i,j)$ and $\psi(d)$ are defined. Lemma 3.1 is stated comparing $A$ with $A'$ (the printed statement says "as well as $A$").

A complete development needs: the discrete model and off-line optimum (finite minimum over schedules), limsup arguments in EReal, continuous-time schedules with piecewise-constant costs, and the recursion defining $A^*_d$. Proofs of any milestone, including the purely combinatorial Lemmas 6.3 and 6.4, are welcome, as is a formal composition of Lemma 3.1 with Theorem 6.1.

Selected references

• A. Borodin, N. Linial, M. E. Saks, An optimal on-line algorithm for metrical task system, Journal of the ACM 39(4):745–763, 1992. https://doi.org/10.1145/146585.146588
• 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

Motivation

Paging is the problem of managing a two-level memory: a fast cache holds $k$ pages out of an address space of $n$ pages, requests to pages arrive one at a time, and a request to a page outside the cache (a page fault) forces the algorithm to bring that page in and, when the cache is full, to evict another. The cost is the number of faults. An on-line algorithm decides which page to evict without knowing future requests. The comparison of paging policies with the optimal off-line policy is where competitive analysis began.

Sleator and Tarjan showed that LRU and FIFO are within a factor $k$ of the off-line optimum and that no deterministic on-line algorithm does better than $k$ (Sleator–Tarjan 1985). Randomization changes the picture: Fiat, Karp, Luby, McGeoch, Sleator and Young introduced the marking algorithm and proved that its expected cost is within a factor $2H_k$ of the optimum, where $H_k = 1 + \frac12 + \dots + \frac1k \approx \ln k$ (arXiv:cs/0205038).

Timeline.

• 1985: Sleator and Tarjan: LRU and FIFO are $k$-competitive; no deterministic algorithm beats $k$.
• 1988: Karlin, Manasse, Rudolph and Sleator coin "competitive" and analyse flush-when-full (Algorithmica 3).
• 1990: Manasse, McGeoch and Sleator introduce the $k$-server problem and define competitiveness for randomized algorithms (J. Algorithms 11).
• 1991: Fiat et al.: the marking algorithm is $2H_k$-competitive, and $H_{n-1}$-competitive when $k = n-1$; no randomized paging algorithm beats $H_k$.
• 1991: McGeoch and Sleator give an $H_k$-competitive randomized paging algorithm (Algorithmica 6).
• 2000: Achlioptas, Chrobak and Noga determine the exact competitive ratio of the marking algorithm, $2H_k - 1$ (Theoret. Comput. Sci. 234).

Setting

The paper works in the uniform $k$-server problem, which is isomorphic to paging. There is a set $M$ of $n$ vertices, enumerated $e(0), \dots, e(n-1)$, and moving a server between two distinct vertices costs $1$. There are $k$ servers, $1 \le k \le n$. A request is a vertex, and after each request some server must be on it. Cached pages are covered vertices; a fault is a server move.

The marking algorithm starts with its servers on $e(0), \dots, e(k-1)$ and keeps a set of marked vertices, initially the covered ones. On a request to $r$:

1. Marking. $r$ is marked; the moment $k+1$ vertices are marked, all marks except the one on $r$ are erased.
2. Serving. If $r$ is covered, nothing moves. Otherwise a server is chosen uniformly at random among the covered unmarked vertices and moved to $r$.

The marks are updated before the server is chosen. For a finite request sequence $\sigma$, $C_M(\sigma)$ is the algorithm's expected number of server moves. $\mathrm{OPT}(\sigma)$ is the least number of moves with which $k$ servers, starting from the same configuration $C_0$ and knowing $\sigma$ in advance, can serve $\sigma$.

A randomized algorithm is $c$-competitive if there is a constant $a$ such that $C_M(\sigma) \le c \cdot C_B(\sigma) + a$ for every request sequence $\sigma$ and every algorithm $B$.

The marks divide $\sigma$ into phases. A new phase begins at the request that would make $k+1$ vertices marked. A vertex is clean in a phase if it was not requested in the previous phase and not yet in this one, and stale if it was requested in the previous phase but not yet in this one.

Formalization targets

Goal: Theorem 1

$$\exists\, a \in \mathbb R\ \ \forall \sigma:\qquad C_M(\sigma) \;\le\; 2H_k \cdot \mathrm{OPT}(\sigma) + a .$$

The constant $a$ may depend on $n$, $k$ and the enumeration, never on $\sigma$.

Milestones (proof of Theorem 1, pp. 4–5)

1. Without loss of generality the adversary is lazy: no move on a covered request, exactly one move otherwise (reference item, already proved on the platform).
2. At the start of every phase the marked vertices are exactly the covered ones, and the first request of a phase is unmarked.
3. In a phase with $l$ clean requests, a lazy adversary pays $C_A \ge l - d$, where $d$ counts its servers off the marking algorithm's servers at the start of the phase.
4. It also pays $C_A \ge d'$, where $d'$ counts its servers off the final marked set at the end of the phase.
5. Hence $C_A \ge \max(l-d, d') \ge \tfrac12(l - d + d')$.
6. A request to a stale vertex is a fault with probability $c/s$ ($c$ clean vertices requested so far, $s$ stale vertices left).
7. The marking algorithm's expected cost in a phase is at most $l(H_k - H_l + 1) \le lH_k$.

Companions

• Theorem 2: for $k = n-1$, $C_M(\sigma) \le H_{n-1} \cdot \mathrm{OPT}(\sigma) + a$.
• Tightness remark (pp. 5–6): for $k = 2$, $n = 4$ there is no $a$ with $C_M(\sigma) \le H_2 \cdot \mathrm{OPT}(\sigma) + a$ for all $\sigma$.

Significance

The result. Theorem 1 was the first proof that randomization beats the deterministic barrier $k$ for paging, bringing the ratio down to $O(\log k)$. Together with the paper's lower bound $H_k$ for every randomized algorithm, it determines the randomized competitive ratio of paging up to a factor $2$. Its phase and clean/stale accounting is reused throughout the analysis of randomized caching.

Formalizing it. The theorem is proved (1991). As far as is known it has no machine-checked proof. Formalizing it requires a probabilistic model of a randomized on-line algorithm, an off-line optimum, and a phase decomposition with an exchangeability argument, and these are the first such objects in this library. Theorem 2 and the $k = 2$, $n = 4$ example use the same definitions and also check that the formal algorithm is the paper's. The sharp ratio $2H_k - 1$ is a natural follow-up.

Difficulty

The comparison is between a random process and a deterministic adversary, and each side has its own obstacle.

On the algorithm's side, the configuration inside a phase is random, and the fault probability of a stale request depends on the whole history of the phase. The claim that the $c$ uncovered stale vertices form a uniformly random subset of the $s$ stale ones is an exchangeability property of the process, and must be established from the step-by-step uniform choice. The worst-case ordering of the requests within a phase then has to be justified as a bound, not assumed.

On the adversary's side, the per-phase bound $\max(l-d, d')$ does not sum directly. The $d$ and $d'$ terms telescope across phases only because the configuration of the marking algorithm at each phase boundary is deterministic. The first phase, which begins after an initial run of requests to $e(0), \dots, e(k-1)$, and the last, incomplete phase have to be absorbed into the additive constant.

Formalization scope

The vertex set is an abstract metric space $M$ with $e : \mathrm{Fin}\,n \simeq M$ and $\mathrm{dist}(x,y) = 1$ for $x \ne y$. The natural metric $|i - j|$ on $\mathrm{Fin}\,n$ is deliberately not used. The configurations and the off-line optimum $\mathrm{OPT}$ are the published KServer definitions (KServer.Config, KServer.offlineCost), with $\mathrm{OPT}$ taken from the marking algorithm's initial configuration. An off-line algorithm starting elsewhere changes the cost by at most $k$, which is absorbed into $a$.

The marking algorithm is a Markov chain on pairs (covered set, marked set). Each step is a PMF, with the eviction drawn by PMF.uniformOfFinset from the covered unmarked vertices. The expected cost is the sum over requests of the probability that the request is not covered, which is exact because the algorithm moves exactly one server per fault. Harmonic numbers are Mathlib's harmonic, cast to $\mathbb R$. Phases, clean counts and lazy off-line schedules are defined once, in the mission's definition file, and all milestones use them.

A trivializing formalization is ruled out as follows. The additive constant is quantified before $\sigma$, so a per-sequence constant cannot be used. The comparison is with the optimum over all off-line schedules, not a particular one. The random choice is among the covered unmarked vertices, with marks updated first. The hypothesis $1 \le k \le n$ excludes the degenerate case $k = 0$, where $H_0 = 0$.

Proofs of individual milestones are welcome. The laziness reduction for off-line schedules, the exchangeability lemma for the uniform eviction process, and the harmonic-sum identity $\sum_{j=l+1}^{k} l/j = l(H_k - H_l)$ are reusable beyond this mission.

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; arXiv:cs/0205038v1. 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
• A. R. Karlin, M. S. Manasse, L. Rudolph, D. D. Sleator, Competitive Snoopy Caching, Algorithmica 3:79–119, 1988. https://doi.org/10.1007/BF01762111
• 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. https://doi.org/10.1007/BF01759073
• D. Achlioptas, M. Chrobak, J. Noga, Competitive Analysis of Randomized Paging Algorithms, Theoret. Comput. Sci. 234:203–218, 2000. https://doi.org/10.1016/S0304-3975(98)00116-9

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