Online Algorithms

Motivation

The $k$-server problem was introduced by Manasse, McGeoch, and Sleator (STOC 1988 / J. Algorithms 1990) as a common generalization of paging, weighted caching, and related sequential decision problems, and their $k$-server conjecture has since become the central open question of competitive analysis. The conjecture asserts that a single ratio — exactly $k$ — governs deterministic online server management on every metric space.

Timeline

• 1985. Sleator and Tarjan introduce competitive analysis — an online algorithm judged against the offline optimum on every input — for list update and paging, and ask for a theory of such guarantees.
• 1988–1990. Manasse, McGeoch, and Sleator introduce the $k$-server problem (STOC 1988; J. Algorithms 1990) and settle its extremes: no deterministic algorithm beats ratio $k$ on any space with more than $k$ points (Corollary 7), two servers admit a $2$-competitive algorithm (Theorem 5, algorithm RES), and $k$ servers on $k+1$ points admit a $k$-competitive one (Theorem 4, algorithm BAL). Section 8 poses the $k$-server conjecture, in the symmetric finite setting of the paper.
• 1990. Fiat, Rabani, and Ravid (FOCS 1990) give the first competitive ratio depending on $k$ alone — exponential in $k$, but finite on every metric space.
• 1991. Chrobak, Karloff, Payne, and Vishwanathan (SIAM J. Discrete Math.) prove the conjecture on the real line via Double Coverage; Chrobak and Larmore (SIAM J. Comput.) extend it to all tree metrics.
• 1995. Koutsoupias and Papadimitriou (J. ACM) prove the Work Function Algorithm is $(2k-1)$-competitive on every metric space — the breakthrough, and still the best general bound. Their Conjecture 1.1 fixes the conjecture's modern form: for every metric space there is an online algorithm with competitive ratio $k$.
• 1996. The same authors verify the conjecture on spaces of $k+2$ points via the dual 2-evader problem (Inf. Process. Lett. 57).
• 2004. Bartal and Koutsoupias prove the WFA itself is $k$-competitive on the line, weighted stars, and all spaces of $k+2$ points.
• 2021. Coester and Koutsoupias (ICALP) give a unifying potential for all known WFA analyses and push the frontier to the circle.
• 2023. Bubeck, Coester, and Rabani (STOC) refute the randomized analogue: no $o(\log^2 k)$-competitive randomized algorithm exists in general. The deterministic conjecture — this mission's goal — survives as the central open question, with the gap between $k$ and $2k-1$ unmoved since 1995.
• 2026. Coester, Koutsoupias, and Zbysiński post The $k$-server conjecture is true (arXiv:2609.15979), a claimed proof of the full conjecture: the Work Function Algorithm itself is $k$-competitive on every metric space, via a matrix representation of work functions and a potential function built on it. The preprint is not yet peer-reviewed; this mission's goal stays open until a machine-checked proof exists.

Setting

Fix a metric space $M$ with distance function $d$, and a number of servers $k \ge 1$. A configuration records where the $k$ servers stand: it is a function $C$ assigning to each server $i \in \{1, \dots, k\}$ a point $C(i) \in M$. Moving the servers from configuration $C$ to configuration $C'$ means server $i$ travels from $C(i)$ to $C'(i)$; the movement cost is the total distance traveled,

$$\mathrm{moveCost}(C, C') \;=\; \sum_{i=1}^{k} d\bigl(C(i),\, C'(i)\bigr).$$

A request sequence is a finite list $\sigma = (r_1, \dots, r_n)$ of points of $M$, presented one at a time; write $\sigma_{\le j} = (r_1, \dots, r_j)$ for the list of the first $j$ requests (so $\sigma_{\le 0}$ is the empty list).

A deterministic online algorithm $A$ is a rule that, for every finite request sequence $\ell$, specifies a configuration $A(\ell)$ — where the servers stand after serving the requests of $\ell$ in order. In particular $A(\text{empty list})$ is the initial configuration, before any request arrives. Two points about this way of modeling an algorithm:

• Online and deterministic, by construction. The configuration after $j$ requests is $A(\sigma_{\le j})$, a function of those first $j$ requests only — the algorithm cannot see the future, and makes no random choices.
• The service constraint. Whenever a request sequence ends with a request $r$, some server must stand at $r$ immediately after: for every list $\ell$ and every point $r$, the configuration reached after serving $\ell$ followed by $r$ places at least one server at the point $r$.

Running $A$ on $\sigma = (r_1, \dots, r_n)$ produces the configurations $A(\sigma_{\le 0}),\, A(\sigma_{\le 1}),\, \dots,\, A(\sigma_{\le n})$, and its cost is the total movement along this trajectory:

$$\mathrm{cost}_A(\sigma) \;=\; \sum_{j=1}^{n} \mathrm{moveCost}\bigl(A(\sigma_{\le j-1}),\, A(\sigma_{\le j})\bigr).$$

For comparison, an offline schedule for $\sigma$ starting at a configuration $C_0$ is any sequence of configurations $S_0 = C_0, S_1, \dots, S_n$ in which $S_j$ places a server at the request $r_j$, for each $j$ — chosen with the whole of $\sigma$ known in advance. The optimal offline cost $\mathrm{OPT}(C_0, \sigma)$ is the infimum, over all such schedules, of the total movement $\sum_{j=1}^{n} \mathrm{moveCost}(S_{j-1}, S_j)$.

Finally, $A$ is $c$-competitive if there is a constant $a$ — depending on the algorithm, hence possibly on the metric space and the initial configuration, but never on the request sequence — with

$$\mathrm{cost}_A(\sigma) \;\le\; c \cdot \mathrm{OPT}\bigl(A(\text{empty list}),\, \sigma\bigr) + a \qquad \text{for every request sequence } \sigma.$$

Formalization targets

Goal — the $k$-server conjecture

$$\text{For every } k \ge 1,\ \text{every metric space } M,\ \text{and every initial configuration } C_0:\ \exists\, A \text{ starting at } C_0 \text{ that is } k\text{-competitive.}$$

The goal fixes no algorithm: any $k$-competitive construction settles it. This is the weakest stable form of the conjecture — it survives every improvement in constants or techniques short of a disproof.

Milestones — the known ladder

The milestones are the classical results between the trivial and the conjectured, each an existence or impossibility statement over the same definitions: the lower bound $c \ge k$ on any space with at least $k+1$ points; the conjecture for $k = 2$; for spaces of exactly $k+1$ points; for the real line; the $(2k-1)$ upper bound of the Work Function Algorithm on every space; the conjecture for spaces of exactly $k+2$ points; the conjecture for three servers in the Manhattan plane $(\mathbb{R}^2, \ell^1)$ — the one settled case over a genuinely two-dimensional continuum (Bein–Chrobak–Larmore 2002; reproved by the unifying potential of Coester–Koutsoupias 2021); Coester–Koutsoupias's 2021 result that the Work Function Algorithm itself — not just some algorithm — is $3$-competitive for three servers on trees, stated over an explicit formalization of the WFA; and the 2023 Bubeck–Coester–Rabani refutation of the randomized analogue: there are $(k+1)$-point spaces on which every randomized algorithm is $\Omega(\log^2 k)$-competitive, stated over a mixed-strategy model of randomized online algorithms.

Significance

A proof of the conjecture would close the founding problem of competitive analysis and pin down the exact power of determinism in online optimization over arbitrary metrics; a disproof would separate general metric spaces from every special class where the ratio $k$ is known tight. Either outcome recalibrates the field's standard model of adversarial request sequences.

None of these results — not even the lower bound — has a machine-checked proof, and online algorithms as a subject are absent from Mathlib. This mission builds the base layer: a faithful model of online service systems (configurations, online algorithms as prefix functions, offline schedules, competitiveness), the classical possibility and impossibility results over it, and, at the top, the Koutsoupias–Papadimitriou bound, whose potential-function argument is self-contained but delicate. The model is reusable for paging, weighted caching, metrical task systems, and the randomized $k$-server problem.

Difficulty

The obvious first idea — the greedy algorithm, moving the nearest server to each request — is not competitive for any constant, already on three points of the line: two nearby points can ping-pong one server forever while a server parked slightly farther away never moves. Every known competitive algorithm must sometimes move a server other than the nearest one, and the whole difficulty of the conjecture is quantifying exactly how much such foresight-free hedging can achieve. The Work Function Algorithm's analysis via a potential over offline work functions loses a factor of two for reasons nobody has been able to remove; on the lower-bound side, no metric space is known where the deterministic ratio exceeds $k$.

Formalization scope

The Lean model commits to: configurations as functions Fin k → M (labeled servers — equivalent in cost to the unlabeled multiset model, since offline can permute labels for free); algorithms as total functions List M → (Fin k → M) with the service constraint, so a step may move several servers (the standard laziness reduction makes this equivalent to one-move-per-request); costs in ℝ via Metric.dist; the offline optimum as an sInf over schedules, which agrees with the attained minimum on finite spaces; and the additive-constant form of competitiveness, quantified as ∃ a, ∀ σ.

Two conventions guard against trivialization. The additive constant is quantified before the request sequence — allowing it to depend on $\sigma$ would make every algorithm $1$-competitive. And the lower-bound milestone requires $k+1$ distinct points (Finset.card = k + 1); on spaces with at most $k$ points the conjecture is trivially true and the lower bound false.

