Online Algorithms

Motivation

Paging is the problem of managing a fast memory that holds $k$ pages out of $n$: when a requested page is not in fast memory (a page fault), some resident page must be evicted, and the cost of an algorithm is its number of faults. Practitioners have many eviction rules. Least-recently-used (LRU) performs well on real workloads but can be $k$ times worse than the optimal off-line schedule; the randomized marking algorithm of the same paper is $2H_k$-competitive and so has better worst-case guarantees. Fiat, Karp, Luby, McGeoch, Sleator and Young asked in 1991 whether one on-line algorithm can combine the advantages of several given ones, and answered the question exactly: the attainable combinations of ratios are characterized by one inequality (arXiv:cs/0205038, §6).

The question of combining on-line algorithms has since become a theme of its own: combining heuristics with worst-case-safe algorithms, and, more recently, combining machine-learned predictions with robust fallbacks, both ask for the same kind of guarantee against several reference algorithms at once.

Setting

A type $(k,n)$ consists of $k$ servers and a finite set $M$ of $n$ vertices with the uniform metric: two distinct vertices are at distance $1$. This is paging: vertices are pages, the vertices covered by servers are the pages in fast memory, and a server move is a page fault.

A deterministic on-line algorithm $A$ of type $(k,n)$ has an initial configuration of its $k$ servers and, after each request $r\in M$, moves servers so that some server covers $r$; its configuration after a request sequence depends only on that sequence. Its cost $C_A(\sigma)$ on a request sequence $\sigma$ is the total distance its servers travel, i.e. the number of server moves.

For algorithms $A$ and $B$ of the same type and a constant $c$, $A$ is $c$-competitive against $B$ if there is a constant $a$ such that for every request sequence $\sigma$

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

A sequence $c^*=(c(1),\dots,c(m))$ of positive reals is realizable if for every type $(k,n)$ and every $m$ deterministic on-line algorithms $B(1),\dots,B(m)$ of that type there is a deterministic on-line algorithm $A$ of the same type that is $c(i)$-competitive against $B(i)$ for every $i$.

Formalization targets

Goal: Theorem 6

For $m\ge1$ and positive reals $c(1),\dots,c(m)$,

$$c^*\ \text{is realizable}\iff \sum_{1\le i\le m}\frac1{c(i)}\le 1 .$$

Milestones

In the order of the paper's proof:

1. Punishments are paid for. If $A$ punishes $B$ at a time step (an $A$-interval on a vertex $v$ ends at that step and contains the end of a $B$-interval on $v$ that began no later), then $B$ has moved a server; the number of such steps is at most $C_B(\sigma)$.
2. A fault leaves room to punish. If $|S_A|=k$, $|S_B|\le k$, $x\in S_B$ and $x\notin S_A$, then some $u\in S_A$ is not in $S_B$.
3. The greedy quota claim. If $\sum_i 1/c(i)\le 1$ and each unit of cost punishes the $B(i)$ minimizing $c(i)(\mathrm{PUN}(i)+1)$ (other algorithms may be punished incidentally), then after cost $r$ every $B(i)$ has been punished at least $\lfloor r/c(i)\rfloor$ times.
4. Shuttle algorithms. With $2m-1$ servers on $2m$ vertices there are $m$ algorithms, each keeping all vertices outside its own pair covered, no two of which move at the same step; in particular their total cost on any $\sigma$ is at most $|\sigma|$.
5. A forcing adversary. With $2m-1$ servers on $2m$ vertices every algorithm can be forced to move at each of $N$ steps, so $C_A(\tau(N))\ge N$.

Significance

The result. Theorem 6 is an exact characterization, not a bound: the region of simultaneously attainable ratios against arbitrary deterministic paging algorithms is $\{c:\sum 1/c(i)\le 1\}$. For example, any two paging algorithms can be combined into one that is $2$-competitive against each, and no better symmetric pair is possible in general. Combined with Theorem 7 of the same paper (not part of this mission), the same region is attainable against randomized algorithms, which is how LRU's practical behaviour and the marking algorithm's $2H_k$ worst-case guarantee can be obtained within constant factors by one algorithm.

Formalizing it. The theorem has been proved since 1991; no machine-checked proof is known. A formal proof produces a reusable notion of competitiveness of one on-line algorithm against another, built on the published KServer_model definitions, and a formal account of the scheduling fact at the core of the sufficiency proof.

Difficulty

Sufficiency looks like an averaging argument, but the combined algorithm cannot simulate the $B(i)$ and follow one of them: switching between their configurations costs up to $k$ per switch, which no additive constant absorbs. The accounting has to charge each of $A$'s faults to a specific move of a specific $B(i)$, and the charge must be injective; the paper's claim that $C_B(\sigma)$ is at least the number of punishments is where this happens, and it depends on how server intervals are matched. The allocation of faults to algorithms is then a deadline-scheduling problem whose feasibility is exactly $\sum 1/c(i)\le 1$, and the floor functions make the counting delicate at the boundary. The paper's own definition of punishment only counts intervals that start with a move, so the first $k$ faults of $A$ (servers on their initial vertices) need separate treatment; they are absorbed by the additive constant.

Necessity needs the right family of hard instances: the $m$ algorithms must never move at the same step, which pins the type to $(2m-1,2m)$.

Formalization scope

The Lean development works in the namespace CompetitivePaging.Combining and imports the published KServer_model definitions: KServer.OnlineAlgorithm k M (a configuration map from request prefixes to Fin k → M with a serving condition) and OnlineAlgorithm.cost. Committed conventions:

