Probability

Motivation

Maximizing a nonnegative submodular set function without constraints contains Max Cut, Max Directed Cut and facility-location problems as special cases. In the value-oracle model an algorithm knows nothing about the function except the values $f(S)$ of the sets $S$ it queries, and it is judged by the number of queries it makes. Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011) gave constant-factor algorithms in this model and matching limits on what any algorithm can do. For symmetric functions, such as cut functions of undirected graphs, a uniformly random set already achieves $\tfrac12$ of the optimum in expectation (Theorem 2.1 of the paper). The question this mission formalizes is whether any algorithm can do better, and the answer given by Theorem 4.5 is: not without exponentially many value queries. The same factor $\tfrac12$ was later shown to be achievable for general (non-symmetric) nonnegative submodular functions by Buchbinder, Feldman, Naor and Schwartz (FOCS 2012 / SIAM J. Comput. 2015), so the bound of Theorem 4.5 is the tight limit of the whole problem in the value-oracle model.

Timeline:

• 2007 (FOCS) / 2011 (SIAM J. Comput.): Feige, Mirrokni and Vondrák prove that no algorithm with subexponentially many value queries achieves $(\tfrac12 + \epsilon)$ of the optimum on symmetric nonnegative submodular functions, and give $\tfrac25$ for general functions.
• 2011: Vondrák's symmetry-gap framework (SIAM J. Comput. 42(1), 2013) generalizes the construction to constrained problems.
• 2012: Buchbinder, Feldman, Naor and Schwartz give a randomized $\tfrac12$-approximation for general nonnegative submodular functions, matching the bound.

Setting

Let $[n] = \{0, \dots, n-1\}$ be the ground set, with $n$ even. A set function $f : 2^{[n]} \to \mathbb{R}$ is submodular if $f(S \cup T) + f(S \cap T) \le f(S) + f(T)$ for all $S, T$, symmetric if $f([n]\setminus S) = f(S)$ for all $S$, and $\mathrm{OPT}(f) = \max_{S} f(S)$.

Fix an integer $m$ with $1 \le m \le n/2$ and write $\epsilon = m/n$, so that $\epsilon n$ is an integer. For integers $k, \ell$ put

$$f(k,\ell) = \begin{cases} (k+\ell)(n-k-\ell) & |k-\ell| \le m,\\ k(n-2\ell) + (n-2k)\ell + m^2 - 2m|k-\ell| & |k-\ell| > m. \end{cases}$$

For a set $C \subseteq [n]$ with $|C| = n/2$ and $D = [n] \setminus C$, the hard instance is $f_C(S) = f(|S\cap C|, |S\cap D|)$. The cut function of the complete graph is $g(S) = |S|(n-|S|)$, with maximum $\tfrac14 n^2$. A set $Q$ is balanced for $C$ if $\bigl||Q\cap C| - |Q\cap D|\bigr| \le m$; on balanced sets $f_C = g$.

A deterministic adaptive $q$-query algorithm $A$ chooses each query from the answers received so far, and after $q$ answers outputs a set $A(h)$ when run against an oracle $h$. A randomized algorithm is a distribution $\mu$ over deterministic ones, with expected value $\mathbb{E}_{A\sim\mu}[h(A(h))]$.

Formalization targets

Goal: Theorem 4.5 with the constants of its proof

For every such $n, m$:

1. every $f_C$ with $|C| = n/2$ is nonnegative, symmetric and submodular, with

$$\mathrm{OPT}(f_C) = \tfrac12 n^2 (1 - 2\epsilon + 2\epsilon^2);$$

2. for every $q < e^{\epsilon^2 n/8}$ and every randomized $q$-query algorithm $\mu$ there is a $C$ with $|C| = n/2$ and

$$\mathbb{E}_{A\sim\mu}\bigl[f_C(A(f_C))\bigr] \le \tfrac14 n^2 + \bigl(2e^{-\epsilon^2 n/8} + 2e^{-\epsilon^2 n/4}\bigr)\,\mathrm{OPT}(f_C).$$

Hence the ratio attained is at most $\frac{1}{2(1-2\epsilon+2\epsilon^2)} + 4e^{-\epsilon^2 n/8} = \tfrac12 + \epsilon + O(\epsilon^2) + 4e^{-\epsilon^2 n/8}$.

Milestones

• Theorem 1.2, the Chernoff bound for independent variables in $[-1,1]$.
• Submodularity of $f_C$.
• The value $\mathrm{OPT}(f_C) = \tfrac12 n^2(1 - 2\epsilon + 2\epsilon^2)$, attained at $S = C$.
• A fixed query is unbalanced for at most a $2e^{-\epsilon^2 n/4}$ fraction of the half-size sets $C$.
• If all queries are balanced, the algorithm cannot distinguish $f_C$ from $g$.
• The deterministic case of the bound, averaged over $C$.

Significance

The theorem shows that the factor $\tfrac12$ for symmetric submodular maximization, and hence for unconstrained submodular maximization in general, cannot be improved by any algorithm that uses a subexponential number of value queries, whatever its running time. It is an information-theoretic bound and needs no complexity assumption. Along with the later matching $\tfrac12$-approximation, it settles the value-oracle approximability of the problem. The construction, a function equal to a symmetric function on "balanced" sets and larger elsewhere, is the prototype of the symmetry-gap technique used for many later oracle lower bounds.

The result is proved in the paper. No machine-checked version is known to exist: the platform has no value-oracle or query-lower-bound statement. Formalizing it requires a precise model of adaptive randomized query algorithms, a concentration bound for the hypergeometric distribution, and a finite verification of submodularity of an explicit two-regime function, and it fixes the constants that the printed statement leaves as $O(\cdot)$ terms.

Difficulty

Two steps of the printed argument do not go through as written. First, the proof bounds the probability that a fixed query is unbalanced by citing the Chernoff bound for independent variables, but for a uniformly random half-size set $C$ the count $|Q\cap C|$ is hypergeometric, and the summands are not independent. A bound for sampling without replacement is needed instead. Replacing the balanced partition by independent coin flips is not an option: then $|C| \ne n/2$ in general, and the function is no longer the paper's instance.

Second, the argument counts only the queries, but the value an algorithm receives is $f_C$ of its output, which equals $g$ of the output only if the output is balanced as well. That event has to be controlled too.

Finally, submodularity of $f_C$ must be checked across the boundary $|k-\ell| = \epsilon n$ between the two regimes, where the formula changes.

Formalization scope

• The ground set is Fin n with $n$ even; $\epsilon n$ is an integer $m$ with $1 \le m$ and $2m \le n$, following the paper's "assume that $\epsilon n$ is an integer". Sets are Finset (Fin n), and all values are real.
• $\mathrm{OPT}$ is Finset.sup' over all subsets. There is no junk value.
• The partition $(C, D)$ is uniform over half-size sets; probabilities over it are counts of n/2-subsets divided by $\binom{n}{n/2}$, written multiplied out.
• A deterministic algorithm is a pair of decision rules query, output : List ℝ → Finset (Fin n) making exactly $q$ adaptive queries with arbitrary real answers. A randomized algorithm is a PMF over deterministic algorithms, which covers every randomization with countable support. The algorithm sees $f$ only through query answers; it never receives $C$.
• Pinned-down constants. The printed theorem, "fewer than $e^{\epsilon^2 n/8}$ queries" and "expected value at least $(\tfrac12+\epsilon)\mathrm{OPT}$", is not what the proof gives for one and the same $\epsilon$. On the proof's instances $\mathrm{OPT} = \tfrac12 n^2(1-2\epsilon+2\epsilon^2)$, and the ratio held is $\frac{1}{2(1-2\epsilon+2\epsilon^2)} > \tfrac12 + \epsilon$. The formal goal states the explicit bound the proof establishes. The literal printed pair, stated for the proof's family with the same $\epsilon$, is false: the zero-query algorithm that outputs a fixed half-size set gets at least $\tfrac14 n^2 > (\tfrac12+\epsilon)\mathrm{OPT}$.
• Added term. The error term $2e^{-\epsilon^2 n/4}$ for the output set is added to the paper's $2e^{-\epsilon^2 n/8}$.
• Ruled-out trivializations. A restricted algorithm class (non-adaptive, deterministic, or one that must return a queried set) would give a different, weaker theorem. So would a bound that lets the algorithm read $C$, which would make the statement false. Both the instance's properties (nonnegativity, symmetry, submodularity, the value of OPT) and the bound are part of the goal, so an empty or degenerate family cannot satisfy it. The quantifier order is: for every algorithm there is an instance.
• Needed infrastructure: a value-oracle algorithm model; tail bounds for the hypergeometric distribution (Hoeffding's inequality for sampling without replacement), which Mathlib lacks; averaging over a PMF of algorithms. The algorithm model and the hypergeometric bound are reusable for other oracle lower bounds. Proofs of any milestone, and alternative derivations of the balance bound, are welcome.

Selected references

• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM J. Comput. 40(4):1133–1153, 2011. https://doi.org/10.1137/090779346
• N. Alon, J. H. Spencer, The Probabilistic Method, Wiley (source of Theorem 1.2).
• W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, J. Amer. Statist. Assoc. 58(301):13–30, 1963. https://doi.org/10.1080/01621459.1963.10500830
• J. Vondrák, Symmetry and Approximability of Submodular Maximization Problems, SIAM J. Comput. 42(1):265–304, 2013. https://doi.org/10.1137/110832318
• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM J. Comput. 44(5):1384–1402, 2015. https://doi.org/10.1137/130929205

Motivation

Many optimization problems ask for a subset of a finite ground set that maximizes a submodular function, a set function with diminishing marginal returns. Max Cut and Max Directed Cut in graphs, facility location with fixed costs, and the maximization of mutual information or entropy of a subset of random variables are all of this form. Unlike the monotone case, where a greedy algorithm achieves $1 - 1/e$, a general nonnegative submodular function may decrease when elements are added, and the empty set and the full set can both be poor. The question is how large a constant fraction of the optimum a polynomial-time algorithm can guarantee when the function is given only through an oracle that returns $f(S)$ for a queried set $S$.

Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011) gave the first constant-factor algorithms for this problem. A uniformly random set achieves $1/4$ of the optimum, a deterministic local search achieves $1/3 - \epsilon/n$, and a randomized smooth local search achieves $2/5 - o(1)$. The last result is the paper's best approximation for general nonnegative submodular functions (Table 1, p. 1136), and it is the subject of this mission.