Three further definitional layers extend the model. The work function workFunction C₀ σ C is the sInf of (schedule cost + final move to C) over schedules serving σ from C₀, and the Work Function Algorithm WFA is defined on finite spaces with k ≥ 1 servers: after each request it moves to a configuration containing the request minimizing (movement cost) + (work function of the history including the request), a minimizer existing by finiteness and ties broken by a fixed arbitrary choice — matching the standard definition with its "ties broken arbitrarily" (our fixed choice is one admissible instance). A tree is a finite metric space carrying a tree graph whose weighted path lengths realize the metric — exactly "the set of vertices of a tree" of the sources. A randomized algorithm is a mixed strategy: a probability measure over an index type together with a deterministic algorithm per outcome and measurable per-sequence cost; its expected cost is a lower Lebesgue integral in $[0,\infty]$, and $c$-competitiveness from $C_0$ demands every outcome start at $C_0$ and one additive constant work for all request sequences.

Welcome contributions: proofs of any milestone in any order (the lower bound and the $(k+1)$-point case are the natural entry points); alternative algorithms for milestones already closed; and infrastructure lemmas about moveCost, schedules, and work functions published as reusable platform theorems.

Selected references

• M. Manasse, L. McGeoch, D. Sleator, Competitive algorithms for server problems, J. Algorithms 11 (1990). doi:10.1016/0196-6774(90)90003-W
• A. Fiat, Y. Rabani, Y. Ravid, Competitive k-server algorithms, FOCS 1990. doi:10.1109/FSCS.1990.89566
• M. Chrobak, H. Karloff, T. Payne, S. Vishwanathan, New results on server problems, SIAM J. Discrete Math. 4 (1991). doi:10.1137/0404017
• M. Chrobak, L. Larmore, An optimal on-line algorithm for k servers on trees, SIAM J. Comput. 20 (1991). doi:10.1137/0220008
• E. Koutsoupias, C. Papadimitriou, On the k-server conjecture, J. ACM 42 (1995). doi:10.1145/210118.210128
• E. Koutsoupias, C. Papadimitriou, The 2-evader problem, Inf. Process. Lett. 57(5) (1996), 249–252.
• C. Coester, E. Koutsoupias, Towards the k-server conjecture: a unifying potential, pushing the frontier to the circle, ICALP 2021. arXiv:2102.10474
• S. Bubeck, C. Coester, Y. Rabani, The randomized k-server conjecture is false!, STOC 2023. arXiv:2211.05753
• E. Koutsoupias, The k-server problem (survey), Computer Science Review 3 (2009). doi:10.1016/j.cosrev.2009.04.002

Motivation

Many online problems — renting vs. buying equipment, routing traffic without knowing future demand, allocating advertising budget as bids arrive — share a common linear-programming shape: a covering (minimization) problem whose constraints appear one at a time, or its dual packing (maximization) problem whose variables appear one at a time, with no ability to revisit past decisions. Buchbinder and Naor's survey [1] recasts the online primal-dual method, originally developed for offline approximation in Section 2 of the same survey (already covered on this platform via the PrimalDualOnline namespace, citing Buchbinder's thesis [2]), as a general recipe for such online problems, unifying earlier ad hoc analyses of the ski-rental problem (Chapter 3) and paving the way for the online set-cover, routing, caching, and ad-auction algorithms formalized elsewhere in this series. This mission covers Chapter 4, "The Basic Approach": the framework itself and its three founding algorithms.

Setting

Fix a finite index set $I$ of primal variables with non-negative cost coefficients $c_i$, and a finite index set $J$ of covering constraints, revealed one at a time in the order enumerated by $J$. Each constraint $j$ is given by a set $S(j) \subseteq I$ (the book's simplified setting, in which every non-zero coefficient equals $1$ and every right-hand side equals $1$; Chapter 14 removes this restriction) and asserts $\sum_{i \in S(j)} x_i \ge 1$. An online covering algorithm may only increase the $x_i$, never decrease them, and upon a constraint's arrival must eventually make it hold. The online covering problem is to minimize $\sum_i c_i x_i$ subject to every revealed constraint, online. Its Lagrangian dual is the online packing problem: a dual variable $y_j$ arrives together with constraint $j$, may only be increased while $j$ is being processed, and the objective is to maximize $\sum_j y_j$ subject to $\sum_{j \mid i \in S(j)} y_j \le c_i$ for every $i$ — the packing constraint on $i$ becomes fully known only once every $j$ with $i \in S(j)$ has arrived, so it, too, is revealed gradually. $d := \max_j |S(j)|$, the largest constraint size, is carried as an explicit parameter throughout.

Section 4.2 gives three algorithms solving both problems simultaneously — the same run produces a covering solution $x$ and a packing solution $y$ — with the same worst-case guarantee but different flavors: Algorithm 1 is a discrete process (each processing round performs a whole number of identical multiplicative-plus-additive updates until its constraint is satisfied); Algorithm 2 is the continuous limit of Algorithm 1 (dual variables increase continuously and $x_i$ follows an explicit exponential of the accumulated dual sum); Algorithm 3 replaces the continuous update with one triggered by an approximate complementary-slackness condition, at the cost of a mild dual infeasibility. All three make essential use of the online order: an algorithm that saw the whole instance up front would trivially solve the offline LP.

Formalization targets

Theorem 4.3 (Algorithm 3 — the goal, p. 124):

$$\Big(\forall i,\ \textstyle\sum_{j \mid i \in S(j)} y_j \le c_i(1+\ln d)\Big) \ \wedge\ \Big(\forall x''\text{ feasible},\ \textstyle\sum_i c_i x_i \le 2(1+\ln d)\sum_i c_i x''_i\Big) \ \wedge\ \Big(\forall y''\text{ feasible},\ \textstyle\sum_j y''_j \le 2\sum_j y_j\Big).$$

Theorem 4.1 (Algorithm 1) and Theorem 4.2 (Algorithm 2, p. 118 and p. 121) are the same three-part guarantee for the other two algorithms, with $\log_2(3d+1)$ in place of $1+\ln d$ for Algorithm 1 (and its packing solution genuinely integral), and with $2\ln(1+d)$ in place of both $2(1+\ln d)$ and $2$ for Algorithm 2 (whose packing solution is exactly feasible, not merely approximately so). The competitive ratios are stated against an arbitrary offline-feasible comparison solution on each side (covering and packing) rather than against an unconstructed LP optimum — the standard weak-duality reformulation of "$c$-competitive", and the one the book's own proofs (which invoke weak duality directly, never LP optimality) actually establish.

Significance

The framework converts three qualitatively different design intuitions — the ski-rental-style discrete doubling, the continuous primal-dual differential equation, and complementary slackness — into three algorithms with an identical asymptotic guarantee, $\Theta(\log d)$, matching the $\Omega(\log d)$ (packing) and $\Omega(\log n)$ (covering) lower bounds the book proves in Section 4.3 (Lemmas 4.5-4.6, not part of this mission). This is the load-bearing substrate for the rest of the survey: Chapter 5's online set-cover algorithm, Chapter 13's bounded-allocation problem, and Chapter 14's general packing-covering constraints all restate this chapter's framework locally rather than re-deriving it, and are formalized as separate missions in this series. Formalizing it here, once, with the exact constants each proof establishes, is what lets those missions cite a single faithful statement instead of three independently-drifting restatements. No formal development of this framework was found on the platform as of 2026-09-20 (searches below); this mission is the first.

Difficulty

The central obstacle is not the algebra of any single algorithm's proof — each is a short, self-contained argument — but stating the guarantee for an online process using only its final output. An algorithm is characterized here by the closed-form relation its update rule establishes between the accumulated dual sum and the primal value (e.g., Algorithm 3's $x_i = \min(1, d^{-1}\exp(d_i/c_i - 1))$ once activated, $0$ before), together with primal feasibility as the hypothesis that a run has completed; a formalization that instead handed the algorithm the whole instance in advance, or dropped primal feasibility as a hypothesis, would either trivialize the online promise or make the stated bound simply false. A second difficulty specific to this formalization: Theorem 4.3's own proof bounds the primal cost by splitting it into a piece controlled by the final-state complementary-slackness conditions (immediate from the closed form and the $d$-bound) and a piece controlled by a derivative/telescoping argument over the continuous accumulation process itself — the latter is a genuinely dynamic fact about the trajectory, not just its endpoint, and is recorded as a documented simplification below rather than folded into the hypotheses, since the goal is a faithful statement, not a proof.

Formalization scope