• a type $(k,n)$ is any k : ℕ and any finite M : Type with a metric in which distinct points are at distance $1$; realizability quantifies over all of them, never over one fixed type;
• servers are labelled; each algorithm has its own initial configuration, and the additive constant $a$ is chosen before the request sequence;
• $c(i)>0$ and $m\ge1$ are hypotheses of the goal, as in the paper; without positivity, $1/0=0$ in Lean would make a zero ratio free;
• time $t$ is the step processing the $t$-th request; the paper's $\mathrm{PUN}$ counts time steps.

Trivializing encodings are ruled out: realizability is not stated for a single fixed type, the metric is not the metric of Fin n, and the competitive constant is not allowed to depend on the request sequence.

A complete proof needs the construction of the punishing algorithm as a KServer.OnlineAlgorithm (a lazy, injective algorithm whose moves depend on the prefix and on the $B(i)$'s configurations), the injective charging argument, the scheduling lemma, and the explicit shuttle algorithms. The scheduling lemma and the charging lemma are independent of paging and reusable. Proofs of any milestone are welcome, as are alternative statements of the sufficiency construction.

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. doi:10.1016/0196-6774(91)90041-V; preprint arXiv:cs/0205038.
• D. D. Sleator, R. E. Tarjan, Amortized efficiency of list update and paging rules, Comm. ACM 28(2):202–208, 1985. doi:10.1145/2786.2793
• M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive algorithms for server problems, J. Algorithms 11(2):208–230, 1990. doi:10.1016/0196-6774(90)90003-W

Motivation

In a shared-memory multiprocessor, each processor keeps copies of memory blocks in its own cache, and all caches listen ("snoop") on a common bus. Every bus cycle spent keeping these copies consistent is a cycle not available for useful work, so the protocol that decides when a block is shared by several caches and when it is private to one cache directly controls bus traffic. The decision has to be made on-line, without knowing which processor will touch the block next.

Karlin, Manasse, Rudolph and Sleator (Algorithmica 1988) introduced competitive analysis for this problem and gave a deterministic algorithm with competitive ratio $2$, which is optimal among deterministic algorithms. Karlin, Manasse, McGeoch and Owicki (Algorithmica 1994) showed that randomization helps: against an oblivious adversary the optimal ratio for block snoopy caching is $e_p/(e_p-1)$, where $p$ is the cost of transferring a block. The same paper develops a general method for "nonuniform" problems, in which some state transitions are much more expensive than others, and the snoopy-caching result is its first application.

Setting

Fix $n$ processors and one memory block $B$ holding $p-1$ variables; transferring $B$ over the bus costs $p$ bus cycles. The block is in one of $n+1$ states: shared between all caches, or private to the cache of processor $i$.

A request is a read $\mathrm{R}_i$ or a write $\mathrm{W}_i$ by processor $i$. Moving from a private state to any other state costs $p$; moving from the shared state is free. A read $\mathrm{R}_i$ costs $0$ if $B$ is shared or private to $i$ and $+\infty$ otherwise. A write $\mathrm{W}_i$ costs $0$ if $B$ is private to $i$, $1$ if $B$ is shared (one bus cycle broadcasts the new value), and $+\infty$ otherwise.

Before request $j$ the system is in state $s_{j-1}$. A read is a look-ahead-one request: the algorithm may change state at the moment of the request, after seeing it. A write is a look-ahead-zero request: it is served in whatever state the system is in. After either kind, the algorithm may move again. The cost of a request is the cost of the move to the serving state, plus the task cost there, plus the cost of the move afterwards. Every write is preceded by a read to the same block, so in an admissible sequence each write $\mathrm{W}_i$ directly follows $\mathrm{R}_i$ or $\mathrm{W}_i$.

The off-line optimum $C_{opt}(s_0,\sigma)$ is the least total cost of serving $\sigma$ from the initial state $s_0$ with full knowledge of $\sigma$. A randomized on-line algorithm $A$ is a probability distribution over deterministic on-line algorithms; its expected cost on $\sigma$ is $\mathbf{E}C_A(\sigma)$. $A$ is $c$-competitive against an oblivious adversary from $s_0$ if there is a constant $a$ with

$$\mathbf{E}C_A(\sigma)\le c\cdot C_{opt}(s_0,\sigma)+a$$

for every admissible $\sigma$. Put

$$e_p=\left(1+\frac1p\right)^p .$$

Formalization targets

Goal: Theorem 4

For $n\ge 2$, $p\ge 1$ and every initial state $s_0$:

$$\Big(\forall A\ \forall c:\ A \text{ is } c\text{-competitive from } s_0 \Rightarrow c\ge \tfrac{e_p}{e_p-1}\Big)\ \wedge\ \exists A:\ A \text{ is } \tfrac{e_p}{e_p-1}\text{-competitive from } s_0 .$$

The two conjuncts are milestones of their own: the lower bound (Theorem 4, first claim) and attainment (Theorem 4, second claim).

The phase linear program (§3.2, pp. 552–554)

For $p\ge1$, real $\pi_1,\dots,\pi_{p+1}$ with $\pi_{p+1}=1$, and real $\alpha$ with

$$\pi_{k+1}p+\sum_{i=1}^{k}(1-\pi_i)\le\alpha k\qquad(k=0,\dots,p),$$

one has $\alpha\ge e_p/(e_p-1)$. Conversely, at $\alpha=e_p/(e_p-1)$ the choice $\pi_k=(\alpha-1)\big(((p+1)/p)^{k-1}-1\big)$ satisfies $\pi_{p+1}=1$, $0\le\pi_1\le\dots\le\pi_{p+1}$, and makes every constraint an equality.

Significance

The theorem settles the randomized competitive ratio of block snoopy caching exactly: $2$ at $p=1$, $9/5$ at $p=2$, decreasing to $e/(e-1)\approx1.582$ as $p\to\infty$, against the deterministic optimum $2$. The same ratio $e/(e-1)$ is the randomized optimum for the continuous ski-rental and spin-block problems treated later in the paper, and the snoopy-caching case is its discrete counterpart with ratio $e_p/(e_p-1)$. The phase-LP method used here recurs in the paper's two-server results.

The result is proved in the paper; to our knowledge it has no machine-checked proof. This mission produces a formal model of the snoopy-caching task system with look-ahead-zero requests, of randomized algorithms against an oblivious adversary with infinite task costs allowed, and of the off-line optimum, together with the exact optimal ratio. The platform's fractional ski-rental result (PrimalDualOnline.SkiRental.fractional_competitive) proves an $e_B/(e_B-1)$ bound for a different model: one deterministic fractional algorithm, with no lower bound over randomized algorithms. It is related work, not a special case.

Difficulty

The linear program is elementary. The gap is between the LP and the algorithms. The paper's lower bound reduces arbitrary randomized algorithms to phase-based ones, whose state distribution at the end of each phase agrees with the optimal algorithm's known state, and whose behaviour inside a phase depends only on the number of writes so far. This reduction (Theorems 1 and 3 of the paper, pp. 545–549) is where the argument is not routine. An algorithm may keep the block private to a processor that is not the active one, may randomize over histories rather than over phase lengths, and the off-line optimum is not a sum of per-phase costs at the ends of the sequence. The obvious approach, bounding a single adversarial phase, does not suffice, because an algorithm may pay more in one phase and recover it in the next; the additive constant $a$ and the infinite horizon have to be handled. For attainment, the mixture of threshold algorithms must be written as a genuine distribution over on-line algorithms, with the initial phase from a private state absorbed into the additive constant.

Formalization scope

Everything lives in the namespace NonuniformCompetitive.Snoopy. States are Option (Fin n) (none = shared). Costs are in ℝ≥0∞; $+\infty$ is a genuine outcome, so an algorithm that ever pays $+\infty$ with positive probability on an admissible sequence is not competitive. A deterministic on-line algorithm is a pair of functions of the request prefix (the state at the moment of the last request, and the state after it), with the look-ahead-zero rule as a field. Moves "immediately before" a request are made without knowledge of it and are recorded as moves after the previous request. A randomized algorithm is a probability space with a measurable cost on every sequence, and its expected cost is a lower Lebesgue integral. The off-line optimum is an infimum in ℝ≥0∞ over schedules starting in $s_0$; it is finite on admissible sequences.

Conventions added to the printed statement, all from the paper's setting: (i) $n\ge2$, since with one processor the block can stay private for free; (ii) one block, since the proof of Theorem 4 splits a multi-block system into independent blocks (p. 551); (iii) admissibility in the form "each write of $i$ directly follows a read or write of $i$", the reading of "every write is preceded by a read to the same block" that the proof uses; without it every algorithm is defeated by a write from a processor whose block copy was invalidated; (iv) $p\in\mathbb{N}$, $p\ge1$; (v) both claims from every initial state, with an additive constant depending on $n$, $p$, $s_0$.

The lower bound is over all randomized algorithms, not over phase-based or deterministic ones; a statement restricted to phase-based algorithms, or the LP alone in place of the goal, would not be Theorem 4. The LP variables are free, as in the paper.

Welcome contributions: a formal version of the phase reduction (Theorems 1 and 3 of the paper) for this task system, which is reusable for the paper's other nonuniform problems; the threshold algorithms and their mixture; and a proof that the off-line optimum decomposes by write runs up to a bounded error.

Selected references

• A. R. Karlin, M. S. Manasse, L. A. McGeoch, S. Owicki, Competitive Randomized Algorithms for Nonuniform Problems, Algorithmica 11 (1994), 542–571. https://doi.org/10.1007/BF01189993
• A. R. Karlin, M. S. Manasse, L. Rudolph, D. D. Sleator, Competitive Snoopy Caching, Algorithmica 3 (1988), 79–119. https://doi.org/10.1007/BF01762111
• A. Borodin, R. El-Yaniv, Online Computation and Competitive Analysis, Cambridge University Press, 1998.

Motivation

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

Timeline:

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

Setting

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

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

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 10 (p. 559)

For every $C>0$:

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

Milestones

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

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

The k-server problem of Manasse, McGeoch and Sleator (J. Algorithms 11 (1990)) asks how $k$ mobile servers in a metric space should respond, on-line, to a sequence of requests at points of the space, each of which must be covered by a server. It is the central model of on-line computation: paging is the special case of a uniform metric, and many caching and scheduling problems reduce to it. For two servers the deterministic picture is complete: the optimal competitive ratio is $2$ on every metric space with at least three points.

Randomization changes the picture, and the smallest nontrivial case already shows how. On the equilateral triangle the optimal randomized ratio against an oblivious adversary is $3/2$. Karlin, Manasse, McGeoch and Owicki (Algorithmica 11 (1994) 542–571) computed the exact optimal randomized ratio for several nonuniform triangles, where the distances differ, and showed that it depends on the geometry. Their Theorem 12 settles the whole family of isosceles triangles with edge lengths $1$, $d$, $d$. These exact values are among the few known optimal randomized ratios for server problems.

Timeline:

• 1990: Manasse, McGeoch and Sleator introduce the $k$-server problem and prove the deterministic two-server ratio is $2$.
• 1990–1994: Karlin, Manasse, McGeoch and Owicki submit this paper (received August 1990, revised September 1991) and publish it in Algorithmica in 1994, with the isosceles-triangle ratios of Theorem 12 and the 3-4-5 triangle ratio $1652/1069$ of Theorem 13.
• Later: Karloff, Rabani and Ravid extend the technique to $\Omega(\log\log k)$ and $\Omega(\log k)$ randomized lower bounds (cited on p. 564); Bubeck, Coester and Rabani (STOC 2023) refute the randomized $k$-server conjecture.

Setting

Fix an integer $d\ge1$. The isosceles triangle $M$ has three points $a$, $b$, $c$ with

$$\operatorname{dist}(a,b)=1,\qquad \operatorname{dist}(a,c)=\operatorname{dist}(b,c)=d.$$

A configuration $C:\{0,1\}\to M$ places two labelled servers on points of $M$. A deterministic on-line algorithm assigns to every finite request sequence $\sigma=(r_1,\dots,r_n)$ a configuration, computed from $\sigma$ alone and covering the last request; its value on the empty sequence is its initial configuration. Its cost $C_A(\sigma)$ is the total distance its servers move while serving $\sigma$ request by request. The off-line optimum $C_{opt}(\sigma)$ from an initial configuration $C_0$ is the least total movement of any schedule that starts at $C_0$ and covers each request in turn, knowing $\sigma$ in advance.

A randomized algorithm is a probability distribution on deterministic on-line algorithms; its expected cost is $\mathbf{E}C_A(\sigma)$. It is $\rho$-competitive against an oblivious adversary from $C_0$ if every algorithm in its support starts at $C_0$ and there is a constant $a$ such that

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

The request sequence is fixed in advance and does not react to the algorithm's coin flips.

Write $e_p=(1+1/p)^p$ and

$$\alpha_d=\frac{e_{2d-1}+1/4d}{(e_{2d-1}-1)+1/2d},\qquad e_{2d-1}=\left(\frac{2d}{2d-1}\right)^{2d-1}.$$

In Lean this is NonuniformCompetitive.Isosceles.isoscelesRatio d.

Formalization targets

Goal: Theorem 12

For every $d\ge1$ and every initial configuration $C_0$:

$$\forall A,\ \forall\rho,\quad A\text{ is }\rho\text{-competitive from }C_0\ \Longrightarrow\ \rho\ge\alpha_d,$$ $$\exists A:\ A\text{ is }\alpha_d\text{-competitive from }C_0.$$

The two claims are also milestones of their own (no_better_ratio, ratio_attained).

The phase LP (§5, pp. 565–566)

For free real $\pi_1,\dots,\pi_{2d-1}$ and real $\alpha$ with

$$(\pi_k)2d+\sum_{i=1}^k(1-\pi_i)\le\alpha k\ \ (1\le k<2d),\qquad 2d+\sum_{i=1}^{2d-1}(1-\pi_i)+\tfrac12\le\alpha\cdot2d,$$

one has $\alpha\ge\alpha_d$ (lp_lower_bound); and $\pi_k=(\alpha_d-1)\big((2d/(2d-1))^k-1\big)$, $\pi_{2d}=1$ is nondecreasing from $\pi_1\ge0$ to $1$ and makes every constraint an equality (lp_attained).

The limit remark (§5, p. 566)

$$\alpha_1<\alpha_2<\alpha_3<\cdots,\qquad \lim_{d\to\infty}\alpha_d=\frac{e}{e-1}$$

(ratio_increases_to_e_ratio).

Significance

The theorem gives an exact optimal randomized ratio for an infinite family of metric spaces. It shows that the optimal randomized two-server ratio is not a constant: it runs from $3/2$ on the equilateral triangle to $e/(e-1)\approx1.582$ as the triangle becomes long and thin, where the problem resembles ski rental. With the deterministic ratio $2$, it quantifies exactly how much randomization gains on these spaces.

The results are proved in the paper; none is formalized on Prove2Me, and no machine-checked proof of them is known. A formal proof would require the paper's phase framework (Theorems 1–3 and the appendix's Theorem 15) for server problems, which this mission does not state separately, and a concrete randomized algorithm as a measurable mixed strategy. Both would be reusable for Theorem 13 (the 3-4-5 triangle) and for other exact ratios on small metric spaces.

