All missions

Motivation

A conic quadratic program minimizes a linear objective subject to constraints of the form $\|A_\ell x-b_\ell\|_2\le c_\ell^Tx-d_\ell$. Interior-point methods solve such programs in polynomial time, but around 2000 the available solvers handled far smaller instances than linear programming codes did. Ben-Tal and Nemirovski (Math. Oper. Res. 26(2), 2001) asked whether a conic quadratic program can be replaced by a linear program of comparable size, and answered it by approximating each second-order cone by a projection of a polyhedral cone. Their Theorem 1.1 builds such an approximation with accuracy $\varepsilon$ using $O(k\ln(2/\varepsilon))$ variables and inequalities. The present mission is their Proposition 3.1: this size is optimal in order, because every polyhedral $\varepsilon$-approximation needs $\Omega(k\ln(1/\varepsilon))$ inequalities.

The question of how many linear inequalities are needed to represent or approximate a convex set as a projection (its extension complexity) has since become a subject of its own, and the lower bound of Proposition 3.1 is one of its early explicit instances for a non-polyhedral cone.

Setting

For $y\in\mathbb R^k$ write $\|y\|_2=\sqrt{y_1^2+\dots+y_k^2}$. The Lorentz cone is

Let $\varepsilon>0$. A polyhedral $\varepsilon$-approximation of $L^k$ is a linear map $\Pi:\mathbb R^k\times\mathbb R\times\mathbb R^p\to\mathbb R^q$ such that

1. if $(y,t)\in L^k$, then $\Pi(y,t,u)\ge0$ for some $u\in\mathbb R^p$;
2. if $\Pi(y,t,u)\ge0$ for some $u$, then $\|y\|_2\le(1+\varepsilon)t$.

Here $\ge0$ is componentwise, $p$ is the number of auxiliary variables and $q$ the number of homogeneous linear inequalities. Equivalently, the polyhedral cone $K=\{(y,t,u)\mid\Pi(y,t,u)\ge0\}$ projects onto a cone $\widehat L^k$ of the $(y,t)$-space with $L^k\subseteq\widehat L^k\subseteq\{(y,t)\mid\|y\|_2\le(1+\varepsilon)t\}$. The slice of $\widehat L^k$ at height one is $G=\{y\mid(y,1)\in\widehat L^k\}$, and $B=\{y\mid\|y\|_2\le1\}$ denotes the closed unit ball.

Formalization targets

Goal: Proposition 3.1, Eq. (13)

The constant is absolute, as in the paper, and no value is fixed; the goal asserts only the order of growth.

Milestones (claims of the proof, in order)

1. Reduction. For $\varepsilon>0$ one may replace $\Pi$ by an approximation with the same $q$, at most $p$ auxiliary variables and the same projection, whose cone $K$ contains no line.
2. Extreme rays. A line-free cone $\{z\mid Az\ge0\}$ defined by $q$ inequalities is the conic hull of at most $2^q$ extreme rays.
3. Sandwich. $B\subseteq G\subseteq(1+\varepsilon)B$.
4. Vertices. If $K$ has no line, $G$ is the convex hull of $N\le2^q$ points.
5. Covering. If $\operatorname{conv}\{y_1,\dots,y_N\}\supseteq B$ and all $\|y_i\|_2\le1+\varepsilon$, the closed balls of radius $\sqrt{2\varepsilon(1+\varepsilon)}$ about the $y_i$ cover the sphere $\{\|y\|_2=1+\varepsilon\}$.
6. Counting. For $k\ge2$ and $\varepsilon\le\tfrac12$ such a covering needs $N\ge\exp\{c\,k\ln(1/\varepsilon)\}$ balls.

Significance

