All missions

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

Motivation

Stochastic gradient methods minimize a function $f$ when only noisy estimates of its gradient are available: each step moves along a descent direction corrupted by random noise. They are the standard training algorithm for neural networks and the basic tool of stochastic approximation, and the question every user faces is what can be guaranteed when $f$ is nonconvex, possibly unbounded below, and the noise is allowed to grow with the gradient.

D. P. Bertsekas and J. N. Tsitsiklis, Gradient Convergence in Gradient Methods with Errors, SIAM J. Optim. 10(3):627–642, 2000 (DOI), answer this under minimal assumptions. Noise with variance growing in $\|\nabla f(x_t)\|$ had been handled for related methods (Poljak and Tsypkin 1973), but typically together with a lower bound on $f$, under which $f(x_t)$ is approximately a supermartingale and the supermartingale convergence theorem applies (see the monographs of Kushner and Clark 1978; Benveniste, Métivier and Priouret 1990; Kushner and Yin 1996). Section 4 of the paper (p. 635) removes the lower bound: it proves that, with probability 1, either $f(x_t)\to-\infty$ or $f(x_t)$ converges and $\nabla f(x_t)\to 0$, without assuming bounded iterates. Section 5 shows that the randomized incremental gradient method for a finite-sum objective is a special case. This mission formalizes Section 4 and the Section 5 application. A companion mission covers the deterministic counterpart (Proposition 1 of the same paper).

Setting

Let $f:\mathbb R^n\to\mathbb R$ be continuously differentiable with a Lipschitz gradient: there is $L\ge 0$ with

$$\|\nabla f(x)-\nabla f(\bar x)\|\le L\|x-\bar x\|\qquad\forall x,\bar x. \tag{2.1}$$

Let $(\Omega,\mathcal F,P)$ be a probability space and $\mathcal F_0\subseteq\mathcal F_1\subseteq\cdots$ an increasing sequence of $\sigma$-fields (a filtration; $\mathcal F_t$ is the history of the algorithm just before the noise $w_t$ is drawn). The stochastic gradient method generates random vectors by

$$x_{t+1}=x_t+\gamma_t(s_t+w_t),$$

where $\gamma_t>0$ is a deterministic stepsize, $s_t$ is a descent direction and $w_t$ is a noise term. The assumptions of Proposition 3 are:

• (a) $x_t$ and $s_t$ are $\mathcal F_t$-measurable;
• (b) there are $c_1,c_2>0$ with $c_1\|\nabla f(x_t)\|^2\le-\nabla f(x_t)'s_t$ and $\|s_t\|\le c_2(1+\|\nabla f(x_t)\|)$ for all $t$; (4.1)
• (c) for all $t$, with probability 1, $E[w_t\mid\mathcal F_t]=0$ (4.2) and $E[\|w_t\|^2\mid\mathcal F_t]\le A(1+\|\nabla f(x_t)\|^2)$ (4.3), with $A>0$ deterministic;
• (d) $\sum_t\gamma_t=\infty$ and $\sum_t\gamma_t^2<\infty$.

The noise variance in (c) may grow quadratically with $\|\nabla f(x_t)\|$ and is therefore unbounded in general. A point $\bar x$ is stationary if $\nabla f(\bar x)=0$.

Formalization targets

Goal: Proposition 3 (p. 635)

Under (2.1) and (a)–(d), with probability 1,

$$f(x_t)\to-\infty\quad\text{or}\quad\Bigl(f(x_t)\to\ell\in\mathbb R\ \text{ and }\ \nabla f(x_t)\to 0\Bigr),$$

and every limit point of $(x_t)$ is a stationary point of $f$. The dichotomy is per sample path: different paths may take different branches.

Milestones

1. (4.4), p. 636. The pathwise one-step inequality: if $\gamma\,2Lc_2^2\le c_1/2$ and $s$ satisfies (4.1) at $x$, then for every $w$,

$$f(x+\gamma(s+w))\le f(x)-\gamma\tfrac{c_1}{2}\|\nabla f(x)\|^2+\gamma\nabla f(x)'w+\gamma^2 2Lc_2^2+\gamma^2L\|w\|^2.$$

2. Lemma 2, p. 637. If $r_t$ is $\mathcal F_{t+1}$-measurable with $E[r_t\mid\mathcal F_t]=0$, $E[\|r_t\|^2\mid\mathcal F_t]\le B$ and $\sum\gamma_t^2<\infty$, then $\sum_{t\le T}\gamma_tr_t$ and $\sum_{t\le T}\gamma_t^2\|r_t\|^2$ converge almost surely.
3. Lemma 6, p. 640. For every $\delta>0$, almost surely $f(x_t)$ converges to a finite value or to $-\infty$, and if the limit is not $-\infty$ then $\limsup_t\|\nabla f(x_t)\|\le\delta$.

Further result: §5, pp. 641–642

For $f=\frac1m\sum_i f_i$ with Lipschitz gradients $\nabla f_i$ satisfying $\|\nabla f_i(x)\|\le C+D\|\nabla f(x)\|$ (5.2), the randomized incremental gradient method $x_{t+1}=x_t-\gamma_t\nabla f_{k(t)}(x_t)$, with independent uniform indices $k(t)$, satisfies the conclusion of Proposition 3.