Difficulty

The phase LP milestones are finite real arithmetic. The difficulty is the passage between them and the goal. The lower bound must hold for every randomized algorithm, not only phase-based lazy ones: an arbitrary algorithm may condition on the whole history, move non-lazily, and randomize in ways that do not reduce to the probabilities $\pi_k$. The paper handles this with Theorem 3, which says that the LP bound of phase-based algorithms bounds the competitive factor of all algorithms; its proof uses an averaging argument over histories that must be made rigorous. The upper bound needs a mixed strategy over infinitely many phases, with measurable costs, an explicit additive constant covering the first partial phase from an arbitrary initial configuration, and an accounting of $C_{opt}$ across phase boundaries.

Formalization scope

The model is the platform's published KServer_model and KServer_randomized (reference items): labelled servers Fin 2 → M; a deterministic on-line algorithm as a map from request prefixes to configurations; a randomized algorithm as a probability measure over deterministic algorithms, with the cost of each fixed sequence measurable in the random outcome; expected cost as a lower Lebesgue integral in $[0,\infty]$; the off-line optimum as a real infimum over schedules from $C_0$ (nonempty and bounded below by $0$); and IsCompetitiveFrom A C₀ c with a real additive constant.

Committed conventions:

• The triangle is any metric space whose points are exactly $a,b,c$ at distances $1,d,d$, with $d$ a natural number and $d\ge1$. Every such space is isometric to the paper's triangle; at $d=0$ it would not be a triangle.
• Both claims are stated for every initial configuration, including both servers on one point. The paper treats the initial state $\{a,b\}$ separately and absorbs the first partial phase into the additive constant.
• The lower bound quantifies over all randomized algorithms (deterministic ones are point masses), never over phase-based ones only.
• In the LP milestones the $\pi_k$ are free reals, as printed; no box $0\le\pi_k\le1$ is imposed.
• "Grows" in the limit remark is read as strictly increasing.
• The paper prints the recurrence on p. 565 as $\pi_k=\frac{\alpha-1+(\pi_{k-1})2d-1}{2d}$; the equations $(*)$ give $\pi_k=\frac{\alpha-1+2d\,\pi_{k-1}}{2d-1}$. The recurrence is not used; the closed form printed on p. 566 is correct and is the one stated.

