Theoretical Computer Science

Motivation

Unconstrained submodular maximization (USM) asks for a subset $S$ of a finite ground set $\mathcal N$ maximizing a nonnegative submodular function $f$. It contains Max-Cut, Max-DiCut and maximum facility location as special cases, and it is the basic subproblem of many constrained submodular maximization algorithms. Because $f$ is given only through a value oracle, the question is how close to the optimum a polynomial number of queries can get.

Timeline of the approximation ratio for USM in the value oracle model:

• Feige, Mirrokni and Vondrák (FOCS 2007; SIAM J. Comput. 2011) showed that a uniformly random set achieves $1/4$, local search achieves $1/3$ and $2/5$, and that no algorithm making polynomially many queries achieves $1/2 + \varepsilon$ for any fixed $\varepsilon > 0$.
• Oveis Gharan and Vondrák (SODA 2011) reached $0.41$ by simulated annealing; Feldman, Naor and Schwartz (ICALP 2011) reached $0.42$.
• Buchbinder, Feldman, Naor and Schwartz (FOCS 2012) closed the gap with the double greedy algorithms: a deterministic $1/3$-approximation and a randomized $1/2$-approximation, both linear in the number of oracle calls. Their Appendix A gives a third, fractional variant, which is the subject of this mission.

This is the third mission on the FOCS 2012 paper; the first two treat the deterministic and the randomized double greedy on sets.

Setting

Let $\mathcal N$ be a finite ground set with $n$ elements and $f : 2^{\mathcal N} \to \mathbb R_{\ge 0}$. The function $f$ is submodular if

$$f(A) + f(B) \ge f(A \cup B) + f(A \cap B) \qquad \text{for all } A, B \subseteq \mathcal N .$$

Write $f(OPT) = \max_{S \subseteq \mathcal N} f(S)$ and let $OPT$ be a maximizing set.

The multilinear extension of $f$ is the function on vectors $x \in [0,1]^{\mathcal N}$

$$F(x) = \sum_{S \subseteq \mathcal N} f(S) \prod_{u \in S} x_u \prod_{u \notin S} (1 - x_u) = \mathbb E\bigl[f(R(x))\bigr],$$

where the random set $R(x)$ contains each element $u$ independently with probability $x_u$. A set is identified with its characteristic vector, so $F$ agrees with $f$ on $\{0,1\}^{\mathcal N}$, and $\{u\}$ also denotes the unit vector at $u$. For vectors, $x \vee y$ and $x \wedge y$ are the coordinate-wise maximum and minimum.

Algorithm 4 (MultilinearUSM). Fix an arbitrary order $u_1, \dots, u_n$ of $\mathcal N$ and start from $x_0 = \emptyset$ and $y_0 = \mathcal N$ (the vectors $\mathbf 0$ and $\mathbf 1$). In iteration $i = 1, \dots, n$ compute

$$a_i = F(x_{i-1} + \{u_i\}) - F(x_{i-1}), \qquad b_i = F(y_{i-1} - \{u_i\}) - F(y_{i-1}),$$

set $a_i' = \max\{a_i, 0\}$, $b_i' = \max\{b_i, 0\}$, and update

$$x_i = x_{i-1} + \frac{a_i'}{a_i' + b_i'} \{u_i\}, \qquad y_i = y_{i-1} - \frac{b_i'}{a_i' + b_i'} \{u_i\},$$

with the convention that the two fractions are $1$ and $0$ when $a_i' = b_i' = 0$. The output is the random set $R(x_n)$. Every choice before the output is deterministic; the algorithm queries $F$ at four points per element.

For the analysis, $OPT_i = (OPT \vee x_i) \wedge y_i$.

Formalization targets

Goal: Theorem A.1, oracle-access clause

For every nonnegative submodular $f$ and every order of the ground set,

$$x_n = y_n \qquad\text{and}\qquad f(OPT) \le 2\,F(x_n) = 2\,\mathbb E\bigl[f(R(x_n))\bigr].$$

Milestones, in the order the proof uses them