Timeline. Feige, Mirrokni and Vondrák: $1/4$, $1/3$ and $2/5$ (FOCS 2007; journal version 2011). Gharan and Vondrák (SODA 2011): about $0.41$ by simulated annealing. Buchbinder, Feldman, Naor and Schwartz (FOCS 2012; SIAM J. Comput. 2015): a randomized double greedy algorithm achieving $1/2$, which matches the $1/2$ hardness in the value oracle model proved in the same paper by Feige, Mirrokni and Vondrák.

Setting

Let $X$ be a finite ground set with $n = |X| \ge 1$ elements and $f : 2^X \to \mathbb{R}$ a function with $f(S) \ge 0$ for all $S$ and

$$f(S \cup T) + f(S \cap T) \le f(S) + f(T) \quad (S, T \subseteq X).$$

Write $OPT = \max_{S \subseteq X} f(S)$. The multilinear extension of $f$ is

$$F(x) = \sum_{S \subseteq X} f(S) \prod_{i \in S} x_i \prod_{j \notin S} (1 - x_j),$$

the expected value of $f$ on a random set containing each $i$ independently with probability $x_i$.

For $A \subseteq X$ and $\delta \in [-1,1]$, the random set $\mathcal{R}(A,\delta)$ is sampled with bias $\delta$ based on $A$: each element of $A$ is included independently with probability $p = (1+\delta)/2$, each element of $B = X \setminus A$ with probability $q = (1-\delta)/2$. The potential is $\Phi(A) = \mathbf{E}[f(\mathcal{R}(A,\delta))]$ and the smoothed marginal value of $x$ is

$$\omega_{A,\delta}(x) = \mathbf{E}[f(\mathcal{R}(A,\delta) \cup \{x\})] - \mathbf{E}[f(\mathcal{R}(A,\delta) \setminus \{x\})].$$

Algorithm SLS starts from $A = \emptyset$. At each iteration it obtains estimates $\tilde\omega_{A,\delta}(x)$ within $\pm\frac{1}{n^2}OPT$ of $\omega_{A,\delta}(x)$. If some $x \notin A$ has $\tilde\omega_{A,\delta}(x) > \frac{2}{n^2}OPT$ it adds $x$; otherwise, if some $x \in A$ has $\tilde\omega_{A,\delta}(x) < -\frac{2}{n^2}OPT$ it removes $x$; otherwise it stops and returns a random set $\mathcal{R}(A, \delta')$.

Formalization targets

Goal: Theorem 3.6 in the explicit form of its proof

With $\delta = 1/3$, and $\delta' = 1/3$ with probability $0.9$ or $\delta' = -1$ with probability $0.1$: for every run from $\emptyset$ whose estimates are all accurate and which has terminated at $A$,

$$\tfrac{9}{10}\,\mathbf{E}[f(\mathcal{R}(A,\tfrac13))] + \tfrac{1}{10}\,f(X \setminus A) \ge \Big(\frac{2}{5} - \frac{9}{5n}\Big) OPT,$$

and, for every $\delta \in (0,1]$, every run of $k$ iterations with accurate estimates has $k < n^2/\delta$ (fewer than $3n^2$ for $\delta = 1/3$).

Milestones, in attack order

• Lemma 2.2: $\mathbf{E}[g(A(p))] \ge (1-p)g(\emptyset) + p\,g(A)$.
• Display (∗): for three independently sampled sets, $\mathbf{E}[f(A_1(p_1) \cup A_2(p_2) \cup A_3(p_3))] \ge \sum_{I \subseteq \{1,2,3\}} \prod_{i\in I} p_i \prod_{i \notin I}(1-p_i) f(\bigcup_{i \in I} A_i)$.
• The increment identity $\Phi(A \cup \{x\}) - \Phi(A) = \delta\,\omega_{A,\delta}(x)$ for $x \notin A$, and its removal counterpart.
• $0 \le \Phi(A) \le OPT$.
• The terminal upper estimates $\mathbf{E}[f(R \cup (B\cap C))],\ \mathbf{E}[f(R \cap (B \cup C))] \le \mathbf{E}[f(R)] + \frac{2}{n}OPT$.
• The two lower bounds in $27$ths on the same two expectations.
• The final chain $\mathbf{E}[f(R)] + \frac19 f(B) + \frac2n OPT \ge \frac49 OPT$.

Significance

The $2/5$ bound showed that local search on a smoothed objective, the multilinear extension restricted to points with two coordinate values, beats both uniform sampling and plain local search for non-monotone submodular maximization. The multilinear extension later became the standard tool for submodular maximization under constraints, through continuous greedy methods, contention resolution schemes and the analysis of randomized rounding. Display (∗) and Lemma 2.2 are the basic sampling inequalities for submodular functions and are reused throughout that literature.

The result is proved in the paper; it has been superseded in ratio by later algorithms reaching $1/2$. To our knowledge none of it is machine-checked: Mathlib has no multilinear extension and no submodular maximization results. This mission produces a checked form of the analysis with every constant explicit: the $o(1)$ as $\frac{9}{5n}$, "polynomial time" as $n^2/\delta$ iterations, and the dependence on the accuracy of the sampled estimates as an explicit hypothesis.

Difficulty

The iteration bound and the increment identity are routine once the multilinear extension is set up. The substance lies in the lower bounds. The returned set $R$ is random, so the comparison with the optimal set $C$ cannot be made through a single local-optimality inequality as in deterministic local search; and approximate local optimality holds only for the smoothed marginals $\omega_{A,\delta}$, which are averages over the random set, not for $f$ at any fixed set. Sampling inequalities such as (∗) are stated for independent samples of arbitrary, possibly overlapping sets, and their expectations are sums over products of subsets; the bookkeeping of such sums is the main formalization burden. The constants must also balance exactly: with $\delta = 1/3$ the $27$ths add up so that the $\frac{9}{10}/\frac{1}{10}$ mixture yields $2/5$. A different split or a different $\delta$ gives a different constant.

Formalization scope

The ground set is a Fintype X with decidable equality; sets are Finset X; $f$ is real valued, with nonnegativity and submodularity as hypotheses. The standing assumptions of the paper are made explicit: $f \ge 0$ (§3), value-oracle access (modelled by $f$ itself), $n = |X|$, and $n \ge 1$ (Nonempty X), so that $\frac{1}{n^2}$ and $\frac{9}{5n}$ are not Lean's junk value of division by zero. $OPT$ is Finset.sup' over all subsets, which has no junk value. Every expectation over independently sampled sets is an exact finite sum: the multilinear extension for $\mathcal{R}(A,\delta)$, and iterated sums over subsets for the several independent samples in Lemma 2.2 and (∗). Sampling probabilities carry $0 \le p \le 1$.

The algorithm is a relation, not a choice: any element meeting the step-3 condition may be added, and removal is allowed only when no addition applies. The goal quantifies over every run from $\emptyset$, every choice of accurate estimates, recomputed at every iteration, and every termination point. Accuracy is non-strict ("within $\pm$"); the thresholds are strict. The thresholds and accuracy use $OPT$ itself, as the proof does, although step 1 of the algorithm says an estimate of $OPT$ is used. The sampling that produces the estimates and its "with high probability" are not modelled, and the goal is conditional on accurate estimates. The value of the $\delta' = -1$ branch is written as $\mathbf{E}[f(\mathcal{R}(A,-1))]$, which equals $f(X \setminus A)$.

A statement "every $A$ satisfying the terminal conditions gives $2/5 - 9/(5n)$" would be the final milestone plus arithmetic and is not the goal. The goal fixes the start at $\emptyset$, the thresholds, the step order, the accuracy of every estimate, termination and the $0.9/0.1$ mixture.

A complete development needs basic calculus of the multilinear extension: affinity in one coordinate, translation $f(\cdot \cup D)$ and restriction $f(\cdot \cap D)$, and splitting a sample into disjoint pieces. These lemmas are reusable for any work on submodular maximization, and contributions of them as separate theorems are welcome. The golden-ratio variant $\delta = \delta'$ (proof omitted in the paper), the tight example and the hardness results of §4 are out of scope.

Selected references

• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM J. Comput. 40(4):1133–1153, 2011. https://doi.org/10.1137/090779346
• S. O. Gharan, J. Vondrák, Submodular Maximization by Simulated Annealing, SODA 2011. https://doi.org/10.1137/1.9781611973082.83
• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM J. Comput. 44(5):1384–1402, 2015. https://doi.org/10.1137/130929205
• 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):1740–1766, 2011. https://doi.org/10.1137/080733991