Without the measurability field of a randomized algorithm the lower integral would under-report expected cost and the attainment claim would become easier than the paper's; the published definition includes it. The lower bound is not vacuous: the triangle hypotheses are satisfiable for every $d\ge1$.

Welcome contributions: a formal version of the phase framework (Theorems 1–3, 15) for finite metric spaces, reusable across missions III and IV; a measurable construction of phase-based randomized algorithms; and proofs of the LP milestones.

Selected references

• A. R. Karlin, M. S. Manasse, L. A. McGeoch, S. Owicki, Competitive Randomized Algorithms for Nonuniform Problems, Algorithmica 11 (1994) 542–571. https://doi.org/10.1007/BF01189993
• M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive Algorithms for Server Problems, J. Algorithms 11 (1990) 208–230. https://doi.org/10.1016/0196-6774(90)90003-W
• H. Karloff, Y. Rabani, Y. Ravid, Lower Bounds for Randomized k-Server and Motion-Planning Algorithms, SIAM J. Comput. 23 (1994) 293–312. https://doi.org/10.1137/S0097539792224838
• S. Bubeck, C. Coester, Y. Rabani, The Randomized k-Server Conjecture Is False!, STOC 2023. https://arxiv.org/abs/2211.05753

Motivation

The $k$-server problem is a basic model of on-line decision making. $k$ mobile servers move in a metric space, requests for points arrive one at a time, and each request has to be covered by a server before the next one arrives. The cost is the total distance the servers move. The problem includes paging, caching and disk-head scheduling as special cases (Manasse, McGeoch, Sleator 1990). An on-line algorithm is judged by its competitive factor: how much its cost can exceed that of an off-line algorithm that knows the whole request sequence in advance.