1. $a_i + b_i \ge 0$ at every iteration (proof of Lemma A.2; the page cites Lemma II.1).
2. Endpoints: $OPT_0 = OPT$ with $F(OPT) = f(OPT)$, and $OPT_n = x_n = y_n$.
3. (4) and (5): if $a_i \ge 0$ and $b_i > 0$, then $F(x_i) - F(x_{i-1}) = a_i^2/(a_i+b_i)$ and $F(y_i) - F(y_{i-1}) = b_i^2/(a_i+b_i)$.
4. (6): in the same case, $F(OPT_{i-1}) - F(OPT_i) \le a_i b_i/(a_i + b_i)$, whether or not $u_i \in OPT$.
5. Lemma A.2: for every $1 \le i \le n$,

$$F(OPT_{i-1}) - F(OPT_i) \le \tfrac12\bigl[F(x_i) - F(x_{i-1}) + F(y_i) - F(y_{i-1})\bigr].$$

6. Telescoped display: $F(OPT_0) - F(OPT_n) \le \tfrac12[F(x_n) - F(x_0)] + \tfrac12[F(y_n) - F(y_0)] \le \tfrac12(F(x_n) + F(y_n))$.

Significance

The result. Theorem A.1 shows that the double greedy analysis survives a change of domain: the factor $1/2$ is obtained by a procedure that never flips a coin until the end, and whose state is a pair of fractional points. The ratio matches the Feige–Mirrokni–Vondrák hardness bound, so it cannot be improved in the value oracle model. Its output is a fractional point together with an independent rounding, which separates the optimization from the rounding step.

Formalizing it. The result is proved on paper; no machine-checked proof of a double greedy guarantee is known. A complete development yields reusable facts about the multilinear extension of a submodular function on a finite type: $F$ is affine in each coordinate, its coordinate increments are antitone in the other coordinates on $[0,1]^{\mathcal N}$, and $F$ restricted to characteristic vectors is $f$. These are the standard tools of every continuous-relaxation argument for submodular maximization.

Difficulty

The proof on the page is short, but it relies on two facts it does not prove. First, the page justifies $a_i + b_i \ge 0$ "by Lemma II.1", which is a statement about sets; for vectors it requires that the increment of $F$ along a coordinate decreases as the other coordinates increase, a property of the multilinear extension of a submodular function that must be derived from the sum defining $F$. Second, inequality (6) is written out only for $u_i \notin OPT$, and Case 2 of Lemma A.2 is omitted as analogous; the formal statements cover all cases. The main technical work is the bookkeeping of the run: that each coordinate is touched once, that $x_{i-1}(u_i) = 0$ and $y_{i-1}(u_i) = 1$ when it is touched, that $x_i \le OPT_i \le y_i$, and that every state stays in $[0,1]^{\mathcal N}$, where the antitonicity applies.

Formalization scope

• The ground set is a Fintype $X$ with decidable equality; sets are Finset X; $f$ is real-valued, with nonnegativity a hypothesis ∀ S, 0 ≤ f S wherever the page uses it (the goal and the telescoped display). Submodularity is the published NonmonotoneSubmod.Shared.Submodular, the lattice form $f(S \cup T) + f(S \cap T) \le f(S) + f(T)$; $f(OPT)$ is the published NonmonotoneSubmod.Shared.OPT; $F$ is the published NonmonotoneSubmod.Shared.F, the sum above, defined for every $x : X \to \mathbb R$.
• The order $u_1, \dots, u_n$ is a duplicate-free list containing every element; $u_i$ is the entry at index $i-1$, and $n$ is the list's length. The state after $i$ iterations is obtained by folding one step over the first $i$ entries from $(\mathbf 0, \mathbf 1)$. Statements hold for every such order.
• The footnote's convention $a_i'/(a_i'+b_i') = 1$, $b_i'/(a_i'+b_i') = 0$ when $a_i' = b_i' = 0$ is an explicit case split; with Lean's $0/0 = 0$ it would otherwise be reversed and the run would no longer end with $x_n = y_n$.
• Corrected slips of the page: lines 3–4 of Algorithm 4 assign $a_i', b_i'$ but define $a_i, b_i$; "$f : \mathcal N \to \mathbb R^+$" means $f : 2^{\mathcal N} \to \mathbb R^+$; "$F(x) \triangleq \mathbb E[R(x)]$" means $\mathbb E[f(R(x))]$; "NSM" in Theorem A.1 means USM. The main text's one-line definition of submodularity, read literally, forces monotonicity; the footnote's lattice form is used.
• Not formalized: the sampling clause of Theorem A.1 (ratio $(1/2) - o(1)$ without oracle access to $F$, whose proof the paper refers to Calinescu, Chekuri, Pál and Vondrák) and the running time. The guarantee is stated for the algorithm as printed, so the trivial existence of a $1/2$-approximation by exhaustive search does not satisfy it. A statement in which $x_n$ is an arbitrary point, or the state any process with $x_i \le y_i$, would not be this theorem.
• Contributions welcome: the multilinear-extension facts above as general lemmas, the run invariants, and proofs of the milestones in any order.