CoveringInstance I J bundles S : J → Finset I, c : I → ℝ, and d : ℝ with 0 < d and ∀ j, (S j).card ≤ d as explicit hypotheses (never derived as d := ⨆ j, (S j).card, matching the book's own presentation and avoiding a vacuous formalization in which d is chosen after the fact to make the bound trivial). dualSum inst y i := ∑_{j \mid i \in S(j)} y_j. Each algorithm's output is a noncomputable def from the accumulated dual data to ℝ (alg1X, alg2X, alg3X), so that "the algorithm's output" is genuinely a function of its dual trajectory rather than an independently-constrained free variable — ruling out the trivializing formalization in which $x$ and $y$ are unrelated variables merely required to satisfy the conclusion's own inequalities. Reals throughout (ℝ, not ℝ≥0 or ENNReal); Finset.filter realizes "$j$ such that $i \in S(j)$"; Real.logb 2 and Real.log (natural log) match the book's own log₂ and ln. Reusable beyond this mission: CoveringInstance, dualSum, and the weak-duality-style "competitive against any feasible comparison solution" pattern, which 05-online-set-cover, 13-bounded-allocation, and 14-general-packing-covering are expected to restate locally (per this series' own rule against cross-draft imports between concurrent missions) rather than import directly. Welcome contributions: completing any of the three sorrys, and formalizing the Section 4.3 lower bounds (Lemmas 4.5-4.6) as a 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
• N. Buchbinder. Designing Competitive Online Algorithms via a Primal-Dual Approach. PhD thesis, Tel Aviv University, 2008. https://www.tau.ac.il/~nivb/download/phd-thsis.pdf

Motivation

Search-engine ad-auctions sell items (ad slots) to buyers who arrive with per-item bids and a fixed daily budget, online: each item must be allocated the moment it appears, with no ability to revisit past allocations, and no buyer may ever be charged more than its budget. Buchbinder and Naor's survey [1] models this as a generalization of online bipartite matching and derives an allocation algorithm through the same online primal-dual recipe formalized elsewhere in this series (Chapter 4's framework), applied to a genuinely different LP shape — a maximization (revenue) problem whose "packing" role and "covering" role are the reverse of Chapters 4, 5 and 7 — and to a different constraint structure (budget caps on a per-buyer accumulated sum, not a per-constraint 0/1 covering requirement). This mission covers Section 10.1, "The Basic Algorithm": the single-slot allocation algorithm and its $(1-1/c)(1-R_{\max})$-competitive analysis (Theorem 10.1). Sections 10.2-10.3 (multiple ad-slots via strong duality; stochastic per-buyer spending guarantees) are out of scope — see Formalization scope.

Setting

Fix a finite set $I$ of buyers, each with budget $B_i > 0$, and a finite set $M$ of items; buyer $i$ bids $b_{ij} \ge 0$ for item $j$, revealed one item at a time in the order enumerated by $M$. Let $R_{\max} := \max_{i,j} b_{ij}/B_i$, carried as an explicit positive parameter. The Allocation algorithm (p. 212), upon each item $j$'s arrival, allocates it to the buyer $i$ maximizing $b_{ij}(1-x_i)$ (where $x_i \in [0,1]$ is buyer $i$'s current primal value); if $x_i \ge 1$ already, nothing happens (the buyer is "full"). Otherwise it charges buyer $i$ the minimum of $b_{ij}$ and its remaining budget, sets the dual allocation variable $y_{ij} \leftarrow 1$, sets $z_j \leftarrow b_{ij}(1-x_i)$, and updates $x_i \leftarrow x_i(1+b_{ij}/B_i) + b_{ij}/((c-1)B_i)$ for a constant $c$ fixed by the analysis. The revenue actually collected from buyer $i$ is $\min\!\big(\sum_j b_{ij}y_{ij},\,B_i\big)$ — the buyer is never charged more than its budget. Unlike Chapters 4/7, this LP's dual (the ad-auctions revenue objective, Fig. 10.1) is the maximization problem being solved online; the "primal" covering LP ($x_i$, $z_j$ variables) exists only as a duality certificate.

Formalization targets