For randomized algorithms against an oblivious adversary (one that fixes the whole request sequence before the algorithm flips any coins), the best-understood case is paging, which is the $k$-server problem on a uniform metric space. There the optimal factor is the harmonic number $H_k=\sum_{i=1}^k 1/i$. Fiat et al. proved the lower bound (1991) and McGeoch and Sleator the matching upper bound (1991). Karlin, Manasse, McGeoch and Owicki (Algorithmica 11, 1994, §5) asked whether $H_k$-competitive algorithms also exist when the metric space is not uniform. They answered no, already for two servers on three points: on certain triangles the optimal randomized factor is strictly larger than $H_2 = 3/2$. This mission formalizes their Theorem 13, which gives the exact optimal factor on the triangle with edge lengths 3, 4 and 5.

Timeline:

• 1990: Manasse, McGeoch and Sleator introduce the $k$-server problem; $k$ is the deterministic optimum for $k=2$.
• 1991: Fiat, Karp, Luby, McGeoch, Sleator and Young prove the $H_k$ lower bound for randomized paging. McGeoch and Sleator give an $H_k$-competitive paging algorithm.
• 1994: Karlin, Manasse, McGeoch and Owicki determine the optimal randomized two-server factors on the isosceles triangles $1$-$d$-$d$ (Theorem 12) and on the 3-4-5 triangle (Theorem 13, the ratio $1652/1069$). Both exceed $3/2$.

Setting

Let $M$ be a metric space with exactly three points $a, b, c$, where $d(a,b)=3$, $d(a,c)=5$ and $d(b,c)=4$. A configuration $C$ gives the positions of two labelled servers in $M$. A request sequence $\sigma$ is a finite list of points of $M$.

A deterministic on-line algorithm assigns to each prefix of a request sequence a configuration, in which the last request is covered. Its configuration after a prefix therefore cannot depend on later requests. Its initial configuration is the one it assigns to the empty prefix, and its cost $C_A(\sigma)$ on $\sigma$ is the total distance its servers move while serving $\sigma$ request by request.

