Online Algorithms

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

Motivation

The multi-secretary problem is the basic model of selecting under a budget from a stream of offers. Hiring a fixed number of candidates, accepting a fixed number of requests for a perishable resource, and admitting customers into a capacity-limited service all have this structure. Each item must be accepted or rejected on arrival, and the comparison point is the offline decision maker, who sees the whole sequence and keeps the best $k$ items. The gap between the two expected values is the regret.

A common class of heuristics in revenue management and online resource allocation does not react to the realised history. These policies fix in advance, period by period, a probability of accepting each type of item, and then follow it until the budget runs out; static bid-price and randomised-acceptance rules are of this kind (Talluri and van Ryzin 2004). Arlotto and Gurvich (arXiv:1710.07719v2, Theorem 1) show that when abilities take finitely many values, an adaptive policy has regret bounded uniformly in the horizon $n$ and the budget $k$. Their Theorem 3 shows that the restriction to non-adaptive policies costs order $\sqrt n$ over a wide range of budgets. Read together, these two results separate adaptive from non-adaptive control by an unbounded factor. This mission formalizes the non-adaptive half.

Setting

There are $n$ candidates with abilities $X_1,\dots,X_n$, independent and identically distributed on $m$ values $0<a_m<a_{m-1}<\dots<a_1$, with masses $f_j=\mathbb P(X_1=a_j)>0$ and $\sum_jf_j=1$. Write $\epsilon=\tfrac12\min_jf_j$ and $\bar F(a_j)=f_1+\dots+f_{j-1}$. The budget is $k$, with $0\le k\le n$.

The offline value is

$$V^*_{\mathrm{off}}(n,k)=\mathbb E\Big[\max\Big\{\textstyle\sum_tX_t\sigma_t:\sigma\in\{0,1\}^n,\ \sum_t\sigma_t\le k\Big\}\Big].$$

A non-adaptive policy is a matrix $\pi=\{p_{j,t}\in[0,1]\}$. At time $t$, if budget remains and $X_t=a_j$, the candidate is selected with probability $p_{j,t}$, independently of everything else. The selection coins $B_t$ are then independent Bernoulli variables with $q_t=\mathbb E[B_t]=\sum_jp_{j,t}f_j$. The policy selects until $k$ coins have come up. Its value $V^\pi_{\mathrm{on}}(n,k)$ is the expected total ability selected, and

$$V^*_{\mathrm{na}}(n,k)=\sup_{\pi}V^\pi_{\mathrm{on}}(n,k).$$

The deterministic relaxation replaces the random counts $Z^n_j=\#\{t:X_t=a_j\}$ by their means. Its value is

$$DR(n,k)=\max\Big\{\textstyle\sum_ja_js_j:0\le s_j\le nf_j,\ \sum_js_j\le k\Big\},$$

with solution $s^*_j=\min\{nf_j,(k-n\bar F(a_j))_+\}$. The index policy takes its probabilities from $s^*$: $p_{j,t}=s^*_j/(nf_j)$.

Formalization targets

Goal: Theorem 3 (p. 25)

For every $\epsilon>0$, $m$ and $a$ there is $M=M(\epsilon,m,a)>0$ such that, for all masses with $\tfrac12\min_jf_j=\epsilon$ and all $(n,k)$ with $(f_1+\epsilon)n\le k\le(1-f_m-\epsilon)n$,

$$M\sqrt n\le V^*_{\mathrm{off}}(n,k)-V^*_{\mathrm{na}}(n,k).$$

The constant does not depend on the masses beyond $\epsilon$, nor on $n$ or $k$.

Milestones