The result. Proposition 3.1 shows that the construction of Theorem 1.1 is optimal up to an absolute factor in the number of inequalities: approximating a conic quadratic constraint in dimension $k$ to relative accuracy $\varepsilon$ by linear inequalities costs $\Theta(k\ln(1/\varepsilon))$ inequalities, no more and no less. It separates what lifting (auxiliary variables) buys, a logarithmic dependence on $1/\varepsilon$, from what it cannot buy, a sub-linear dependence on $k$ or on $\ln(1/\varepsilon)$. Without auxiliary variables a polytope approximating the ball needs $\varepsilon^{-\Omega(k)}$ facets; the proposition says the logarithm of that count is the true cost even when lifting is allowed.

Formalizing it. The result is proved in the paper, in about fifteen lines that appeal to "elementary geometry" and to an unstated covering estimate. No machine-checked proof is known to exist. The mission produces a checked proof of the lower bound together with reusable facts: the finiteness bound on extreme rays of a pointed polyhedral cone and a lower bound on the number of balls needed to cover a Euclidean sphere, which Mathlib does not contain in this form. A companion mission of this series formalizes the matching upper bound (Theorem 1.1).

Difficulty

The obvious argument counts vertices of $G$: at most $2^q$ of them, and a polytope between $B$ and $(1+\varepsilon)B$ needs many vertices. The difficulty is in making "many" quantitative with the right exponent. A direct volume comparison of $G$ with $B$ gives nothing, since $G$ may have the volume of $(1+\varepsilon)B$. The argument needs the transfer from "the convex hull of the points contains $B$" to "the points are $\sqrt{2\varepsilon(1+\varepsilon)}$-dense on the outer sphere", and then a lower bound on the size of a covering of a sphere by balls whose centres need not lie on the sphere, uniform down to $k=2$ and up to $\varepsilon=\tfrac12$, where $\ln(1/\varepsilon)$ is only $\ln2$ and the radius $\sqrt{2\varepsilon(1+\varepsilon)}$ is comparable to the sphere's radius. A second, easily overlooked step is the passage to a line-free cone: $K$ itself may contain lines in the $u$-directions, in which case it has no extreme rays at all.

Formalization scope

Vectors of $\mathbb R^k$ are Fin k → ℝ, and the Euclidean norm is written out as eucNorm y = √(∑ i, y i ^ 2); the norm Mathlib puts on Fin k → ℝ is the sup norm, under which $L^k$ is polyhedral and the goal is false. A polyhedral approximation is an $\mathbb R$-linear map (Fin k → ℝ) × ℝ × (Fin p → ℝ) →ₗ[ℝ] (Fin q → ℝ), and $p$, $q$ are the dimensions of its types; with arbitrary (nonlinear) maps, $\Pi(y,t)=t-\|y\|_2$ would give $q=1$, so linearity is what makes the statement non-trivial. "Extreme ray" means a ray $\{sr\mid s\ge0\}$, $r\ne0$, that is an extreme subset (Mathlib IsExtreme) of the cone, counted once per ray.

Corrections of the printed statement. Proposition 3.1 is printed for every positive integer $k$. It is false for $k=1$: $L^1=\{|y|\le t\}$ is polyhedral, and $\Pi(y,t)=(t-y,t+y)$ is a polyhedral $\varepsilon$-approximation with $q=2$ for every $\varepsilon$, so $q\ge c\ln(1/\varepsilon)$ fails for small $\varepsilon$. The goal and the counting milestone are therefore stated for $k\ge2$, which is the case the proof covers. The phrase "polyhedral $\alpha$ approximation" in the proof is read as $\varepsilon$. The paper's $O(1)$ constants are existential and quantified before every variable they are uniform over; no numerical value is asserted.

A complete development needs the Minkowski–Weyl representation of pointed polyhedral cones by extreme rays, basic convex-hull and separation arguments in Euclidean space, and a lower bound for covering numbers of spheres (for instance by a cap-measure or volume argument). The extreme-ray and covering lemmas are independent of the Lorentz cone and are welcome as stand-alone contributions.

Selected references