The optimal off-line cost $C_{opt}(\sigma)$ from an initial configuration $C_0$ is the infimum, over all schedules that start at $C_0$ and cover each request of $\sigma$ in turn, of the total distance moved.

A randomized on-line algorithm $A$ is a probability distribution over deterministic on-line algorithms, all starting at $C_0$. The cost on each fixed $\sigma$ is required to be measurable in the random choice, and $\mathbf{E}C_A(\sigma)$ is the expected cost. $A$ is $\rho$-competitive against an oblivious adversary if there is a constant $a$ such that for every request sequence $\sigma$,

$$\mathbf{E}C_A(\sigma) \le \rho\cdot C_{opt}(\sigma) + a .$$

These are the definitions of p. 543 of the paper. They are the platform's published KServer_model and KServer_randomized, which this mission reuses unchanged: KServer.RandomizedAlgorithm 2 M and A.IsCompetitiveFrom C₀ ρ.

Formalization targets

Goal: Theorem 13

For every initial configuration $C_0$ of the two servers,

$$\Big(\forall A,\ \forall \rho,\ A \text{ is } \rho\text{-competitive from } C_0 \Rightarrow \rho \ge \tfrac{1652}{1069}\Big)\ \wedge\ \Big(\exists A,\ A \text{ is } \tfrac{1652}{1069}\text{-competitive from } C_0\Big).$$

The first claim is quantified over all randomized algorithms, so it also covers deterministic ones (point masses). The second claim asks for one algorithm. Together they say that $1652/1069 \approx 1.545$ is the exact optimal randomized factor on this triangle.

Milestones

1. The phase LP lower bound (p. 568). Twelve linear constraints in nine probabilities $\pi_1,\dots,\pi_9$, three potentials $\Phi_{ab},\Phi_{ac},\Phi_{bc}$ and a ratio $\alpha$, one constraint for each possible phase of the request sequence, of the form

$$\text{A's cost} \le \alpha\cdot(\text{opt's cost}) + \Phi_{\text{initial}} - \Phi_{\text{final}}.$$

Every real solution has $\alpha \ge 1652/1069$. 2. The LP attainment (p. 568). The paper's printed probabilities lie in $[0,1]$, and with suitable potentials they satisfy all twelve constraints at $\alpha = 1652/1069$. 3. Theorem 13, first claim: the lower bound for every randomized algorithm. 4. Theorem 13, second claim: a $1652/1069$-competitive randomized algorithm exists.

Significance

The result. Theorem 13 shows that the $H_k$ behaviour of randomized paging does not carry over to general metric spaces. Two servers on a three-point space already force a factor above $3/2$. The value is exact, which makes this triangle a test case for any general theory of randomized $k$-server algorithms on small metric spaces. With Theorem 12 (the isosceles triangles, a companion mission of this series), it is one of the few non-uniform metric spaces with a known optimal randomized factor.

Formalizing it. The result has been proved since 1994. To our knowledge there is no machine-checked proof. The paper derives both bounds from two framework theorems for phase-based algorithms: Theorem 3 (an LP lower bound for phase-based algorithms bounds every algorithm) and Theorem 2 (a lazy phase-based algorithm with LP bound $\alpha$ is $\alpha$-competitive). The phase tables themselves (which phases can occur and what they cost) are stated without detailed proof. A formal proof has to supply both framework arguments for this space and verify the phase tables, as well as the finite linear algebra of milestones 1 and 2. The milestones isolate the exact-arithmetic core so that it can be closed independently of the probabilistic part.

Difficulty

The two LP milestones are finite exact-arithmetic facts. The hard part is linking them to Theorem 13.