• Lemma 2 (p. 8): binomial overshoot, $\mathbb E[(B-k)_+]\le1/(4\varepsilon)$ when $k$ exceeds the mean by $\varepsilon n$, and the symmetric bound.
• Remark 2 (pp. 10–11): $s^*$ solves the relaxation, and $V^*_{\mathrm{off}}\le DR$.
• Lemma 3 (p. 25): the index policy satisfies $DR-V^{\mathrm{id}}_{\mathrm{na}}\le\varepsilon^{-1}a_1\sqrt n$ when $k/n\ge\varepsilon$, so the order $\sqrt n$ is attained.
• Lemma 5 (p. 26): for a centred Bernoulli sum with variance $\varsigma^2$, $\mathbb E[(\pm N-\Upsilon\varsigma)_+]\ge\beta_1\varsigma-(2+3\sqrt2)$ with $\beta_1(\Upsilon)>0$, and $\mathbb E[(N+\Upsilon\varsigma)_+^2]\le\beta_2\varsigma^2$.
• Lemma 7 (p. 27): an optimal non-adaptive policy exists, and any optimal one has $f_1/2\le q_t\le1-f_m/2$ outside $2M\sqrt n$ periods, so $\sum_tq_t(1-q_t)\ge\tfrac{f_1f_m}4(n-2M\sqrt n)$.
• Lemma 4 (p. 25): for $k\le n(f_1-\epsilon)$ the non-adaptive regret is at most $a_2/(4\epsilon)$.
• Lemma 8 and Proposition 6 (p. 40): $\mathbb E[\mathfrak S^n_j]=s^*_j\pm M\sqrt n$, and $0\le DR-V^*_{\mathrm{off}}\le M\sqrt n$ in general and $\le a_1m/(4\epsilon')$ when $k/n$ is $\epsilon'$ away from the jump points of $\bar F$.

Significance

Theorem 3 is the lower half of the separation in Theorem 1 of the paper. The Budget-Ratio policy and the dynamic-programming policy have regret $O(1)$, uniformly in $(n,k)$, while every non-adaptive policy has regret $\Omega(\sqrt n)$ when $k/n$ lies strictly between $f_1$ and $1-f_m$. The order $\sqrt n$ of fluid and static randomised policies is therefore a property of the whole class, not of a poor choice inside it. Lemma 4 shows that the budget range cannot be removed: with a small budget a non-adaptive policy is as good as any.

The result is proved in the source but has not been machine-checked. A complete development would formalize, inside one finite probabilistic model: the binomial overshoot bound, a uniform anti-concentration estimate for Bernoulli sums, the structure of optimal non-adaptive policies, and the comparison with the offline sort. The source's proof of Theorem 3 also relies on a lemma that fails as printed (see Formalization scope), so a formal proof would close a real gap in the published argument.

Difficulty

The upper bound of order $\sqrt n$ (Lemma 3) follows from a variance computation. The lower bound must hold for every non-adaptive policy, including time-varying ones, and the obvious argument does not cover them. That argument compares a policy with the index policy and shows the index policy loses $\sqrt n$. A policy can, however, differ from the index policy by order $\sqrt n$ in its expected selection counts and still have regret of the same order. The step "small regret forces $s_j(\pi)\approx s^*_j$", which the source uses, is exactly the step that fails.

What has to be shown is that the selection count $\sum_tB_t$ of an optimal policy fluctuates by order $\sqrt n$, uniformly in the policy. A policy that runs out of budget early then misses top-value candidates late in the horizon, and one that keeps budget wastes slots. Both effects must be bounded below by a multiple of $\sqrt n$ that is uniform over all masses with the same $\epsilon$. Lemma 5 needs a normal approximation with an explicit, $q$-independent error. Lemma 7 needs the existence of an optimal policy, which is a maximisation over a continuum of matrices.

Formalization scope

The source is the arXiv preprint arXiv:1710.07719v2 (1 June 2018). Its printed page numbers equal the PDF page numbers.

• Indices. The value and mass vectors are a f : Fin m → ℝ. Lean index $j$ is the paper's index $j+1$, so a 0 $=a_1$ is the largest value and f (Fin.rev 0) $=f_m$ is the mass of the smallest. The standing assumptions of Sec. 2 are IsValues a (strictly decreasing, positive) and IsMasses f (positive, summing to one).
• Expectations. All expectations are finite sums over outcome sequences. For the offline problem these are $x:\mathrm{Fin}\,n\to\mathrm{Fin}\,m$ with weight $\prod_tf_{x_t}$. For a non-adaptive policy they are pairs $(X_t,B_t)$ with weight $\prod_tf_{x_t}\,p_{x_t,t}^{b_t}(1-p_{x_t,t})^{1-b_t}$. No measure theory is used.
• Selection rule. A candidate is selected iff its coin is $1$ and fewer than $k$ earlier coins were $1$. This equals the paper's "up to the stopping time $\nu$" for $k\ge1$. At $k=0$ the printed $\nu=1$ would allow a selection without budget, and the feasible rule is used.
• Suprema. $V^*_{\mathrm{na}}$ is a supremum over all matrices with entries in $[0,1]$, not over $0/1$ matrices or the index policy alone. $DR$ is the supremum of its linear program; it is not defined by the formula $\sum_ja_js^*_j$, which is a milestone.
• Index policy. $j_{\mathrm{id}}$ is the largest index with $\bar F(a_{j_{\mathrm{id}}})\le k/n$. As printed the defining inequality has no solution at $k=n$.
• Constants. Each constant is quantified after $(\epsilon,m,a)$ and before $(f,n,k)$. The goal's $M$ and Lemma 5's $\beta_1$ are strictly positive; with $M=0$ the goal would reduce to $V^*_{\mathrm{na}}\le V^*_{\mathrm{off}}$. Theorem 3 is posed for all $n$ in the range, as printed, without a threshold on $n$. Lemma 2 is stated in the multiplied form $(p+\varepsilon)n\le k$ of its proof. Lemma 4 adds $m\ge2$, so that $a_2$ exists.
• Disclosed gaps in the source. The source's proof of Theorem 3 relies on a lemma that fails as printed (Lemma 6, p. 26), so Lemma 6 is not part of this mission. The statement of Theorem 3 is posed as in the source. The printed argument for the second inequality of Lemma 7's (36) does not go through, and a corrected one also uses $a_{m-1}$. Lemma 7's constant is therefore quantified after all of $a$.

Contributions of any kind are welcome. Reusable pieces include binomial overshoot bounds, anti-concentration for sums of independent Bernoulli variables (for example via a Wasserstein normal approximation, which Mathlib lacks), and compactness arguments for optimal randomised policies.

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.07719v2
• K. T. Talluri, G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000
• N. Ross, Fundamentals of Stein's method, Probability Surveys 8, 2011. https://doi.org/10.1214/11-PS182
• S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities, Oxford University Press, 2013. https://doi.org/10.1093/acprof:oso/9780199535255.001.0001

Motivation

Many resource-allocation problems arrive one request at a time and must be answered immediately: a bandwidth request is admitted or refused when it appears, an advertiser's budget is charged when a query arrives, a job is accepted before later jobs are seen. Their linear-programming relaxations are packing problems: maximize a total profit subject to capacity constraints, where the variables are revealed online and each must be set irrevocably when it is revealed. A standard yardstick for such an online algorithm is its competitive ratio, the worst-case ratio between the offline optimum and the algorithm's value.

Buchbinder and Naor (Math. Oper. Res. 2009) gave a single online primal-dual scheme for the general online fractional packing problem, together with a matching scheme for covering. The scheme raises the newly revealed packing variable while increasing the dual covering variables along an exponential curve, and its analysis is a short primal-dual argument. Earlier online algorithms for throughput-competitive routing and for set cover (Alon et al. 2009) can be read as instances of it, and the same template later became the basis of a monograph on the primal-dual approach to online algorithms (Buchbinder, Naor 2009).

This mission formalizes the paper's headline result, Theorem 3.1, for the scheme exactly as the paper defines it.

Setting

Fix a finite set $I$ of $n\ge1$ packing constraints (equivalently, primal covering variables), with known capacities $c(i)>0$. Packing variables $y(1),\dots,y(m)$ arrive one per round; in round $j$ the variable $y(j)$ is revealed together with its non-negative column $a(i,j)$, $i\in I$. The offline problems form the primal-dual pair of Figure 1 of the paper:

$$\text{(P)}\ \min\sum_i c(i)x(i)\ \text{ s.t. } \sum_i a(i,j)x(i)\ge1\ \forall j,\ x\ge0;\qquad \text{(D)}\ \max\sum_j y(j)\ \text{ s.t. } \sum_j a(i,j)y(j)\le c(i)\ \forall i,\ y\ge0.$$

The profit of every $y(j)$ is normalized to $1$. Every column is assumed to have a positive entry; otherwise the packing problem is unbounded. An online algorithm may set $y(j)$ only in round $j$ and never changes it later.

The scheme with parameter $B>0$ keeps a primal vector $x$ (initially $0$) and the dual vector $y$. In round $j$ it computes the prefix maximum $a_i(\max)=\max_{k\le j}a(i,k)$. If the new covering constraint $\sum_i a(i,j)x(i)\ge1$ already holds, it sets $y(j)=0$. Otherwise it sets $y(j)$ to the least $t\ge0$ at which the constraint holds after every $x(i)$ is replaced by

$$\max\Big\{x(i),\ \frac{1}{n\,a_i(\max)}\Big[\exp\Big(\frac{B}{2c(i)}\sum_{k=1}^{j}a(i,k)y(k)\Big)-1\Big]\Big\},\qquad y(j)=t.$$

After $r$ rounds, $X(r)=\sum_i c(i)x(i)$ is the primal value and $Y(r)=\sum_{k\le r}y(k)$ the dual value. For the analysis, $a_i(\max)$ and $a_i(\min)$ also denote the largest and the smallest non-zero coefficient of row $i$ over all $m$ columns.

Formalization targets

Goal: Theorem 3.1

For every $B>0$, the scheme's dual solution is non-negative; after every round $r$, every non-negative $y'$ that satisfies the packing constraints restricted to the first $r$ columns has $\sum_{k\le r}y'(k)\le B\,Y(r)$ (the scheme is $B$-competitive); and after all $m$ rounds, for every $i$,

$$\sum_{k=1}^{m}a(i,k)\,y(k)\ \le\ c(i)\cdot\frac{2\log\big(1+n\,a_i(\max)/a_i(\min)\big)}{B}.$$

The paper states the second part as $c(i)\cdot O\big((\log n+\log(a_i(\max)/a_i(\min)))/B\big)$; the bound above is the one its proof establishes.

Milestones: the three claims of the proof

1. Claim (i): $X(r)\le B\cdot Y(r)$ after every round $r$.
2. Claim (ii): after every round, $x\ge0$ and $x$ satisfies every covering constraint revealed so far; no $x(i)$ ever decreases.
3. Claim (iii): the violation bound of the goal.

Significance

Theorem 3.1 says that a solution within factor $B$ of the optimum can be maintained online at the price of overloading each packing constraint by a factor of order $(\log n+\log(a_{\max}/a_{\min}))/B$. Scaling the output down by the overload gives a feasible online packing solution with competitive ratio $O(\log n+\log(a_{\max}/a_{\min}))$, and Lemma 3.1 of the paper shows that no online algorithm does better up to constant factors. The same trade-off underlies the paper's online rounding results for routing (§5.2) and, through the covering counterpart, for set cover (§5.1).

The result is proved in the paper. As far as the platform's record shows, it is not formalized: the published OnlinePrimalDual.GeneralPacking.theorem14_1 (a restatement of the monograph's version) takes the inequality $X\le BY$ and primal feasibility as hypotheses on arbitrary vectors $x,y$ and derives competitiveness by weak duality; it does not mention the scheme and has no violation bound. The published OnlinePrimalDual.GeneralPacking.lemma14_2 is the matching lower bound (Lemma 3.1) and is not part of this mission. A formalization here would give the first machine-checked guarantee for the scheme itself and a reusable analysis pattern (a potential bound integrated along a monotone path) for the other schemes of the paper.