Motivation

Many computations need the trace of a matrix $A$ that is never formed explicitly and can only be applied to vectors: the trace of a matrix function such as $\mathrm{trace}(A^{-1})$ or $\log\det A = \mathrm{trace}(\log A)$ in statistics and lattice QCD, the Frobenius norm $\|B\|_F^2 = \mathrm{trace}(B^TB)$ of an operator, or the number of triangles of a graph. The standard tool is Monte-Carlo estimation, introduced by M. F. Hutchinson (Hutchinson 1989): average $M$ quadratic forms $z_i^TAz_i$ over random sign vectors $z_i$. Each sample costs one matrix–vector product, uses one random bit per entry, and needs only additions and subtractions.

Before Avron and Toledo (2011), only the variance of such estimators had been analysed. A small variance does not say how many samples guarantee a given relative error with a given probability. Avron and Toledo gave the first bounds of this kind for several estimators. This mission covers the bound for Hutchinson's estimator, their Theorem 7.1.

Setting

A Rademacher random variable takes the values $+1$ and $-1$, each with probability $1/2$. Let $A \in \mathbb{R}^{n\times n}$ be symmetric positive semi-definite. Draw $M \ge 1$ independent random vectors $z_1, \ldots, z_M \in \mathbb{R}^n$ whose $Mn$ entries are independent Rademacher variables. Hutchinson's trace estimator is

$$H_M = \frac{1}{M}\sum_{i=1}^{M} z_i^TAz_i .$$

A single sample $z^TAz$ is an unbiased estimator of $\mathrm{trace}(A)$ (Lemma 2.1 of the paper, due to Hutchinson). For symmetric $A$ its variance is $2\bigl(\|A\|_F^2 - \sum_i A_{ii}^2\bigr)$, twice the squared Frobenius mass of $A$ off the diagonal.

Given $\epsilon > 0$ and $\delta \in (0,1)$, a random estimator $T$ is an $(\epsilon,\delta)$-approximator of $\mathrm{trace}(A)$ if

$$\Pr\bigl(|T - \mathrm{trace}(A)| \le \epsilon\,\mathrm{trace}(A)\bigr) \ge 1 - \delta .$$

The rank $\mathrm{rank}(A)$ is the number of nonzero eigenvalues $\lambda_j$ of $A$, counted with multiplicity.

Formalization targets

Goal: Theorem 7.1, sample bound for $H_M$

For every symmetric positive semi-definite $A$, every $0 < \epsilon \le 1/2$ and every $0 < \delta < 1$,

$$M \ge 6\epsilon^{-2}\ln\!\left(\frac{2\,\mathrm{rank}(A)}{\delta}\right) \quad\Longrightarrow\quad H_M \text{ is an } (\epsilon,\delta)\text{-approximator of } \mathrm{trace}(A).$$

The bound depends on $A$ only through its rank. It does not depend on the dimension $n$, on the condition number, or on how the trace is spread over the diagonal.

Milestones

1. Lemma 7.2 (Achlioptas 2001, Lemma 5). For a unit vector $\alpha \in \mathbb{R}^n$ and $S = \frac1M\sum_{i=1}^M(\alpha^Tz_i)^2$, for every $\epsilon > 0$,

$$\Pr(|S - 1| \ge \epsilon) \le 2\exp\!\left(-\frac{M}{2}\left(\frac{\epsilon^2}{2} - \frac{\epsilon^3}{3}\right)\right).$$

2. Per-direction bound (proof of Theorem 7.1, p. 8:11). Let $r \ge 1$ and $0 < \epsilon \le 1/2$. If $M \ge 6\epsilon^{-2}\ln(2r/\delta)$, then $\Pr(|S - 1| \ge \epsilon) \le \delta/r$.
3. From directions to the trace (proof of Theorem 7.1, p. 8:11). Write $A = U\Lambda U^T$ and $y_i = U^Tz_i$. If $|\frac1M\sum_i y_{ij}^2 - 1| \le \epsilon$ for every $j$ with $\lambda_j \ne 0$, then $|H_M - \mathrm{trace}(A)| \le \epsilon\,\mathrm{trace}(A)$. This step is deterministic.
4. Lemma 2.1 (Hutchinson). $\mathrm{E}(z^TAz) = \mathrm{trace}(A)$, and for symmetric $A$, $\mathrm{Var}(z^TAz) = 2(\|A\|_F^2 - \sum_i A_{ii}^2)$.

Significance

Theorem 7.1 gives a practitioner an explicit number of matrix–vector products after which Hutchinson's method is guaranteed to reach relative accuracy $\epsilon$ with confidence $1-\delta$. No bound was available before, although the method had been in wide use for two decades. The bound exceeds the one the same paper proves for Gaussian test vectors ($20\epsilon^{-2}\ln(2/\delta)$) by a $\ln(\mathrm{rank}(A))$ factor. The authors conjecture that this factor is not needed. Later work removed it: Roosta-Khorasani and Ascher (2015) proved a rank-free bound for the Rademacher case, and Cortinovis and Kressner (2022) extended sample bounds to indefinite matrices. Sample bounds of this type underlie variance-reduced estimators such as Hutch++ (Meyer et al. 2021).

The theorem is proved in the literature. To the platform's knowledge it has no machine-checked proof. Formalizing it produces a checked Rademacher concentration inequality for averages of squared linear forms (Achlioptas' lemma, which is also a core lemma of database-friendly Johnson–Lindenstrauss projections), and a checked spectral reduction from a quadratic-form estimator to its eigen-directions. Neither is currently in Mathlib.

Difficulty

The estimator is not an average of independent copies of a bounded variable with a small range: a single sample $z^TAz$ can deviate from $\mathrm{trace}(A)$ by an amount comparable to $\|A\|_F\sqrt n$. Chebyshev's inequality with the variance of Lemma 2.1 only gives a polynomial dependence on $1/\delta$. Hoeffding's inequality applied to $z^TAz$ directly gives a dependence on $n$ and on the size of the entries of $A$. Unlike the Gaussian case, the estimator cannot be written as a weighted sum of independent chi-squared variables, because rotating a Rademacher vector does not give another Rademacher vector. The central difficulty is Lemma 7.2: a tail bound for $(\alpha^Tz)^2$ that holds uniformly over every unit direction $\alpha$, including directions in which $\alpha^Tz$ is far from Gaussian (for $\alpha = e_1$ it is a constant).

Formalization scope