Selected references

• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, FOCS 2012, 649–658. https://doi.org/10.1109/FOCS.2012.73 (journal version: SIAM J. Comput. 44(5), 2015, https://doi.org/10.1137/130929205; its numbering differs and is not used here).
• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-monotone Submodular Functions, SIAM J. Comput. 40(4), 2011, 1133–1153. https://doi.org/10.1137/090779346
• S. Oveis Gharan, J. Vondrák, Submodular Maximization by Simulated Annealing, SODA 2011, 1098–1117. https://doi.org/10.1137/1.9781611973082.83
• M. Feldman, J. Naor, R. Schwartz, Nonmonotone Submodular Maximization via a Structural Continuous Greedy Algorithm, ICALP 2011, 342–353. https://doi.org/10.1007/978-3-642-22006-7_29
• G. Calinescu, C. Chekuri, M. Pál, J. Vondrák, Maximizing a Monotone Submodular Function Subject to a Matroid Constraint, SIAM J. Comput. 40(6), 2011, 1740–1766. https://doi.org/10.1137/080733991

Why randomization matters in online algorithms

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

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

Request-answer games and competitive cost

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

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

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

Formalization targets

Randomization against adaptive off-line adversaries

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

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

Composition of two guarantees

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

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

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

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

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

What the result supplies

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

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

Why the proof is difficult

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

Formalization scope

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

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

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

Selected references

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

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

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

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

Setting

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 4.4 with its explicit constant

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

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

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

Timeline:

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

Setting

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

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

The proof uses three auxiliary problems:

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

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

Formalization targets

Goal: Theorem 8

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

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

Milestones

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

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

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

Significance

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

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

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

Difficulty

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

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

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

Formalization scope

Conventions committed to in Lean:

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

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

Out of scope:

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

Infrastructure that a complete development needs:

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

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

Selected references

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

Motivation