• A. Ben-Tal and A. Nemirovski, On Polyhedral Approximations of the Second-Order Cone, Mathematics of Operations Research 26(2):193–205, 2001. https://doi.org/10.1287/moor.26.2.193.10561
• A. Ben-Tal and A. Nemirovski, Lectures on Modern Convex Optimization: Analysis, Algorithms, and Engineering Applications, SIAM, 2001. https://doi.org/10.1137/1.9780898718829

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

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

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$,

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$,

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

The finite-horizon theory of chunk 02a-model-bellman-equation (Bäuerle and Rieder's Theorem 2.3.8, the Structure Theorem) reduces the existence of an optimal policy and the validity of the Bellman equation to a single abstract hypothesis: the Structure Assumption (SAN), the existence of function classes $\mathrm{IM}_n$ and decision-rule classes $\Delta_n$ closed under the one-step optimality operator $T_n$. That theorem does not say when (SAN) actually holds for a given Markov Decision Model — checking it directly from the definition would require exhibiting, for every value function that could arise, both its regularity and a measurable action attaining its supremum, an infinite regress. This mission formalizes the classical resolution: sufficient conditions on the primitive data of the model (the admissible-action correspondence, the transition kernel, the one-stage reward) under which (SAN) is guaranteed, so that Theorem 2.3.8 becomes usable in practice rather than merely an existence statement.

Setting

Fix a Markov Decision Model $(E, A, D_n, Q_n, r_n, g_N)_{n=0,\dots,N-1}$ (chunk 02a's Definition 2.1.1), now with $E$, $A$ Borel spaces. A measurable $b : E \to \mathbb{R}_+$ is an upper bounding function (Definition 2.4.1) if $r_n^+(x,a) \le c_r b(x)$, $g_N^+(x) \le c_g b(x)$, and $\int b(x')\, Q_n(dx' \mid x,a) \le \alpha_b b(x)$ for constants $c_r, c_g, \alpha_b \ge 0$; write $\mathrm{IB}_b^+$ for the value functions of weighted growth at most $c\, b$ for some $c$. A set-valued map $x \mapsto D(x)$ is upper semicontinuous if $x_n \to x$ and $a_n \in D(x_n)$ force $(a_n)$ to have an accumulation point in $D(x)$ (Definition A.2.1); it is continuous if also every point of $D(x)$ is approximated by a sequence from the $D(x_n)$.

Formalization targets

Goal: Theorem 2.4.13

Suppose the model has an upper bounding function $b$, and for every $n < N$: (i) $D_n(x)$ is compact for every $x$; (ii) $a \mapsto \int v(x')\, Q_n(dx' \mid x,a)$ is upper semicontinuous on $D_n(x)$ for every $v \in \mathrm{IB}_b^+$ and every $x$; (iii) $a \mapsto r_n(x,a)$ is upper semicontinuous on $D_n(x)$ for every $x$. Then $\mathrm{IM}_n := \mathrm{IB}_b^+$, $\Delta_n := F_n$ satisfy (SAN). Unlike the two milestone theorems that precede it in the chapter (Theorem 2.4.6 and Theorem 2.4.10, both of which also assume the correspondence $x \mapsto D_n(x)$ varies semicontinuously or continuously with $x$), Theorem 2.4.13 assumes nothing about $D_n(\cdot)$ as a set-valued map beyond pointwise compactness of each fiber $D_n(x)$; correspondingly it needs semicontinuity of the objective only in the action variable, at each state separately, and it recovers all of $\mathrm{IB}_b^+$ as the regularity class rather than a semicontinuous or continuous sub-class of it.

Milestones

Proposition 2.4.3 and Proposition 2.4.8 show, respectively, that $T_n$ preserves upper semicontinuity (resp. continuity) of $v$ and that a maximizer exists, when $D_n(x)$ is compact and $x \mapsto D_n(x)$ is upper semicontinuous (resp. continuous); Theorem 2.4.6 and Theorem 2.4.10 package these into concrete instances of (SAN). Lemma 2.4.7 gives a checkable criterion — weak continuity of the kernel $Q_n$ — for Theorem 2.4.6's integral-semicontinuity hypothesis. Proposition 2.4.11 drops all topological structure on $D_n(\cdot)$ itself, keeping only pointwise compactness of $D_n(x)$ plus semicontinuity of the objective in the action alone, and is what the goal theorem invokes directly, via a projection theorem of Kunugui and Novikov in place of the sequential compactness argument used for Proposition 2.4.3.

Significance

Compactness of the action set together with semicontinuity of the reward is the textbook Weierstrass mechanism for the existence of a maximizer in ordinary optimization; the content of this chapter is doing the same thing correctly when the maximization varies measurably over an uncountable state space $E$, so that the resulting maximizer is not just pointwise-optimal but a genuine decision rule (a measurable function of the state). No formalized version of this theory exists on the platform: BertsekasDP's existence theorems are for finite state-and-action-space models, where $D(x)$ is automatically compact (in the discrete topology) and every real-valued function on it is automatically semicontinuous, so none of this chapter's actual content — choosing a measurable maximizing selection as the state varies continuously — has any analogue there. This chunk earns the generalization rather than restating that finite-state prior art.

Difficulty

The three "compactness implies (SAN)" theorems of this chapter (2.4.6, 2.4.10, 2.4.13) trade regularity of the action correspondence $x \mapsto D_n(x)$ against regularity of the resulting value-function class: assuming more about how $D_n(\cdot)$ varies (continuity, in Theorem 2.4.10) buys a stronger conclusion (continuous, not merely upper semicontinuous, value functions); assuming nothing about $D_n(\cdot)$ beyond pointwise compactness (Theorem 2.4.13, the goal) forces the weakest conclusion, that the whole class $\mathrm{IB}_b^+$ is preserved, via a genuinely different, measure-theoretic argument (a projection theorem) rather than the sequential compactness argument common to Propositions 2.4.3 and 2.4.8. Formalizing all three side by side, rather than only the goal in isolation, is what exposes this trade-off as three logically independent theorems rather than one theorem instantiated three times, and is why every one of the section's numbered results is kept as an item of this mission (per the CAPTAIN's budget instruction to include, not cut, results of genuine independent content) rather than only the smallest set literally required by the goal's own proof tree.

Formalization scope

State and action spaces carry MeasurableSpace, TopologicalSpace, BorelSpace instances throughout (the section's own standing assumption that $E$, $A$ are Borel spaces), but no metrizability or separability instance is required beyond what each statement's own topology needs — sequences suffice for every semicontinuity notion used here, matching the book's own Appendix A, which is stated for metric spaces. The Markov Decision Model, its operators ($L_n$, $T_n$, $T_n^f$), the notion of a maximizer, and the Structure Assumption are restated from chunk 02a-model-bellman-equation in this mission's own MDPFinance.Semicontinuous namespace (drafts in this series cannot import one another). Set-valued upper/lower semicontinuity (Appendix A.2.1) is formalized with the book's own sequential definition, not Mathlib's neighborhood-filter-based UpperHemicontinuous/LowerHemicontinuous for correspondences — the book explicitly remarks that its own definition is "slightly more restrictive than other definitions appearing in the literature" (p. 351), so identifying the two without proof would silently substitute a different notion. The classes $\mathrm{IB}_b$, $\mathrm{IB}_b^+$ are formalized via the book's own equivalent bound-by-a-constant characterization rather than through the weighted supremum norm $\|\cdot\|_b$ itself, avoiding EReal division and its 0/0 := 0 convention for no loss of content. Each of Theorem 2.4.6's and Theorem 2.4.10's closing "in particular" sentences — restating chunk 02a's Theorem 2.3.8 applied to the (SAN) instance just constructed — is not repeated in this mission's Lean, since it is a corollary of a different chunk's goal, not new content of this section; only the "(SAN) is satisfied" conclusion that is this section's own contribution is stated. A trivializing formalization of the goal would specialize $A$ to a finite type or fix $D_n(x)$ to a single compact set independent of $x$, making hypotheses (i)-(iii) vacuous; this mission states the theorem for arbitrary Borel $A$ and a genuinely state-dependent $D_n(x)$.

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.
• C. J. Himmelberg, T. Parthasarathy, and F. S. Van Vleck, "Optimal plans for dynamic programming problems", Mathematics of Operations Research 1 (1976), 390-394.
• K. Kuratowski and C. Ryll-Nardzewski, "A general theorem on selectors", Bulletin de l'Académie Polonaise des Sciences 13 (1965), 397-403.

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

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)$,

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$,

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

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

Cooperative games model the division of a jointly produced surplus, or a jointly incurred cost, among the participants of an enterprise: towns sharing a water supply system, divisions of a firm sharing overhead, members of a consortium sharing the savings of joint investment. In such applications allocations are rarely fixed once and for all. Costs and revenues are re-estimated, projects are re-scoped, and the allocation is recomputed. A natural requirement on any allocation method is then monotonicity: when the underlying data change in a player's favour, that player's share should not fall.

H. P. Young, Monotonic Solutions of Cooperative Games (Int. J. Game Theory 14, 1985), studies several forms of this principle. The weakest, aggregate monotonicity, asks that no player lose when only the value of the grand coalition increases; Megiddo (1974) had already shown that the nucleolus violates it. The paper's first theorem concerns a stronger and more natural form, coalitional monotonicity, which was first proposed by Shubik (1962) in the context of cost allocation within a firm, and shows that it cannot be reconciled with the core, the most widely used stability requirement. This mission formalizes that impossibility theorem.

Setting

Fix $n$ players, $N = \{1, 2, \dots, n\}$. A cooperative game on $N$ is a function $v$ assigning a real number $v(S)$ to every coalition $S \subseteq N$, with $v(\emptyset) = 0$. No superadditivity or other structural assumption is imposed.

An allocation procedure is a map $\varphi$ that assigns to every game $v$ on $N$ an allocation $\varphi(v) = (\varphi_1(v), \dots, \varphi_n(v)) \in \mathbb{R}^N$ satisfying efficiency:

The core of $v$ is the set of allocations that no coalition can improve upon on its own:

It may be empty. An allocation procedure is a core allocation rule if $\varphi(v) \in C(v)$ for every game $v$ whose core is nonempty. The nucleolus is the standard example.

An allocation procedure is coalitionally monotonic (Eq. (4) of the paper) if raising the value of a single coalition, with all other values unchanged, never decreases the allocation of any member of that coalition: for all games $v, w$ and every coalition $T \subseteq N$,

The paper notes that this is equivalent to its one-player form (5): if every coalition containing player $i$ weakly gains in value and every coalition not containing $i$ is unchanged, then $\varphi_i$ does not decrease.

In the Lean development these objects are Game n, IsAllocationProcedure, IsCoreRule and IsCoalitionallyMonotonic in the namespace MonotonicSolutions.CoreRules, and the core is the published definition Supermodularity.Cooperative.Core.

Formalization targets

Goal: Theorem 1

For every $n \ge 5$,

Milestones

1. Eqs. (4)–(5). Coalitional monotonicity is equivalent to the one-player condition (5).
2. The core of the game $w$. For the explicit five-player game $w$ of the proof, built from the coalitions $S_1 = \{3,5\}$, $S_2=\{1,2,3\}$, $S_3=\{1,3,4\}$, $S_4=\{2,4,5\}$, $S_5=\{1,2,4,5\}$ with values $3,3,9,9,9$ and $w(N) = 11$, the core is the single point $(0,1,2,7,1)$.
3. The core of the game $v$. For the game $v$ equal to $w$ except $v(S_5) = v(N) = 12$, the core is the single point $(3,0,0,6,3)$.
4. The case $|N| = 5$. The goal with $n = 5$.

An additional statement records the paper's remark that the egalitarian rule $\varphi_i(v) = v(N)/|N|$ satisfies (5), so that the monotonicity axiom on its own is satisfiable.

Significance

The theorem shows that no refinement of the core, however cleverly designed, can be coalitionally monotonic once there are five or more players. For the nucleolus this strengthens Megiddo's earlier observation, and the paper uses it to motivate the search for monotonic solution concepts outside the core, which leads to its second theorem: the Shapley value is the unique symmetric allocation procedure satisfying an even stronger monotonicity property (the subject of the companion mission). In cost-allocation practice the result says that an allocation method that is always stable against coalitional secession must sometimes penalise a division for making its own operations cheaper.

The result has been proved since 1985, and its proof is a short explicit counterexample. What the formalization adds is a machine-checked version of the counterexample (two explicit games whose cores are single points), a verified equivalence between the coalition-wise and player-wise forms of monotonicity, and the extension from five to arbitrarily many players, which the paper dismisses as an "obvious extension". To the best of the curators' knowledge none of these statements is formalized in any proof assistant.

Difficulty

The individual steps are elementary, but each requires care. Determining the core of each counterexample game exactly means showing both that the given point satisfies all $2^5$ coalition constraints and that no other point does. The equivalence of (4) and (5) is stated in the paper as following from "successive application" of (4), and every game involved must vanish on the empty coalition. The two counterexample games differ on two coalitions, $S_5$ and $N$, so a single application of (4) does not suffice. Finally, the paper passes from five players to $n \ge 5$ players with the words "by obvious extension"; a formal proof has to make that step explicit, for arbitrary $n$ and for rules defined on all games with $n$ players, not only on those derived from five-player games.

Formalization scope

• Players are Fin n; the paper's player $k$ is the Lean index $k-1$. Thus the core points $(0,1,2,7,1)$ and $(3,0,0,6,3)$ appear as ![0,1,2,7,1] and ![3,0,0,6,3], and the players "2 and 4" whose allocations decrease are indices 1 and 3.
• A game is the subtype Game n := {v : Finset (Fin n) → ℝ // v ∅ = 0}. Monotonicity axioms therefore quantify only over normalised games, as in the paper.
• Allocations are real vectors Fin n → ℝ. Efficiency is part of the goal's hypotheses, matching the paper's definition of an allocation procedure.
• The core is Supermodularity.Cooperative.Core Finset.univ v.1, the published core definition from Supermodularity and Complementarity, which coincides with the set on p. 68 of the paper.
• IsCoreRule requires $\varphi(v) \in C(v)$ only when $C(v)$ is nonempty. The unconditional requirement would be unsatisfiable, because some games have an empty core, and would make the goal trivially true; that reading is ruled out.
• IsCoalitionallyMonotonic is Eq. (4) with $T$ ranging over all coalitions, including $N$. Restricting to $T \ne N$, or restricting the games to superadditive ones, would change the theorem.
• The counterexample games are defined in YoungGames: for $S \ne N$, the value is the largest listed $w(S_k)$ over the $S_k \subseteq S$, and $0$ if there is none.

Contributions welcome: proofs of the four milestones and the goal; a general lemma that padding a game with null players preserves the core up to zeros, which is reusable for other small-counterexample results in cooperative game theory; and decision procedures for linear feasibility over the coalitions of small games.

Selected references

• H. P. Young, Monotonic Solutions of Cooperative Games, International Journal of Game Theory 14 (1985), 65–72. https://doi.org/10.1007/BF01769885
• N. Megiddo, On the Nonmonotonicity of the Bargaining Set, the Kernel and the Nucleolus of a Game, SIAM Journal on Applied Mathematics 27 (1974), 355–358. https://doi.org/10.1137/0127026
• M. Shubik, Incentives, Decentralized Control, the Assignment of Joint Costs and Internal Pricing, Management Science 8 (1962), 325–343. https://doi.org/10.1287/mnsc.8.3.325
• D. B. Gillies, Solutions to General Non-Zero-Sum Games, in Contributions to the Theory of Games IV, Annals of Mathematics Studies 40 (1959), 47–85 (Princeton University Press). Cited as in Young (1985); no DOI checked.

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.