Matrices are Matrix (Fin n) (Fin n) ℝ, and positive semi-definiteness is Matrix.PosSemidef. The Rademacher law is $\tfrac12(\delta_1 + \delta_{-1})$ on ℝ. The sample space is Fin M → Fin n → ℝ with the product of $Mn$ copies of this law (hutchinsonSampleMeasure), so the law of the estimator is constructed, not assumed. $H_M(\omega) = (M:\mathbb{R})^{-1}\sum_i \omega_i\cdot(A\omega_i)$. Probabilities are Measure.real, and the $(\epsilon,\delta)$-approximator is Definition 4.1 verbatim. $\mathrm{rank}(A)$ is Matrix.rank. In Lemma 7.2 the i.i.d. copies $Q_i$ are the functions $(\alpha\cdot z_i)^2$ on this product space.

Corrections of printed statements, each recorded in the item's Formalization Note:

• Theorem 7.1 is printed without a range on $\epsilon$. Its proof needs $\frac{M}{2}(\frac{\epsilon^2}{2} - \frac{\epsilon^3}{3}) \ge \frac{M\epsilon^2}{6}$, which holds exactly when $\epsilon \le 1/2$. Without a range the printed statement is false: take $A = \frac1n\mathbf 1\mathbf 1^T$, $n = 10^4$, $\epsilon = 10$ and $\delta = 10^{-4}$. The condition admits $M = 1$, while $\Pr(H_1 > 11) \approx 9\cdot10^{-4} > \delta$. The goal and milestone 2 are therefore stated for $0 < \epsilon \le 1/2$.
• Lemma 2.1 is printed for an arbitrary $n\times n$ matrix. The variance formula fails for non-symmetric $A$: for $A = \begin{pmatrix}0&1\\0&0\end{pmatrix}$ the variance is $1$, not $2$. Symmetry is assumed for the variance part only.
• Proof of Theorem 7.1. The proof writes $\Lambda = UAU^T$ together with $y_i = U^Tz_i$. These fit together only for $A = U\Lambda U^T$, which is the convention of milestone 3.

For $A = 0$ the threshold involves $\ln 0$. Lean's Real.log 0 = 0 turns the condition into $M \ge 0$, which agrees with the paper's reading $\ln 0 = -\infty$. The conclusion then holds because $H_M = \mathrm{trace}(A) = 0$, so no extra hypothesis is added. A formalization that took the law of the samples as a hypothesis could make that hypothesis unsatisfiable and the theorem vacuous; the constructed product space rules this out.

A complete development needs:

• the product Rademacher measure and moment generating functions of Rademacher sums;
• a Chernoff bound for averages of i.i.d. bounded variables on a product space;
• the spectral theorem for real symmetric matrices, with rank equal to the number of nonzero eigenvalues;
• a finite union bound.

The Rademacher concentration results are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of Lemma 7.2.

Selected references

• H. Avron and S. Toledo, Randomized algorithms for estimating the trace of an implicit symmetric positive semi-definite matrix, Journal of the ACM 58(2), Article 8, 2011. https://doi.org/10.1145/1944345.1944349
• M. F. Hutchinson, A stochastic estimator of the trace of the influence matrix for Laplacian smoothing splines, Communications in Statistics – Simulation and Computation 18(3), 1059–1076, 1989. https://doi.org/10.1080/03610918908812806
• D. Achlioptas, Database-friendly random projections, Proceedings of PODS 2001, 274–281. https://doi.org/10.1145/375551.375608
• F. Roosta-Khorasani and U. Ascher, Improved bounds on sample size for implicit matrix trace estimators, Foundations of Computational Mathematics 15, 1187–1212, 2015. https://doi.org/10.1007/s10208-014-9220-1
• A. Cortinovis and D. Kressner, On randomized trace estimates for indefinite matrices with an application to determinants, Foundations of Computational Mathematics 22, 875–903, 2022. https://doi.org/10.1007/s10208-021-09525-9
• R. A. Meyer, C. Musco, C. Musco and D. P. Woodruff, Hutch++: Optimal stochastic trace estimation, SOSA 2021, 142–155. https://doi.org/10.1137/1.9781611976496.16

Motivation

A Markov Decision Model (MDM) formalizes sequential decision-making under uncertainty: a controller observes the current state of a system, chooses an action, receives a reward, and the system moves to a new (random) state whose law depends on the current state and action. This framework underlies dynamic programming across operations research, economics, and engineering — inventory control, sequential portfolio choice, queueing control, and reinforcement learning are all instances of it. The finite-horizon theory developed here is the foundation on which every later chapter of Bäuerle and Rieder's Markov Decision Processes with Applications to Finance (Springer, 2011) builds, including the infinite-horizon, partially observed, and optimal-stopping variants treated later in the book.

The classical treatment of dynamic programming for finite state and action spaces goes back to Bellman (1957) and is standard textbook material (see e.g. Puterman, Markov Decision Processes, 1994). The generalization to Borel state and action spaces — needed as soon as a state variable is continuous, as in almost every financial application — requires genuine measure-theoretic care: suprema over an infinite (even uncountable) action set need not be attained, and the resulting value function need not be measurable. Bertsekas and Shreve's Stochastic Optimal Control: The Discrete Time Case (1978) is the classical reference for this general theory; Bäuerle and Rieder's treatment isolates the exact abstract hypothesis — the Structure Assumption (SAN) below — under which the finite-horizon theory goes through cleanly, separating the recursive (Bellman) machinery from the case-by-case verification of when it applies.

Setting

A Markov Decision Model with planning horizon $N \in \mathbb{N}$ consists of a state space $E$ and action space $A$ (measurable spaces), and, for each stage $n = 0,\dots,N-1$: a measurable set $D_n \subseteq E \times A$ of admissible state-action pairs (containing the graph of some measurable selection $E \to A$); a stochastic transition kernel $Q_n(\cdot \mid x,a)$ giving the law of the next state; a measurable one-stage reward $r_n : D_n \to \mathbb{R}$; and a terminal reward $g_N : E \to \mathbb{R}$.

A decision rule at time $n$ is a measurable $f_n : E \to A$ with $f_n(x) \in D_n(x) := \{a : (x,a) \in D_n\}$ for every $x$; an $N$-stage policy $\pi = (f_0,\dots,f_{N-1})$ is a sequence of such rules. Given $\pi$ and an initial state $x$ at time $n$, the process evolves as a (non-stationary) Markov chain, and the value of $\pi$ is the expected total reward

$$V_n^\pi(x) := \mathbb{E}^\pi_{n,x}\!\left[\sum_{k=n}^{N-1} r_k\bigl(X_k, f_k(X_k)\bigr) + g_N(X_N)\right],$$

with value function $V_n(x) := \sup_\pi V_n^\pi(x)$, the best attainable expected reward. A policy is optimal if $V_0^\pi = V_0$. Write $\mathrm{IM}(E)$ for the measurable functions $E \to [-\infty,\infty)$ (never $+\infty$), and define, for $v \in \mathrm{IM}(E)$, the one-step operators $L_n v(x,a) := r_n(x,a) + \int v(x')\, Q_n(dx' \mid x,a)$, $T_n^f v(x) := L_n v(x, f(x))$, and $T_n v(x) := \sup_{a \in D_n(x)} L_n v(x,a)$. A decision rule $f$ is a maximizer of $v$ at time $n$ if $T_n^f v = T_n v$.

Formalization targets

Goal: Theorem 2.3.8 (the Structure Theorem)

Under the Structure Assumption (SAN) — the existence of sets $\mathrm{IM}_n \subseteq \mathrm{IM}(E)$, $\Delta_n \subseteq F_n$ with $g_N \in \mathrm{IM}_N$, $T_n$ mapping $\mathrm{IM}_{n+1}$ into $\mathrm{IM}_n$, and every $v \in \mathrm{IM}_{n+1}$ admitting a maximizer in $\Delta_n$ — the value function satisfies the Bellman equation $V_n = T_n V_{n+1}$ (with $V_n \in \mathrm{IM}_n$), and every sequence of maximizers of $V_1,\dots,V_N$ defines an optimal policy. This is the weakest level at which the theorem holds: it names an abstract structural hypothesis rather than a specific sufficient condition (e.g. compactness plus semicontinuity, treated in a later mission), so any future refinement of sufficient conditions for (SAN) leaves this statement untouched.

Significance