Learning an unknown quantum state is expensive. Full quantum state tomography of a $D$-dimensional mixed state $\rho$ to accuracy $\varepsilon$ in trace distance needs on the order of $D^2/\varepsilon^2$ copies of $\rho$ (O'Donnell–Wright 2016; Haah et al. 2017), and this is optimal. For a system of $n$ qubits, $D = 2^n$, so full tomography is out of reach beyond a few dozen qubits.

Often one does not need the whole density matrix, only the behaviour of $\rho$ on a fixed list of tests: acceptance probabilities of verification circuits, expectation values of observables, or the answers a piece of quantum advice gives to a set of questions. Aaronson (arXiv:1711.01053, STOC 2018) named this task shadow tomography and asked whether the number of copies can be polylogarithmic in both the dimension and the number of tests. Measuring each test on separate copies costs $\tilde O(M/\varepsilon^2)$ copies, which is linear in $M$.

Timeline.

• 2016: the question was posed at a mini-course without a name (Aaronson, The Complexity of Quantum States and Transformations, §8.3.1).
• 2016: Harrow, Lin and Montanaro gave a correct "quantum OR" test, repairing an earlier flawed claim (arXiv:1607.03236, Corollary 11).
• 2017–2018: Aaronson proved the first polylogarithmic bound, the theorem of this mission.
• Later work improved the exponents, notably Bădescu–O'Donnell 2021, and introduced the related "classical shadows" of Huang–Kueng–Preskill 2020.

Setting

A mixed state of dimension $D$ is a $D\times D$ Hermitian positive semidefinite matrix $\rho$ with $\mathrm{Tr}\,\rho = 1$. A two-outcome measurement is a $D\times D$ Hermitian matrix $E$ with all eigenvalues in $[0,1]$. Equivalently, $0 \preceq E \preceq \mathbb 1$. It accepts $\rho$ with probability $\mathrm{Tr}(E\rho)$.

The state $\rho^{\otimes k}$ consists of $k$ independent copies of $\rho$. A measurement of $\rho^{\otimes k}$ with classical output is a POVM: a finite family of positive semidefinite matrices $P_\omega$ on the $k$-register space with $\sum_\omega P_\omega = \mathbb 1$. Outcome $\omega$ occurs with probability $\mathrm{Tr}(P_\omega\rho^{\otimes k})$. An adaptive procedure that measures the copies one after another is described by one such POVM.

Problem 1 (shadow tomography). Given an unknown $\rho$ and known two-outcome measurements $E_1,\dots,E_M$, output numbers $b_1,\dots,b_M\in[0,1]$ with $|b_i-\mathrm{Tr}(E_i\rho)|\le\varepsilon$ for all $i$, with success probability at least $1-\delta$. The output must come from a measurement of $\rho^{\otimes k}$, with $k=k(D,M,\varepsilon,\delta)$ as small as possible. The measurement may depend on the $E_i$, but not on $\rho$.

Formalization targets

Goal: Theorem 2, in the explicit form proved in §5

There is a universal constant $C$ such that, for $M\ge2$ and $0<\varepsilon,\delta\le 1/2$, Problem 1 is solvable with

$$k \le C\,\frac{\log D}{\varepsilon}\Big(\frac{\log\log D+\log\frac1\varepsilon}{\varepsilon^{2}}\Big)^{2}\log^4 M\Big(\log\log M+\log\log D+\log\frac1\varepsilon+\log\frac1\delta\Big) = \tilde O\Big(\frac{\log 1/\delta}{\varepsilon^5}\log^4 M\log D\Big)$$

copies. This is the last display of the proof (p. 19). The goal fixes no constant, so any improvement of $C$ remains consistent with it.

Milestones

• Theorem 13 (Harrow–Lin–Montanaro). A one-copy test that accepts with probability at least $(1-\epsilon)^2/7$ if some $\mathrm{Tr}(E_i\rho)\ge1-\epsilon$, and at most $4\Delta M$ if $\sum_i\mathrm{Tr}(E_i\rho)\le\Delta M$.
• Lemma 14 (Quantum OR Bound). Deciding whether $\max_i\mathrm{Tr}(E_i\rho)\ge c$ or $\le c-\varepsilon$ with $O(\log(1/\delta)\log M/\varepsilon^2)$ copies, independent of $D$.
• Lemma 15 (Gentle Search). Finding $j$ with $\mathrm{Tr}(E_j\rho)\ge c-\varepsilon$ with $O(\frac{\log^4M}{\varepsilon^2}(\log\log M+\log\frac1\delta))$ copies.
• Amplification claims (p. 16). The threshold tests $E^*_{i,t,\pm}$ on $\rho^{\otimes q}$ accept with probability at least $5/6$ when the hypothesis is off by $\varepsilon$, and at most $1/3$ when it is within $\varepsilon/2$.
• Markov claim (p. 17). The postselection test $F_t$ on an arbitrary, possibly entangled, $q$-register state accepts with probability at most $\frac{a q}{(a+\varepsilon/4)q}$.
• Lemma 12 (Quantum Union Bound, probability part). Measurements each accepting with probability at least $1-\varepsilon$ all accept in succession with probability at least $1-2M\sqrt\varepsilon$.
• Chernoff claim (p. 18). $1-\mathrm{Tr}(F_t\rho^{\otimes q})\le\varepsilon^4/\log^2D$.
• Proposition 20. Promise-gap thresholds for all $i$ at once can be decided with $O(\log(M/\delta)/\varepsilon^2)$ copies.

Significance

The result. Theorem 2 shows that a state of exponential dimension can be learned "for all practical purposes" on exponentially many tests from polynomially many copies. Applications in the paper include a bound on quantum advice and one-way communication, and implications for quantum money and copy-protection. It also shows that the information needed to predict many measurement outcomes is far smaller than the description of $\rho$.

Formalizing it. The theorem is proved in the paper, and later work improves its exponents. As far as is known it has not been machine-checked. A complete development formalizes the gentle-measurement toolkit (Lemma 12, Lemma 14, Lemma 15), the amplification of two-outcome measurements on tensor powers, and the postselection argument. These are standard tools of quantum learning theory and quantum complexity with no formal counterpart yet. Lemma 14 and Lemma 15 are reusable beyond this mission.

Difficulty

The naive approach measures the $E_i$ directly on shared copies. A measurement that is likely to reject disturbs the state, so later measurements see a damaged state, and separate copies per measurement cost $M$ copies.

The proof needs three ingredients:

• a gentle search that finds a measurement on which the current hypothesis is wrong while damaging the copies only slightly;
• a potential argument showing that postselection cannot happen too often;
• a uniform control of the damage.

The potential argument has to hold for the state after postselection, which is correlated or entangled across registers. Independence-based concentration fails there, which is why the Markov claim, not a Chernoff bound, governs that step. Theorem 13 itself rests on a delicate ancilla-based procedure of Harrow, Lin and Montanaro, and the mission cites it as a milestone without its proof.

Formalization scope

• Representation.
  • Operators are complex matrices over a finite index type, and states use the published WildeQIT.IsDensityOperator (positive semidefinite, trace one).
  • A two-outcome measurement is IsEffect E: both $E$ and $\mathbb 1-E$ are positive semidefinite.
  • $\rho^{\otimes k}$ is a matrix indexed by $k$-tuples Fin k → n.
  • A measurement with output is a POVM structure with a finite outcome type. Probabilities are real parts of traces.
• Quantifier order of the goal. $\exists C$, then for all $D,M,\varepsilon,\delta$ there is $k$; then for all $E_i$ there are a POVM and outputs $b$; then for all $\rho$. Choosing the measurement after $\rho$ would make the goal trivial (output the true values with $k=0$), and this order rules that out.
• Disclosed hypotheses.
  • Theorem 2 assumes $M\ge2$, $\varepsilon\le1/2$ and $\delta\le1/2$. These keep the logarithmic factors positive; at $M=1$ the bound would force $k=0$.
  • Lemma 14 assumes $M\ge2$, and Lemmas 14 and 15 bound $\delta$.
  • Theorem 13 assumes $\epsilon\le1/2$, as in Harrow–Lin–Montanaro's Corollary 11.
  • The Chernoff claim assumes $D\ge2$.
• Conventions.
  • All logarithms are natural, including inside $\log\log$.
  • Amplified tests use real thresholds.
  • "Applied in succession" in Lemma 12 uses Lüders instruments ($\sqrt{E}$ Kraus operators), in the order $E_1,E_2,\dots$.
  • The hypothesis $\rho_t$ enters the amplification claims only as the number $a=\mathrm{Tr}(E\rho_t)$.
• Printed steps not drafted.
  • The printed $\varepsilon^{-4}$ form of Theorem 2 relies on an external online-learning algorithm that is only sketched.
  • The halting rule of §5 is unspecified, because Lemma 15 always returns an index.
  • The asymptotic claims $p_t\ge0.9/D^q$ for $t=o(\log^2D/\varepsilon^4)$ and $t=O(q\log D/\varepsilon)$ use a circular $o(\cdot)$.
  • The trace-distance part of Lemma 12 has an unquantified $O(\cdot)$.
  • Lemma 12's printed bound $1-2M\sqrt\varepsilon$ is weaker than its use on p. 18. It is stated as printed. The proof of the goal must retune constants or use Wilde's stronger $1-2\sqrt{M\varepsilon}$-type bound.
• Contributions welcome. Proofs of any milestone; a formal Hoeffding bound for binomial counts of product effects; the gentle measurement lemma for Lüders instruments; Naimark dilation for effects.

Selected references

• S. Aaronson, Shadow Tomography of Quantum States, STOC 2018; arXiv:1711.01053v2, 2018. https://arxiv.org/abs/1711.01053
• A. W. Harrow, C. Y.-Y. Lin, A. Montanaro, Sequential measurements, disturbance and property testing, SODA 2017. https://arxiv.org/abs/1607.03236
• M. M. Wilde, Sequential decoding of a general classical-quantum channel, Proc. R. Soc. A, 2013. https://arxiv.org/abs/1303.0808
• R. O'Donnell, J. Wright, Efficient quantum tomography, STOC 2016. https://arxiv.org/abs/1508.01907
• J. Haah, A. W. Harrow, Z. Ji, X. Wu, N. Yu, Sample-optimal tomography of quantum states, IEEE Trans. Inf. Theory, 2017. https://arxiv.org/abs/1508.01797
• C. Bădescu, R. O'Donnell, Improved quantum data analysis, STOC 2021. https://arxiv.org/abs/2011.10908
• H.-Y. Huang, R. Kueng, J. Preskill, Predicting many properties of a quantum system from very few measurements, Nature Physics, 2020. https://arxiv.org/abs/2002.08953

Motivation

Linear programming is usually described as "solvable in polynomial time", but that statement is about rational inputs given exactly. In Smale's list of problems for the 21st century (Smale 1998), Problem 9 asks for a polynomial-time algorithm over the reals deciding the feasibility of $Ax \ge y$, and Smale explicitly calls for "models which process approximate inputs and which permit round-off computations". Real data such as $\sqrt 2$, entries of a discrete cosine transform, or even $1/3$ in floating point can only be accessed approximately.

Bastounis, Hansen and Vlačić pose the extended Smale's 9th problem: in a model where the algorithm can only query approximations of the input to any requested accuracy, can one compute minimisers of linear programming, basis pursuit and Lasso to $K$ correct digits? Their Main Theorem I (Theorem 3.4) shows that the answer depends on $K$ in a sharp way: for a suitable class of well-conditioned, bounded inputs, no algorithm at all (not only no efficient one) produces $K$ correct digits, while $K-1$ digits are computable (but not in bounded time) and $K-2$ digits are computable in polynomial time.

This mission targets the first, impossibility, half of Theorem 3.4(i) for linear programming.

Setting

Linear program. For $A \in \mathbb R^{m\times N}$, $y\in\mathbb R^m$ and $c = \mathbf 1_N=(1,\dots,1)$, the solution set is

$$\Xi(y,A) = \operatorname*{argmin}_{x\in\mathbb R^N}\ \langle x, c\rangle \quad\text{subject to}\quad Ax = y,\ x\ge 0 .$$

It is a subset of $M_N = \mathbb R^N$ with the $\ell^p$ norm, $p\in[1,\infty]$. An input is a pair $\iota = (y,A)$, and the evaluations of $\iota$ are its coordinates $y_i$ and entries $A_{ij}$.

Extended model ($\Delta_1$-information). Let $D_n = \{k2^{-n} : k\in\mathbb Z\}$. An oracle representation of $\iota$ is a family $\tilde\iota = (\tilde\iota_{j,n})$, indexed by evaluations $j$ and accuracies $n = 1,2,\dots$, with $\tilde\iota_{j,n}\in D_n + iD_n$ and $|\tilde\iota_{j,n} - f_j(\iota)|\le 2^{-n}$. An algorithm must succeed on every oracle representation of every input.

General algorithm. To make impossibility results independent of the machine model, the paper uses general algorithms (Definition 9.3): a map $\Gamma$ from inputs to $M\cup\{\mathrm{NH}\}$ ($\mathrm{NH}$ = no output) together with a nonempty set $\Lambda_\Gamma(\iota)$ of evaluations read on $\iota$. This set is finite whenever $\Gamma$ halts. The output is determined by the values read, and any input that agrees on those values reads the same set. Turing machines and BSS machines with an oracle are special cases; general algorithms can even solve the halting problem.

Error and breakdown epsilon. The error is $\operatorname{dist}(\Gamma(\iota),\Xi(\iota)) = \inf_{\xi\in\Xi(\iota)} d(\Gamma(\iota),\xi)$, with distance $\infty$ from $\mathrm{NH}$. The strong breakdown epsilon $\varepsilon_B^s$ is the supremum of all $\varepsilon\ge 0$ such that every general algorithm has error $>\varepsilon$ on some input (Definition 9.17).

Formalization targets

Goal: Theorem 3.4(i), deterministic part, for LP

For every integer $K\ge1$, all dimensions $4\le m<N$ and every $p\in[1,\infty]$ there is a nonempty class $\Omega_{m,N}$ of inputs $(y,A)$ with nonempty solution sets, $\|y\|_\infty\le 2$ and $\|A\|_{\max}=1$, such that

$$\neg\,\exists\,\Gamma\ \text{general algorithm on oracle representations}:\quad \forall\,\tilde\iota,\ \ \operatorname{dist}_{\ell^p}\big(\Gamma(\tilde\iota),\,\Xi(\iota)\big)\le 10^{-K}.$$

Milestones

1. Lemma 11.1: the explicit solution sets of the LP inputs $(y_1e_1, A(\alpha,\beta,m,N))$.
2. Proposition 10.5 (ii), deterministic part: two input sequences that converge in evaluation to a common input and whose solutions stay $\kappa$ apart force $\varepsilon_B^s\ge\kappa/2$ for a suitable choice of $\Delta_1$-information.
3. §9.6, (i) ⇒ (ii): a lower bound on $\varepsilon_B^s$ for one specific $\Delta_1$-information transfers to the problem with all oracle representations.
4. Proposition 9.32 (i) (deterministic consequence via Proposition 10.1): $\varepsilon_B^s>10^{-K}$ for LP on a suitable $\Omega_{m,N}$.

Significance

The theorem shows that for LP with inexact input, being non-computable in Turing's sense does not rule out a finer complexity theory. The paper builds a "$K$ / $K-1$ / $K-2$ digits" classification on this. It also explains why established solvers can return wrong answers with a success flag on small, well-conditioned LPs (§4 of the paper), and it bears on computer-assisted proofs that rely on inexact LP, such as the Flyspeck proof of the Kepler conjecture.

The result is proved on paper. As far as the proposer knows, it has not been machine-checked. This mission formalizes the deterministic impossibility part for LP and puts in place reusable infrastructure: general algorithms, breakdown epsilons and $\Delta_1$-information. That infrastructure is the base for later missions on the randomised parts of Theorem 3.4(i)–(ii), the weak breakdown epsilon (iii), the exit-flag theorem (Theorem 5.1), and basis pursuit and Lasso.

Difficulty

The obvious objection is that LP is in P for rational inputs, so some rounding scheme ought to work. It fails because an algorithm must halt after reading finitely many approximations. Two inputs that agree to that accuracy but have minimisers far apart then receive the same output. Setting this up needs a notion of algorithm strong enough to cover every computational model, a precise $\Delta_1$-information model in which the adversary controls the approximations, and explicit LP geometry in which an arbitrarily small perturbation of $A$ moves the minimiser by a fixed amount.

Formalization scope

• Inputs are $(y,A)\in(\mathrm{Fin}\,m\to\mathbb R)\times\mathrm{Matrix}(\mathrm{Fin}\,m)(\mathrm{Fin}\,N)\,\mathbb R$. Evaluations are complex-valued, as in Definition 9.2. Outputs lie in PiLp p (Fin N → ℝ).
• A general algorithm is a structure with an output run : Ω → Option M (none = NH) and a read set queried, satisfying the axioms (i)–(iii) of Definition 9.3.
• Errors take values in $[0,\infty]$ (ℝ≥0∞), and the error of NH is $\infty$. The infimum over an empty solution set is $\infty$. The goal also requires nonempty solution sets, so no junk value enters.
• Oracle accuracies are indexed by $n\in\{1,2,\dots\}$ (ℕ+). An oracle input is stored as a pair (input, oracle family), and algorithms can read only the oracle family.
• Out of scope: randomised algorithms, the positive statements (iii)–(iv), runtime, and the condition-number bounds $\mathrm{Cond}(AA^*)\le3.2$, $C_{FP}\le4$, $\mathrm{Cond}(\Xi)\le179$.

Selected references

• A. Bastounis, A. C. Hansen, V. Vlačić, The extended Smale's 9th problem — On computational barriers and paradoxes in estimation, regularisation, computer-assisted proofs, and learning, preprint (2021).
• S. Smale, Mathematical problems for the next century, Math. Intelligencer 20 (1998). https://doi.org/10.1007/BF03025291