Theorem 10.1 (the goal, p. 212), given the milestone's dual near-feasibility bound and the fact that each buyer's total accrued bids exceed its budget by at most a factor of $R_{\max}$ (Claim (3)'s consequence):

$$\forall\, (x'', z'')\text{ feasible for Fig. 10.1's covering LP},\ \ \textstyle\sum_i \mathrm{actualCharge}(i) \ \ge\ (1-\tfrac1c)(1-R_{\max}) \Big(\textstyle\sum_i B_i x''_i + \sum_j z''_j\Big),$$

with $c = (1+R_{\max})^{1/R_{\max}}$ taken verbatim from the theorem's own statement — the exact formula, not an $O(\cdot)$ instantiation. Inequality (10.1) (p. 213), the milestone, is the book's own induction-proved lower bound on a buyer's primal value in terms of its accrued bids: $x_i \ge \frac{1}{c-1}\big(c^{(\sum_j b_{ij}y_{ij})/B_i} - 1\big)$.

Significance

Theorem 10.1 is the entry point to a short but influential sub-line of the online primal-dual method — Section 10.2 extends it to multiple ad-slots via strong duality for maximum-weight matching (rather than the weak duality this framework otherwise relies on throughout), and Section 10.3 incorporates stochastic per-buyer spending guarantees, both reusing this section's constant $c=(1+R_{\max})^{1/R_{\max}}$ and its limit $c\to e$ as $R_{\max}\to0$ (recovering the classic $(1-1/e)$-competitive ratio for the unweighted, unbudgeted case). It is also the first mission in this series to apply the online primal-dual method to a genuine revenue-maximization problem rather than a covering/packing pair with matching roles. No formal development of ad-auctions, budgeted online matching, or this constant was found on the platform as of 2026-09-20 (searches below); this mission is the first.

Difficulty

As with 04-framework's Algorithm 3 and 07-generalized-caching's Fractional Caching algorithm, the central obstacle is characterizing an online process by its own final output. Unlike those two chapters, however, step (3)'s update increment varies per allocation (bd, the specific bid of the item just won), so no closed-form solution of the recurrence exists in general; buyerX is instead defined as an explicit List.foldl realizing the exact per-step update, over the (temporally ordered) list of bids a buyer actually won — a faithful, if less immediately readable, transcription of "the algorithm's output as a function of its own trajectory," in the same spirit as this series' other closed-form definitions. A second difficulty specific to this chapter: the book's derivation of inequality (10.1) is itself an induction on iterations (not a single algebraic step, unlike Eq. (7.2) in 07-generalized-caching), and the theorem's final bound further combines it with a separate "at most one undercharged iteration" argument (Claim (3)'s conclusion, p. 214-215) turning the raw accrued-bid bound into one about the actually collected (budget-capped) revenue — both are stated here as explicit hypotheses (the milestone, and h_at_most_one_undercharge) rather than derived, since the goal is a faithful statement, not a proof; both sorrys are documented, not silently discharged.

Formalization scope

AdAuctionsInstance I M bundles b : I → M → ℝ, B : I → ℝ (hB_pos), and Rmax : ℝ with hRmax_pos : 0 < Rmax and hRmax_bound : ∀ i j, b i j ≤ Rmax * B i — the last two as explicit hypotheses, never derived via Finset.sup, matching 04-framework's d and 07-generalized-caching's k. cParam inst := (1+Rmax)^(1/Rmax) uses Real.rpow (ℝ^ℝ). buyerX inst i bids folds step (3)'s update over a list of won bids; revenue/actualCharge realize $\sum_j b_{ij}y_{ij}$ and its budget-capped charge. Reals throughout. Explicitly out of scope: Section 10.2's multiple-slot generalization (Theorem 10.2), which requires strong duality for maximum-weight bipartite matching as an explicit premise (the book: "our analysis... crucially relies on strong duality") — a substantially different LP structure (an integral matching LP, not this section's per-buyer budget LP) that this mission's AdAuctionsInstance does not model, and whose applicability of PrimalDualOnline.LP.strong_duality_adapter (this book's own Theorem 2.2) was not verified in the time available. Section 10.3's stochastic guarantee (Theorem 10.3) is likewise out of scope, and its own BRIEF.md-flagged ambiguity (whether its scalar g is $\min_i g_i$ or another aggregate of the per-buyer vector $g_i$) was not resolved. Both are natural follow-on missions, not attempted here. Welcome contributions: completing the two sorrys, and the Section 10.2-10.3 follow-on mission(s).

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

Metrical task systems, introduced by Borodin, Linial and Saks (J. ACM 39(4), 1992), are a common abstraction of on-line problems in which a server occupies one of finitely many states, pays a cost for each task depending on its current state, and may pay a transition cost to change state first. Paging, list update and the $k$-server problem all fit into this framework. The paper's first main result is that every deterministic on-line algorithm on an $n$-state metrical task system has competitive ratio at least $2n-1$, and that $2n-1$ is attained. The lower bound comes from an adversary that always charges the state the algorithm currently occupies. That adversary needs to know the algorithm's state, which suggests that randomization can help.

Section 7 of the paper makes this precise for the simplest system, the uniform task system, in which all transitions cost $1$. There the randomized competitive ratio against an oblivious adversary is between $H(n)$ and $2H(n)$, where $H(n)=1+\tfrac12+\cdots+\tfrac1n$ is between $\ln n$ and $1+\ln n$. This was the first logarithmic bound for a task system.

Timeline:

• 1985: Sleator and Tarjan introduce competitive analysis for list update and paging (CACM 28(2)).
• 1987/1992: Borodin, Linial and Saks define metrical task systems, prove the deterministic ratio $2n-1$, and prove $H(n)\le\bar w\le 2H(n)$ for the uniform system (conference version STOC 1987; journal version cited above).
• 1991: Fiat, Karp, Luby, McGeoch, Sleator and Young prove the analogous $2H_k$ upper bound for randomized paging (J. Algorithms 12(4)).

Setting

A task system $(S,d)$ is a finite set $S$ of $n$ states with a transition-cost matrix $d$: $d(i,i)=0$, $d(i,j)>0$ for $i\ne j$, and $d(i,k)\le d(i,j)+d(j,k)$. In the uniform task system, $d(i,j)=1$ for all $i\neq j$. A task is a vector $T\in\mathbb R_{\ge0}^S$ of processing costs. Given an initial state $s_0$ and tasks $\mathbf T=T^1\cdots T^m$, a schedule is $\sigma:\{0,\dots,m\}\to S$ with $\sigma(0)=s_0$, of cost

$$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 least cost over all schedules.

A deterministic on-line algorithm chooses $\sigma(i)$ from $s_0$ and $T^1,\dots,T^i$. A randomized on-line algorithm $R$ chooses $\sigma(i)$ at random, with a distribution that depends on $s_0$, on $T^1,\dots,T^i$ and on the states $\sigma(0),\dots,\sigma(i-1)$ already visited. The task sequence is fixed before any random choice is made (an oblivious adversary). With $\mathrm{pr}(\sigma\mid\mathbf T)$ the probability that $R$ follows $\sigma$, the expected cost is $\bar c_R(\mathbf T)=\sum_\sigma c(\mathbf T;\sigma)\,\mathrm{pr}(\sigma\mid\mathbf T)$. For $w>0$, $R$ is expected $w$-competitive if there is a constant $K$ with

$$\bar c_R(\mathbf T)\le w\,c_0(\mathbf T)+K$$

for every finite task sequence and every initial state. The randomized competitive ratio $\bar w(S,d)$ is the infimum of all such $w$ over all $R$.

Formalization targets

Goal: Theorem 7.1

For the uniform task system on $n\ge1$ states,

$$H(n)\;\le\;\bar w(S,d)\;\le\;2H(n).$$

Milestones

1. Upper bound (p. 759). Some randomized on-line algorithm is expected $2H(n)$-competitive on the uniform task system.
2. Lemma 7.2 (p. 759). Let $D$ be a distribution on infinite task sequences over a finite task alphabet, with $E(c_0(\mathbf T^j))\to\infty$, and let $m_j=\inf_A E(c_A(\mathbf T^j))$ over deterministic on-line algorithms. Then every achievable $w$ satisfies

$$\limsup_{j\to\infty}\frac{m_j}{E(c_0(\mathbf T^j))}\le w .$$

3. $m_j\ge j/n$ (p. 760) when the tasks are independent uniformly random unit elementary tasks $U_s$ (cost $1$ in $s$, $0$ elsewhere).
4. Coupon collector (p. 760). For i.i.d. uniform states on $S$, the expected number of draws until every state has appeared is $nH(n)$.
5. Off-line cost (p. 760). Under the same distribution, $E(c_0(\mathbf T^j))\le j/(nH(n))+C$ for a constant $C$ independent of $j$.

Significance

The theorem shows that randomization reduces the competitive ratio of the uniform task system from $2n-1$ to $\Theta(\log n)$. That is an exponential improvement, and it identifies the adversary's knowledge of the algorithm's state as the source of the deterministic lower bound. Lemma 7.2 is a form of Yao's principle adapted to the additive-constant definition of competitiveness. It is the standard tool for randomized lower bounds in on-line computation, and the same argument shape reappears for paging and $k$-server lower bounds.

On the formalization side, the result is proved but, as far as is known, has not been machine-checked. A complete development yields a reusable model of randomized on-line algorithms with oblivious adversaries, a Yao-type lemma usable for other on-line problems, and a coupon-collector expectation in the product-measure setting. The upper half additionally needs the continuous-time reduction of the paper's Lemma 3.1 in randomized form, or a direct discrete-time algorithm.

Difficulty

For the upper bound, the natural algorithm is continuous-time. It proceeds in phases, and inside a phase it stays in a state until that state has accumulated cost $1$. A discrete task can saturate several states at once and straddle a phase boundary. So a discrete algorithm must either simulate the continuous one or be analyzed directly, and the expected transition count per phase must be controlled with the first phase starting in a deterministic state.

For the lower bound, the first obstacle is that the natural statement "$\bar w\ge\limsup m_j/E(c_0)$" silently assumes that a randomized algorithm's expected cost, averaged over random inputs, is at least that of the best deterministic algorithm. With the behavioural (kernel) definition used here, this requires converting a kernel into a mixture of deterministic algorithms, which is Kuhn's theorem on each finite horizon. The second obstacle is that the paper's claim $E(c_0(\mathbf T^j))\le j/(nH(n))+O(1)$ is supported only by the elementary renewal theorem, which gives a limit of ratios; the additive bound needs a sharper renewal estimate. Mathlib has no renewal theory. The hypothesis $E(c_0(\mathbf T^j))\to\infty$ of Lemma 7.2 must also be established for the uniform distribution; the paper does not prove it separately.

Formalization scope

• States form a finite nonempty type S, and $n$ = Fintype.card S; no $n\ge2$ assumption is made (at $n=1$ the goal reads $1\le\bar w\le2$, and $\bar w=1$). $H(n)$ is Mathlib's harmonic n, cast to $\mathbb R$. The uniform system has unit transition cost.
• Tasks are finite and nonnegative. The paper also allows $+\infty$ entries; these are excluded. Task sequences are Fin m → S → ℝ and schedules are Fin (m+1) → S with σ 0 = s₀. $c_0$ is a finite minimum.
• A randomized algorithm is a kernel S → List (S → ℝ) → List S → PMF S. This is the paper's scheduler–taskmaster description (p. 758), equivalent to a distribution over deterministic algorithms on every finite task sequence. $\mathrm{pr}(\sigma\mid\mathbf T)$ is the product of kernel probabilities, and $\bar c_R$ is a finite sum. That $\mathrm{pr}(\cdot\mid\mathbf T)$ sums to $1$ has been checked locally.
• $\bar w(S,d)$ is the real sInf of $\{w : \exists R,\ R \text{ expected } w\text{-competitive}\}$. On the empty set this would be $0$, so the upper bound is stated as the existence of an expected $2H(n)$-competitive algorithm, and Lemma 7.2 is stated for every achievable $w$. The goal's lower half forces the set to be nonempty. Statements of the form "$\bar w\le c$" alone are therefore not acceptable substitutes for milestones 1 and 2.
• Lemma 7.2 is restricted to task sequences over a finite alphabet, with the product $\sigma$-algebra and measurable singletons. This makes every $E(c_A(\mathbf T^j))$ a genuine integral for every deterministic $A$, and it covers the paper's application. The $\limsup$ of Lemma 7.2 is taken in EReal.
• The coupon-collector time takes values in $[0,\infty]$ and its expectation is a lower Lebesgue integral. Milestone 5 renders the paper's $O(1)$ as an explicit constant $C$ chosen before $j$.

Contributions welcome: proofs of any milestone; a discrete-time randomized phase algorithm; a general Kuhn-type conversion from kernels to mixtures of deterministic algorithms; renewal-theoretic lemmas.

Selected references

• A. Borodin, N. Linial, M. Saks, An Optimal On-Line Algorithm for Metrical Task System, J. 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, Commun. ACM 28(2):202–208, 1985. https://doi.org/10.1145/2786.2793
• A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive Paging Algorithms, J. Algorithms 12(4):685–699, 1991. https://doi.org/10.1016/0196-6774(91)90041-V
• A. C.-C. Yao, Probabilistic Computations: Toward a Unified Measure of Complexity, FOCS 1977, 222–227. https://doi.org/10.1109/SFCS.1977.24
• S. M. Ross, Applied Probability Models with Optimization Applications, Holden-Day, 1970 (the elementary renewal theorem cited as [20] in the paper).

Motivation

Caching (online paging) is one of the oldest problems in online algorithms: a fast memory of $k$ slots serves a sequence of requests, and every request for an element not in the fast memory is a cache miss that forces the element to be loaded, possibly evicting another one. With the whole request sequence known in advance, evicting the element whose next request is furthest in the future is optimal (Bélády, 1966). Without that knowledge, no deterministic algorithm is better than $k$-competitive, and the best randomized algorithms are $\Theta(\log k)$-competitive (Fiat, Karp, Luby, McGeoch, Sleator and Young, 1991).

Lykouris and Vassilvitskii asked what happens in between: an online algorithm receives, with every request, a machine-learned prediction of the element's next arrival time. A good predictor should make the algorithm nearly as good as Bélády's rule (consistency), and a bad predictor should never make it worse than a classical algorithm (robustness). Their paper (arXiv:1802.05399v4; J. ACM 2021) is one of the founding papers of learning-augmented algorithms, and its algorithm, Predictive Marker, is the reference point for the later literature on caching with predictions.

Timeline.

• 1966: Bélády's furthest-in-future rule is optimal offline.
• 1985: Sleator and Tarjan show that deterministic online paging is at best $k$-competitive.
• 1991: Fiat et al. introduce the Marker algorithm, $2H_k$-competitive, and the clean-element lower bound on the optimum.
• 2018: Lykouris and Vassilvitskii (arXiv:1802.05399) introduce Predictive Marker, with ratio $2\min(1+2S_\ell(\epsilon), 2H_k)$ for an $\epsilon$-accurate predictor.
• 2020: Rohatgi (arXiv:1910.12172, SODA 2020) and Wei (arXiv:2005.13716, APPROX/RANDOM 2020) improve the dependence on the error.

Setting

A request sequence $\sigma = (z_1, \dots, z_n)$ lists elements of a set $Z$. A cache of size $k \ge 1$ starts empty. A request for a cached element is a hit; otherwise it is a miss, the element is loaded, and if the cache is full some element is evicted first. The offline optimum $\mathrm{Opt}(\sigma)$ is the least number of misses over all eviction schedules chosen with knowledge of $\sigma$.

With each request $z_i$ the algorithm receives a real prediction $h_i$. The true label $y_i$ is the position of the next request of $z_i$, or $n+1$ if there is none. For a loss function $\ell \ge 0$, the error of the predictions is $\eta_\ell(h,\sigma) = \sum_i \ell(y_i, h_i)$, and the predictions are $\epsilon$-accurate when $\eta_\ell(h,\sigma) \le \epsilon \cdot \mathrm{Opt}(\sigma)$.

The spread of $\ell$ measures how cheaply a predictor can get the order of arrivals completely wrong: $S_\ell(m)$ is the least length $T \ge 1$ such that every strictly increasing integer sequence $a_1 < \dots < a_T$ and every non-increasing real sequence $b_1 \ge \dots \ge b_T$ have total loss $\sum_i \ell(a_i, b_i) \ge m$.

Predictive Marker (Algorithm 1) works in the phases of the Marker algorithm. Requested elements are marked. A phase ends when the cache is full, every cached element is marked, and a miss occurs; then all marks are removed. An element requested in a phase but not in the previous one is clean, and $Q(\sigma)$ is the total number of clean elements. Each clean miss starts a chain. An element evicted in the current phase that is requested again (a stale miss) extends the chain in which it was evicted. Evictions are among unmarked elements. As long as the chain's length $n(r,c)$ is at most $H_k = 1 + \tfrac12 + \dots + \tfrac1k$, the evicted element is one with the largest prediction. After that it is chosen uniformly at random. The expected number of misses of Predictive Marker is $\mathrm{cost}_{PM}(\sigma)$.

Formalization targets

Goal: Theorem 3.3

If $S$ is concave on $[0,\infty)$ and majorizes the spread, then for every $\epsilon \ge 0$, every tie-breaking rule, and every sequence with $\epsilon$-accurate predictions,

$$\mathbb E\bigl[\mathrm{cost}_{PM}(\sigma)\bigr] \le 2\cdot\min\bigl(1 + 2S(\epsilon),\ 2H_k\bigr)\cdot \mathrm{Opt}(\sigma).$$

Milestones

• Claim 1 (Fiat et al.): $Q(\sigma) \le 2\,\mathrm{Opt}(\sigma)$.
• Proof of Theorem 3.3, last sentence: $\mathrm{Opt}(\sigma) \le Q(\sigma)$.
• Lemma 3.3: a chain that evicts by the predictions only has length $n(r,c) \le 1 + S(\eta_{r,c})$, where $\eta_{r,c}$ is the error of the predictions on the elements evicted into it.
• Lemma 3.4: $\mathbb E[n(r,c)] \le \mathbb E[\min(1 + 2S(\eta_{r,c}), 2H_k)]$.

Significance

The result. Theorem 3.3 gives both guarantees at once. For an exact predictor ($\epsilon = 0$) the ratio is a constant, $2(1 + 2S(0))$, independent of $k$; for an arbitrary predictor it is $4H_k$, within a constant factor of the optimal randomized ratio. In between, the ratio degrades with the error at the rate of the spread: for the absolute loss the spread grows like $\sqrt m$, so the ratio grows like $\sqrt\epsilon$. The spread and the chain decomposition are the tools later papers build on to trade consistency against robustness.

Formalizing it. The theorem is proved on paper; no machine-checked proof of it, of the Marker analysis, or of the clean-element bound of Fiat et al. is known. A formalization supplies a precise model of a randomized online algorithm with predictions. It also settles the details the paper leaves implicit: the eviction missing from the clean branch of Algorithm 1 as printed, the cap $2H_k$ printed as $2\log k$ in Lemma 3.4, and the behaviour of the spread at $0$.

Difficulty

The obvious argument charges every miss to a chain and bounds each chain separately. That works for chains that follow the predictions, but a chain that switches to random evictions interacts with every other chain of the phase, because all of them evict from the same pool of unmarked elements. A bound on its expected length must hold whatever the other chains evict, including evictions that depend on earlier coin flips. A second difficulty is summing. The chain errors $\eta_{r,c}$ and the chain lengths are both random, while the hypothesis controls only the total error $\eta_\ell(h,\sigma)$ against $\mathrm{Opt}(\sigma)$, not the number of chains $Q(\sigma)$ in which the error is spread.

Formalization scope

Elements form a type with decidable equality. A request sequence is a list; predictions are one real per request, and every real sequence is allowed. Labels are 1-based next-arrival positions, with $n+1$ for elements never requested again. The paper prints the label with equal features; the element is meant. $\mathrm{Opt}$ is computed as the minimum over all demand-paging schedules from the empty cache, which loses no generality. $H_k$ is harmonic k as a real number, never $\log k$.

Predictive Marker is a PMF over final states. The random eviction of line 21 is uniform over the unmarked cached elements, and ties in the arg max are a parameter quantified universally. The eviction of lines 23–24 is also performed after a clean miss; as printed, it sits only in the stale branch. The expected cost lies in $[0,\infty]$.

The spread takes real arguments and lengths $T \ge 1$. $S$ must be concave on $[0,\infty)$, finite, and at least the spread. It must also be continuous at $0$, which the paper does not say: without it the chain lemma fails for losses whose minimal reversed-order loss stays $0$ over several lengths. $\epsilon$-accuracy is the pointwise condition on the given pair $(\sigma, h)$. The competitive ratio is written as a product, so $\mathrm{Opt}(\sigma) = 0$ needs no special case. Lemma 3.3 is stated pointwise for chains without random evictions, as its proof shows. Lemma 3.4 has $2H_k$ in place of the printed $2\log k$, with the minimum inside the expectation because $\eta_{r,c}$ is random.

The statement must not be trivialized. $\mathrm{Opt}$ is the true offline optimum, not Bélády's rule applied to the predictions. The expectation is taken over Predictive Marker's own run, never compared with itself. The spread hypothesis is satisfiable; for example, the constant loss $1$ has spread $\max(1,\lceil m\rceil) \le m + 1$.

Out of scope: Lemma 3.2 (the special-marking algorithm SM, which enters only through Lemma 3.4's proof); Lemma 3.1 and Corollaries 1–2, whose printed constants are false for small $m$ or disagree with Theorem 3.3; the lower bounds of §3.1 and §3.4; the extensions of §4; the experiments of §5; running time and learnability.

Welcome contributions: the Marker phase structure and its equivalence with the combinatorial phases, the clean-element bounds $Q/2 \le \mathrm{Opt} \le Q$ (reusable for any marking algorithm), and a bound on the expected number of misses caused by elements evicted uniformly at random within a phase.

Selected references

• T. Lykouris, S. Vassilvitskii, Competitive Caching with Machine Learned Advice, arXiv:1802.05399v4, 2020; J. ACM 68(4), 2021. https://arxiv.org/abs/1802.05399v4
• A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive paging algorithms, J. Algorithms 12(4), 1991. https://doi.org/10.1016/0196-6774(91)90041-V
• L. A. Bélády, A study of replacement algorithms for a virtual-storage computer, IBM Systems Journal 5(2), 1966. https://doi.org/10.1147/sj.52.0078
• D. D. Sleator, R. E. Tarjan, Amortized efficiency of list update and paging rules, Comm. ACM 28(2), 1985. https://doi.org/10.1145/2786.2793
• D. Rohatgi, Near-optimal bounds for online caching with machine learned advice, SODA 2020. https://arxiv.org/abs/1910.12172
• A. Wei, Better and simpler learning-augmented online caching, APPROX/RANDOM 2020. https://arxiv.org/abs/2005.13716

Motivation

A single machine must process $n$ jobs that arrive over time. Job $j$ is released at time $r_j$, needs $p_j$ units of uninterrupted processing, and has weight $w_j > 0$; the goal is to minimize the total weighted completion time $\sum_j w_j C_j$. Offline, with all release dates equal to zero, Smith's rule (sequence by nondecreasing $p_j/w_j$) is optimal (Smith 1956); with arbitrary release dates the problem $1\,|\,r_j\,|\,\sum w_j C_j$ is strongly NP-hard (Lenstra, Rinnooy Kan and Brucker 1977).

In the online version the scheduler learns of job $j$ only at time $r_j$, and at each moment must either start a released job or keep the machine idle. Its quality is measured by its competitive ratio: the worst case, over all instances, of the ratio between the online schedule's cost and the offline optimum. Release-date scheduling is one of the basic test cases of online optimization.

Timeline:

• 1996. Hoogeveen and Vestjens show that no online algorithm has competitive ratio below 2, even with equal weights, and give the 2-competitive algorithm Delayed SPT for equal weights.
• 1997. Hall, Schulz, Shmoys and Wein give a $(3+\varepsilon)$-competitive algorithm for arbitrary weights, based on geometric intervals and linear programming.
• 1998. Phillips, Stein and Wein give another 2-competitive algorithm for equal weights, which does not extend to arbitrary weights.
• 2002. Goemans, Queyranne, Schulz, Skutella and Wang obtain a $(1+\sqrt2)$-competitive deterministic algorithm from an LP relaxation.
• 2004. Anderson and Potts show that Delayed SWPT has competitive ratio exactly 2 for arbitrary positive weights, matching the lower bound.

Setting

An instance has jobs $j \in J = \{1,\dots,n\}$ with integer release dates $r_j \ge 0$, integer processing times $p_j \ge 1$ and real weights $w_j > 0$. A schedule assigns each job an integer start time $S_j$. It is feasible if $S_j \ge r_j$ for every $j$ and no two intervals $[S_j, S_j + p_j)$ overlap; idle time is allowed. Its cost is $C(S) = \sum_j w_j (S_j + p_j)$.

Delayed SWPT runs over unit time slots $[t, t+1)$. When the machine is available at time $t$, it looks at the jobs released by $t$ and not yet started, and selects one with the smallest ratio $p_j/w_j$. Ties go to the smaller $p_j$, then to the smaller index. If $p_j \le t$, it starts $j$ at $t$ and the machine is busy until $t + p_j$. Otherwise the machine stays idle and the rule is applied again at $t+1$. The resulting schedule is written $\pi$, or dswpt I in Lean. In particular no job starts before time $p_j$.

The proof uses three auxiliary problems:

• the doubled problem (2P), with data $(2r_j, 2p_j, w_j)$;
• the extended problem (E), with release dates $r'_j = \max\{p_j, f(r_j)\}$, where $f(t)$ is the first time at or after $t$ at which $\pi$ leaves the machine free;
• one unit-length gap job $g_t$ for each slot $[t,t+1)$ in which Delayed SWPT idles although a job $j$ is available. The gap job has release date $f(r_j)$ and weight $w_j/p_j$.

The schedule $\pi_E$ of (E) runs the original jobs as in $\pi$ and each $g_t$ in $[t,t+1)$.

Formalization targets

Goal: Theorem 8

$$\min\Bigl\{\rho \;:\; \sum_j w_j C_j(\pi) \le \rho \sum_j w_j C_j(S)\ \text{for every instance and every feasible schedule } S\Bigr\} = 2.$$

Lean: IsLeast {ρ | ∀ n I S, IsFeasible I.r I.p S → cost I.w I.p (dswpt I) ≤ ρ * cost I.w I.p S} 2. Both halves are required: the upper bound $2$ and the fact that no smaller constant is valid for this algorithm.

Milestones

1. $\pi_j \ge p_j$ for every job (§2) and $r'_j \le \max\{2r_j, p_j\}$ (§3.2).
2. $\pi_E$ is feasible for (E) (§3.2).
3. Lemma 1. If $\pi^*$ and $\mu^*$ are optimal for (P) and (2P), then $C(\mu^*) = 2\,C(\pi^*)$.
4. Lemma 2. $\pi_E$ is optimal for (E).
5. Lemma 3. If $\mu^*$ is optimal for (2P) and a feasible $\sigma_E$ for (E) satisfies

$$\sum_{j\in J} w_j C_j(\sigma_E) + \sum_{g\in G} w_g C_g(\sigma_E) \le \sum_{j\in J} w_j C_j(\mu^*) + \sum_{g\in G} w_g C_g(\pi_E), \tag{1}$$

then $C(\pi) \le 2\,C(S)$ for every feasible $S$. 6. Inequality (1) holds for some feasible $\sigma_E$, for every optimal $\mu^*$ of (2P) (§§3.4–3.6).

Significance

The theorem shows that a deterministic online algorithm can match the lower bound of Hoogeveen and Vestjens for arbitrary positive weights. This settles the best competitive ratio for deterministic online algorithms for $1\,|\,r_j\,|\,\sum w_j C_j$. The algorithm needs no linear program. The analysis also does not compare the algorithm with a lower bound on the optimum. Instead it shows that the online schedule is optimal for a modified problem (E), and it converts an optimal schedule of (2P) into a schedule of (E).

The result was proved on paper in 2004. Neither Mathlib nor the Prove2Me catalog contains a machine-checked proof of it, or of any competitive ratio for online scheduling with release dates. This mission provides several reusable pieces:

• an executable, verified-terminating definition of an online scheduling rule;
• the doubling lemma for release-date problems;
• the optimality criterion behind Lemma 2;
• the block-by-block exchange argument of §§3.3–3.6.

Difficulty

The obvious argument fails at Lemma 2. Delayed SWPT is far from optimal for (P) itself, and its idle time is unbounded in relative terms. The proof therefore has to show that the inserted gap jobs make every idle slot "justified", so that a preemptive best-available argument becomes valid for (E). That argument rests on an optimality criterion of Belouadah, Posner and Potts (1992), which is not in Mathlib.

The second difficulty is inequality (1). Once $\mu^*$ is doubled and the gap jobs are inserted, nongap jobs must be shifted, and the gain of each gap-generating job must be charged against the delay of the gap jobs in its block. That accounting (Lemmas 4–7 of the paper) is an induction over blocks with signed differences of completion times.

The natural first idea, plain online SWPT (start the available job with the smallest $p_j/w_j$ whenever the machine is free), has no finite competitive ratio (Example 1 of the paper), so the delay $\pi_j \ge p_j$ is essential to the bound and must be tracked through the whole argument.

Formalization scope

Conventions committed to in Lean:

• Data. Jobs are Fin n (0-based, so "smallest index" is the order of Fin n). Times are natural numbers, the paper's standing integer-data assumption (p. 688), and weights are real. Every instance carries $p_j \ge 1$ and $w_j > 0$.
• Schedules and optimality. Schedules are integer start times. Feasibility, cost and optimality are defined for any finite job type, so (E), with job type Fin n ⊕ gapTimes I, uses the same notions. "Optimal" means optimal among all feasible nonpreemptive schedules with integer start times.
• The algorithm. Delayed SWPT is a def: a unit-time simulation that compares ratios by cross-multiplication and re-applies the rule at every slot. It runs to the horizon $\sum_j (r_j + 2p_j) + 1$. A sorry-free check (not uploaded) shows that every job has started by then, and that the simulation reproduces Examples 3 and 4 of the paper, including the gap times $0,2,3,4,5,6$ of Table 2.
• Completion times. In (2P) the completion time is $\mu^*_j + 2p_j$, and gap jobs have unit length.

The goal quantifies over every feasible schedule of every instance. It cannot be met by restricting the competitor to schedules without idle time or to list schedules, by dropping release-date feasibility, or by leaving jobs unscheduled.

Out of scope:

• The general lower bound "no online algorithm beats 2" (Example 2 of the paper, due to Hoogeveen and Vestjens) is not part of the mission. The lower half of the goal concerns Delayed SWPT only.
• The Belouadah–Posner–Potts optimality criterion is an external ingredient of Lemma 2. Solvers may formalize it as a supporting theorem.

Infrastructure that a complete development needs:

• simulation invariants for the algorithm;
• exchange and left-shift arguments for single-machine schedules;
• the job-splitting relaxation behind the best-available criterion.

The schedule vocabulary and the criterion are reusable for other release-date scheduling results. Contributions toward the block lemmas of §§3.3–3.6 (Lemmas 4–7, the bound (9)) are welcome as supporting theorems.

Selected references

• E. J. Anderson and C. N. Potts, Online Scheduling of a Single Machine to Minimize Total Weighted Completion Time, Mathematics of Operations Research 29(3), 686–697, 2004. https://doi.org/10.1287/moor.1040.0092
• J. A. Hoogeveen and A. P. A. Vestjens, Optimal On-Line Algorithms for Single-Machine Scheduling, IPCO 1996, LNCS 1084, 404–414. https://doi.org/10.1007/3-540-61310-2_30
• L. A. Hall, A. S. Schulz, D. B. Shmoys and J. Wein, Scheduling to Minimize Average Completion Time: Off-line and On-line Approximation Algorithms, Mathematics of Operations Research 22(3), 513–544, 1997. https://doi.org/10.1287/moor.22.3.513
• C. Phillips, C. Stein and J. Wein, Minimizing Average Completion Time in the Presence of Release Dates, Mathematical Programming 82, 199–223, 1998. https://doi.org/10.1007/BF01585872
• M. X. Goemans, M. Queyranne, A. S. Schulz, M. Skutella and Y. Wang, Single Machine Scheduling with Release Dates, SIAM Journal on Discrete Mathematics 15(2), 165–192, 2002. https://doi.org/10.1137/S089548019936223X
• H. Belouadah, M. E. Posner and C. N. Potts, Scheduling with Release Dates on a Single Machine to Minimize Total Weighted Completion Time, Discrete Applied Mathematics 36(3), 213–231, 1992. https://doi.org/10.1016/0166-218X(92)90255-9
• J. K. Lenstra, A. H. G. Rinnooy Kan and P. Brucker, Complexity of Machine Scheduling Problems, Annals of Discrete Mathematics 1, 343–362, 1977. https://doi.org/10.1016/S0167-5060(08)70743-X
• W. E. Smith, Various Optimizers for Single-Stage Production, Naval Research Logistics Quarterly 3, 59–66, 1956. https://doi.org/10.1002/nav.3800030106

Motivation

The k-server problem (Manasse, McGeoch and Sleator, 1990) is the central problem of online computation: $k$ servers sit on points of a metric space, requests arrive one at a time at points of the space, and each request must be served by moving a server to it, at a cost equal to the distance travelled. An online algorithm decides without knowing future requests; its quality is its competitive ratio, the worst-case ratio between its cost and the cost of an optimal offline schedule. Paging (caching) is the special case of a uniform metric, and weighted paging the case of a weighted star.

Timeline of the upper bounds for general metrics:

• 1990: Manasse, McGeoch and Sleator prove that every deterministic algorithm has ratio at least $k$ and conjecture that $k$ is achievable.
• 1991: Fiat, Rabani and Ravid give the first ratio depending on $k$ only (exponential in $k$).
• 1995: Koutsoupias and Papadimitriou prove that the work function algorithm is $(2k-1)$-competitive.
• For randomized algorithms against an oblivious adversary, the conjectured answer is $O(\log k)$, achieved for paging (Fiat et al., 1991), but until 2011 nothing better than the deterministic $2k-1$ was known for general metrics, even when the ratio may depend on the number of points $n$.
• 2011: Bansal, Buchbinder, Mądry and Naor give the first polylogarithmic bound, $O(\log^2 k\log^3 n\log\log n)$ (arXiv:1110.1580; J. ACM 62(5), 2015, DOI 10.1145/2783434), the result of this mission.

Setting

Let $(M,\mathrm{dist})$ be a finite metric space with $n$ points and $k$ a number of servers. A configuration $C:\{1,\dots,k\}\to M$ places server $i$ at $C(i)$. A deterministic online algorithm maps each prefix of the request sequence to a configuration that has a server at the last request; its cost on a sequence $\rho$ is the total distance travelled. $\mathrm{OPT}(C_0,\rho)$ is the least cost of any schedule serving $\rho$ from the initial configuration $C_0$. A randomized algorithm is a probability distribution over deterministic online algorithms, all starting at $C_0$; it is $c$-competitive if there is a constant $a$ such that its expected cost on every request sequence $\rho$ is at most $c\cdot\mathrm{OPT}(C_0,\rho)+a$.

The paper works with three auxiliary objects. A σ-HST is a rooted tree whose leaves are the points, in which all edges from a node to its children have one common length, equal to $1/\sigma$ times the length of the edge above that node; the distance between two leaves is the length of the tree path. A weighted σ-HST only requires that the edge above a non-root internal node be at least $\sigma$ times each edge below it. In the fractional k-server problem on a tree, the state is a vector $x$ of server probabilities on the leaves with $0\le x_i\le1$ and $\sum_i x_i=k$, a request at leaf $i$ forces $x_i=1$, and moving from $x$ to $x'$ costs $\sum_v W(v)\,|x'_v-x_v|$, where $x_v$ is the mass below node $v$ and $W(v)$ the length of the edge above $v$. In the allocation problem on a weighted star with weights $w_i$, requests carry a location $i^t$, a monotone cost vector $h^t(0)\ge\dots\ge h^t(k)\ge0$ (the cost of serving with $j$ servers there) and a server quota $\kappa(t)\le k$.

Formalization targets

Goal: Theorem 1

There is a universal constant $C>0$ such that for all $k\ge2$, every metric space $M$ with $n\ge3$ points and every initial configuration $C_0$, some randomized online algorithm starting at $C_0$ is

$$C\,\log^2 k\,\log^3 n\,\log\log n\text{-competitive.}$$

Milestones

In the order the proof uses them:

1. Claim 15: the fix-stage inequality behind the allocation algorithm's analysis.
2. Theorem 5: for every $0<\varepsilon\le1$, a fractional allocation algorithm whose hit cost is at most $(1+\varepsilon)(\mathrm{Opt}+w_{\max}g(\kappa))+a$ and whose movement cost is at most $O(\log(k/\varepsilon))(\mathrm{Opt}+w_{\max}g(\kappa))+a$, where $g(\kappa)=\sum_t|\kappa(t)-\kappa(t-1)|$.
3. Theorem 6: given such allocation algorithms, an $O(\ell\log(k\ell))$-competitive fractional k-server algorithm on every weighted σ-HST of depth $\ell$ with $\sigma=\Omega(\ell\log(k\ell))$.
4. Theorem 8: every σ-HST with $n$ leaves becomes a weighted σ-HST of depth $O(\log n)$ on the same leaves, with distances distorted by at most $2\sigma/(\sigma-1)$.
5. Lemma 25 and Theorem 24: on a σ-HST with $\sigma>5$, randomized states consistent with a changing fractional state can be maintained online at cost $O(c_t)$ per step.
6. Theorem 7: on a σ-HST with $\sigma>5$, a $c$-competitive fractional algorithm yields an $O(c)$-competitive randomized one.

Significance

The theorem broke the exponential gap between the $\Omega(\log k)$ lower bound and the $2k-1$ upper bound for randomized k-server, and showed that randomization helps on every finite metric, not only on uniform or specially structured ones. Its two-level method (a fractional algorithm on trees driven by per-node allocation problems, followed by an online rounding) became the template for later work, including the $O(\log^2 k)$ bound on HSTs of Bubeck, Cohen, Lee, Lee and Mądry (STOC 2018) and Lee's $O(\log^6 k)$ bound on general metrics (FOCS 2018).

The result is proved, in this paper. As far as is known it has no machine-checked proof. Formalizing it means formalizing the analysis of an online algorithm driven by a continuous-time process, a potential-function argument with exact constants, a tree contraction with a distortion bound, and an online randomized rounding against a transportation cost. The allocation, HST and rounding statements are reusable for other online problems on trees (metrical task systems, weighted paging).

Difficulty

For a deterministic or randomized algorithm on a tree, the natural recursion splits the servers of each node among its children. Coté, Meyerson and Poplawski showed that this works if each node solves an allocation problem with a strong guarantee: hit cost within a factor $1+\varepsilon$ of optimal. Integral allocation algorithms cannot achieve this; the integrality gap example of the paper (p. 8) gives a factor $\Omega(k)$. The fractional relaxation avoids the gap, but then the rounding step must keep a randomized state consistent with a fractional state at constant-factor cost, and the HSTs obtained from general metrics have depth growing with the aspect ratio, which a depth-dependent ratio cannot afford. Each of the three reductions (allocation to fractional k-server, deep HST to shallow weighted HST, fractional to randomized) loses only polylogarithmic or constant factors, and the main theorem needs all three at once.

Formalization scope

The k-server model, randomized algorithms and competitiveness are the published definitions KServer_model and KServer_randomized; competitiveness carries an additive constant fixed before the request sequence. Trees are finite rooted trees with a parent map, a depth function and positive edge lengths; points of the k-server problem are the leaves, and the theorems take an arbitrary finite metric space together with a bijection to the leaves and the hypothesis that the distance equals the tree distance. Fractional k-server states have exactly $k$ units of mass, each leaf at most $1$, and fractional algorithms are measured against the integral offline optimum. The allocation optimum is the integral optimum; cost vectors are finite, non-negative and non-increasing; the diameter of the star is $w_{\max}=\max_i w_i$. The cost of changing a randomized state is the transportation cost over couplings, with minimum-matching cost between configurations. Every $O(\cdot)$ is an explicit constant quantified before the instance, except that in Theorems 7 and 24 and Lemma 25 it may depend on $\sigma$.

Formalizations that make the targets trivial are excluded: the fractional state must place a full server on every request and stay in $[0,1]$, the benchmark is the integral optimum (not the algorithm's own or the fractional cost), and no constant may depend on $k$, $n$, the metric or the tree, since otherwise Theorem 1 would follow from the $2k-1$ bound.

The proof of Theorem 1 also uses the embedding of Fakcharoenphol, Rao and Talwar [18] of a finite metric into a distribution over σ-HSTs with expected distortion $O(\sigma\log_\sigma n)$. It is an external ingredient, not a result of this paper, and is not a milestone; contributions formalizing it (or Bartal's earlier embedding) are welcome, as are formalizations of the integral optimum's properties on trees (Lemmas 21–22 of the paper), which are not stated here.

Selected references

• N. Bansal, N. Buchbinder, A. Mądry, J. Naor, A Polylogarithmic-Competitive Algorithm for the k-Server Problem, arXiv:1110.1580v1, 2011; J. ACM 62(5), 2015. https://arxiv.org/abs/1110.1580, https://doi.org/10.1145/2783434
• M. Manasse, L. McGeoch, D. Sleator, Competitive algorithms for server problems, J. Algorithms 11, 1990. https://doi.org/10.1016/0196-6774(90)90003-W
• E. Koutsoupias, C. Papadimitriou, On the k-server conjecture, J. ACM 42(5), 1995. https://doi.org/10.1145/210118.210128
• A. Fiat, R. Karp, M. Luby, L. McGeoch, D. Sleator, N. Young, Competitive paging algorithms, J. Algorithms 12, 1991. https://doi.org/10.1016/0196-6774(91)90041-V
• J. Fakcharoenphol, S. Rao, K. Talwar, A tight bound on approximating arbitrary metrics by tree metrics, J. Comput. Syst. Sci. 69(3), 2004. https://doi.org/10.1016/j.jcss.2004.04.011
• A. Coté, A. Meyerson, L. Poplawski, Randomized k-server on hierarchical binary trees, STOC 2008. https://doi.org/10.1145/1374376.1374474

Motivation

The multi-secretary problem is the simplest model of capacity allocation under uncertainty: a decision maker sees $n$ candidates one at a time and may hire at most $k$ of them, with every decision final. The same structure underlies single-resource revenue management (accepting or rejecting booking requests against a fixed inventory; see Talluri and van Ryzin, The Theory and Practice of Revenue Management, 2004), online knapsack and packing problems, and dynamic assortment of limited stock.

The performance of an online policy is measured against the offline benchmark, the value of the best $k$ candidates chosen with full hindsight. The gap between the two is the regret.

• In the version where the values arrive as a uniform random permutation, Kleinberg (2005) proved that the minimal regret is of order $\sqrt k$ and gave an algorithm attaining it (as summarized in Remark 1 of the paper below).
• Arlotto and Gurvich (arXiv:1710.07719, 2017; Stochastic Systems 2019) showed that when the values have a finite support, the optimal online policy, and an explicit simple policy, have regret bounded by a constant that does not depend on $n$ or $k$. The constant depends only on the smallest probability mass.

This mission formalizes that upper bound.

Setting

Abilities take values in a finite set $\mathcal A=\{a_m<a_{m-1}<\dots<a_1\}$ of distinct positive reals, with probabilities $f_j=\mathbb P(X=a_j)>0$, $\sum_j f_j=1$. Write $\bar F(a_j)=f_1+\dots+f_{j-1}$ for the mass strictly above $a_j$, and

$$\epsilon=\tfrac12\min\{f_m,\dots,f_1\}.$$

The abilities $X_1,\dots,X_n$ are independent with this distribution. Budget pairs range over the triangle $\mathcal T=\{(n,k):0\le k\le n\}$.

• Offline value. $V^*_{\mathrm{off}}(n,k)=\mathbb E\big[\max\{\sum_t X_t\sigma_t:\sigma\in\{0,1\}^n,\ \sum_t\sigma_t\le k\}\big]$.
• Online policies. A policy decides $\sigma_t\in\{0,1\}$ using only $X_1,\dots,X_t$ and must select at most $k$ candidates on every realization. $\Pi(n,k)$ is the set of such policies, $V^\pi_{\mathrm{on}}(n,k)=\mathbb E[\sum_t X_t\sigma^\pi_t]$, and $V^*_{\mathrm{on}}(n,k)=\max_{\pi\in\Pi(n,k)}V^\pi_{\mathrm{on}}(n,k)$.
• Counts. $Z^r_j$ is the number of $a_j$-candidates among the first $r$. The offline sort selects $\mathfrak S^r_j=\min\{Z^r_j,(k-\sum_{i<j}Z^r_i)_+\}$ of them. $S^{\pi,r}_j$ counts those selected by $\pi$.
• Action index. $j_0(n,k)$ is the largest $j$ with $\bar F(a_j)+\tfrac12f_j\le k/n$, or $1$ if there is none.
• Thresholds. $T_1=0$, $T_j=\bar F(a_j)+\tfrac12 f_j$ for $2\le j\le m$, and $T_{m+1}=+\infty$.
• Budget-Ratio (BR) policy. With remaining budget $K_t$ ($K_0=k$), at time $t+1$ the policy finds $j$ with $T_j\le K_t/(n-t)<T_{j+1}$. It selects $X_{t+1}$ if and only if $K_t>0$ and $X_{t+1}\ge a_j$.
• Stopping times. For $0<\delta<\epsilon$, $\tau_0$ is the first time the budget ratio comes within $\delta/2$ of a threshold, or the cut-off $n-2\delta^{-1}-1$. The time $\tau$ of (20) is the first later time the ratio leaves the $\delta$-band around that threshold, or the cut-off.

Formalization targets

Goal: Theorem 1 (first display)

For every $\epsilon>0$ there is a constant $M$ such that for every instance with $\tfrac12\min_jf_j=\epsilon$ and all $(n,k)\in\mathcal T$, $\mathrm{br}\in\Pi(n,k)$ and

$$V^*_{\mathrm{off}}(n,k)-V^*_{\mathrm{on}}(n,k)\le V^*_{\mathrm{off}}(n,k)-V^{\mathrm{br}}_{\mathrm{on}}(n,k)\le a_1M.$$

No constant is fixed. Only the shape is asserted: a bound uniform in $n$, $k$, the support size and the distribution, given $\epsilon$.

Milestones, in the order the proof uses them

• The benchmark inequality $V^\pi_{\mathrm{on}}\le V^*_{\mathrm{off}}$ (p. 5).
• The sort identity $V^*_{\mathrm{off}}=\sum_ja_j\mathbb E[\mathfrak S^n_j]$ (4).
• The binomial overshoot bound $\mathbb E[(B-k)_+]\le1/(4\varepsilon)$ (Lemma 2).
• The offline decomposition $V^*_{\mathrm{off}}=\sum_{i<j}a_i\mathbb E[Z^n_i]+a_j\mathbb E[\mathfrak S^n_j]+a_{j+1}\mathbb E[\mathfrak S^n_{j+1}]\pm a_1/(4\epsilon)$ (Proposition 1).
• The sufficient condition: four properties (i)–(iv) of a policy up to a stopping time imply regret at most $3a_1M+a_1/(4\epsilon)$ (Proposition 2).
• The identification $j_0(n,k)=j$ on $k/n\in[T_j,T_{j+1})$ (p. 17).
• The BR selection probability and the jump bound $|K_t/(n-t)-K_{t+1}/(n-t-1)|\le\delta/2$ (p. 13).
• $\mathbb E[\tau]\ge n-M$ (Theorem 2).
• BR and $\tau$ satisfy (i)–(iv) (Corollary 1).
• The state-space reduction $v_\ell(w,\kappa)=w+g_\ell(\kappa)$ of the Bellman recursion (Proposition 5).

Significance

The result. Bounded regret means that the loss from not knowing the future is a fixed number of candidates' worth of value, however long the horizon and however large the budget. The bound holds uniformly over all distributions with the same $\epsilon$. It is attained by an explicit, adaptive, non-randomized rule that compares one ratio with $m$ fixed thresholds. The companion result of the same paper shows that every non-adaptive policy suffers regret of order $\sqrt n$ in the interior regime. Together they quantify the value of adapting to the remaining budget. Lemma 1 of the paper shows the dependence on $\epsilon$ cannot be removed.

Formalizing it. The result is proved in the paper, but no part of it is machine-checked; there is no multi-secretary or bounded-regret development on the platform. The mission produces several pieces of machinery: a reusable finite model of sequential selection with online policies and the offline benchmark; an explicit online policy with its stopping-time analysis; and a binomial overshoot bound usable elsewhere. The constant $M$ is not made explicit in the paper. A formal proof would give one, and sharper constants are welcome.

Difficulty

The offline decomposition and the sufficient condition are bookkeeping with counts and one concentration bound. The hard step is Theorem 2: showing that the budget ratio $K_t/(n-t)$ stays within $\delta$ of its attracting threshold until a bounded expected number of periods before the end. Near the horizon a single selection moves the ratio by about $1/(n-t)$, so the band becomes easy to leave. Equivalently, the target $\delta(n-\tau_0-u)$ that the deviation process must exceed shrinks to zero. A standard martingale or drift argument with a fixed band therefore does not give a bound uniform in $n$. The paper combines the mean-reverting drift of the deviation process with an exponential tail bound (its Proposition 4) and a Lyapunov argument. A second subtlety is uniformity: every constant must depend on $\epsilon$ (and $\delta$) only, never on $m$, the $a_j$, $n$ or $k$.

Formalization scope

The source is arXiv:1710.07719v2; its printed page numbers equal the PDF page numbers.

Representation.

• Ability levels are Fin m, with index 0 the largest value $a_1$; Lean index $i$ is the paper's $i+1$.
• Each instance carries $a$ strictly decreasing and positive, $f$ positive with $\sum f=1$.
• Expectations are finite sums over sequences $x:\mathrm{Fin}\,n\to\mathrm{Fin}\,m$ weighted by $\prod_tf(x_t)$, so no measure theory is needed.
• Policies are deterministic selection rules $\sigma(x,t)$ that are non-anticipating and feasible. $V^*_{\mathrm{on}}$ is a maximum over this finite set. The paper allows randomized policies; for this finite problem the optimal values coincide (p. 39). In any case, restricting to deterministic policies can only lower $V^*_{\mathrm{on}}$ and so does not weaken the goal.
• $V^*_{\mathrm{off}}$ is defined as an expected maximum over selection vectors, not by the sort formula. The sort formula is a milestone.

Quantifiers. The constant $M$ in the goal is chosen after $\epsilon$ and before $m$, the instance, $n$ and $k$. A statement with $M$ chosen after the instance, or after $n$, is trivial (regret $\le a_1n$) and is excluded.

Corrections to the printed text, disclosed in the items.

1. In Theorem 2 and Corollary 1, $M$ depends on the auxiliary $\delta\in(0,\epsilon)$ as well, because $\tau$ does. $\delta$ is quantified before $M$. The goal itself is $\delta$-free.
2. Lemma 2's conditions $p+\varepsilon\le k/n$, $k/n\le p-\varepsilon$ are stated as $(p+\varepsilon)n\le k$, $k\le(p-\varepsilon)n$, the form used in its proof. This avoids a false case at $n=0$.
3. The BR rule is applied at every time $t+1\in\{1,\dots,n\}$; p. 11 writes $\{1,\dots,n-1\}$.
4. $\tau$ is capped at $n$, which matters only when $n=0$.
5. In Proposition 5 the recursions are imposed for $\kappa\ge1$ (boundary conditions at $\kappa=0$), and only identity (49) is stated.

Infrastructure. The model definitions (instance, offline value, online policies, counts, thresholds, action index) and the binomial overshoot lemma are reusable for other finite-support online selection and revenue-management results. All of the following are welcome:

• proofs of individual milestones;
• an explicit constant;
• a formal derivation of $V^*_{\mathrm{on}}(n,k)=v_n(0,k)$ connecting Proposition 5 to $V^*_{\mathrm{on}}$.

Selected references

• A. Arlotto, I. Gurvich, Uniformly Bounded Regret in the Multi-Secretary Problem, arXiv:1710.07719v2, 2018; Stochastic Systems 9(3), 2019. https://arxiv.org/abs/1710.07719
• R. Kleinberg, A multiple-choice secretary algorithm with applications to online auctions, SODA 2005. https://dl.acm.org/doi/10.5555/1070432.1070519
• K. T. Talluri, G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000
• D. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978.
• S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities, Oxford University Press, 2013. https://doi.org/10.1093/acprof:oso/9780199535255.001.0001