For the lower bound, an algorithm need not be phase-based at all. Its probabilities may depend on the whole history, not only on the current phase, and it may leave the configuration of the off-line optimum at the end of a phase. The obvious attempt is to fix one hard request sequence and compare costs, but that cannot work: randomization defeats any single sequence. The reduction from arbitrary algorithms to phase-based ones (the paper's Theorem 3) is the substantive step.

For the upper bound, the printed probabilities describe the algorithm's marginal position after each prefix of a phase. They have to be realized as a single probability distribution over deterministic on-line algorithms that is lazy (it moves only to serve a request) and whose expected cost per phase equals the table's entry. On top of this, the LP accounting has to be turned into a bound on arbitrary request sequences, including partial phases and a start away from the optimum's configuration.

Formalization scope

• Model. The platform definitions KServer_model and KServer_randomized are used unchanged. Servers are labelled (Config 2 M = Fin 2 → M). A deterministic algorithm is a function of the request prefix, which makes it on-line by construction. A randomized algorithm is a mixed strategy with a probability measure and a measurability field, and its expected cost is the lower Lebesgue integral of the nonnegative cost. The off-line optimum is a real infimum over schedules from $C_0$; the set is nonempty and bounded below by $0$. Competitiveness allows any real additive constant.
• The triangle is given by hypotheses on an arbitrary metric space: every point equals $a$, $b$ or $c$, and $d(a,b)=3$, $d(a,c)=5$, $d(b,c)=4$. These hypotheses are satisfiable ($3+4\ge5$) and force three distinct points.
• Initial configuration. Both claims are stated for every initial configuration $C_0$, including both servers on one point. The paper does not fix the start; the additive constant absorbs it.
• LP milestones. The thirteen LP variables are free reals, with no box $0\le\pi_i\le 1$, exactly as the paper permits. This makes milestone 1 stronger than the boxed version; the minimum is the same either way. The twelve constraints are written out one per hypothesis, in the table's order, with the potential difference $\Phi_{\text{initial}} - \Phi_{\text{final}}$ on the right. In milestone 2 the potentials are existentially quantified, since the paper names none.
• Not stated. The paper's Theorems 2 and 3 (the phase framework) and the phase tables are not separate milestones. Milestone 1 feeds the first claim through Theorem 3, and milestone 2 feeds the second claim through Theorem 2. Contributions formalizing phase-based algorithms, laziness and the LP-bound reduction for finite metric spaces would be reusable for Theorem 12 and Theorem 14 of the same paper.
• Ruled out. The lower bound is not restricted to deterministic or to phase-based algorithms, and it is not stated as "one sequence defeats every algorithm". The constant is exactly $1652/1069$, not an approximation, and the attainment claim is not weakened to "for some initial configuration".

Selected references

• A. R. Karlin, M. S. Manasse, L. A. McGeoch, S. Owicki, Competitive Randomized Algorithms for Nonuniform Problems, Algorithmica 11 (1994) 542–571. https://doi.org/10.1007/BF01189993
• M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive Algorithms for Server Problems, Journal of Algorithms 11 (1990) 208–230. https://doi.org/10.1016/0196-6774(90)90003-W
• A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive Paging Algorithms, Journal of Algorithms 12 (1991) 685–699. https://doi.org/10.1016/0196-6774(91)90041-V
• L. A. McGeoch, D. D. Sleator, A Strongly Competitive Randomized Paging Algorithm, Algorithmica 6 (1991) 816–825. https://doi.org/10.1007/BF01759073

Motivation

Search engines sell advertisement slots next to their results through ad-auctions. Advertisers bid on keywords, and each advertiser also sets a daily budget: the most it is willing to pay in a day. Queries arrive one at a time and each must be assigned to an advertiser at once, with no knowledge of the queries still to come. The seller's revenue from an advertiser is capped by its budget, so an allocation rule that ignores budgets can exhaust a high bidder early and forgo revenue that a more even allocation would have collected. The question is how much of the offline optimum an online rule can guarantee against every arrival sequence.

Mehta, Saberi, Vazirani and Vazirani (FOCS 2005 / J. ACM 2007) gave a deterministic algorithm whose competitive ratio tends to $1 - 1/e$ when bids are small compared with budgets, and showed that no deterministic algorithm does better. Their algorithm builds on online bipartite matching (Karp, Vazirani and Vazirani, STOC 1990) and online $b$-matching (Kalyanasundaram and Pruhs, 2000). Buchbinder, Jain and Naor (ESA 2007) rederived the $1 - 1/e$ bound with an online primal-dual algorithm, which gives the ratio in closed form for every value of the bid-to-budget ratio and extends to multiple slots, stochastic information, bounded degree and budget flexibility. This mission formalizes the basic algorithm of that paper and its Theorem 1.

Setting

There is a finite nonempty set $I$ of buyers. Buyer $i$ has a known budget $B(i) > 0$. Products $j = 1, \dots, m$ arrive one by one; when product $j$ arrives, every buyer's bid $b(i,j) \ge 0$ on it is revealed. The bid-to-budget ratio is

$$R_{\max} = \max_{i \in I,\, j} \frac{b(i,j)}{B(i)} .$$

A fractional allocation $y(i,j) \ge 0$ assigns fractions of products to buyers; the revenue from buyer $i$ is the minimum of $\sum_j b(i,j)\,y(i,j)$ and $B(i)$.

The offline fractional problem is the packing LP, which the paper calls the dual:

$$\max \sum_{j}\sum_{i} b(i,j)\,y(i,j) \quad\text{s.t.}\quad \sum_i y(i,j) \le 1 \ \ \forall j,\qquad \sum_j b(i,j)\,y(i,j) \le B(i)\ \ \forall i,\qquad y \ge 0 .$$

Its LP dual, the paper's primal, is the covering LP:

$$\min \sum_i B(i)\,x(i) + \sum_j z(j) \quad\text{s.t.}\quad b(i,j)\,x(i) + z(j) \ge b(i,j)\ \ \forall i,j,\qquad x, z \ge 0 .$$

The Allocation Algorithm has a parameter $c > 1$ and starts from $x \equiv 0$. When product $j$ arrives it takes a buyer $i$ maximizing $b(i,j)(1 - x(i))$. If $x(i) \ge 1$, the product is not sold. Otherwise it charges $i$ the minimum of $b(i,j)$ and $i$'s remaining budget, sets $y(i,j) \leftarrow 1$ and $z(j) \leftarrow b(i,j)(1 - x(i))$, and updates

$$x(i) \leftarrow x(i)\Big(1 + \frac{b(i,j)}{B(i)}\Big) + \frac{b(i,j)}{(c-1)\,B(i)} .$$

Its revenue is the total amount charged.

Formalization targets

Goal: Theorem 1

For every instance and every bound $R > 0$ with $b(i,j) \le R\,B(i)$ for all $i, j$, the Allocation Algorithm run with $c = (1+R)^{1/R}$, under any tie-breaking of the maximum, satisfies for every feasible $y'$ of the packing LP

$$\mathrm{Revenue} \;\ge\; \Big(1 - \frac1c\Big)(1 - R)\sum_{j}\sum_{i} b(i,j)\,y'(i,j).$$

With $R = R_{\max}$ this is the paper's statement that the algorithm is $(1 - 1/c)(1 - R_{\max})$-competitive; the fractional optimum bounds every integral offline allocation.

Milestones

The proof of Theorem 1 rests on three claims and three auxiliary facts, each a milestone:

1. the inequality $\ln(1+x)/x \ge \ln(1+y)/y$ for $0 < x \le y \le 1$;
2. Claim (1): the final $(x, z)$ is feasible for the covering LP;
3. Claim (2): the covering cost of the run equals $(1 + 1/(c-1))$ times the packing value of the run's own $y$;
4. Inequality (1): $x(i) \ge \frac{1}{c-1}\big(c^{\sum_j b(i,j) y(i,j)/B(i)} - 1\big)$ at every stage of the run;
5. Claim (3): $\sum_j b(i,j)\,y(i,j) \le B(i) + \max_j b(i,j)$, and the amount charged to $i$ is at least $(1 - R)\sum_j b(i,j)\,y(i,j)$;
6. weak duality for the LP pair above;

and, separately, the second sentence of Theorem 1,

$$\lim_{R\to 0^+}\Big(1 - \frac{1}{(1+R)^{1/R}}\Big)(1-R) = 1 - \frac1e .$$

Significance

Theorem 1 gives an explicit ratio for every value of $R_{\max}$, not only in the limit. It tends to the optimal deterministic ratio $1 - 1/e$ as bids become small, and it quantifies how the guarantee degrades as single bids become a larger share of a budget. The primal-dual analysis is the template for the paper's later sections and for a line of work on online packing and covering problems, surveyed in Buchbinder and Naor's monograph The Design of Competitive Online Algorithms via a Primal-Dual Approach (Foundations and Trends in TCS, 2009).

The result is proved in the paper, and the proof is short. What this mission adds is a machine-checked proof about an algorithm that is defined, not described: the run is computed by recursion from the instance, and the guarantee is proved for that run and every tie-breaking. A related private mission on the platform, The Design of Competitive Online Algorithms via a Primal-Dual Approach VI: Maximizing Ad-Auctions Revenue, states the monograph's Theorem 10.1, which is this theorem, in a form that takes the analysis's intermediate inequalities as hypotheses over arbitrary lists of won bids; the present mission states it for the algorithm itself. No machine-checked proof of Theorem 1 is known to this mission.

Difficulty

Each step of the proof is elementary; the difficulty is the bookkeeping of an online process. Claims (1) and (2) are statements about a single iteration that must be lifted to the whole run: Claim (1) uses that $x$ only increases, and Claim (2) that each product is processed once. Inequality (1) is an induction over the iterations that allocate to one buyer, interleaved with iterations that allocate to others and is the only place where the value of $c$ matters. Claim (3) needs a further invariant: the amount charged equals the minimum of the allocated bids and the budget.

A tempting shortcut is to take Inequality (1) and the "at most one undercharge" fact as hypotheses about some list of bids. That does not describe the algorithm and is not the theorem; here the only hypotheses are on the instance and on the tie-breaking rule.

Formalization scope

Buyers are a type I with [Fintype I] and [Nonempty I]; products are Fin m, whose order is the arrival order. Bids and budgets are real, with $B(i) > 0$ and $b(i,j) \ge 0$. The state of the algorithm records $x$, the amounts charged, $y$ and $z$; one iteration is step, the run after $k$ products is runPrefix, and revenue sums the charges of the final state. The tie-breaking rule is a function sel of the current $x$ and the product, required to return a maximizer of $b(i,j)(1-x(i))$; the theorem holds for every such rule. The constant $c = (1+R)^{1/R}$ is a real power and requires $R > 0$. The theorem is stated for any bound $R$ on the ratios, of which the exact maximum is one instance. Claims (1) and (2) are stated for every $c > 1$, which covers the paper's choice. The paper's inequality for $\ln(1+x)/x$ allows $x = 0$, read as a limit; the Lean statement requires $x > 0$.

A statement over an unconstrained allocation, or one conditioned on the proof's own intermediate inequalities, would be trivially true or false; the targets here concern only the run the definitions compute.

The development needs finite sums, real powers and logarithms from Mathlib and an induction principle for the run. The LP pair and weak duality are reusable for the paper's extensions, and the run invariants for any primal-dual online algorithm with multiplicative updates. Proofs of any milestone are welcome, as are sharper variants, such as the exact-$R_{\max}$ form or the bound against integral allocations.

Selected references

• N. Buchbinder, K. Jain, J. Naor, Online Primal-Dual Algorithms for Maximizing Ad-Auctions Revenue, Algorithms – ESA 2007, LNCS 4698, 2007. https://doi.org/10.1007/978-3-540-75520-3_24
• A. Mehta, A. Saberi, U. Vazirani, V. Vazirani, AdWords and Generalized Online Matching, Journal of the ACM 54(5), 2007. https://doi.org/10.1145/1284320.1284321
• R. M. Karp, U. V. Vazirani, V. V. Vazirani, An Optimal Algorithm for On-line Bipartite Matching, STOC 1990. https://doi.org/10.1145/100216.100262
• B. Kalyanasundaram, K. R. Pruhs, An Optimal Deterministic Algorithm for Online b-Matching, Theoretical Computer Science 233(1–2), 2000. https://doi.org/10.1016/S0304-3975(99)00140-1
• 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), 2009. https://doi.org/10.1561/0400000024