Significance

Proposition 3 is a convergence guarantee for stochastic gradient descent on smooth nonconvex objectives that needs neither a lower bound on $f$, nor bounded iterates, nor bounded noise variance. It contains, as special cases, stochastic gradient descent with unbiased gradient estimates whose variance grows with the gradient, the randomized incremental (single-sample) gradient method for finite sums of Section 5, and scaled or approximate gradient directions through condition (4.1). Its conclusion is the strongest one available at this generality: if $f(x_t)$ stays bounded below along a path, then the gradient vanishes along that path and every limit point is stationary.

The result is proved in the paper; to our knowledge it has not been machine-checked. Its formalization requires a working theory of generalized conditional expectations of non-integrable noise, square-integrable martingales in $\mathbb R^n$ and pathwise arguments over random interval partitions, which is reusable for other stochastic approximation results (Robbins–Monro type schemes, TD-learning, stochastic subgradient methods).

Difficulty

The natural first idea is to view $f(x_t)$ as a supermartingale up to summable errors and apply the supermartingale convergence theorem (Robbins–Siegmund). This fails here: the theorem needs $f(x_t)$ bounded below, and $f$ is not assumed bounded below; in addition the noise term $\gamma_t^2L\|w_t\|^2$ in (4.4) has conditional mean of order $\gamma_t^2\|\nabla f(x_t)\|^2$, which is not summable when the gradient is unbounded. Any argument must therefore extract a decrease of $f$ that dominates noise of the same order as the gradient itself, without a lower bound to anchor a supermartingale, and must do so along every sample path while the hypotheses are only conditional-expectation statements about non-integrable noise.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), $\nabla f$ is Mathlib's gradient f, $f$ is ContDiff ℝ 1, and the Lipschitz constant is L : ℝ≥0 with LipschitzWith L (gradient f) (the standing assumption (2.1), equivalent to the page's form).
• The probability space is a Measure Ω with IsProbabilityMeasure, the $\sigma$-fields are a Mathlib Filtration ℕ, and measurability in (a) is StronglyMeasurable[ℱ t]. The recursion and (4.1) hold on every sample path. Stepsizes are deterministic.
• Conditional expectations of the noise. The page assumes no integrability of $w_t$, of $\|w_t\|^2$ or of $f(x_t)$, and none is added. Mathlib's condExp is $0$ for non-integrable functions, so stating (4.2)–(4.3) with it would make them hold vacuously for any non-integrable noise; that encoding is ruled out. Instead (4.3) says that for every $\mathcal F_t$-measurable set $S$, $\int_S\|w_t\|^2\,dP\le\int_S A(1+\|\nabla f(x_t)\|^2)\,dP$ (in $[0,\infty]$), and (4.2) says that $\int_S w_t\,dP=0$ for every $\mathcal F_t$-measurable $S$ on which $w_t$ is integrable. These are exactly the generalized conditional-expectation statements of the page.
• In Lemma 2 the bound $B$ is a constant, so Mathlib's condExp is used there, with integrability of $\|r_t\|^2$ stated explicitly; the page's hypothesis implies it. Lemma 2 is stated over any finite-dimensional real inner-product space, since the paper applies it to real and to vector-valued sequences.
• $\sum\gamma_t=\infty$ is divergence of the partial sums; $\sum\gamma_t^2<\infty$ is Summable. Convergent random series (Lemma 2) are convergence of partial sums, not Summable, which would mean unconditional convergence. "$\limsup\|\nabla f(x_t)\|\le\delta$" is "for every $\delta'>\delta$, eventually $\|\nabla f(x_t)\|\le\delta'$". Limit points are MapClusterPt.
• In the §5 result the page's references to "section 4" and "(4.1)" are read as section 3 and condition (3.1), the indices $k(t)$ run from $t=0$, $x_0$ is deterministic, and the stepsizes are nonnegative as on the page.
• Not stated: Lemma 3 (it needs the random interval construction of p. 636 as a definition), Lemmas 4–5 (steps that depend on the proof's own choice of $\epsilon$), and the Remarks of §4.

Contributions welcome: a proof of Lemma 2 from Mathlib's martingale convergence theorems (Submartingale.exists_ae_tendsto_of_bdd), a proof of (4.4) from the descent lemma, a general bridge between the set-integral encoding of conditional expectations and Mathlib's condExp on localizing sets, and the interval construction behind Lemmas 3–6.

Selected references

• D. P. Bertsekas and J. N. Tsitsiklis, Gradient Convergence in Gradient Methods with Errors, SIAM J. Optim. 10(3):627–642, 2000. https://doi.org/10.1137/S1052623497331063
• B. T. Poljak and Y. Z. Tsypkin, Pseudogradient adaptation and training algorithms, Automat. Remote Control 12 (1973), 83–94.
• H. J. Kushner and D. S. Clark, Stochastic Approximation Methods for Constrained and Unconstrained Systems, Springer, 1978.
• H. J. Kushner and G. Yin, Stochastic Approximation Methods, Springer, 1996 (as cited in the paper).
• A. Benveniste, M. Métivier and P. Priouret, Adaptive Algorithms and Stochastic Approximations, Springer, 1990.
• D. P. Bertsekas and J. N. Tsitsiklis, Neuro-Dynamic Programming, Athena Scientific, 1996.

Motivation

Temporal-difference (TD) learning estimates the value of a policy by moving a current estimate toward a target built from observed rewards and from the estimate itself. Chapter 7 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) interpolates between the two extreme targets of the preceding chapters: the one-step TD target, which uses one reward and then bootstraps, and the Monte Carlo target, which uses every reward until the end of the episode. The intermediate target, the $n$-step return, uses $n$ rewards and then bootstraps from the current estimate. The family underlies $n$-step TD, $n$-step Sarsa, the off-policy per-decision methods and the tree-backup algorithm, and it is the introduction to eligibility traces (Chapter 12).