Reducing an $N$-stage optimization over an infinite-dimensional policy space to $N$ one-stage optimizations — literally the content of the Bellman equation — is what makes dynamic programming computationally and theoretically tractable at all. For finite state and action spaces this reduction is elementary (a supremum over a finite set is always attained); the content of the Structure Theorem is doing this correctly when $E$, $A$ are general Borel spaces, where existence of the supremum and of a measurable maximizing selection are not automatic and must be assumed abstractly.

Formalizing this theorem produces machine-checked statements of the finite-horizon Bellman equation and verification theorem in the generality actually used throughout the book's finance applications (wealth is real-valued, portfolios are vector-valued — never finite sets). The statement, proof, and every hypothesis are original to this textbook chapter; no formalized version of this general-Borel-space theory exists on the platform. The closest prior art, finite state-and-action-space Bellman equations and verification theorems (e.g. discounted infinite-horizon and stochastic-shortest-path theorems for finite MDPs), is a strictly weaker special case in which the Structure Assumption's existence-of-maximizer clause is automatic; this mission's goal is not restated as a reference to that prior art; the generalization is exactly the mission's content.

Difficulty

The obvious first attempt — prove $V_n = T_n V_{n+1}$ directly from the definitions of $V_n$ and $V_n^\pi$ — runs into two separate obstructions that (SAN) is built to bypass simultaneously. First, $\sup_\pi V_n^\pi(x)$ and $\sup_{a \in D_n(x)} L_n V_{n+1}(x,a)$ are a priori different suprema (over policies versus over actions), and showing they agree requires that the pointwise supremum over decision rules $f \in F_n$ of $L_n V_{n+1}(x, f(x))$ equals the supremum over bare actions $a \in D_n(x)$ — which needs a measurable selection achieving (or approaching) the action-wise optimum, not just its existence pointwise. Second, $V_{n+1}$ itself must be shown measurable — an a priori supremum of measurable functions over an uncountable index set (all policies) need not be measurable — before the integral $\int V_{n+1}\, dQ_n$ even makes sense. (SAN)'s three clauses are exactly what supplies both a well-behaved measurability class $\mathrm{IM}_n$ closed under $T_n$ and a measurable maximizing selection at every stage, letting a backward induction on $n$ establish both facts together.

Formalization scope

State and action spaces are arbitrary measurable spaces (MeasurableSpace E, MeasurableSpace A type classes), not restricted to Borel subsets of Polish spaces, since none of this mission's statements use topology. Time is indexed by ℕ rather than Fin N, with n < N as an explicit side condition throughout (documented in MODERATION_NOTES.md); this changes no content but avoids Fin-cast noise in the several backward recursions the chapter's operators require. Extended-real values (EReal) are used throughout for value functions, restricted by hypothesis to never equal $+\infty$, matching $\mathrm{IM}(E) := \{v : E \to [-\infty,\infty)\}$ exactly; a formalization using plain ℝ-valued value functions would be a strictly stronger — and unfaithful — claim, since it silently assumes no policy can drive the expected reward to $-\infty$.