Difficulty

The paper's argument is a derivative comparison along a continuous process: while $y(j)$ rises, $\partial X/\partial y(j)\le B$. In the discrete formulation each round jumps directly to the least admissible $y(j)$, and each $x(i)$ is a maximum of its old value and an exponential, so it is continuous but not differentiable where the maximum switches; the comparison must be turned into an integral inequality over $[0,y(j)]$ for such functions. The prefix maximum $a_i(\max)$ changes between rounds, and the claim that this never lowers or raises the primal value needs an invariant ($x(i)$ is always at least the current increment value). The violation bound rests on a second invariant, $x(i)\le1/a_i(\min)$, which holds because $y(j)$ is the least admissible value; any formalization that loses minimality (for example by taking an arbitrary admissible $t$) loses claim (iii).

Formalization scope

• The instance is the published OnlinePrimalDual.GeneralPacking.GeneralInstance I (Fin m) (costs $c>0$, coefficients $a\ge0$); $n=|I|$ with [Nonempty I]; columns are Fin m, arrive in index order, and are 0-based in Lean, so "the first $r$ columns" is (k : ℕ) < r. $m\ge1$ is [NeZero m].
• $a_i(\max)$, $a_i(\min)$ over all columns are the published aMax and aMin. For a row with no non-zero coefficient aMin is $0$ and both sides of the violation bound are $0$.
• The scheme is a function, stateAfter inst B r. The continuous loop of the paper is replaced by its discrete implementation, which the paper itself prescribes (p. 4): $y(j)$ is the least $t\ge0$ restoring the new covering constraint, written as sInf. Every theorem assumes that every column has a positive entry (the paper's standing assumption, p. 4); this makes the infimum attained. If the prefix maximum is $0$, Lean's $1/0=0$ gives increment $0$, which agrees with the paper's bracket being $0$.
• Explicit constant. The paper's $c(i)\cdot O((\log n+\log(a_i(\max)/a_i(\min)))/B)$ is instantiated as $c(i)\cdot 2\log(1+n\,a_i(\max)/a_i(\min))/B$, from claim (iii) of the proof. Logarithms are natural (Real.log), since they invert Real.exp.
• $B$-competitiveness is stated against every non-negative feasible packing solution of every prefix of the input, not only at the end.
• A formalization in which the inequality $X\le BY$, primal feasibility, or the bound $x(i)\le1/a_i(\min)$ is assumed rather than derived from the scheme is ruled out: every statement here is about the vectors the scheme computes from the instance.
• Needed infrastructure: monotonicity and continuity of the per-round primal path, attainment of the infimum, an integral (or mean-value) form of the derivative comparison for maxima of exponentials, and weak duality for finite LPs. The weak-duality step and the per-round integration lemma are reusable for missions 2–4 of this series. Proofs of the milestones, and of helper lemmas such as the invariant $x(i)\le1/a_i(\min)$, are welcome.

Selected references

• N. Buchbinder, J. Naor, Online Primal-Dual Algorithms for Covering and Packing, Mathematics of Operations Research, 2009. https://doi.org/10.1287/moor.1080.0363
• 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
• N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor, The Online Set Cover Problem, SIAM Journal on Computing 39(2), 2009. https://doi.org/10.1137/060661946

Motivation

In online routing of virtual circuits, connection requests between pairs of nodes of a capacitated network arrive one at a time. Each request must be accepted and routed on a single path with bandwidth $1$, or rejected, immediately and irrevocably, and no edge may carry more than its capacity. The goal is to maximize the number of accepted requests (the throughput). The model goes back to Awerbuch, Azar and Plotkin (FOCS 1993), whose deterministic algorithm has a logarithmic competitive ratio when edge capacities are at least logarithmic in the size of the network, and it underlies the analysis of admission control in circuit-switched and bandwidth-reserved networks.

Buchbinder and Naor (Math. Oper. Res. 2009) recover an algorithm with the same competitive factor from a general recipe: an online primal–dual scheme first produces a feasible fractional routing online, and an online version of Raghavan's pessimistic estimator (J. Comput. Syst. Sci. 1988) then rounds it, also online. This mission formalizes that construction and its guarantee (Section 5.2 of the paper, with the Section 3 scheme it uses).

Timeline:

• 1987–1988: Raghavan and Thompson introduce randomized rounding for multicommodity flow; Raghavan derandomizes it with pessimistic estimators.
• 1993: Awerbuch, Azar and Plotkin give the deterministic throughput-competitive online routing algorithm.
• 2005–2009: Buchbinder and Naor's primal–dual framework (ESA 2005; MOR 2009) derives an algorithm with the same factor systematically.

Setting

Let $E$ be a finite set of $m$ edges with capacities $u(e) > 0$, and $u(\min) = \min_e u(e)$. Requests $r_1, r_2, \dots$ arrive online; request $r_i$ comes with a finite list $\mathcal P(r_i)$ of admissible paths, each a set of edges, all of size at most $P(\max)$.

A fractional routing assigns flows $f(r_i, P) \ge 0$; it is feasible when $\sum_{P \in \mathcal P(r_i)} f(r_i, P) \le 1$ for every request and the load $\sum_{r_i}\sum_{P \ni e} f(r_i, P)$ of every edge is at most $u(e)$. Its value is $\mathrm{val}(f) = \sum_{r_i}\sum_P f(r_i, P)$; $\mathrm{OPT}$ is the largest value of a feasible routing of the arrived requests, an upper bound on the integral optimum.

The fractional scheme. The covering LP paired with the routing LP (the paper's primal, Fig. 3) has variables $x(e)$ (cost $u(e)$) and $Z(r_i)$ (cost $1$) with constraints $\sum_{e \in P} x(e) + Z(r_i) \ge 1$. When $r_i$ arrives, its paths are visited in order; for each path whose constraint fails, $f(r_i,P)$ is raised from $0$ to the least value restoring it, while $x(e) = \max\big(x(e), \tfrac1\ell(e^{B' F_e/(2u(e))}-1)\big)$ for $e \in P$ and $Z(r_i) = \max\big(Z(r_i), \tfrac1\ell(e^{B' f(r_i)/2}-1)\big)$ follow the flow ($F_e$ the load of $e$, $f(r_i)$ the flow of $r_i$). The parameters are $\ell = P(\max)+1$ and $B' = 2\ln(1+\ell)$.

The rounding. With the rounding scale $B = \exp(1 + \ln(2m)/u(\min)) - 1$, the integral edge usage $\chi(e)$ and the number $s$ of served requests, the potential is $\Phi = \Phi_1 + \Phi_2$,

$$\Phi_1 = \tfrac12\exp\Big(\frac{\mathrm{val}(f)}{2B} - s\ln 2\Big), \qquad \Phi_2 = \frac1{2m}\sum_{e}\exp\Big(\Big(1+\frac{\ln 2m}{u(e)}\Big)\chi(e) - F_e\Big).$$

After the fractional round of $r_i$, the algorithm serves $r_i$ on a path $P \in \mathcal P(r_i)$ (adding $1$ to $\chi(e)$ for $e \in P$) if this gives potential at most the potential $\Phi^{\mathrm{start}}$ before the round; otherwise it rejects $r_i$.

Formalization targets

Goal: Lemma 5.4

For every request sequence, the algorithm never exceeds a capacity, and for every feasible fractional routing $f$,

$$\chi(e) \le u(e)\ \ \forall e, \qquad \sum_{r_i}\chi(r_i) \ \ge\ \frac{\mathrm{val}(f)}{4B\ln 2\cdot\ln(P(\max)+2)} - 1 .$$

Milestone: Theorem 3.2 (packing half, on routing)

The fractional scheme's flows $f^{\mathrm{alg}}$ are feasible and $\mathrm{val}(f) \le 2\ln(P(\max)+2)\,\mathrm{val}(f^{\mathrm{alg}})$ for every feasible $f$.

Milestone: Lemma 5.3

$\Phi \le 1$ initially, $\Phi > 0$ always, and whenever the flows of a request are raised by a non-negative amount of total at most $1$, serving the request on some path or rejecting it does not increase $\Phi$.

Significance

The result shows that a deterministic online algorithm for throughput-competitive routing, previously designed by hand, falls out of two generic components: an online fractional packing scheme and an online pessimistic estimator. A side product is that the fractional phase alone produces, online, a near-optimal routing that respects all capacities exactly, independently of their size. When $u(\min) \ge \log n$ the rounding loses only a constant factor and the algorithm is $O(\log P(\max))$-competitive, as in Awerbuch–Azar–Plotkin.

The results are proved in the paper; none is machine-checked. A formalization supplies a checked instance of the online primal–dual method together with derandomized online rounding, and fixes the constants the paper leaves inside $O(\cdot)$. Related platform content: the monograph's OnlinePrimalDual.Routing.per_copy_guarantee and routing_competitive concern the Buchbinder–Naor $(1, O(\log n))$-competitive algorithm with copies of the graph, a different scheme.

Difficulty

The fractional guarantee is argued in the paper continuously (rates of change of the primal and dual values), while the scheme as formalized is discrete: each flow is the least value restoring a constraint, and every primal variable is a maximum whose branch may switch during the increase. The continuous argument does not transfer verbatim, and feasibility depends on the least value restoring the constraint with equality.

The rounding is a derandomization. The existence of a good path or a good rejection is established in the paper as an expectation over a random trial; a deterministic statement about finitely many alternatives is what the mission asks for, with all $m+1$ exponential terms of $\Phi$ under control at once. A frequent first attempt compares with the potential after the fractional round; the rule compares with $\Phi^{\mathrm{start}}$, before the flow increase, and the guarantee is stated for that comparison.

Formalization scope

• Edges are a non-empty Fintype E; capacities are real and positive. A request is a List (Finset E) of paths; the request sequence is a list. Simple paths of a graph are a special case; nothing in the argument uses graph structure. $P(\max)$ is a parameter with every path of size at most $P(\max)$.
• A routing is a List (List ℝ) of the shape of the request sequence. $\mathrm{OPT}$ is quantified as "every feasible fractional routing".
• The continuous increase is its discrete equivalent (an attained sInf). Ties among good paths are broken by list order; only paths that received flow in the current round are candidates for serving, so a request whose flow was not increased is rejected.
• Explicit constants replacing $O(\cdot)$: Theorem 3.2's $O(\log \ell)$ becomes $2\ln(1+\ell) = 2\ln(P(\max)+2)$; Lemma 5.4's $O(\log P(\max)\cdot[\exp(1+2\ln m/u(\min))-1])$ becomes $4B\ln 2\cdot\ln(P(\max)+2)$ with additive $-1$, where $B = \exp(1+\ln(2m)/u(\min))-1$ is the scale chosen on p. 15. The printed "$2\ln m$" differs from the proof's "$\ln 2m$"; the proof's constant is used (it is at least as strong for $m \ge 2$). All logarithms are natural.
• The algorithm is a fully specified function: a formalization in which requests are never served, or $\mathrm{OPT}$ is a free variable pinned by hypotheses, would trivialize the goal and is ruled out.
• Not included: the covering half of Theorem 3.2, and the remark on $u(\min) \ge \log n$.

Contributions welcome: proofs of the milestones, a reusable lemma "convex combination $\le$ value $\Rightarrow$ some outcome $\le$ value" for derandomization, and the discrete-to-continuous bridge for the Section 3 scheme.

Selected references

• N. Buchbinder, J. Naor, Online Primal-Dual Algorithms for Covering and Packing, Mathematics of Operations Research, 2009. https://doi.org/10.1287/moor.1080.0363
• B. Awerbuch, Y. Azar, S. Plotkin, Throughput-Competitive On-Line Routing, Proc. 34th FOCS, pp. 32–40, 1993. https://doi.org/10.1109/SFCS.1993.366884
• P. Raghavan, Probabilistic construction of deterministic algorithms: approximating packing integer programs, J. Comput. Syst. Sci. 37(2), 1988. https://doi.org/10.1016/0022-0000(88)90003-7
• P. Raghavan, C. D. Thompson, Randomized rounding: a technique for provably good algorithms and algorithmic proofs, Combinatorica 7(4), 1987. https://doi.org/10.1007/BF02579324

Motivation

Online bipartite matching models a platform that must commit each arriving request to a resource immediately. The motivating application of Feldman, Mehta, Mirrokni and Muthukrishnan is display advertising: an ad server knows from past traffic how many impressions of each type (web page, audience segment) to expect, sells them to advertisers in advance, and must assign each impression to an interested advertiser the moment a user loads the page. The goal is to fill as many contracted impressions as possible.

When arrivals are chosen by an adversary, the best ratio an online algorithm can guarantee is $1 - 1/e \approx 0.632$, achieved by the RANKING algorithm of Karp, Vazirani and Vazirani (STOC 1990). The ad server, however, is not facing an adversary: it has a forecast. The i.i.d. model captures this: the graph and the distribution of impression types are known in advance, and the impressions are independent draws. The paper asks whether this knowledge allows an online algorithm to beat $1 - 1/e$, and answers yes.

Timeline.

• 1990: Karp, Vazirani and Vazirani give RANKING, with ratio $1 - 1/e$ for adversarial arrivals, and show this is optimal in that model.
• 2005: Mehta, Saberi, Vazirani and Vazirani obtain $1 - 1/e$ for the budgeted AdWords generalization.
• 2009: Feldman, Mehta, Mirrokni and Muthukrishnan (arXiv:0905.4100, FOCS 2009) show that in the i.i.d. model the two suggested matchings algorithm achieves about $0.670$ with high probability when OPT is linear in $n$, the first ratio above $1 - 1/e$ for this model, and that no online algorithm reaches $26/27$ in expectation.

Setting

An instance is a bipartite graph $G = (A, I, E)$ with a finite set $A$ of advertisers, a finite set $I$ of impression types, and edges $E \subseteq A \times I$ recording which advertisers want which types. The mission treats the case analysed throughout §4.2 of the paper, in which one impression of each type is expected ($e_i = 1$). So $n = |I|$ impressions arrive one at a time, with types $\omega(0), \dots, \omega(n-1)$ drawn independently and uniformly from $I$. On arrival an impression must be assigned at once and irrevocably to a still unassigned advertiser adjacent to its type, or discarded. $\mathrm{ALG}(\omega)$ is the number of impressions an algorithm assigns. $\mathrm{OPT}(\omega)$ is the size of a maximum matching of the realization graph, which has one node per arrival $t$, joined to every advertiser $a$ with $(a, \omega(t)) \in E$.

The two suggested matchings (TSM) algorithm works offline first. Its boosted flow graph $G_f$ has a source arc of capacity $2$ into every advertiser, a unit-capacity arc along every edge of $E$, and an arc of capacity $2$ from every type to a sink. The algorithm takes the edge set $E_f$ of an integral maximum flow. Every vertex then has at most two edges of $E_f$, so $E_f$ splits into vertex-disjoint paths and cycles. The algorithm colours each component blue and red:

• on cycles, the colours alternate;
• on odd paths, the colours alternate, with more blue than red;
• on even paths between advertisers, the colours alternate;
• on even paths between types, the first two edges are blue, then the colours alternate, ending in blue.

Online, the first arrival of type $i$ tries the advertiser along $i$'s blue edge, the second tries the one along its red edge, and later arrivals are discarded. A tried advertiser that is already taken is not reassigned. The advertisers fall into four classes by their coloured edges: $A_{BR}$ (one blue, one red), $A_{BB}$ (two blue), $A_B$ (one blue only) and $A_R$ (one red only).

Formalization targets

Goal: Theorem 5, first sentence, $e_i = 1$

Let

$$\alpha = \frac{1 - 2/e^2}{4/3 - 2/(3e)} \approx 0.67029 .$$

The goal has three parts. First, every maximum flow edge set admits a colouring that follows the rules. Second, for every $\varepsilon > 0$ and $c > 0$ there are $\delta > 0$ and $N$ such that, for every instance with $n \ge N$, every maximum flow edge set and every rule-following colouring,

$$\Pr_\omega\big[\ \mathrm{OPT} \ge c\,n \implies \mathrm{ALG} \ge (\alpha - \varepsilon)\,\mathrm{OPT}\ \big] \;\ge\; 1 - e^{-\delta n}.$$

Third, $\alpha > 1 - 1/e$.

Milestones

1. Facts 1 and 2: concentration for two balls-in-bins statistics.
2. The note of §4.2.1: each type has no coloured edge, one blue edge, or one blue and one red edge.
3. Equation (1): $|E_f| = 2|A_{BR}| + 2|A_{BB}| + |A_B| + |A_R|$.
4. Equation (2): with high probability, $\mathrm{ALG} \ge (1 - 1/e^2)|A_{BB}| + (1 - 2/e^2)|A_{BR}| + (1 - 3/(2e))(|A_B| + |A_R|) - 4\varepsilon n$.
5. Equation (3): $|E_f| = 2(|A_T| + |I_S|) + |E_\delta|$ for the surgered residual cut $(S,T)$ of $G_f$.
6. Equation (4): with high probability, $\mathrm{OPT} \le |A_{BR}| + |A_{BB}| + \tfrac12(|A_B| + |A_R|) + (\tfrac12 - \tfrac1e)|E_\delta| + \varepsilon n$.
7. Lemma 1: $|E_\delta| \le \tfrac23|A_{BR}| + \tfrac43|A_{BB}| + |A_B| + \tfrac13|A_R|$.

Significance

The theorem separates the i.i.d. model from the adversarial one: knowing the distribution is worth a constant factor above $1 - 1/e$. The suggested matching algorithm of the same paper (Theorem 4) shows that following a single offline matching gets exactly $1 - 1/e$, so the second, red matching is what crosses the barrier. The paper's question started a line of work on the i.i.d. and random-order models, with later improvements to the constant by other authors under further assumptions.

The result has a written proof but, as far as the platform record shows, no machine-checked one. The mission formalizes the paper's own argument: the flow-and-colouring construction, the balls-in-bins concentration facts, the cut-based bound on OPT and the combinatorial Lemma 1. It also fixes two slips in the printed statements (see Formalization scope). The pieces are reusable beyond this paper. The occupancy concentration (Fact 1) and the satisfied-sequences bound (Fact 2) recur in analyses of online algorithms with stochastic input. The degree-capped flow encoding and its path/cycle decomposition are standard tools for 2-matchings.

Difficulty

The upper bound on OPT is the delicate part. A cut of the flow graph bounds the maximum matching of the realization graph only after a second surgery that depends on the random arrivals. Its size must then be compared with the colour classes, which are defined by a different structure (the components of $E_f$). Lemma 1 bridges the two, and it depends on the exact colouring rules: a colouring that only satisfies local degree conditions can put red edges at both ends of an even advertiser path, which breaks the inequality $|A_B| \ge |A_R|$ behind (2). On the probabilistic side, the advertisers of $A_{BR}$ share impression types with each other, so the success events are dependent, and Fact 2 needs a bounded-differences argument in which one ball affects up to $d$ sequences.

Formalization scope

All declarations live in the namespace OnlineStochMatching.TSM. Advertisers and types are finite types A I : Type, and $E$ is a Finset (A × I). Probabilities are counting ratios $\#\{\omega : \mathrm{Fin}\ n \to I \mid P\,\omega\}/|I|^n$, so there are no measurability side conditions. OPT is a maximum over the finite, nonempty set of partial injective assignments. An integral flow of $G_f$ is its set of saturated middle edges, i.e. a subset of $E$ with at most two edges per vertex; $E_f$ is such a set of maximum cardinality. A colouring is given by a listing of the components of $E_f$ as vertex sequences. Every theorem quantifies over every maximum $E_f$ and every colouring the rules allow, since the paper fixes neither.

The paper's asymptotic phrases are replaced by explicit quantifiers that come from its own proofs:

• "with probability $1 - e^{-\Omega(n)}$" and "with high probability" (Theorem 5, (2), (4)) become: $\exists\, \delta > 0,\ \exists\, N$, chosen before the instance, with probability at least $1 - e^{-\delta n}$ for all $n \ge N$;
• "as long as OPT $= \Omega(n)$" becomes the event $\mathrm{OPT} \ge c\,n$ for an arbitrary $c > 0$ fixed before $\delta$ and $N$;
• the $O(1)$ term in the bound on $|A^*_\delta|$ (p. 8) is absorbed into $\varepsilon n$ for $n \ge N$.

Corrections to the printed statements:

• Theorem 5 prints $\mathrm{ALG}/\mathrm{OPT} - \epsilon \ge \alpha$; the proof concludes $\mathrm{ALG}/\mathrm{OPT} + \epsilon \ge \alpha$, so the goal states $\mathrm{ALG} \ge (\alpha - \varepsilon)\mathrm{OPT}$;
• Fact 1 prints the failure probability $2e^{-\epsilon n/2}$; its proof gives $2e^{-\epsilon^2 n/2}$, which is used;
• Fact 2 states two hypotheses its proof uses: the bins of a sequence are distinct, and $c^2 < n$.

The ratio is multiplied out, so no division by OPT occurs. A colouring condition that is unsatisfiable, or a flow set that is not maximum, would make the goal vacuous or false; part (a) of the goal rules out the first, and every statement requires maximality. Not included: the reduction to general integer $e_i$ (§4.2.4), the tightness sentence of Theorem 5 (§4.2.5), and footnote 7's variant of the algorithm.

Useful infrastructure: bounded-differences (McDiarmid/Azuma) inequalities for functions of i.i.d. uniform variables, which exist on the platform as separate theorems; path/cycle decomposition of graphs of maximum degree two; and max-flow min-cut for unit-capacity bipartite networks. Contributions are welcome on Facts 1 and 2 independently of the combinatorics, and on Lemma 1 and equations (1) and (3), which are deterministic.

Selected references

• J. Feldman, A. Mehta, V. Mirrokni, S. Muthukrishnan, Online Stochastic Matching: Beating 1-1/e, FOCS 2009; arXiv:0905.4100v1. https://arxiv.org/abs/0905.4100
• 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
• A. Mehta, A. Saberi, U. Vazirani, V. Vazirani, AdWords and generalized online matching, FOCS 2005; J. ACM 54(5), 2007. https://doi.org/10.1145/1284320.1284321