The book justifies the whole family with one inequality, the error reduction property (7.3), p. 144: the expected $n$-step return is closer to the true value than the estimate it bootstraps from, by a factor $\gamma^n$ in the worst state. It is the reason given for calling $n$-step TD methods "sound". The same chapter states, mostly as exercises without solutions, a series of exact identities that rewrite each kind of $n$-step return as a sum of one-step TD errors.

Setting

A finite Markov decision process has finite state and action sets $\mathcal S$, $\mathcal A$, a finite reward set $\mathcal R \subset \mathbb R$, and dynamics $p(s', r \mid s, a)$, the probability of next state $s'$ and reward $r$ after action $a$ in state $s$ (Eqs. (3.2)–(3.3)). A policy $\pi(a \mid s)$ is a probability distribution over actions for each state. Following $\pi$ from $S_t = s$ produces a random trajectory $A_t, R_{t+1}, S_{t+1}, A_{t+1}, R_{t+2}, \dots$ For a discount factor $0 \le \gamma < 1$ the state-value function is the expected discounted return (3.12),

$$v_\pi(s) = \mathbb E_\pi\Big[\sum_{k=0}^{\infty} \gamma^k R_{t+k+1} \,\Big|\, S_t = s\Big].$$

Given any function $V : \mathcal S \to \mathbb R$ (an estimate of $v_\pi$), the $n$-step return (7.1) is

$$G_{t:t+n} = R_{t+1} + \gamma R_{t+2} + \cdots + \gamma^{n-1} R_{t+n} + \gamma^n V(S_{t+n}).$$

In an episode that terminates at time $T$ it is replaced by the complete return $G_t$ when $t + n \ge T$. The TD error (6.5) is $\delta_k = R_{k+1} + \gamma V(S_{k+1}) - V(S_k)$. Off-policy variants use a behavior policy $b$ that generates the data, the per-decision ratio $\rho_t = \pi(A_t \mid S_t)/b(A_t \mid S_t)$, and the return with control variate (7.13), $G_{t:h} = \rho_t(R_{t+1} + \gamma G_{t+1:h}) + (1-\rho_t) V(S_t)$, $G_{h:h} = V(S_h)$. The tree-backup return (7.15)–(7.16) uses action values $Q$ and the expected approximate value $\bar V(s) = \sum_a \pi(a \mid s) Q(s, a)$ (7.8).

Formalization targets

Goal: the error reduction property (7.3)

For a finite MDP, a policy $\pi$, $0 \le \gamma < 1$, any $V : \mathcal S \to \mathbb R$ and every $n \ge 1$,

$$\max_s \big|\mathbb E_\pi[G_{t:t+n} \mid S_t = s] - v_\pi(s)\big| \le \gamma^n \max_s \big|V(s) - v_\pi(s)\big|.$$

Milestones, in the book's order

1. Exercise 7.1, p. 143: with $V$ fixed and $V(S_T) = 0$, $G_{t:t+n} - V(S_t) = \sum_{k=t}^{\min(t+n,T)-1} \gamma^{k-t}\delta_k$.
2. Exercise 7.4, Eq. (7.6), p. 148: the $n$-step Sarsa return equals $Q_{t-1}(S_t, A_t) + \sum_{k=t}^{\min(t+n,T)-1} \gamma^{k-t}[R_{k+1} + \gamma Q_k(S_{k+1}, A_{k+1}) - Q_{k-1}(S_k, A_k)]$, with estimates changing from step to step.
3. Eq. (7.12), p. 150: $G_{t:h} = R_{t+1} + \gamma G_{t+1:h}$ for $t < h < T$, $G_{h:h} = V(S_h)$.
4. Exercise 7.6, p. 151, for (7.13): under coverage, $\mathbb E_b$ of the control-variate return equals $\mathbb E_b$ of the same return without the control variate, and both equal $\mathbb E_\pi[G_{t:t+n} \mid S_t = s]$.
5. Exercise 7.8, p. 151: $G_{t:h} - V(S_t) = \sum_{k=t}^{h-1} \gamma^{k-t} \big(\prod_{i=t}^{k}\rho_i\big) \delta_k$ for the return (7.13).
6. Exercise 7.11, p. 153: the tree-backup return equals $Q(S_t, A_t) + \sum_{k=t}^{\min(t+n-1,T-1)} \delta_k \prod_{i=t+1}^{k} \gamma\pi(A_i \mid S_i)$ with the expectation-based TD error $\delta_k = R_{k+1} + \gamma\bar V(S_{k+1}) - Q(S_k, A_k)$.

Significance

The result. The error reduction property makes the expected $n$-step target a $\gamma^n$-contraction toward $v_\pi$ in the sup norm, uniformly over the estimate it starts from. It is the one-line reason the book offers for the soundness of every $n$-step TD method, and the same contraction is what the $\lambda$-return of Chapter 12 averages over $n$. The TD-error identities are the algebra behind implementations that accumulate TD errors instead of storing returns, and behind the forward/backward-view equivalences of Chapter 12. Exercise 7.6 is the unbiasedness of the control-variate return, which is what allows (7.13) to replace plain importance weighting without changing the expected update.

Formalizing it. All results are elementary and well known, but the book gives no proofs: (7.3) is asserted, and the identities are exercises without published solutions. None is formalized on Prove2Me. The mission produces machine-checked versions with every hypothesis explicit (discounting, the fixed estimate, terminal values, coverage), and a trajectory-level expectation for finite MDPs that other chapters of the series can reuse.

Difficulty

The obvious proof of (7.3) is a matrix computation: $\mathbb E_\pi[G_{t:t+n} \mid S_t = s] - v_\pi(s) = \gamma^n (P_\pi^n (V - v_\pi))(s)$, and a stochastic matrix does not increase the sup norm. The difficulty lies in the step before it. The left side is an expectation over trajectories, and $v_\pi$ is an infinite discounted series; neither is a matrix power by definition. Connecting them requires a Chapman–Kolmogorov identity for the finite-trajectory distribution induced by $\pi$ and $p(s', r \mid s, a)$, the splitting of $v_\pi$ at time $n$, and summability of the discounted series. Defining the expected $n$-step return as the matrix expression would reduce the goal to the last line and remove its content; that shortcut is ruled out below.

The TD-error identities are telescoping sums, but each has its own boundary: termination inside the $n$ steps, the convention that terminal states have value zero, the index $Q_{-1}$ at $t = 0$ in (7.6), the special case $G_{T-1:t+n} = R_T$ of the tree backup, and ratios with vanishing denominators in (7.13).

Formalization scope

• Model. The finite MDP, policies and $v_\pi$ follow the series conventions: dynamics $p(s', r \mid s, a)$ over a finite reward set, one action set for all states, $v_\pi(s) = \sum_k \gamma^k (P_\pi^k r_\pi)(s)$ computed from expected rewards and never defined as a Bellman solution.
• Expectations are over trajectories. $\mathbb E_\pi[\,\cdot \mid S_t = s]$ is the finite sum over $n$-step segments $(A_{t+k}, S_{t+k+1}, R_{t+k+1})_{k<n}$ weighted by $\prod_k \pi(A_{t+k}\mid S_{t+k})\,p(S_{t+k+1}, R_{t+k+1}\mid S_{t+k}, A_{t+k})$. The expected $n$-step return is not defined as $\sum_{k<n}\gamma^k P_\pi^k r_\pi + \gamma^n P_\pi^n V$, which would make the goal a two-line matrix inequality.
• The estimate is fixed. In the algorithm, $V_{t+n-1}$ is the current random estimate. Every statement takes a fixed function $V$ (or $Q$), which is the book's own reading ("if the value estimates don't change"). The only exception is Exercise 7.4, whose estimates $Q_k$ are indexed by time $k \in \mathbb Z$ exactly as in (7.6).
• Discounting. The goal assumes $0 \le \gamma < 1$ and takes the maximum over all states. Episodic tasks enter through absorbing zero-reward terminal states. The undiscounted episodic case $\gamma = 1$ is not stated.
• Episodes. Sample-path identities use sequences $S_k, A_k, R_k$ and a termination time $T$. The book's convention that terminal states have value $0$ is a hypothesis ($V(S_T) = 0$, $Q(S_T, \cdot) = 0$).
• Exercise 7.6 is stated for the state-value return (7.13) of p. 150, although the exercise follows the action-value return (7.14). Its conclusion includes, besides the literal "does not change the expected value", equality with the on-policy expected return, the property the book states on p. 150. Coverage ($\pi(a\mid s) > 0 \Rightarrow b(a\mid s) > 0$) is assumed.
• Not stated. The convergence of $n$-step TD methods "under appropriate technical conditions" (p. 144), and the programming exercises.

Needed infrastructure: finite sums over function types, Chapman–Kolmogorov for the segment distribution, summability of $\sum_k \gamma^k P_\pi^k r_\pi$. The trajectory layer is reusable for the importance-sampling and eligibility-trace chapters. Alternative proofs of the goal, and proofs of the undiscounted episodic version as a separate theorem, are welcome.

Selected references

• R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, Chapter 7, pp. 141–158. http://incompleteideas.net/book/the-book-2nd.html
• C. J. C. H. Watkins, Learning from Delayed Rewards, PhD thesis, University of Cambridge, 1989 (the $n$-step return and its error reduction property, as credited on p. 158 of the book). https://www.cs.rhul.ac.uk/~chrisw/new_thesis.pdf
• D. Precup, R. S. Sutton and S. Singh, Eligibility traces for off-policy policy evaluation, Proceedings of the 17th International Conference on Machine Learning (ICML), 2000, pp. 759–766 (the tree-backup algorithm, as credited on p. 158 of the book; no DOI).

Motivation

In data-driven algorithm design, an algorithm or mechanism comes with a vector of tunable parameters $\rho$, and the parameters are chosen by optimizing average performance over sample instances drawn from an unknown distribution. How many samples suffice for the empirical optimum to be near-optimal in expectation is governed by the pseudo-dimension of the class $\mathcal U=\{u_\rho\}$ of performance functions, where $u_\rho(x)$ is the performance of the parameter $\rho$ on instance $x$. Balcan, DeBlasio, Dick, Kingsford, Sandholm and Vitercik (arXiv:1908.02894v4, 2021) give a general upper bound on $\mathrm{Pdim}(\mathcal U)$ for classes whose dual functions are piecewise structured (their Theorem 3.3, the subject of mission 1 of this series), and apply it across integer programming, computational biology, clustering and mechanism design.

A general upper bound raises the question of whether it can be improved. Section 5 of the paper answers it for one application: neutral affine maximizers (NAMs), a family of voting mechanisms studied by Roberts (1979), Mishra and Sen (2012) and Nath and Sandholm (2019). For NAMs with $n$ agents and $m$ alternatives the general theorem gives $\mathrm{Pdim}(\mathcal U)=O(n\ln m)$, and Theorem 5.2 shows a lower bound linear in $n$. So the sample complexity of tuning a NAM by sampling cannot be reduced below order $n$ by a sharper analysis, and the general bound is tight up to logarithmic factors.

Setting

There are $n$ agents and $m$ alternatives. Agent $i$ has a value $v_i(j)\in\mathbb R$ for each alternative $j\in[m]$; a valuation profile is $v=(v_1,\dots,v_n)\in\mathbb R^{nm}$.

A NAM is specified by a weight vector $\rho=(\rho[1],\dots,\rho[n])\in\mathbb R^n_{\ge0}$ in which at least one agent has weight zero; an agent with $\rho[i]=0$ is a sink agent. The NAM's outcome on a profile $v$ is an alternative maximizing the weighted value,

$$\psi_\rho(v)\in\operatorname*{argmax}_{j\in[m]}\ \sum_{i=1}^n\rho[i]\,v_i(j).$$

Its utility is the social welfare of that outcome,

$$u_\rho(v)=\sum_{i=1}^n v_i\bigl(\psi_\rho(v)\bigr),$$

and the class studied is $\mathcal U=\{u_\rho \mid \rho\in\mathbb R^n_{\ge0},\ \{i\mid\rho[i]=0\}\ne\emptyset\}$. NAMs also charge VCG-style payments that are redistributed to the sink agents; these do not enter $u_\rho$.

A class $\mathcal H$ of real-valued functions on a set $Y$ shatters points $y_1,\dots,y_N$ if there are thresholds $z_1,\dots,z_N\in\mathbb R$ such that every pattern $b\in\{0,1\}^N$ is realized by some $h\in\mathcal H$, in the sense that $h(y_\ell)>z_\ell$ exactly when $b_\ell=1$. The pseudo-dimension $\mathrm{Pdim}(\mathcal H)$ is the largest $N$ for which some $N$ points are shattered. In Lean: a profile is v : Fin n → Fin m → ℝ, the outcome rule is ψ, the utility is welfare ψ ρ, the class is namClass ψ, and shattering is the published FoundationsML.Regression.Shatters.

Formalization targets

Goal: Theorem 5.2, corrected

For every $n\ge1$, every $m\ge2$ and every tie-breaking rule,

$$\mathrm{Pdim}(\mathcal U)\ \ge\ \Bigl\lfloor\frac n2\Bigr\rfloor .$$

The printed statement reads $\mathrm{Pdim}(\mathcal U)\ge n/2$; see Formalization scope for why the floor is needed.

Milestones: the two claims of the proof (p. 24)

The proof fixes $N=\lfloor n/2\rfloor$ explicit profiles $v^{(1)},\dots,v^{(N)}$ and, for each bit vector $b\in\{0,1\}^N$, an explicit weight vector $\rho\in\{0,1\}^n$ (both are definitions of this mission). The two milestones are the claims the proof makes about them: for every $\ell\in[N]$ and $\varepsilon\in(0,\tfrac12)$,

$$b_\ell=0\ \Longrightarrow\ u_\rho\bigl(v^{(\ell)}\bigr)=\varepsilon,\qquad b_\ell=1\ \Longrightarrow\ u_\rho\bigl(v^{(\ell)}\bigr)=1 .$$

Significance

The result. Theorem 5.2 is the paper's evidence that its main upper bound cannot be improved in general by more than logarithmic factors: for NAMs the upper bound is $O(n\ln m)$ and the lower bound is of order $n$. Through the standard link between pseudo-dimension and uniform convergence, it also means that any learner choosing NAM weights from samples needs a number of samples growing with the number of agents, whatever tie-breaking rule the mechanism uses.

Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of any pseudo-dimension lower bound for a mechanism class, was found on Prove2Me. This mission produces a Lean model of NAM outcomes and welfare that does not fix a tie-breaking rule, an explicit lower-bound construction stated as definitions, and a pseudo-dimension lower bound in the vocabulary of the published FoundationsML pseudo-dimension items. It complements mission 1, which formalizes the matching upper-bound machinery.

Difficulty

The mathematical content is a single explicit construction, and the work lies in stating and verifying it at full generality rather than in a deep argument. Three points make the naive transcription wrong. First, the printed bound $n/2$ is false at $n=1$ and is not what the proof establishes for odd $n$; the even-$n$ reduction must be replaced by a statement in $\lfloor n/2\rfloor$. Second, the outcome $\psi_\rho(v)$ is defined by an argmax with unspecified tie-breaking, so the claims must hold for every maximizer; this requires showing the relevant maximizers are unique on the constructed profiles, not reading off a convenient one. Third, the construction embeds $\lfloor n/2\rfloor$ indices into the $n$ agents twice (as $\ell$ and $\lfloor n/2\rfloor+\ell$), and the printed index condition for the second alternative is a typo; an off-by-one in this embedding silently breaks both claims. Finally, every constructed $\rho$ must be admissible: it needs a sink agent, which holds only because $N\ge1$ or because $n$ is odd and the last agent keeps weight $0$.

Formalization scope

Representation. Agents are Fin n, alternatives Fin m, profiles Fin n → Fin m → ℝ, all 0-based: the paper's agent $i$ is i - 1, and its first and second alternatives are 0 and 1. Bits are Bool with true for $1$. An outcome rule is any ψ : (Fin n → ℝ) → (Fin n → Fin m → ℝ) → Fin m with IsArgmaxSelector ψ, which requires ψ ρ v to maximize ∑ i, ρ i * v i j for every ρ and v; the theorem and both claims are stated for every such ψ. "$\mathrm{Pdim}(\mathcal U)\ge N$" is the existence of an $N$-tuple of profiles shattered by namClass ψ in the sense of FoundationsML.Regression.Shatters, whose strict threshold t i < g (z i) shatters the same tuples as the paper's sign convention.

Corrections and readings of the printed text.

1. The bound is $\lfloor n/2\rfloor$ (natural-number division n / 2) instead of $n/2$. The proof assumes $n$ even; at $n=1$ the only admissible $\rho$ is $0$, so $\mathcal U$ is a single function and $\mathrm{Pdim}(\mathcal U)=0<\tfrac12$.
2. The hypotheses $n\ge1$ and $m\ge2$ are explicit. For $n=0$ no weight vector has a zero coordinate and $\mathcal U=\emptyset$; for $m=1$ the class is a single function. The proof takes $m=2$; the statement is for every $m\ge2$, with value $0$ on every further alternative in the constructed profiles.
3. The set-builder "$\{\rho[i]\mid i=0\}\ne\emptyset$" in Theorem 5.2 is read as $\{i\mid\rho[i]=0\}\ne\emptyset$, as written in Lemma 5.1.
4. The construction's condition "$\ell=n/2+i$" for $v_i^{(\ell)}(2)=\varepsilon$ is read as $i=n/2+\ell$, as the paper's own $n=6$ example shows. The milestone texts are verbatim and keep the printed "$v^{(\ell)}_{n/2+\ell}(1)$", which should read "$(2)$".

Ruled-out trivializations. Fixing one tie-breaking rule would state a special case and is excluded by quantifying over all argmax selectors. Dropping the sink-agent condition, or allowing $n=0$ or $m=1$, would change the class or make the statement vacuous or false; the conventions above exclude all three.

Infrastructure. Only Mathlib finite sums over Fin and the published Shatters definition are needed. The NAM model (IsNAMParam, IsArgmaxSelector, welfare, namClass) is reusable for any further statement about learning NAM parameters, including the matching $O(n\ln m)$ upper bound once mission 1's general theorem is available. Proofs of the two claims, of the admissibility of the constructed weight vectors, and of the goal are all welcome.

Selected references

• M.-F. Balcan, D. DeBlasio, T. Dick, C. Kingsford, T. Sandholm, E. Vitercik, How Much Data Is Sufficient to Learn High-Performing Algorithms? Generalization Guarantees for Data-Driven Algorithm Design, arXiv:1908.02894v4, 2021. https://arxiv.org/abs/1908.02894v4
• K. Roberts, The characterization of implementable social choice rules, in J.-J. Laffont (ed.), Aggregation and Revelation of Preferences, North-Holland, 1979 (reference [86] of the paper).
• D. Mishra, A. Sen, Roberts' theorem with neutrality: a social welfare ordering approach, Games and Economic Behavior 75(1):283–298, 2012 (reference [74] of the paper).
• S. Nath, T. Sandholm, Efficiency and budget balance in general quasi-linear domains, Games and Economic Behavior 113:673–693, 2019 (reference [78] of the paper).
• D. Pollard, Convergence of Stochastic Processes, Springer, 1984 (pseudo-dimension; reference [83] of the paper).

Counting lattice points in fixed dimension

How many integral points does a polytope contain? The question arises in integer programming, where it measures the size of a feasible set, in combinatorics, where many enumeration problems are lattice-point counts in a polytope (contingency tables, magic squares, flows), in the representation theory of Lie groups, and in the analysis of loop nests in compilers. Counting is #P-hard when the dimension is part of the input, so the natural question is whether the count can be computed in polynomial time when the dimension $d$ is fixed.

Timeline:

• 1899. In dimension $2$, Pick's formula leads to a polynomial algorithm.
• 1983. Lenstra shows that integer feasibility is decidable in polynomial time for fixed $d$ (Lenstra 1983). Deciding whether a lattice point exists does not count them.
• 1988, 1992. Brion proves that the exponential sum over the lattice points of a rational polytope is the sum of the exponential sums of its vertex cones.
• 1991. Dyer gives polynomial algorithms in dimensions $3$ and $4$, based on Dedekind sums (Dyer 1991).
• 1994. Barvinok proves that for every fixed $d$ the number of lattice points of an integral simplex, and hence of a rational polyhedron, can be computed in polynomial time (Barvinok 1994). The algorithm was later implemented (LattE, barvinok) and is the standard method.

Setting

Points of $\mathbb{R}^d$ have real coordinates and $\langle c,x\rangle=\sum_l c_lx_l$. For integral vectors $u_1,\dots,u_k\in\mathbb{Z}^d$, the rational cone they generate is $\operatorname{co}\{u_1,\dots,u_k\}=\{\sum_i\lambda_iu_i:\lambda_i\ge0\}$. The generators are simple if they are linearly independent, and primitive if moreover they form a basis of the lattice $\mathbb{Z}^d\cap\operatorname{Lin}\{u_1,\dots,u_k\}$.

The index $\operatorname{Ind}K$ of the cone given by simple generators is the number of integral points in the semi-open parallelepiped $\Pi=\{\sum_i\alpha_iu_i:0\le\alpha_i<1\}$. It equals $1$ exactly for primitive generators.

The exponential sum of $K$ is $\sigma(K;c)=\sum_{x\in K\cap\mathbb{Z}^d}e^{\langle c,x\rangle}$. Where it converges it has the closed form

$$\sigma(K;c)=\Bigl(\sum_{x\in\Pi\cap\mathbb{Z}^d}e^{\langle c,x\rangle}\Bigr)\prod_{i=1}^k\frac{1}{1-e^{\langle c,u_i\rangle}},$$

and this closed form defines $\sigma$ at every regular point, i.e. every $c$ with $\langle c,u_i\rangle\ne0$ for all $i$.

An integral simplex is $\Delta=\operatorname{conv}\{v_1,\dots,v_{k+1}\}$ with affinely independent $v_j\in\mathbb{Z}^d$. Its supporting cone at a vertex $v$ is $K_v=\{u:v+\delta u\in\Delta\text{ for all sufficiently small }\delta>0\}$. A signed decomposition $K=\sum_i\varepsilon_iK_i$ with integers $\varepsilon_i$ means $\chi_K=\sum_i\varepsilon_i\chi_{K_i}$ on all of $\mathbb{R}^d$. The constant term of the Laurent expansion of $f$ at $t=0$ is the coefficient of $t^0$ in the expansion of $f$ around its pole at $0$.

Formalization targets

Goal: the short signed formula (Theorem 1.2, mathematical content)

For $d\ge2$ and every integral simplex $\Delta\subseteq\mathbb{R}^d$ there are, for each vertex $v_j$, primitive cones $K_{j,i}$ and integers $\varepsilon_{j,i}$ with $K_{v_j}=\sum_i\varepsilon_{j,i}K_{j,i}$ and at most $(2^d)^{T_j}$ terms. Here $T_j$ is the smallest integer

$$T_j\ge\frac{-\log\log1.9+\log\log\operatorname{Ind}_j}{\log d-\log(d-1)},$$

and $\operatorname{Ind}_j$ is the index of the edge vectors at $v_j$. Moreover, for every $c$ orthogonal to no generator of any $K_{j,i}$,

$$\#(\Delta\cap\mathbb{Z}^d)=\sum_j\sum_i\varepsilon_{j,i}\,R(K_{j,i},v_j,c),$$

where $R(K,v,c)$ is the constant term at $t=0$ of $t\mapsto e^{t\langle c,v\rangle}\sigma(K;tc)$.

Milestones

1. Proposition 2.4 with Remark 2.5: the closed form of $\sigma$ for simple cones.
2. Proposition 4.1: for primitive cones, $\sigma(K;c)=\prod_i(1-e^{\langle c,u_i\rangle})^{-1}$.
3. Proposition 2.7 (Brion), for integral simplices.
4. Corollary 4.2: $R(K,v,c)=Q_k(x;y)\prod_ix_i^{-1}$ with $\deg Q_k\le k$.
5. Primitive generators iff $\operatorname{Ind}K=1$ (§5).
6. Lemma 5.2: a short lattice vector $w$ with $\operatorname{Ind}K_j\le(\operatorname{Ind}K)^{(d-1)/d}$.
7. Lemma 5.3: at most $2^d$ cones of smaller index, with signs $\pm1$.
8. Theorem 5.4: decomposition into at most $(2^d)^T$ primitive cones.
9. The display in the proof of Theorem 5.4: $(2^d)^T\le C_1(d)(\log\operatorname{Ind}K)^{C_2(d)}$.
10. Lemma 6.1: some $c(t)=(1,t,\dots,t^{d-1})$, $t\in\{0,\dots,m(d-1)\}$, is orthogonal to none of $m$ nonzero vectors.

Significance

The goal is the reason Barvinok's algorithm is polynomial. For fixed $d$, the number of terms is bounded by a polynomial in $\log\operatorname{Ind}K$, which is polynomial in the input size. Each term is an explicit rational function of inner products (Corollary 4.2). The identity therefore turns lattice-point counting into the evaluation of a short sum. Its consequences include polynomial-time counting for rational polyhedra in fixed dimension, polynomial-time computation of Ehrhart quasi-polynomials, and the theory of short rational generating functions (Barvinok–Woods), which underlies algorithms for parametric integer programming.

The result is proved and classical. As far as known it has not been machine-checked: Mathlib has convex cones, Minkowski's convex body theorem and lattices, but no signed cone decompositions, no generating functions of cones and no Brion identity. The mission produces a formal account of the algorithm's correctness and of the size of its output. Its milestones are statements of independent use: the closed form of cone generating functions, Brion's identity for simplices, and the index-reduction lemma.

Difficulty

The obvious approach is to triangulate the supporting cones into unimodular (primitive) cones. This fails: a cone of index $\operatorname{Ind}K$ may need about $\operatorname{Ind}K$ unimodular cones in any triangulation, which is exponential in the input size. The step that makes the count small is signed decomposition. Signed decomposition uses cones that are not contained in $K$, combined with signs $\pm1$, and controls the index through the geometry of numbers rather than through a subdivision of $K$. The second difficulty is that $c=0$, where the exponential sum equals the count, is a singular point of every $\sigma(K_i;\cdot)$. The count is recovered as a constant term of a Laurent expansion, so every identity has to be valid as an identity of meromorphic functions on regular points, and not only where the series converge.

Formalization scope

• Points of $\mathbb{R}^d$ are Fin d → ℝ, integral vectors Fin d → ℤ used through their real cast, and $\langle\cdot,\cdot\rangle$ is dotProduct. A cone is given by its generator list, because index, parallelepiped and the closed form of $\sigma$ depend on the generators. Logarithms are natural, and $|u|$ is the sup norm.
• Theorem 1.2 is represented by its mathematical content. The paper's statement is "there exists a polynomial time algorithm". No machine model is formalized. The goal is the identity proved on p. 778, with the count of the proof of Theorem 5.4 (p. 777). The algorithmic clauses of Lemmas 5.2, 5.3, 6.1 and Theorem 5.4 are each replaced by the existence statement of the object the algorithm constructs. Lemma 5.3(c), whose constant is unquantified, is omitted.
• Over $\mathbb{R}$. The paper uses $c\in\mathbb{C}^d$ only to speak of meromorphic functions. Here $c$ is real, $\sigma$ is defined by its closed form, and regularity means $\langle c,u_i\rangle\ne0$ for every generator. The constant term is a predicate: $t^Nf(t)$ agrees near $0$ with a real-analytic function whose $N$-th Taylor coefficient is the value.
• Added hypotheses. These are $d\ge2$ wherever $T$ appears, $k\ge1$ in Lemma 5.2, $d\ge1$ in Lemma 5.3, $u_i\ne0$ in Lemma 6.1, and $\operatorname{Ind}K\ge2$ in the display bound. $T=0$ when the index is $1$. Brion's identity is stated for integral simplices, the only case the proof uses.
• Trivializations ruled out. $\sigma$ is never an infinite sum, which would take a junk value off its convergence region. "Primitive" means a lattice basis and not mere linear independence; with the weaker notion the decomposition is trivial. Decompositions hold for every $x\in\mathbb{R}^d$, not only on $\mathbb{Z}^d$. The halfspace of Lemma 5.2 is linear, since an affine one would make it vacuous.
• Infrastructure. A complete development needs generating functions of simplicial cones, Brion's theorem for simplices, the identity theorem for rational functions in $e^{c_1},\dots,e^{c_d}$, Minkowski's theorem on a sublattice, and inclusion–exclusion for triangulations. Each is reusable beyond this mission, and contributions of any of these pieces are welcome.

Selected references

• A. I. Barvinok, A polynomial time algorithm for counting integral points in polyhedra when the dimension is fixed, Mathematics of Operations Research 19(4), 1994, 769–779. https://doi.org/10.1287/moor.19.4.769
• M. Brion, Points entiers dans les polyèdres convexes, Annales scientifiques de l'École Normale Supérieure 21(4), 1988, 653–663. https://doi.org/10.24033/asens.1572
• M. Dyer, On counting lattice points in polyhedra, SIAM Journal on Computing 20(4), 1991, 695–707. https://doi.org/10.1137/0220044
• H. W. Lenstra Jr., Integer programming with a fixed number of variables, Mathematics of Operations Research 8(4), 1983, 538–548. https://doi.org/10.1287/moor.8.4.538
• R. P. Stanley, Enumerative Combinatorics, Vol. 1, Wadsworth & Brooks/Cole, 1986, §4.6. https://doi.org/10.1007/978-1-4615-9763-6
• A. Barvinok, K. Woods, Short rational generating functions for lattice point problems, Journal of the AMS 16(4), 2003, 957–979. https://doi.org/10.1090/S0894-0347-03-00428-4

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