The mission does not construct the canonical path measure on the full trajectory space via the Ionescu–Tulcea theorem; the value of a policy is instead built as an explicit backward accumulator recursion over the model's one-step kernels, which computes the same quantity by the tower property of conditional expectation. Definitions 2.1.1, 2.1.5, 2.2.2, 2.3.1, and 2.3.6 — the Markov Decision Model, (Markov and history-dependent) policies, and the operators — are restated from scratch in this mission's own namespace, since drafts in this series cannot import one another; later missions in the same series restate the same vocabulary independently. A trivializing formalization of the goal would state $V_n$ as an unspecified object merely postulated to satisfy the Bellman equation (Theorem 2.3.7's weaker claim) rather than as the supremum-over-policies value function fixed before the theorem — this mission states the latter.

Selected references

• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. DOI: 10.1007/978-3-642-18324-9.
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete Time Case, Academic Press, 1978.
• K. Hinderer, Foundations of Non-stationary Dynamical Programming with Discrete Time Parameter, Lecture Notes in Operations Research and Mathematical Systems 33, Springer, 1970.
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994.

Motivation

Many matrices in scientific computing are available only implicitly: one can multiply a vector by $A$, for instance by solving a linear system or applying a matrix function, but the entries of $A$ are never formed. Quantities such as the trace must then be estimated from a small number of matrix–vector products. Randomized trace estimators do exactly this: draw random vectors $z$, compute the quadratic forms $z^TAz$, and average.

Avron and Toledo (J. ACM 58(2), 2011) gave the first sample bounds of the form "$M$ samples suffice for relative error $\epsilon$ with probability $1-\delta$" for the standard estimators. Among their results is a case in which the estimate is not merely approximate but exact: when $A$ is a projection matrix, its trace equals its rank, an integer, and rounding a Gaussian trace estimate recovers that integer with high probability. Computing the rank of a projection arises, for example, when charge densities are computed in electronic structure calculations without diagonalization (Bekas, Kokiopoulou and Saad 2007).

Setting

Let $n \ge 1$ and $A \in \mathbb{R}^{n\times n}$. A projection matrix here is an orthogonal projection: $A$ is symmetric and $A^2 = A$. Equivalently, $A$ is symmetric and every eigenvalue of $A$ is $0$ or $1$; its rank $\mathrm{rank}(A)$ is the number of eigenvalues equal to $1$.

Fix a number of samples $M \ge 1$. Let $z_1,\ldots,z_M \in \mathbb{R}^n$ be random vectors whose $Mn$ entries are independent standard normal random variables. The Gaussian trace estimator (Definition 3.1 of the paper) is

$$G_M = \frac{1}{M}\sum_{i=1}^{M} z_i^T A z_i .$$

Its expectation is $\mathrm{trace}(A)$. For $x \in \mathbb{R}$, $\mathrm{round}(x)$ denotes the nearest integer to $x$. For $k \ge 1$, a random variable $X$ has the $\chi^2$ distribution with $k$ degrees of freedom, $X \sim \chi^2(k)$, if it has the law of $g_1^2 + \cdots + g_k^2$ for independent standard normal $g_1, \ldots, g_k$.

Formalization targets

Goal: Lemma 5.3 (p. 8:9)

For a projection matrix $A$, a failure probability $\delta > 0$, and every integer $M \ge 1$ with $M \ge 24\,\mathrm{rank}(A)\ln(2/\delta)$,

$$\Pr\bigl(\mathrm{round}(G_M) \ne \mathrm{rank}(A)\bigr) \le \delta .$$

The number of samples depends on the rank and on $\delta$ only; there is no accuracy parameter, and none on $n$.

Milestones, in the order the proof uses them

1. Law of $MG_M$. $MG_M \sim \chi^2(M\,\mathrm{rank}(A))$.
2. $\chi^2$ tail bound (cited by the paper from Li, Hastie and Church 2007). For $X \sim \chi^2(k)$, $k\ge1$ and $0 < \epsilon \le \tfrac12$,

$$\Pr(|X - k| \ge \epsilon k) \le 2\exp(-k\epsilon^2/6).$$

3. Tail of $G_M$. For $\mathrm{rank}(A) \ge 1$ and $0 < \epsilon \le \tfrac12$,

$$\Pr(|G_M - \mathrm{rank}(A)| \ge \mathrm{rank}(A)\epsilon) \le 2\exp(-M\,\mathrm{rank}(A)\epsilon^2/6).$$

4. Eq. (2). If moreover $M \ge 6\,\mathrm{rank}(A)^{-1}\epsilon^{-2}\ln(2/\delta)$, then $\Pr(|G_M - \mathrm{rank}(A)| \ge \mathrm{rank}(A)\epsilon) \le \delta$.
5. Trace of a projection. $\mathrm{trace}(A) = \mathrm{rank}(A)$.

Significance

The lemma turns a randomized estimator into an exact algorithm with a controlled failure probability: the rank of an implicitly given projection is obtained from $O(\mathrm{rank}(A)\log(1/\delta))$ matrix–vector products, independently of the dimension $n$. It is also an instance where the paper's general relative-error bound for the Gaussian estimator (Theorem 5.2, whose sample count grows like $\epsilon^{-2}$) is improved by exploiting the spectrum of $A$: an absolute error below $\tfrac12$ is a relative error $\epsilon = 1/(2\,\mathrm{rank}(A))$, for which the general bound would require a number of samples quadratic in the rank, whereas Lemma 5.3 needs only a linear number.

The result is proved in the paper. The mission produces a machine-checked version of it, together with two pieces of reusable substrate: the exact $\chi^2$ law of a Gaussian quadratic form in an orthogonal projection, and a two-sided $\chi^2$ tail bound with explicit constant $1/6$ on the range $0<\epsilon\le 1/2$. To the best of available knowledge, none of these statements is formalized in Mathlib; a platform mission on the Johnson–Lindenstrauss lemma states a $\chi^2$ concentration bound with a different exponent, $(\epsilon^2-\epsilon^3)/4$, on the open range $0<\epsilon<1/2$, which does not cover the value $\epsilon = 1/2$ needed here when $\mathrm{rank}(A)=1$.

Difficulty

The deterministic part is short; the probabilistic part is not. The step "$y = Uz$ has independent standard normal entries because $U$ is orthogonal" is the rotation invariance of the standard Gaussian measure on $\mathbb{R}^n$, and it must be combined with the independence of the $M$ samples to identify the law of a sum of $M\,\mathrm{rank}(A)$ squares; this is a statement about product measures and pushforwards, not about moments. The $\chi^2$ tail bound is quoted by the paper without proof. Its constant $1/6$ is not the constant of the usual textbook $\chi^2$ estimates, and the bound is false outside a restricted range of $\epsilon$ (see below), so a generic sub-exponential concentration inequality with unspecified constants does not deliver it. Finally, the rounding step requires matching Mathlib's round with the event $|G_M - \mathrm{rank}(A)| < \tfrac12$.

Formalization scope

All declarations live in the namespace TraceEstimation.ProjectionRank. Matrices are Matrix (Fin n) (Fin n) ℝ. The sample space of $G_M$ is Fin M → Fin n → ℝ with the product measure Measure.pi (fun _ => Measure.pi (fun _ => gaussianReal 0 1)), so the law of the estimator is constructed, not assumed. Probabilities are Measure.real of events. "Projection matrix" is A.IsHermitian ∧ A * A = A (orthogonal projection); a non-symmetric idempotent also has eigenvalues $0$ and $1$, but the paper's proof diagonalizes $A$ by a unitary matrix, which requires symmetry. round is Mathlib's round : ℝ → ℤ; the rank is Matrix.rank. The $\chi^2$ distribution is not defined: its role is played by the pushforward of a product of standard normals under $g \mapsto \sum_l g_l^2$.

Corrections of the printed text, both in the $\chi^2$ tail bound (milestone 2):

• The paper prints $\Pr(|X - k| \le \epsilon k) \le 2\exp(-k\epsilon^2/6)$. The inner $\le$ is a misprint for $\ge$; the next display applies the bound with $\ge$.
• The paper gives no range for $\epsilon$. The bound fails for $\epsilon = 1$ and large $k$, since $\Pr(X \ge 2k)$ decays like $e^{-k(1-\ln 2)/2}$, slower than $e^{-k/6}$. The mission states it for $0<\epsilon\le 1/2$, and milestones 3 and 4 inherit that range; the proof uses only $\epsilon = 1/(2\,\mathrm{rank}(A)) \le 1/2$.

The goal keeps the paper's hypotheses: $\delta > 0$ with no upper bound, and $\mathrm{rank}(A) = 0$ allowed (both are true cases). A statement about the event $|G_M - \mathrm{rank}(A)| < \tfrac12$, or Eq. (2) alone, is not the goal; the goal is about $\mathrm{round}(G_M)$. The sample measure is a probability measure, so the bound $\le \delta$ is not vacuous.

Contributions welcome beyond the milestones: rotation invariance of the standard Gaussian vector under orthogonal matrices, the moment generating function of $\chi^2(k)$, and the spectral fact $\mathrm{trace}(A) = \mathrm{rank}(A)$ for idempotents, each reusable well outside this mission.

Selected references

• H. Avron and S. Toledo, Randomized algorithms for estimating the trace of an implicit symmetric positive semi-definite matrix, Journal of the ACM 58(2), Article 8, 2011. https://doi.org/10.1145/1944345.1944349
• P. Li, T. Hastie and K. Church, Nonlinear estimators and tail bounds for dimension reduction in $l_1$ using Cauchy random projections, in Learning Theory (COLT 2007), Lecture Notes in Computer Science 4539, Springer, 514–529, 2007 (the version the paper cites); journal version in Journal of Machine Learning Research 8, 2497–2532, 2007, https://jmlr.org/papers/v8/li07b.html
• C. Bekas, E. Kokiopoulou and Y. Saad, An estimator for the diagonal of a matrix, Applied Numerical Mathematics 57(11–12), 1214–1229, 2007. https://doi.org/10.1016/j.apnum.2007.01.003
• M. F. Hutchinson, A stochastic estimator of the trace of the influence matrix for Laplacian smoothing splines, Communications in Statistics – Simulation and Computation 19(2), 433–450, 1990. https://doi.org/10.1080/03610919008812866

Motivation

Mission XII (12-packet-networks-model) built the discrete-time, slotted packet-network model from scratch and proved the chapter's own version of the fluid-to-stochastic stability bridge (Theorem 12.10). That result is only useful once paired with an actual control policy whose fluid model can be shown stable. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) supplies exactly such a policy in Sections 12.4-12.5: back-pressure control (called max-weight when the network is single-hop), a rule that has become the default choice in the switching and wireless-scheduling literature because it requires no advance knowledge of arrival rates and achieves the largest possible stability region. This mission formalizes back-pressure control for the discrete-time packet network model and proves it maximally stable — the chapter's own counterpart to mission VIII's continuous-time Theorem 9.12.

Setting

At the start of each timeslot, having observed the current buffer contents $z$, the max-weight/ back-pressure (MW/BP) policy solves $\max_{s\in S(z)} z\cdot Rs$ (Eq. 12.41), where $S(z) := \{s\in S : Bs\le z\}$ restricts the schedule set $S$ (mission XII) to what is actually available given $z$. Equivalently (Eq. 12.42-12.43), writing $w_j(z) := z_{u(j)} - z_{d(j)}$ (with $z_0 := 0$) for the "weight" of activity $j$, the policy maximizes $\sum_j w_j(z) s_j$ — the schedule that clears the most "backlog pressure" per timeslot. The policy is deterministic (no randomization variable is needed, since (12.41) is a genuine optimization problem, not one that inherently requires randomized tie-breaking).

Formalization targets

Goal: Theorem 12.16 — aperiodicity, irreducibility, and conditional positive recurrence

Consider a packet network satisfying (12.1) and Assumption 12.1, operating under back-pressure control. The DTMC $Z$ is aperiodic and irreducible unconditionally. If the stability condition (12.26) — the existence of $\hat s\in\langle S\rangle$ with $\lambda < R\hat s$ — is additionally satisfied, $Z$ is positive recurrent. This is the mission's headline result, and it packages both a structural fact (irreducibility/aperiodicity, needed regardless of load) and a conditional stability fact (positive recurrence, needed only under (12.26)) in one theorem.

Supporting milestones

Lemma 12.17 shows the optimization problem (12.41) always has a nonzero solution whenever the network is nonempty — the fact that back-pressure never "idles unnecessarily," which Lemma 12.18 uses to show every state can reach the empty state (hence irreducibility) and that state $0$ has period $1$ (hence aperiodicity, via (12.1)'s own assumption that no external arrivals is possible with positive probability). Lemma 12.20 is the back-pressure fluid equation (12.44), the discrete-time analog of mission VIII's Theorem 9.8: at each regular point, the fluid-scaled buffer content dotted with the fluid departure rate equals the maximum of that same dot product over the convex hull of the schedule set. Lemma 12.21 shows this fluid model is stable whenever (12.26) holds, via an explicit quadratic Lyapunov function.

Significance

The result itself. Theorem 12.16 shows that back-pressure control — a rule requiring no knowledge of arrival rates, computed fresh from the current buffer contents every timeslot — is maximally stable: combined with Theorem 12.8 and Proposition 12.9 (mission XII), it stabilizes every packet network arrival-rate vector that any policy could possibly stabilize. This is the discrete-time, slotted analog of mission VIII's Theorem 9.12, and the two proofs share their essential Lyapunov argument (the book's own text calls Lemma 12.21's proof "almost identical to that of Theorem 9.12"), even though the two chapters' back-pressure equations are built from different underlying objects — mission VIII's continuous-time allocation polytope versus this chapter's convex hull of a discrete schedule set.

Formalizing it. A live prior-art check (GET /theorems?q=back-pressure, q=max-weight) finds no relevant hits, matching mission VIII's own finding for the continuous-time version. This mission formalizes the back-pressure optimization problem and policy, the back-pressure fluid equation, and its stability from scratch, restating (per this series' convention for concurrently-drafted chunks sharing a sub-namespace) the minimal apparatus needed from mission XII: the packet network model, Assumption 12.1, the raw processes, fluid limit paths, the fluid equations (12.31)-(12.36), and the ambient-chain machinery, plus a new Aperiodic predicate this chunk needs that mission XII's own results do not.

Difficulty

The obvious approach to Lemma 12.20's back-pressure fluid equation — directly differentiate the discrete system equation — obscures the actual argument, which reduces a maximum over the (potentially non-polytope) discrete schedule set $S$ to a maximum over its convex hull $\langle S\rangle$ (justified because a linear functional on a compact polytope is maximized at an extreme point) and then shows that every schedule with a strictly smaller objective value than the maximizer contributes zero derivative to the usage-counting process $\hat T_s$ — the discrete-time analog of mission VIII's Lemmas 9.10-9.11. A second difficulty is connecting the maximum-over-a- finite-set at the fluid-scaled level to Definition 12.3's discrete, arrival-indexed back-pressure policy: this mission's own Lemma 12.20 item states the fluid-relevant consequence of the discrete policy as a documented hypothesis (mirroring mission XI's own scope decision for its structurally identical WWTA fluid equation) rather than re-deriving it from the raw stochastic recursion, which would require reconstructing infrastructure outside this chapter's own numbered results.

Formalization scope

The packet network model, Assumption 12.1, the raw processes, and the fluid-limit apparatus are restated verbatim from mission XII (12-packet-networks-model), since concurrently-drafted chunks sharing a sub-namespace do not import one another's Lean files. IsBPOptimal is phrased via domination over the feasible-at-$z$ schedule set, not sSup/argmax, per this series' junk-value-avoidance convention; the same convention is applied to the maximum over $\langle S\rangle$ in the back-pressure fluid equation. The formalization does not admit a trivializing reading: irreducibility and aperiodicity are the same non-vacuous renewal-theoretic notions used throughout this series (Aperiodic requires a genuine positive self-transition probability, not a vacuously-true condition), and the goal's positive-recurrence conjunct is genuinely conditional on (12.26), stated with the correct strict inequality rather than weakened to $\le$. Contributions completing the five by sorry proofs are welcome, particularly Lemma 12.17's hop-count induction and Lemma 12.20's extreme-point/zero-derivative argument (mirroring mission VIII's own Lemmas 9.10-9.11, adapted to discrete time).

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org

Motivation

Internet routers, wireless base stations, and data-switch fabrics all face the same recurring decision: in each discrete time slot, which of many possible transfer operations should be executed, given the packets currently queued and the physical constraints (link capacities, interference between simultaneous transmissions) on what can be done at once? J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes Chapter 12 to exactly this question, under the name packet networks. Unlike every prior chapter of the book, which works in continuous time with Poisson-driven Markov chains, this chapter builds its stability theory from scratch for a discrete-time, slotted model — the natural setting for a system that makes one scheduling decision per clock tick. This mission formalizes the chapter's foundational layer: the model itself, its notion of a feasible schedule and control policy, subcriticality, and the discrete-time fluid-limit machinery that Chapters 13 and 14 (back-pressure control and random proportional scheduling, respectively) build their own stability proofs on top of.

Setting

A packet network (Section 12.1) has I packet classes and J activities (service types); activity $j$ transfers a packet from its input class $u(j)$ to its output class $d(j)$ (or removes it from the network if $d(j)=0$), giving an $I\times J$ input-output matrix $R$. A processing plan for class $i$ (Definition 12.2) is a chain of activities from $i$ to exit; Assumption 12.1 requires every class to have one and forbids cycles. In each timeslot the system manager chooses a schedule $s\in\mathbb Z^J_+$ from a feasible set $S$ satisfying the packet-availability constraint $Bs\le z$ (the current buffer contents); $S$ is typically built (Section 12.2) from a link usage matrix $A$ and a set $C$ of feasible link configurations via $S_c := \{s : As\le c\}$, $S := \bigcup_{c\in C} S_c$. A Markovian control policy (Definition 12.3, Eq. 12.8) chooses $s(\tau) = f(Z(\tau-1), U(\tau))$ from the current buffer contents and an independent randomization variable; it is admissible if it never overdraws a buffer, and stable if the resulting discrete-time Markov chain $Z$ is irreducible and positive recurrent.

Formalization targets

Goal: Theorem 12.10 — fluid limit stability implies positive recurrence

If the DTMC $Z$ under a Markovian policy $f$ is irreducible and its fluid limit is stable (Definitions 12.14-12.15), then $Z$ is positive recurrent. This is the chapter's own version of Theorem 6.2 (mission III) — the technical fulcrum that lets a deterministic fluid-model stability argument certify the stability of the original discrete, stochastic system — restated for a genuinely different probabilistic model, since Theorem 6.2 was built under continuous-time, Poisson-arrival hypotheses this chapter does not share.

Supporting milestones

Propositions 12.6-12.7 characterize the convex hulls $\langle S_c\rangle$ and $\langle S\rangle$ as explicit polytopes cut out by the link usage matrix — the combinatorial core that Theorem 12.8 (stability implies subcriticality, this chapter's analog of Theorem 5.2) and Proposition 12.9 (a necessary condition for subcriticality) both build on. Lemma 12.11 records that the schedule-usage counting process is Lipschitz; Lemma 12.12 is the functional strong law of large numbers the external arrival process satisfies; and Theorem 12.13 combines them to establish existence of discrete-time fluid limits satisfying the chapter's own fluid equations (12.31)-(12.36) — the chapter's analog of Theorem 6.5.

Significance

The result itself. Theorem 12.10 is what makes the rest of Chapter 12 (and Chapters 13-14) tractable: rather than analyzing an infinite-state discrete-time Markov chain's positive recurrence directly — a notoriously hard problem in general — it suffices to exhibit a deterministic fluid model and show every solution of that fluid model empties in finite time. This is the same strategy Chapter 6 established for the book's continuous-time model, but Chapter 12 cannot simply invoke that earlier theorem: the packet network model uses discrete time slots rather than a continuous clock, and its probabilistic structure (arbitrary i.i.d. arrival increments rather than Poisson arrivals) is different enough that the fluid-limit compactness argument has to be redone, even though — as the book's own text notes — "the proof mimics that of Theorem 6.2."

Formalizing it. A live prior-art check (GET /theorems?q=packet+network, q=discrete-time+Markov+chain, q=slotted+time) finds no relevant hits. A dedicated further check for MarkovMixing, a different mission's own corpus offering a PositiveRecurrent predicate for Markov chains, found a representationally distinct formalization (a row-function transition kernel rather than this series' own PMF-based jump-chain convention); this mission restates positive recurrence and irreducibility locally instead, consistent with every mission in this series since mission I. Everything else — the packet network model, schedules and configurations, the subcritical region, Markovian policies, and the discrete-time fluid-limit apparatus — is formalized from scratch.

Difficulty

The most consequential decision in this mission is representational, not mathematical: Theorem 12.10's fluid-limit-stability hypothesis quantifies over all fluid limit paths, which are themselves scaling limits of a genuinely stochastic discrete-time process — reconstructing that process from Chapter 2/4's own primitive stochastic elements (arrival processes, phase-type service mechanics) would require rebuilding infrastructure this chapter's own numbered results do not supply. Following mission III's own precedent for its structurally identical Theorem 6.5, this mission instead takes the raw, per-initial-state schedule-usage and arrival processes as given data satisfying only the recap properties the chapter's own proofs actually cite (Eq. 12.9-12.10's system equation, monotonicity), and fixes a single sample point together with an explicit SLLN hypothesis rather than a bare "for almost all $\omega$" quantifier — matching the book's own statement of Theorem 12.13, which itself begins "Fix an $\omega\in\Omega_1$" rather than quantifying almost everywhere within the theorem itself. A second difficulty is genuinely combinatorial: Proposition 12.6's proof constructs an explicit product-form probability distribution over schedules (one independent randomization per link) whose mean recovers an arbitrary point of the polytope $\{Ax\le c\}$ — a real combinatorial argument, not a formal consequence of the convex-hull operator's definition.

