Online Algorithms

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

Motivation

In the classical secretary problem a decision maker sees $n$ candidates in uniformly random order, learns each candidate's value on arrival, and must accept or reject it on the spot; the goal is to pick a valuable one. A simple sample-then-select rule picks the best candidate with probability at least $1/e$, so the problem is constant-competitive. The secretary problem is also a model of online mechanism design: a rule that accepts the first agent above a threshold computed from earlier agents is a truthful posted-price mechanism (as the paper notes in §1).

Babaioff, Dinitz, Gupta, Immorlica and Talwar (SODA 2009; authors' version) study the discounted secretary problem, where accepting at time $t$ is worth $d(t)\,v(e)$ for a known discount function $d$. Discounts model settings where a sale is worth more at some times than at others. The case $d(t)=\beta^t$ had been studied before (Rasmussen and Pliska 1976); the paper asks what happens for arbitrary $d$. Its answer has two sides: an $O(\log n)$-competitive algorithm, and the result of this mission, a lower bound showing that no online algorithm is better than $\Omega(\log n/\log\log n)$-competitive. So, unlike the classical problem, the discounted problem with a general discount is not constant-competitive.

Setting

There are $n$ elements $e\in\{0,\dots,n-1\}$ with values $v(e)\ge 0$, and a discount function $d$ on the times. The elements arrive in a uniformly random order $\pi$: element $\pi(t)$ arrives at time $t$. A randomized online stopping rule $A$ specifies, for each time $t$ and each sequence of values seen so far $h=(v(\pi(0)),\dots,v(\pi(t)))$, a probability $p_t(h)\in[0,1]$ of stopping at $t$ if it has not stopped yet. Stopping at $t$ selects $\pi(t)$ and earns $d(t)\,v(\pi(t))$; the rule selects at most one element and may select none. The rule knows $n$ and $d$, but it sees only values, only as they arrive, and it is not told which instance it is facing.

The expected value of $A$ is

$$\mathbb E[A]=\mathbb E_\pi\Bigl[\sum_t d(t)\,v(\pi(t))\,p_t(h_t)\prod_{s<t}\bigl(1-p_s(h_s)\bigr)\Bigr],$$

and the benchmark is the expected offline optimum

$$\mathbb E[\mathrm{OPT}]=\mathbb E_\pi\Bigl[\max_t d(t)\,v(\pi(t))\Bigr],$$

which is itself a random variable averaged over the order. $A$ is $\alpha$-competitive on an instance when $\mathbb E[\mathrm{OPT}]\le\alpha\,\mathbb E[A]$.

The hard family (§4.1.1 of the paper): fix an integer $c\ge1$ and put $L=c$, $n=L^{4c}$, $n_t=L^{2t}$ for $t\le 2c$, and $K=n^2$. The step discount is $d(j)=L^{-1}$ on the times $1\le j\le n_1$ and $d(j)=L^{-t}$ on $n_{t-1}<j\le n_t$. The instance $\mathcal I_1$ has $n/n_1$ elements of value $K$ and the rest $0$; $\mathcal I_{t+1}$ is obtained from $\mathcal I_t$ by raising $n/n_{t+1}$ of its values $K^t$ to $K^{t+1}$, so $\mathcal I_t$ has $n/n_t$ elements of value $K^t$.

Formalization targets

Goal: Theorem 4.3 in the form its proof establishes

For every integer $c\ge1$ and every randomized online stopping rule $A$ for horizon $n=c^{4c}$ and the step discount,

$$\exists\,t\in\{1,\dots,2c\}:\qquad c\cdot\mathbb E[A(\mathcal I_t)]\ <\ 10\cdot\mathbb E[\mathrm{OPT}(\mathcal I_t)].$$

That is, no online rule is $c/10$-competitive on all of $\mathcal I_1,\dots,\mathcal I_{2c}$.

Milestones

1. Lemma 4.1: $\mathbb E[\mathrm{OPT}(\mathcal I_t)]\ge(1-1/e)K^tL^{-t}$ for $1\le t\le 2c$.
2. Coupling step of Lemma 4.2's proof: for every rule and $1\le t<2c$, the probability of stopping among the first $n_t$ arrivals drops by at most $1/L^2$ from $\mathcal I_t$ to $\mathcal I_{t+1}$.
3. Lemma 4.2: a rule that is $c/10$-competitive on $\mathcal I_1,\dots,\mathcal I_{2c}$ stops among the first $n_t$ arrivals of $\mathcal I_t$ with probability at least $t/c$.
4. Theorem 4.3, asymptotic form: for $c\ge2$ and $n=c^{4c}$, every rule has some $\mathcal I_t$ with

$$\frac1{40}\cdot\frac{\log n}{\log\log n}\cdot\mathbb E[A(\mathcal I_t)]<\mathbb E[\mathrm{OPT}(\mathcal I_t)].$$

Significance

The result separates the discounted secretary problem from its classical and weighted relatives, which admit constant-competitive algorithms (the paper's Theorem 3.4 and the $e$-competitive classical rule). Together with the paper's $O(\log n)$ upper bound (Theorem 4.4) it pins the competitive ratio for general discounts between $\log n/\log\log n$ and $\log n$ up to constants, and it motivates the paper's known-$\mathrm{OPT}$ model (§4.2), where an estimate of $\mathbb E[\mathrm{OPT}]$ restores a constant ratio. The construction is a template for lower bounds against randomized online algorithms in random-order models: geometrically nested instances that a rule cannot tell apart early, played against a discount that punishes waiting.

The theorem is proved in the paper, in about a page. To our knowledge no part of it has a machine-checked proof. This mission produces the formal model of randomized online stopping rules in the random-order discounted setting, a reusable object for the paper's other discounted results (the $O(\log n)$ upper bound, and the $\sqrt2$ lower bound with known values of Theorem 4.6), and a checked version of the lower bound with explicit constants.

Difficulty

The obvious attempt is to fix one instance and show that every rule loses on it. That fails: for any single instance there is a rule tuned to it (a rule that waits exactly as long as that instance warrants). The lower bound has to play the $2c$ instances against each other. A rule that does well on $\mathcal I_t$ must commit early, within the first $n_t$ steps, yet the rule cannot distinguish $\mathcal I_t$ from $\mathcal I_{t+1}$ during those steps except with probability $L^{-2}$. Making "cannot distinguish" precise is the central step: it needs a coupling of the two runs over the same random order and the same internal randomness, which works only because the rule's decision at time $t$ depends on the values observed so far and nothing else. The accounting then has to show that the rule's early earnings on $\mathcal I_{t+1}$ and its late earnings are both small compared with $\mathbb E[\mathrm{OPT}(\mathcal I_{t+1})]$, which uses $L\ge 2$ and that $K=n^2$ dwarfs $L^{2c}$.

Formalization scope

• Elements and times are Fin n, 0-based: index $j$ is the paper's time $j+1$, so the paper's block $(n_{t-1},n_t]$ is the index range $[n_{t-1},n_t)$. The random order is π : Equiv.Perm (Fin n) read as time $\mapsto$ element, and every expectation over it is the finite average $\frac1{n!}\sum_\pi$. Values and discounts are real.
• Algorithms are the structure StoppingRule n: stopping probabilities $p_t(h)\in[0,1]$ indexed by time and the arrival-ordered value sequence, with the non-anticipation condition that $p_t(h)$ depends only on $h_0,\dots,h_t$. The theorem quantifies over all such rules, so it covers deterministic and randomized online algorithms that observe values only. A rule may depend on $n$ and $d$ but not on the instance index.
• OPT is $\mathbb E_\pi[\max_t d(t)v(\pi(t))]$ (a supremum over the finite type Fin n), and competitiveness is multiplicative, $\mathbb E[\mathrm{OPT}]\le\alpha\,\mathbb E[A]$, never a quotient.
• Constants. The goal uses the paper's constant $10$ (from "if $A$ is $c/10$-competitive"); the asymptotic form uses $1/40$, from $\log n/\log\log n\le 4c$ for $c\ge2$, with the natural logarithm. $K=n^2$, the value the paper suggests.
• The construction ($n$, $n_t$, $d$, $K$, $\mathcal I_t$) is fixed by explicit formulas in the definition file. A solver cannot choose the discount or the instances, and the goal is not stated for a restricted class of algorithms; a formalization that let the rule see the instance index or future values, or quantified only over threshold rules, would be a different and trivial or weaker theorem. For $c<10$ the goal is immediate, since $\mathbb E[A]\le\mathbb E[\mathrm{OPT}]$ and $\mathbb E[\mathrm{OPT}(\mathcal I_t)]>0$; the content lies in $c\ge10$. The bound is stated only for the horizons $n=c^{4c}$ the paper constructs.
• Needed infrastructure: counting arguments over permutations of Fin n (the probability that a set of $m$ elements misses the first $k$ positions), the coupling of two value sequences that agree on a prefix, and elementary estimates on geometric sums. The rule model and the permutation-counting lemmas are reusable for the paper's other discounted results. Contributions of these supporting lemmas, as well as proofs of the milestones, are welcome.

Selected references

• M. Babaioff, M. Dinitz, A. Gupta, N. Immorlica, K. Talwar, Secretary Problems: Weights and Discounts, Proceedings of the 20th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2009. https://doi.org/10.1137/1.9781611973068.135 (authors' full version, the one cited here: https://www.cs.jhu.edu/~mdinitz/papers/secretary.pdf)
• E. B. Dynkin, Optimal choice of the stopping moment of a Markov process, Doklady Akademii Nauk SSSR, 1963.
• W. T. Rasmussen, S. R. Pliska, Choosing the maximum from a sequence with a discount function, Applied Mathematics and Optimization 2(3), 1976.
• T. S. Ferguson, Who solved the secretary problem?, Statistical Science 4(3), 1989. https://doi.org/10.1214/ss/1177012493

Motivation

In the classical secretary problem a decision maker sees $n$ candidates in a uniformly random order and must accept or reject each one on arrival, irrevocably, aiming to accept a valuable one. Its online, random-order structure models hiring, selling an item to sequentially arriving buyers, and posting prices in online markets. Babaioff, Dinitz, Gupta, Immorlica and Talwar (SODA 2009) study the discounted secretary problem, where the reward of a selection depends on when it is made: a candidate accepted late is worth less (or more) by a time-dependent factor, as with a seller whose revenue decays with time, or a firm that loses value the longer a position stays empty.

Timeline of the setting:

• Dynkin (1963) introduced the classical problem; the rule "observe a $1/e$ fraction, then accept the first record" selects the best candidate with probability tending to $1/e$.
• Rasmussen and Pliska (1975/76) and Mahdian, McAfee and Pennock (2008, personal communication cited by the paper) studied secretary problems with specific "well-behaved" discount functions such as $d(t)=\beta^t$.
• Babaioff et al. (2009) treat an arbitrary discount function $d$. Without prior knowledge, no algorithm is better than $\Omega(\log n/\log\log n)$-competitive (their Theorem 4.3), and $O(\log n)$ is achievable (Theorem 4.4). If the algorithm knows a good estimate $Z$ of the expected offline optimum, a single threshold rule recovers a constant fraction (Theorem 4.7, headlined as Theorem 1.2). This mission formalizes that last result.

Setting

There are $n\ge1$ elements, indexed by $\mathrm{Fin}\,n$. Element $e$ has a value $v(e)\ge0$, and each time $t\in\{1,\dots,n\}$ has a discount $d(t)\ge0$. The elements arrive in a uniformly random order $\pi$, a bijection from times to elements: element $\pi(t)$ arrives at time $t$. Selecting the element that arrives at time $i$ earns $d(i)\,v(\pi(i))$, and an algorithm selects at most one element.

The offline optimum on the order $\pi$ is $\mathrm{OPT}(\pi)=\max_{i=1}^n d(i)\,v(\pi(i))$. It is a random variable, and the benchmark is its expectation

$$\mathbf E[\mathrm{OPT}]=\sum_{\pi\in S_n}\frac1{n!}\max_{i=1}^n\{d(i)\,v(\pi(i))\}.$$

For a real parameter $Z$, algorithm $\mathcal A$ selects the first time $j$ at which $d(j)\,v(\pi(j))\ge Z/2$ and earns that product; if no time qualifies, it selects nothing and earns $0$. It knows $Z$ and $d$, sees the values one at a time, and never sees the future of $\pi$. Its expected value is $\mathbf E[\mathcal A]=\sum_{\pi\in S_n}\frac1{n!}\,\mathcal A(\pi)$.

The proof uses three derived objects:

• the accepting permutations $S_{acc}=\{\pi:\max_i d(i)v(\pi(i))\ge Z/2\}$, on which $\mathcal A$ selects something;
• their contribution $L=\sum_{\pi\in S_{acc}}\frac1{n!}\max_i d(i)v(\pi(i))$ to $\mathbf E[\mathrm{OPT}]$;
• for a time $i$ and an element $j$, the set $G_{ij}$ of orders on which $\mathcal A$ selects $j$ at time $i$. These are the orders with $\pi(i)=j$ and $d(k)v(\pi(k))<Z/2$ for every $k<i$.

Formalization targets

Goal: Theorem 4.7

For every $n\ge1$, all discounts $d\ge0$, all values $v\ge0$ and every real $Z$,

$$Z\le\mathbf E[\mathrm{OPT}]\ \Longrightarrow\ \mathbf E[\mathcal A]\ \ge\ \frac Z4.$$

Taking $Z=\mathbf E[\mathrm{OPT}]$ gives $\mathbf E[\mathrm{OPT}]\le4\,\mathbf E[\mathcal A]$, a $4$-competitive algorithm when the expected optimum is known.

Milestones (in the order of the paper's proof, p. 8)

1. Eq. (4.1). If $Z\le\mathbf E[\mathrm{OPT}]$ then $L\ge Z/2$.
2. Eq. (4.3). If $Z\le\mathbf E[\mathrm{OPT}]$ then

$$\sum_{i=1}^n\sum_{j:\,d(i)v(j)\ge Z/2}\frac1n\,d(i)v(j)\ \ge\ \frac Z2.$$

3. Eq. (4.4). $\displaystyle\mathbf E[\mathcal A]=\sum_{i=1}^n\sum_{j:\,d(i)v(j)\ge Z/2}d(i)v(j)\,\frac{|G_{ij}|}{|S_n|}$.
4. Claim 4.8. For every $i,j$ with $d(i)v(j)\ge Z/2$, $n|G_{ij}|\ge|S_n\setminus S_{acc}|$; and if $2|S_{acc}|\le n!$ then $2n|G_{ij}|\ge n!$.

Significance

The result. The discounted problem separates sharply by information: a logarithmic gap is unavoidable without prior knowledge, while knowledge of the single number $\mathbf E[\mathrm{OPT}]$, or of any lower estimate $Z$ of it, closes the gap to a constant. The algorithm is a fixed posted threshold, so read as a mechanism it is a posted price, which is truthful for single-parameter agents (§1). The paper also notes that when all values are known, $\mathbf E[\mathrm{OPT}]$ can be estimated by sampling (its Lemma A.1), which yields a constant-competitive algorithm in that setting. The companion lower bound (Theorem 4.6) shows that even complete knowledge of the values does not give a ratio better than $\sqrt2$.

Formalizing it. The result is proved on paper; no machine-checked proof is known. The formalization yields a checked version of the paper's counting argument on permutations (Claim 4.8) and of the tie-breaking step behind Eq. (4.3), and reusable finite random-order bookkeeping: expectations over $S_n$ as averages, threshold stopping rules, and the decomposition of an online algorithm's value by the time and element it selects.

Difficulty

The obvious argument fails when $\mathcal A$ rarely selects. $\mathcal A$ earns at least $Z/2$ whenever it selects anything, so $\mathbf E[\mathcal A]\ge\frac Z2\Pr[\mathcal A\text{ selects}]$. That settles the case $\Pr[\mathcal A\text{ selects}]\ge1/2$ and nothing else: the probability of selecting can be tiny while $\mathbf E[\mathrm{OPT}]$ is still large, because the optimum may be concentrated on a few orders with a large product. In that case the bound must come from comparing the algorithm with the optimum pair by pair: every time–element pair $(i,j)$ with $d(i)v(j)\ge Z/2$ must be realized by $\mathcal A$ on a positive fraction of the orders.

Two points need care in a formal proof:

• Eq. (4.2) rewrites $L$ as a sum over pairs weighted by the conditional probability that $d(i)v(j)$ is the highest product. It relies on a consistent tie-breaking rule, which the paper leaves implicit.
• Claim 4.8 is a counting argument on $S_n$. A map from the rejecting orders into $G_{ij}$ swaps element $j$ into position $i$, and must be shown to be at most $n$-to-$1$ and to land in $G_{ij}$.

Neither (4.2) nor the map appears in the statements, so solvers may replace either with any argument they like.

Formalization scope

• Types. Times and elements are Fin n; the paper's time $t$ is the index $t-1$. An order is π : Equiv.Perm (Fin n), read as time ↦ element, as on p. 3. The instance [NeZero n] encodes $n\ge1$, so the maximum over times is a genuine maximum (Finset.sup').
• Expectations. Expectations over the uniform order are finite averages $\frac1{n!}\sum_\pi$. No measure theory is used.
• Values and constants. Values, discounts and $Z$ are real numbers, and the hypotheses $d\ge0$, $v\ge0$ are explicit. The constant $1/4$ is the paper's. The bound is stated multiplicatively, $Z/4\le\mathbf E[\mathcal A]$, never as a ratio.
• Thresholds and ties. Every threshold is non-strict ($\ge Z/2$), exactly as on pp. 7–8. $\mathcal A$ selects the first qualifying time, so it needs no tie-breaking. The tie-breaking remark at Eq. (4.2) concerns only the paper's intermediate identity (4.2), which is not a milestone.
• Claim 4.8. Both inequalities are stated with cleared denominators. The second carries the proof's case hypothesis $2|S_{acc}|\le n!$, which the paper uses in the same place ("at most half the permutations are in $S_{acc}$").
• What is not this theorem. $\mathcal A$ is the online threshold rule with threshold $Z/2$ applied to $\pi$ as it unfolds. An algorithm that inspects the whole order, or that chooses its threshold after seeing the values, would make the bound trivial and is not this theorem.
• Contributions welcome. Proofs of each milestone, including the counting argument of Claim 4.8. Lemmas on averages over Equiv.Perm (Fin n) and on first-hitting times are reusable beyond this mission.

Selected references

• M. Babaioff, M. Dinitz, A. Gupta, N. Immorlica, K. Talwar, Secretary Problems: Weights and Discounts, Proceedings of the 20th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2009.
• E. B. Dynkin, Optimal choice of the stopping moment of a Markov process, Doklady Akademii Nauk SSSR 150:238–240, 1963.
• W. T. Rasmussen, S. R. Pliska, Choosing the maximum from a sequence with a discount function, Applied Mathematics and Optimization 2(3):279–289, 1975/76.
• M. Mahdian, P. McAfee, D. Pennock, The secretary problem with durable employment, personal communication, 2008 (cited as [MMP08]).
• M. Babaioff, N. Immorlica, R. Kleinberg, Matroids, secretary problems, and online mechanisms, SODA 2007, pp. 434–443.

Motivation

In the secretary problem, $n$ candidates with arbitrary values arrive one at a time in a uniformly random order, and an online decision maker must accept or reject each candidate on arrival, irrevocably, keeping at most one. The rule that observes the first $n/e$ candidates and then accepts the first one better than everything seen so far selects the best candidate with probability about $1/e$ (Dynkin, 1963). The problem is a basic model of online selection and, read economically, of posted-price mechanisms for agents who arrive in random order: a rule that compares each agent only against a threshold set by earlier agents is truthful.

Babaioff, Dinitz, Gupta, Immorlica and Talwar (SODA 2009) study a variant in which time costs value. Selecting the candidate who arrives at time $t$ earns that candidate's value multiplied by a discount $d(t)$, for an arbitrary non-negative discount function $d$ known in advance. Earlier work treated only specific discount shapes, such as geometric discounting $d(t)=\beta^t$ (Rasmussen and Pliska, 1976). For a general $d$ the classical rule can fail badly: if all the discount mass sits in the first few time steps, a rule that waits through a sample of size $n/e$ earns nothing. The paper shows that the best competitive ratio for arbitrary discounts lies between $\Omega(\log n/\log\log n)$ (its Theorem 4.3) and $O(\log n)$ (its Theorem 4.4). This mission formalizes the upper bound.

Setting

There are $n\ge1$ elements, indexed $\{0,\dots,n-1\}$, with values $v(e)\ge 0$, and $n$ times with discounts $d(t)\ge0$. A uniformly random permutation $\pi$ fixes the order of arrivals: element $\pi(t)$ arrives at time $t$. An algorithm knows $d$ but not $v$; it sees each value on arrival and may select the current element, irrevocably, earning $d(t)\,v(\pi(t))$. Expectations over $\pi$ are exact averages over the $n!$ orders.

The offline optimum on order $\pi$ is $\mathsf{OPT}(\pi)=\max_t d(t)\,v(\pi(t))$; it is a random variable, and the benchmark is its expectation $\mathbb E_\pi[\mathsf{OPT}]$ (p. 4 of the paper).

Let $d_{\max}=\max_t d(t)$ and $v_{\max}=\max_e v(e)$. For $c\ge1$ the $c$-th discount class is the set of times

$$P_c=\{\,i : 2^{-c}d_{\max}<d(i)\le 2^{-(c-1)}d_{\max}\,\}.$$

The quantity $\mathsf{OPT}_c$ is the part of $\mathbb E_\pi[\mathsf{OPT}]$ earned when the optimal time (the smallest time attaining the maximum) lies in $P_c$.

The classical secretary rule on $m$ arrivals observes the first $\lfloor m/e\rfloor$ and then selects the first arrival that ranks above every earlier arrival. Ranks use a fixed tie-break order: larger value first, and smaller element index among equal values.

The algorithm $\mathcal A$ sets $M=3\lceil\log_2 n\rceil+2$, draws $c\in\{1,\dots,M\}$ uniformly, and runs the classical rule on the subsequence of arrivals at the times of $P_c$, ignoring all other arrivals.

Formalization targets

Goal: Theorem 4.4 with its explicit constant

$$\mathbb E_\pi[\mathsf{OPT}]\;\le\;4e\,\bigl(3\lceil\log_2 n\rceil+2\bigr)\;\mathbb E[\mathcal A]\qquad(n\ge1,\ d\ge0,\ v\ge0).$$

The paper states $\mathbb E[\mathsf{OPT}]/\mathbb E[\mathcal A]\le O(\log n)$; the constant $4e$ is the one its proof yields.

Milestones

1. The classical secretary rule selects the top-ranked of $m\ge1$ elements with probability at least $1/e$ (§2, p. 4).
2. $\mathsf{OPT}_1\ge v_{\max}d_{\max}/n$ (proof of Theorem 4.4, p. 7).
3. $\mathsf{OPT}_c\le 2^{-c}\,2n^2d_{\max}v_{\max}$ for every $c\ge1$ (p. 7).
4. $\sum_{c=1}^{3\lceil\log_2 n\rceil+1}\mathsf{OPT}_c\ge\tfrac12\mathbb E_\pi[\mathsf{OPT}]$ (p. 7).
5. $\mathbb E[\mathcal A_c]\ge\mathsf{OPT}_c/2e$ for every $c\ge1$, where $\mathcal A_c$ is the classical rule on $P_c$ (p. 7).

Significance

The theorem shows that a general discount function costs only a logarithmic factor against the offline benchmark, and that one algorithm achieves this without any knowledge of the values. Together with the lower bound of Theorem 4.3 it pins the competitive ratio of the discounted secretary problem between $\log n/\log\log n$ and $\log n$. The same scale-splitting idea, stated in the paper as Theorem 4.5 without full proof, extends the bound to the weighted discounted problem.

The result is proved in the paper; to our knowledge it has not been formalized. A complete development would also produce a machine-checked proof of the classical secretary guarantee for the rule with sample size exactly $\lfloor m/e\rfloor$ at every finite $m$, with an explicit tie-break, which is reusable by every secretary-type mission. Milestone 1 is that statement. Sharper constants or a smaller class range are welcome as additional statements but do not replace the goal, which is about this algorithm with this $M$.

Difficulty

The obvious argument, running the classical rule on all $n$ arrivals, fails because the discounts can be concentrated at times the rule spends sampling. Splitting by discount scale fixes this but creates two problems. First, there are unboundedly many scales, and one has to show that the offline optimum's mass outside the top $O(\log n)$ of them is negligible against $\mathbb E[\mathsf{OPT}]$, a random quantity rather than a fixed maximum. Second, the classical rule on a class sees only a random subset of the elements, in random order, and the guarantee must be transferred to this subsequence, conditioning on which elements land in $P_c$. Neither step is deep, but both require careful bookkeeping of permutations, and the classical $1/e$ bound at finite $m$ with a floor in the sample size is itself a nontrivial estimate.

Formalization scope

Elements and times are Fin n, an order is π : Equiv.Perm (Fin n) read as time $\mapsto$ element, and the paper's time $t=1,\dots,n$ is index $t-1$. Values and discounts are Fin n → ℝ with non-negativity hypotheses. Every expectation is the finite average $\frac1{n!}\sum_\pi$; the algorithm's random class is the explicit average $\frac1M\sum_{c=1}^M$. Maxima are suprema over the finite index set. The logarithm is base 2, $\lceil\log_2 n\rceil$ is Nat.clog 2 n, and the sample size is Nat.floor (m / Real.exp 1). Ties are broken by the order on Lex (ℝ × (Fin n)ᵒᵈ) (larger value, then smaller index); distinct values are not assumed. The optimal time is the smallest maximizing time, so that the $\mathsf{OPT}_c$ add up to $\mathbb E[\mathsf{OPT}]$. Competitiveness is stated multiplicatively, never as a quotient, so $\mathbb E[\mathcal A]=0$ is not a loophole.

The goal is a statement about the specific algorithm $\mathcal A$, not "there exists an algorithm": an existential over unrestricted algorithms is witnessed by a clairvoyant rule that reads the values in advance. $\mathcal A$ sees the values only through comparisons among arrivals that have already occurred, and $\mathbb E[\mathsf{OPT}]$ is the expected offline maximum over the same random order, not $d_{\max}v_{\max}$.

Needed infrastructure: averages over permutations and the fact that the elements landing at a fixed set of times form a uniformly random subset in uniformly random order; the finite-$m$ analysis of the classical rule; and elementary estimates on geometric sums. Contributions of general lemmas about uniform permutations are welcome and reusable.

Selected references

• M. Babaioff, M. Dinitz, A. Gupta, N. Immorlica, K. Talwar, Secretary Problems: Weights and Discounts, Proc. 20th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2009. https://doi.org/10.1137/1.9781611973068.139
• E. B. Dynkin, The optimum choice of the instant for stopping a Markov process, Soviet Math. Doklady 4, 1963.
• T. S. Ferguson, Who solved the secretary problem?, Statistical Science 4(3), 1989. https://doi.org/10.1214/ss/1177012493
• L. T. Rasmussen, S. R. Pliska, Choosing the maximum from a sequence with a discount function, Applied Mathematics and Optimization 2, 1976. https://doi.org/10.1007/BF01458209
• M. Babaioff, N. Immorlica, R. Kleinberg, Matroids, secretary problems, and online mechanisms, SODA 2007. https://dl.acm.org/doi/10.5555/1283383.1283429

Motivation

An on-line algorithm must answer each request as it arrives, without knowing the requests to come; paging, caching, the $k$-server problem and metrical task systems are standard examples. Its quality is measured by competitive analysis: its cost is compared with the cost of an optimal off-line solution that knows the whole request sequence. For randomized on-line algorithms the comparison depends on how much the adversary producing the requests is allowed to see. Ben-David, Borodin, Karp, Tardos and Wigderson (Algorithmica 11, 1994; conference version STOC 1990) introduced the three standard adversaries — oblivious, adaptive on-line and adaptive off-line — and related the competitive ratios achievable against each.

Their Theorem 2.2 (manuscript p. 10) shows that if a randomized algorithm is $\alpha$-competitive against adaptive on-line adversaries and some randomized algorithm is $\beta$-competitive against oblivious adversaries, then the first algorithm is $\alpha\beta$-competitive against adaptive off-line adversaries. This mission formalizes the paper's claim (manuscript p. 11) that this product bound cannot be improved in general, together with the explicit construction on pp. 12–13 that proves it.

Setting

A request-answer game consists of a request set $R$, a finite answer set $A$, and cost functions $f_n : R^n \times A^n \to \mathbb R$. For a request sequence $\underline r \in R^n$, the off-line optimum is $c(\underline r) = \min_{\underline a \in A^n} f_n(\underline r, \underline a)$. A deterministic on-line algorithm $G$ answers the $i$-th request with $a_i = g_i(r_1, \dots, r_i)$; a randomized one is a probability distribution over deterministic algorithms $G_x$, $x$ being the coin tosses.

An adaptive off-line adversary $Q$ chooses each request $r_{i+1} = q_i(a_1, \dots, a_i)$ from the answers given so far, stops after at most $d_Q$ requests, and pays the off-line optimum $c_Q(G) = c(\underline r)$ of the requests it made; the algorithm pays $c_G(Q) = f_n(\underline r, \underline a)$. An adaptive on-line adversary $S$ must in addition answer each request itself, before the algorithm does, with $b_{i+1} = p_i(a_1, \dots, a_i)$, and pays $c_S(G) = f_n(\underline r, \underline b)$. An oblivious adversary fixes $\underline r$ in advance and pays $c(\underline r)$. A randomized $G$ is $\alpha$-competitive against oblivious adversaries if $\mathbb E_x[c_{G_x}(\underline r)] \le \alpha\, c(\underline r)$ for all $\underline r$, and against adaptive on-line adversaries if $\mathbb E_x[c_{G_x}(S)] \le \mathbb E_x[\alpha\, c_S(G_x)]$ for all $S$.

The construction uses the mates game: $R = A$ is a set of $2t$ elements split into $t$ pairs of mates, and for $n \ge 2$ the cost depends only on the first answer $a_1$ and the second request $r_2$: it is $1$ if $a_1 = r_2$, $M$ if $a_1$ is the mate of $r_2$, and $m$ otherwise. The algorithm $G$ draws $a_1$ uniformly at random. The parameters solve

$$\beta = \frac{(2t-2)m + M + 1}{2t}, \qquad \alpha = \frac{1 + (2t-1)M}{2 + (2t-2)m}.$$

Formalization targets

Goal: tightness of Theorem 2.2

For $1 < \beta \le \alpha$ (or $\alpha = \beta = 1$) and every $C < \alpha\beta$, there are a game and a randomized algorithm $G$ such that

$$G \text{ is } \alpha\text{-competitive against adaptive on-line adversaries}, \qquad G \text{ is } \beta\text{-competitive against oblivious adversaries},$$

and for every randomized algorithm $K$ some adaptive off-line adversary $Q$ achieves

$$\mathbb E[c_Q(K)] > 0, \qquad \mathbb E[c_K(Q)] \ge C\cdot \mathbb E[c_Q(K)].$$

Milestones (pp. 12–13)

1. The closed forms $m(t)$, $M(t)$ are the unique solution of the two equations.
2. $m(t) \to \beta$ and $M(t) \to \alpha\beta$ as $t \to \infty$.
3. For all large $t$: $M(t) \ge \max(m(t)^2, C)$, $1 \le m(t) \le M(t)$, $\alpha(m(t)-1) \le M(t) - m(t)$.
4. $G$ is $\beta$-competitive against oblivious adversaries in the mates game.
5. $G$ is $\alpha$-competitive against adaptive on-line adversaries in the mates game.
6. An adaptive off-line adversary makes every algorithm pay $M$ while paying $1$.

Significance

The result. Together with Theorem 2.2, the claim pins down exactly how much the adaptive off-line adversary can gain over the other two: the product $\alpha\beta$ is an upper bound for every game and is approached by a single game for every admissible pair $(\alpha, \beta)$. It shows that no general argument relating the three adversary models can give a bound better than the product, so any improvement for a specific problem (paging, $k$-server) must use the structure of that problem. The paging example cited on p. 11 (RANDOM against the three adversaries) gives one instance of tightness; the mates game gives tightness for every admissible pair.

Formalizing it. The result is proved in the paper, in about one page, with two steps left to the reader ("by inspection of the equations", "a simple case analysis"). No machine-checked proof of this or of any statement about adaptive adversaries is known to us. The formalization makes the model of §2 precise (sequences, stopping, the order in which adversary and algorithm commit, expectations over coins), checks the asymptotics of the parameters, and verifies the case analysis, which on inspection needs an inequality the page does not state. Two printed formulas on p. 12 contain typos; the formal statements carry the correct values.

Difficulty

The construction is explicit, but each competitiveness claim quantifies over all adversaries, which may adapt their requests to the algorithm's random answers, stop at any time, and (for the on-line adversary) commit to their own answers in advance. The algebra of $\alpha$-competitiveness is tight: the adversary's best expected advantage is exactly zero, so every case of its best reply must be checked with no slack. The page's condition $M \ge m^2$ does not suffice for this: when $a_1$ is neither the adversary's first answer nor its mate, the reply "mate of $a_1$" beats the reply "the adversary's own answer" only when $\alpha(m-1) \le M - m$, which holds for the solved parameters but is not implied by $M \ge m^2$. At $\beta = 1 < \alpha$ the solved parameter $m$ is below $1$ for every $t$, and the oblivious bound fails.

Formalization scope

All declarations live in OnlineRandomization.Tightness. The conventions:

• Costs are real-valued; the paper allows $+\infty$, so the game class is a special case.
• Answer sets are nonempty finite types; request sets are arbitrary types.
• Sequences are Lean lists, oldest first; cost r a is $f_n$ on lists of equal length $n$.
• Adversaries return none for "stop" and carry a depth bound $d_Q$; an on-line adversary's answer $b_{i+1}$ depends only on $a_1, \dots, a_i$.
• Randomized algorithms are a probability space of coins with a deterministic algorithm per coin and measurable answers; expectations are Bochner integrals, with $\alpha$ applied inside the expectation. In the goal, coin spaces range over Type.
• Competitiveness uses the ratio functions $x \mapsto \alpha x$ and $x \mapsto \beta x$, with no additive constant.
• The mates game is on Fin t × Bool, with mate $(i, b) \mapsto (i, \lnot b)$. The paper leaves the costs of plays with fewer than two requests undefined; the formalization sets $f_0 = 0$ and $f_1 \equiv 1$ (with $f_1 \equiv 0$ the algorithm would not be $\alpha$-competitive).
• Range. The goal assumes $1 < \beta \le \alpha$ or $\alpha = \beta = 1$; the page's case $\beta = 1 < \alpha$ is not covered by its construction and is left out. In fact the claim is false there for $1 < C < \alpha$: an algorithm that is $1$-competitive against oblivious adversaries answers optimally, almost surely, on every request sequence (its cost is never below the optimum and its expected cost does not exceed it), and an adaptive off-line adversary reaches only finitely many request sequences, so against $K = G$ every adversary has $\mathbb E[c_G(Q)] = \mathbb E[c_Q(G)]$, a ratio of $1 < C$.

The positivity requirement $\mathbb E[c_Q(K)] > 0$ in the goal is essential: without it the adversary that asks nothing satisfies $\mathbb E[c_K(Q)] \ge C \cdot 0$ for every $K$, and the third clause would hold vacuously.

A complete development needs: finite expectations over a uniform coin, the evaluation of the play of an adversary against a constant algorithm, and limit and eventual-inequality arguments for rational functions of $t$. The model of §2 is shared with the other missions of this series and is reusable for any request-answer formulation of an on-line problem. Proofs of individual milestones are welcome.

Selected references

• S. Ben-David, A. Borodin, R. Karp, G. Tardos, A. Wigderson, On the power of randomization in on-line algorithms, Algorithmica 11 (1994) 2–14. https://doi.org/10.1007/BF01294260 (cited from the authors' manuscript, manuscript pp. 7–13).
• A. Borodin, R. El-Yaniv, Online Computation and Competitive Analysis, Cambridge University Press, 1998. ISBN 0-521-56392-5.
• P. Raghavan, M. Snir, Memory versus randomization in on-line algorithms, IBM Journal of Research and Development 38 (1994) 683–707. https://doi.org/10.1147/rd.386.0683

Why randomization matters in online algorithms

An online algorithm must answer each request before it sees the next one. Its performance is compared with an optimum that may choose all its answers after seeing the complete request string. Randomization can improve an online algorithm's guarantee when the request string is fixed in advance. The comparison changes when an adversary chooses later requests after seeing the algorithm's earlier answers. Ben-David, Borodin, Karp, Tardos and Wigderson studied these choices of adversary in a common request-answer model and proved a general relation between their competitive guarantees (Ben-David et al., 1994, manuscript §§2–3).

The paper distinguishes three adversaries. An oblivious adversary fixes the request string before the algorithm's random choices affect any answer. An adaptive off-line adversary chooses the next request from previous answers but serves the resulting request string optimally after the play. An adaptive on-line adversary also chooses its own answer as each request arrives. The ability to react to answers makes the latter two adversaries materially different from the oblivious one for randomized algorithms (Ben-David et al., 1994, manuscript pp. 7–9).

Request-answer games and competitive cost

A request-answer game has a request set $R$, a finite nonempty answer set $A$, and a real cost $f_n(r,a)$ for a request string $r\in R^n$ and an answer string $a\in A^n$. The off-line optimum for $r$ is $c(r)=\min_{a\in A^n}f_n(r,a)$. A deterministic online algorithm $D$ returns its $i$th answer from the first $i$ requests alone; it has no access to the rest of $r$ or to the eventual stopping time. Its cost on $r$ is $c_D(r)=f_n(r,D(r))$.

A randomized online algorithm is a distribution over deterministic online algorithms. With coins $\omega$, write $G_\omega$ for the resulting deterministic algorithm. For a fixed request string $r$, $G$ is $\beta$-competitive against oblivious adversaries when $\mathbb E_\omega[c_{G_\omega}(r)]\leq\beta(c(r))$. The paper calls a transformation “linear” when it has the affine form $x\mapsto ux+v$ (Ben-David et al., 1994, manuscript p. 7).

An adaptive off-line adversary $Q$ has a rule from prior answer strings to either the next request or a stop signal, together with a common finite upper bound on play length. Let $r(G_\omega,Q)$ denote its request string and $c_Q(G_\omega)=c(r(G_\omega,Q))$. Its competitiveness condition places the transformation inside the expectation: $\mathbb E_\omega[c_{G_\omega}(Q)]\leq\mathbb E_\omega[\alpha(c_Q(G_\omega))]$. An adaptive on-line adversary $S$ has the same request rule and an additional answer rule; its own cost is $c_S(G_\omega)$, and the corresponding condition uses $\mathbb E_\omega[\alpha(c_S(G_\omega))]$ on the right (Ben-David et al., 1994, manuscript pp. 8–9).

Formalization targets

Randomization against adaptive off-line adversaries

The first target is Theorem 2.1: if some randomized algorithm is $\alpha$-competitive against every adaptive off-line adversary, a deterministic algorithm has that same guarantee on every request string:

$$\exists G\;\forall Q,\quad \mathbb E[c_G(Q)]\leq\mathbb E[\alpha(c_Q(G))]\quad\Longrightarrow\quad\exists D\;\forall r,\quad c_D(r)\leq\alpha(c(r)).$$

Composition of two guarantees

Theorem 2.2 takes an $\alpha$ guarantee for $G$ against adaptive on-line adversaries and a $\beta$ guarantee for another randomized algorithm against oblivious adversaries. It concludes that $G$ has the composed guarantee against adaptive off-line adversaries:

$$\mathbb E[c_G(Q)]\leq\mathbb E[(\alpha\circ\beta)(c_Q(G))]\qquad\text{for every }Q.$$

The mission goal is Corollary 2.1, the deterministic consequence of these two results:

$$\exists D\;\forall r,\qquad c_D(r)\leq(\alpha\circ\beta)(c(r)).$$

The milestones follow the paper's two theorems and the stated claims in their proofs, including the finite-horizon winning-position formulation and the adversary that simulates a fixed online algorithm (Ben-David et al., 1994, manuscript pp. 9–13).

What the result supplies

The corollary turns the existence of two randomized guarantees under different information rules into the existence of a deterministic online strategy with an explicit composed cost transformation. It is an existence result: it does not say that the deterministic strategy can be computed efficiently from the randomized algorithms. The paper itself notes that such a construction is unavailable in full generality and then examines settings where constructive versions are possible (Ben-David et al., 1994, manuscript p. 13).

The mathematical results were proved in the 1994 paper; this mission asks for machine-checked Lean proofs of the abstract model, the intermediate claims, and Corollary 2.1. The local draft currently contains compiled statements with proof placeholders, so it does not yet provide checked proofs. A completed development would make the adversary distinctions and the exact placement of expectations available for reuse in later online-algorithm formalizations.

Why the proof is difficult

The apparent shortcut is to treat an adaptive request sequence as fixed and apply a guarantee against oblivious adversaries directly. That loses the dependence of later requests on the algorithm's earlier answers. For Theorem 2.1, a winning request strategy must have one finite horizon that works for every answer path; separate finite horizons for each branch do not suffice when the answer set is infinite. For Theorem 2.2, the simulated adversary must make its own answers before the algorithm answers the current request, while still matching a fixed online benchmark along every resulting play. The expectation inequalities must remain valid when the request string itself depends on the algorithm's coins (Ben-David et al., 1994, manuscript pp. 9–11).

Formalization scope

Lean represents requests and answers as oldest-first lists. List index zero is request one in the paper. The general game is a separate definition; the algorithm, adversary, and competitiveness definitions build on it. An off-line adversary's rule returns Option R, where none is the stop signal, and has a uniform finite depth bound. A randomized algorithm consists of a coin probability space and a deterministic prefix algorithm for each coin; its answer events are measurable. Finiteness of $A$ and bounded play depth make the cost of each fixed adversarial play take finitely many values, so its real expectation is an ordinary integrable expectation.

The formal game uses real-valued costs, a deliberate restriction of the paper's $\mathbb R\cup\{\infty\}$ costs. The answer set is finite and nonempty, while the request set may be infinite. The transformations $\alpha$ and $\beta$ are affine. Theorem 2.2 and the goal assume $\alpha$ is monotone: the paper applies $\alpha$ to an inequality in its proof, and its competitive-ratio examples have positive slope. Theorem 2.1 does not need this added assumption. The two randomized algorithms may have different coin spaces, each an arbitrary Lean type at the declaration's universe level. The off-line and on-line adaptive comparisons retain $\alpha$ inside the expectation.

The target ranges over every equal-length request and answer play generated by these rules, including an adversary that stops without a request. It does not allow the deterministic algorithm to see future requests or choose a different policy for each adversary. Reusable contributions include the game interface, bounded adaptive plays, measurable randomized algorithms, and finite-horizon winning positions. The statements of all three principal results, their intervening claims, and proofs of those statements are within scope.

Selected references

• S. Ben-David, A. Borodin, R. Karp, G. Tardos and A. Wigderson, On the Power of Randomization in On-Line Algorithms, Algorithmica 11, 1994. DOI: 10.1007/BF01294260. The local source is the authors' 20-page manuscript; citations above use its page numbers.