Formalization scope

Classes, activities, links, schedules and configurations are represented via Fin-indexed types throughout; S and C are taken as Finsets (every worked example in the book has finitely many configurations, and the link usage matrix's single-1-per-column structure bounds each schedule component, so this is a genuine, if implicit, standing feature of the model rather than an added restriction). IsScheduleSetAt/IsScheduleSet characterize $S_c$/$S$ via an ↔ against the underlying capacity constraint, rather than constructing them, matching how set-valued model data is handled elsewhere in this series. The formalization does not admit a trivializing reading: the ambient chain's positive recurrence (PositiveRecurrent) is the same non-vacuous renewal-theoretic notion used throughout this series, PacketFluidLimitStable quantifies over every genuine fluid limit path (not a hand-picked one), and subcriticalRegion is stated with a strict inequality ($A\hat s < \hat c$) exactly as Eq. 12.24 requires, not weakened to $\le$. Contributions completing the eight by sorry proofs are welcome, particularly Proposition 12.6's explicit randomized- schedule construction and Theorem 12.13's compactness argument (mirroring mission III's own Theorem 6.5 proof, adapted to discrete time).

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org

Motivation

Large-scale data-intensive computing splits a job into many small "map tasks," each of which must be assigned to one of thousands of general-purpose servers in a data center — the MapReduce paradigm introduced by Dean and Ghemawat (2008). Because a task's input data is stored on only a few of those servers, routing it to a server that already holds its data ("data locality") avoids costly network transfer, so a task-allocation policy that ignores locality can leave a server farm badly underutilized even when raw compute capacity is ample. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes Chapter 11 to a rigorous stability analysis of Xie, Yekkehkhany, and Lu's (2016) workload-weighted task allocation (WWTA) policy, which routes each arriving task to whichever eligible server currently carries the least (locality-weighted) backlog. This mission formalizes the chapter's central result: WWTA is not merely a reasonable heuristic but is maximally stable — it keeps the system stable whenever any routing policy could.

Setting

A task allocation model (Sections 11.2-11.3) has L task categories and K servers; a class is a pair $(\ell,k)$, a category routed to a specific server, with mean service time $m_{\ell k} > 0$ (Eq. 11.3) reflecting both data locality (local, rack-local, or remote access) and the server's relative processing speed. Tasks in category $\ell$ arrive according to a Markovian arrival process (MArP) with long-run average rate $\nu_\ell$ — a substantially more general model than the independent Poisson streams used elsewhere in the book, needed to capture batches of map tasks generated from a single job. Routing is by immediate commitment: each task is assigned to a server the instant it arrives, based only on its category and the current backlog, with no possibility of later reassignment. The workload of server $k$ at time $t$ (Eq. 11.7) is $W_k(t) := \sum_\ell m_{\ell k} Z_{\ell k}(t)$, the locality-weighted total backlog assigned to it. Workload-weighted task allocation (WWTA), Definition 11.3, routes an arriving category-$\ell$ task to any server achieving $\operatorname{argmin}_{k} m_{\ell k} W_k(t-)$ (Eq. 11.8, ties broken arbitrarily), where $W(t-)$ is the workload vector's left limit at the arrival instant.

Formalization targets

Goal: Theorem 11.6 — WWTA fluid model stability under the load condition

If there exists $\lambda = (\lambda_{\ell k}) \ge 0$ with $\sum_k \lambda_{\ell k} = \nu_\ell$ for each category (Eq. 11.4) and $\sum_\ell m_{\ell k}\lambda_{\ell k} < 1$ for each server (Eq. 11.5), then the WWTA fluid model — the deterministic fluid equations (11.11)-(11.16) that arise as scaling limits of the stochastic model under WWTA control — is stable: every solution reaches the zero state in finite time proportional to its initial size.

Supporting milestones

Lemma 11.2 shows this load condition is equivalent to subcriticality of the task allocation model, in the sense of Section 5.2's general definition, reducing an existence statement over the model's full $G,R,A,b$ apparatus to a simple linear-feasibility check. Theorem 11.4 establishes that fluid limits of the stochastic model exist and satisfy the general fluid equations (11.11)-(11.15) under any immediate-commitment routing policy, and the WWTA-specific equation (11.16) under WWTA — the chapter's version of the fluid-limit machinery Chapter 6 builds for the book's standard model, adapted to Markovian (not Poisson) arrivals and immediate-commitment routing. Theorem 11.5 is the corresponding replacement for Theorem 6.2 (mission III): fluid limit stability implies stability of the original stochastic model. Corollary 11.7 is the mission's other headline consequence: WWTA is maximally stable, stabilizing the model whenever any simply structured routing policy could.

Significance

The result itself. A task-allocation heuristic motivated purely by an intuitive "balance-the-weighted-backlog" idea turns out to have the strongest stability guarantee a policy can have: it never needs re-tuning as arrival rates change, and no alternative policy can stabilize a regime WWTA cannot. Xie, Yekkehkhany, and Lu (2016) proved this fact (calling it "throughput optimality") by direct analysis of the discrete stochastic model using a quadratic Lyapunov function; Dai and Harrison's contribution is to prove the same conclusion via the fluid-model route, and — because the task allocation model violates two of the standing assumptions under which Chapter 6's general theory was built (MArP rather than Poisson arrivals, immediate-commitment routing rather than the book's default relaxed control) — to show that the general fluid-stability machinery survives those changes with only minor modification.

Formalizing it. A live prior-art check (GET /theorems?q=task+allocation, q=server%20farm, q=data%20locality) finds no relevant hits on the platform (workload returns one unrelated text-corpus-statistics result). This mission formalizes the task allocation model, WWTA, the fluid equations, and the stochastic-to-fluid bridge from scratch, reusing Mathlib's general real-analysis, measure-theory, and PMF-based Markov-chain substrate, and restating (per this series' convention for concurrently-drafted chunks) the minimal apparatus needed from missions I and III.

Difficulty

The obvious approach to Definition 11.3 — pick a canonical minimizer of $m_{\ell\cdot}W_\cdot(t-)$, e.g. via Finset.min' — silently narrows WWTA to a single tie-breaking rule, when (11.8) explicitly allows any minimizer; this mission instead states WWTA as domination over every server, accepting every admissible tie-break. A second difficulty is genuinely structural: Theorem 11.4's "for almost all $\omega$" existence claim is a measure-theoretic statement about a probability space that mission III's own analogous Theorem 6.5 sidesteps by fixing a sample point $\omega$ together with the specific SLLN limit that argument needs — this mission follows the same precedent rather than introducing a bare "almost everywhere" quantifier, which does not by itself supply the type information Lean's typeclass resolution needs to identify an ambient measure. A third is connecting Definition 11.3's discrete, arrival-indexed routing rule to the raw (pre-limit) process family that Theorem 11.4's existence argument operates on: the book's own proof derives the needed consequence (Eq. 11.22, "server $k$ receives no more category-$\ell$ tasks in a neighbourhood of $t$") via an explicit $\varepsilon$-$\delta$ argument from the discrete policy, which this mission takes as a documented hypothesis rather than re-deriving, since building the arrival-sequence-to-counting-process reconstruction is genuinely Chapter 2/4 machinery outside this chapter's own numbered results.

Formalization scope

Classes are represented as pairs (ℓ,k) : Fin L × Fin K rather than flattened to a single index, avoiding an arbitrary choice of encoding. TaskAllocationProcessFamily, FluidLimitPath, and TaskAllocationFluidLimitStable restate mission III's SPNProcessFamily/FluidLimitPath/ FluidLimitStable apparatus, adapted to this model's (E,D,Z) triple and doubly-indexed classes; PositiveRecurrent restates mission I's renewal-theoretic positive-recurrence notion. The formalization does not admit a trivializing reading: IsWWTA accepts every admissible tie-break rather than a single canonical one, SatisfiesWWTAFluidEquation requires Nonempty (Fin K) so its min_{k} is a genuine minimum rather than a junk value at zero servers, and the goal's conclusion WWTAFluidStable is the same non-vacuous fluid-model-stability predicate (Definition 6.3, specialized) used throughout this series. Contributions completing the five by sorry proofs are welcome, particularly Theorem 11.4's fluid-limit compactness argument (mirroring mission III's own Theorem 6.5 proof) and Theorem 11.6's explicit quadratic-Lyapunov-function argument.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• J. Dean and S. Ghemawat, "MapReduce: simplified data processing on large clusters," Communications of the ACM 51 (2008), 107–113.
• Q. Xie, A. Yekkehkhany, and Y. Lu, "Scheduling with multi-level data locality: throughput and heavy-traffic optimality," IEEE INFOCOM 2016.