Motivation

Many regression problems have far more unknown coefficients $p$ than observations $n$: gene expression studies with tens of samples and thousands of genes, imaging from few measurements, nonparametric curve recovery from a finite number of noisy samples. Estimation is hopeless in general, but becomes possible when the parameter is sparse, that is, has few nonzero entries. Candès and Tao (arXiv:math/0506081; Ann. Statist. 35(6), 2007, doi:10.1214/009053606000001523) proposed the Dantzig selector, an estimator computed by a single linear program, and showed that its squared error is within a logarithmic factor of what an oracle that knew which coefficients matter could achieve.

The estimator became one of the two standard $\ell_1$ methods for high-dimensional regression, alongside the Lasso; the comparison of the two by Bickel, Ritov and Tsybakov (arXiv:0801.1095, 2009) is built on it. This mission targets the paper's main result, the oracle inequality (Theorem 1.2). A companion mission covers the simpler $\ell_2$ bound for sparse parameters (Theorem 1.1).

Setting

Observations follow the linear model

$$y = X\beta + z,$$

where $X\in\mathbb R^{n\times p}$ is a deterministic design matrix with columns $X_1,\dots,X_p$, each of Euclidean norm $\|X_j\|_{\ell_2}=1$; $\beta\in\mathbb R^p$ is an unknown deterministic parameter; and $z=(z_1,\dots,z_n)$ has independent $N(0,\sigma^2)$ coordinates, $\sigma>0$. The vector $\beta$ is $S$-sparse if at most $S$ of its entries are nonzero.

Two constants of $X$ measure how close sparse sets of columns are to being orthonormal. The restricted isometry constant $\delta_S$ is the smallest $\delta\ge0$ such that $(1-\delta)\|c\|_{\ell_2}^2\le\|Xc\|_{\ell_2}^2\le(1+\delta)\|c\|_{\ell_2}^2$ for every $c$ supported on at most $S$ indices. The restricted orthogonality constant $\theta_{S,S'}$ (defined for $S+S'\le p$) is the smallest $\theta\ge0$ with $|\langle Xc,Xc'\rangle|\le\theta\|c\|_{\ell_2}\|c'\|_{\ell_2}$ whenever $c,c'$ are supported on disjoint sets of sizes at most $S$ and $S'$. Below $\delta:=\delta_{2S}$ and $\theta:=\theta_{S,2S}$.

For a tuning level $\lambda_p>0$, a Dantzig selector $\hat\beta$ is any solution of

$$\min_{\tilde\beta\in\mathbb R^p}\|\tilde\beta\|_{\ell_1}\quad\text{subject to}\quad\|X^*(y-X\tilde\beta)\|_{\ell_\infty}=\sup_{1\le j\le p}|\langle y-X\tilde\beta,X_j\rangle|\le\lambda_p\sigma .$$

The ideal mean squared error is $\sum_{i=1}^p\min(\beta_i^2,\sigma^2)$: the risk of an oracle that keeps exactly the coordinates above the noise level.

Formalization targets

Goal: Theorem 1.2 (pp. 8–9)

Let $t>0$, $a\ge0$, and $\lambda_p:=(\sqrt{1+a}+t^{-1})\sqrt{2\log p}$. If $\beta$ is $S$-sparse and $\delta_{2S}+\theta_{S,2S}<1-t$, then with probability exceeding $1-(\sqrt{\pi\log p}\cdot p^a)^{-1}$ every Dantzig selector obeys

$$\|\hat\beta-\beta\|_{\ell_2}^2\le C_2^2\cdot\lambda_p^2\cdot\Big(\sigma^2+\sum_{i=1}^p\min(\beta_i^2,\sigma^2)\Big),$$

with the explicit constant (1.14)

$$C_2=\frac{2C_0}{1-\delta-\theta}+\frac{2\theta(1+\delta)}{(1-\delta-\theta)^2}+\frac{1+\delta}{1-\delta-\theta},\qquad C_0=2\sqrt2\Big(1+\frac{1-\delta^2}{1-\delta-\theta}\Big)+\Big(1+\frac1{\sqrt2}\Big)\frac{(1+\delta)^2}{1-\delta-\theta}.$$

Milestones

1. Lemma 3.2: $\|X\beta\|_{\ell_2}\le\sqrt{1+\delta}\,(\|\beta\|_{\ell_2}+(2S)^{-1/2}\|\beta\|_{\ell_1})$ for every $\beta$.
2. Lemma A.1 (dual sparse reconstruction, $\ell_2$ version): for $c$ supported on $|T|\le2S$, a vector $\beta$ on $T$ whose correlations $\langle X\beta,X_j\rangle$ equal $c_j$ on $T$ and are small off $T$ except on an exceptional set of size at most $S$, with bounds (6.1)–(6.6).
3. Corollary A.2 ($\ell_\infty$ version): the same without exceptional set, constants $1/(1-\delta-\theta)$.
4. Corollary A.3 (constrained thresholding): an $S$-sparse $\beta$ with $\|\beta\|_{\ell_2}<\lambda\sqrt S$ splits as $\beta'+\beta''$ with $\beta'$ small in $\ell_2$ and $\ell_1$ and $\|X^*X\beta''\|_{\ell_\infty}<\frac{1-\delta^2}{1-\delta-\theta}\lambda$.
5. Gaussian tail bound (Section 3, p. 15): $P(\sup_j|\langle z,X_j\rangle|>u)\le2p\,\varphi(u)/u$ for standard Gaussian noise.
6. Lemma 3.1: the $\ell_2$ mass of $h$ on $T_0$ and its top $S$ positions outside $T_0$ is controlled by $\|X^T_{T_{01}}Xh\|_{\ell_2}$ and $\|h\|_{\ell_1(T_0^c)}$.

Significance

The result. Theorem 1.2 says that a single linear program, which knows neither the support of $\beta$ nor which coefficients exceed the noise, matches the oracle risk $\sum_i\min(\beta_i^2,\sigma^2)$ up to a factor $O(\log p)$, uniformly over $S$-sparse parameters and with explicit, nonasymptotic constants. For coefficients well below the noise level it is far sharper than the $\sigma^2 S\log p$ bound of Theorem 1.1. It is the template for later oracle inequalities for $\ell_1$-penalized estimators under restricted isometry or restricted eigenvalue conditions.

Formalizing it. The theorem is proved in the paper, but parts of the argument are only sketched: Corollary A.2 refers to the 2005 Decoding by Linear Programming paper for its convergence argument, and Corollary A.3's $\ell_1$ bound is printed with a constant its own proof does not deliver. A machine-checked proof settles these steps. The restricted isometry and orthogonality constants used here are already published on the platform from the decoding series; the appendix lemmas on dual vectors are reusable for any compressed-sensing result in that framework. No formalization of the Dantzig selector's oracle inequality is known to us.

Difficulty

The natural proof compares $\hat\beta$ with the hard-thresholded parameter $\beta^{(1)}$ that keeps only the large coefficients: if $\beta^{(1)}$ were feasible for the Dantzig constraint, the analysis of Theorem 1.1 would apply directly. It is not feasible in general, because the small coefficients $\beta^{(2)}$, though individually below the noise level, can add up to a large correlation $X^*X\beta^{(2)}$. The central difficulty is to split $\beta^{(2)}$ into a part with controlled $\ell_1$ and $\ell_2$ norm and a part invisible to the constraint; this requires constructing dual vectors with prescribed correlations (Lemma A.1, Corollary A.2), via an iterative, geometrically convergent correction. The probabilistic part is a Gaussian tail estimate plus a union bound, and the bookkeeping of constants must be carried through exactly.

Formalization scope

Vectors are functions Fin p → ℝ, the design is Matrix (Fin n) (Fin p) ℝ, and the noise is a family z : Fin n → Ω → ℝ of mutually independent random variables (iIndepFun) each with law gaussianReal 0 σ². $\delta_{2S}$ and $\theta_{S,2S}$ are the published CandesTao.Decoding.restrictedIsometryConst X (2*S) and restrictedOrthogonalityConst X S (2*S) (infima, absolute value in the orthogonality condition). Domain: $S\ge1$ and $3S\le p$ (the paper defines $\theta_{S,S'}$ for $S+S'\le p$), which forces $p\ge3$ and $\log p>0$. A Dantzig selector is any $\ell_1$ minimizer over the feasible set; the $\ell_\infty$ constraint is a bound on every coordinate.

The goal bounds from above the (outer) probability of the bad event "no Dantzig selector exists, or some Dantzig selector violates (1.13)". Because the event includes non-existence, a definition no vector satisfies cannot make the theorem vacuous; and the constant $C_2$ is the printed (1.14), evaluated at $\delta_{2S}$, $\theta_{S,2S}$ of $X$, not a free constant chosen after the fact.

Corrected constant: Corollary A.3 is stated with $\|\beta'\|_{\ell_1}\le2\frac{1+\delta}{1-\delta-\theta}\|\beta\|_{\ell_2}^2/\lambda$, the bound its proof gives once Corollary A.2 is applied at an integer sparsity level; the printed statement omits the factor $2$. Corollary A.2 carries Lemma A.1's standing hypothesis $\delta+\theta<1$. The deterministic lemmas (3.1, 3.2, A.1–A.3) assume nothing about column norms, since their statements do not need it.

Useful infrastructure: monotonicity of $\delta_S$ and $\theta_{S,S'}$ in their indices (the proof applies the lemmas at a smaller sparsity level), the Gaussian tail bound $1-\Phi(u)<\varphi(u)/u$, existence of minimizers of the Dantzig linear program, and a sorting/blocking toolkit for "the $S$ largest positions". Proofs of individual milestones are welcome independently.

Selected references

• E. Candès and T. Tao, The Dantzig selector: statistical estimation when p is much larger than n, Ann. Statist. 35(6):2313–2351, 2007. arXiv:math/0506081v3, doi:10.1214/009053606000001523
• E. Candès and T. Tao, Decoding by linear programming, IEEE Trans. Inform. Theory 51(12):4203–4215, 2005. arXiv:math/0502327, doi:10.1109/TIT.2005.858979
• P. Bickel, Y. Ritov and A. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4):1705–1732, 2009. arXiv:0801.1095, doi:10.1214/08-AOS620
• D. Donoho and I. Johnstone, Ideal spatial adaptation by wavelet shrinkage, Biometrika 81(3):425–455, 1994. doi:10.1093/biomet/81.3.425

Why the copy count matters

Shadow tomography asks for predictions of many specified measurements of an unknown quantum state, while using as few prepared copies of that state as possible. The requested output is a list of acceptance probabilities, not a full description of the state. A procedure might exploit the fact that these are only $M$ numbers, even when the state has dimension $D$. The natural question is how far this saving can go. Aaronson's paper gives upper bounds and separates two sources of difficulty: one already present for ordinary probability distributions, and one arising from noncommuting quantum measurements.

This mission concerns the first source. It formalizes Theorem 16, which says that even when the state and every requested measurement are diagonal in the same basis, the number of copies must grow with $\min\{D,\log M\}/\varepsilon^2$ in the relevant asymptotic regime. In that special case, the unknown state is an ordinary distribution on $D$ outcomes. The theorem therefore puts a limit on any proposed improvement to shadow tomography that would promise fewer copies in all instances.

States, measurements, and estimates

A mixed state $\rho$ on a $D$-dimensional system is a positive semidefinite $D\times D$ complex matrix with trace one. A two-outcome measurement is represented by an effect $E$ satisfying $0\preceq E\preceq I$; it accepts $\rho$ with probability $\operatorname{Tr}(E\rho)$. When $\rho$ is diagonal, its diagonal entries are the probabilities of the $D$ basis outcomes. When $E$ is diagonal too, it specifies a randomized yes-or-no test on those outcomes. These conventions are stated in Section 3 of the paper.

Given effects $E_1,\ldots,E_M$, a shadow-tomography strategy measures $k$ independent copies $\rho^{\otimes k}$ and outputs estimates $b_1,\ldots,b_M$. It succeeds on $\rho$ when every estimate differs from $\operatorname{Tr}(E_i\rho)$ by at most $\varepsilon$. The lower bound requires success probability at least $2/3$ for every diagonal mixed state. The strategy may make a joint quantum measurement on all copies and may choose its estimates from its observed outcome. This is the same measurement model used in Problem 1.

Formalization targets

Classical special-case lower bound

The goal is the classical clause of Theorem 16. There are absolute constants $c>0$ and $N_0$ such that, for $D\ge N_0$, $\log_2 M\ge N_0$, and $0<\varepsilon\le1/6$, there are $M$ diagonal effects with 0/1 entries, corresponding to the known Boolean functions in Section 6.1, for which every strategy successful on all diagonal states must use

$$k\ge c\,\frac{\min\{D,\log_2 M\}}{\varepsilon^2}.$$

The hard measurements are chosen before the strategy is quantified. The statement therefore also rules out a strategy with a smaller copy count that works uniformly for all quantum states and measurements. Its constants and threshold express the $\Omega$ notation in Theorem 16, rather than specifying a numerical optimum.

Supporting targets

Four milestones come from the proof on pages 20–21: the high-probability overlap bound for independently chosen half-size subsets (Eq. (1)); the acceptance probability of a subset under its associated biased distribution; an upper bound on the mutual information between the hidden subset index and the observed samples; and the exact entropy formula with a quadratic entropy deficit. These statements expose the combinatorial and information-theoretic parts of the lower bound while leaving the goal as the paper's copy-complexity result.

What the result supplies

Theorem 16 sets a floor for shadow tomography that survives even when all operators commute. Any uniform copy bound for the full quantum task must respect this floor. The result also distinguishes the difficulty of predicting many properties of a distribution from the extra difficulty possible for noncommuting states and measurements, which the paper treats in a separate lower bound. Section 6 presents both bounds.

A complete formalization would give machine-checked statements and proofs for the finite subset construction, the entropy calculation, the information inequality, and the reduction from a successful quantum measurement procedure on diagonal states to a lower bound on $k$. The theorem is proved on paper; these draft statements are open Lean goals and do not claim that its proof has been machine checked. The finite-distribution and information-theory infrastructure is reusable for other lower bounds based on hidden-index families.

Where the argument is delicate

Counting how many possible measurements there are does not by itself show that samples reveal enough about which distribution generated them. The lower bound needs a quantitative relation between estimation accuracy and information about a hidden index, while each individual sample carries limited information. The paper's printed overlap condition (1) is too weak for the next displayed $\varepsilon/2$ estimate: at its boundary it gives $\varepsilon$. The milestone preserves Eq. (1) as printed; closing the goal requires the correspondingly sharper overlap fact with $N/24$, which follows from the same type of concentration statement after adjusting its constant. The printed assertion that learning the index requires mutual information at least $\log_2 K$ is also imprecise at success probability $2/3$; a quantitative decoding inequality is needed. Neither incorrect display is a draft milestone.

Formalization scope

Matrices are indexed by Fin D. WildeQIT.IsDensityOperator supplies the mixed-state predicate $\rho\succeq0$ and $\operatorname{Tr}(\rho)=1$. Diagonal states and effects use the standard matrix diagonal predicate. An effect is positive semidefinite together with its complement. The tensor power uses functions Fin k → Fin D as basis indices; at $k=0$ it is a one-by-one identity matrix. A strategy is a finite-outcome POVM on that tensor power, followed by a real estimate vector for each outcome. The output values are not restricted to $[0,1]$: clipping them to this interval cannot worsen an estimate of a probability. No restriction to classical estimators is placed in the goal; that would change the allowed strategies before the theorem has been proved.

The asymptotic threshold excludes the one-dimensional and single-measurement corners where the claimed rate does not describe the problem. The bound $\varepsilon\le1/6$ keeps the biased distributions used on page 20 nonnegative; $\varepsilon\ge1/2$ would permit a zero-copy constant estimate. Subset milestones require even $N$ or explicitly require a half-size subset, so $N/2$ has its intended meaning. The natural logarithm appears nowhere in the lower-bound rate; entropy, mutual information, and $\log_2 M$ use base two. At zero probability the entropy convention is $0\log 0=0$.

The finite distributions, entropy, conditional entropy, and mutual information reuse the published WildeQIT definitions. Contributions that prove the four source milestones, establish the sharper overlap fact, or supply the quantitative decoding step are welcome. The goal must retain its order of quantifiers: one hard measurement family, then every strategy, with success demanded on every diagonal state.

Selected references

• Scott Aaronson, Shadow Tomography of Quantum States, arXiv preprint arXiv:1711.01053v2, 2018. Preprint.

Motivation

In many statistical applications the number of unknown parameters $p$ is far larger than the number of observations $n$: gene-expression studies with tens of samples and thousands of genes, imaging problems with fewer measurements than pixels, and nonparametric curve estimation from finitely many noisy samples. Least squares is useless in this regime, since the system $X\beta=y$ is underdetermined. If the parameter is sparse (only a few of its entries are nonzero), estimation becomes possible, and the question is how accurate a computationally tractable estimator can be.

Candès and Tao (arXiv:math/0506081; Ann. Statist. 35(6), 2007, doi:10.1214/009053606000001523) introduced the Dantzig selector, an estimator computed by a linear program, and proved that its squared error is within a factor of order $\log p$ of the error of an oracle that knows where the nonzero entries are. The paper, with its discussion in the same issue, is one of the founding results of high-dimensional sparse regression, alongside the Lasso analysis of Bickel, Ritov and Tsybakov (arXiv:0801.1095).

Timeline. Candès and Tao (2005, arXiv:math/0502327) showed that $\ell_1$ minimization recovers a sparse vector exactly from noiseless data when the restricted isometry constants of the design satisfy $\delta_S+\theta_{S,S}+\theta_{S,2S}<1$. The Dantzig selector paper (first posted 2005, published 2007) carried this to Gaussian noise, with the $\ell_2$ error bound formalized here (Theorem 1.1) and an oracle inequality (Theorem 1.2). Bickel, Ritov and Tsybakov (2009) replaced the restricted isometry hypothesis by weaker restricted eigenvalue conditions and showed that the Lasso and the Dantzig selector behave alike.

Setting

Observe $y\in\mathbb R^n$ from the linear model

$$y=X\beta+z ,$$

where $X\in\mathbb R^{n\times p}$ is a deterministic design matrix with columns $X_1,\dots,X_p$, each of Euclidean norm $\|X_j\|_{\ell_2}=1$; $\beta\in\mathbb R^p$ is an unknown deterministic parameter; and $z=(z_1,\dots,z_n)$ is a vector of independent $N(0,\sigma^2)$ random variables with $\sigma>0$. The vector $\beta$ is $S$-sparse if at most $S$ of its entries are nonzero.

For $T\subseteq\{1,\dots,p\}$ let $X_T$ be the submatrix of the columns indexed by $T$. The restricted isometry constant $\delta_S$ is the smallest $\delta\ge0$ with

$$(1-\delta)\|c\|_{\ell_2}^2\le\|X_Tc\|_{\ell_2}^2\le(1+\delta)\|c\|_{\ell_2}^2$$

for all $|T|\le S$ and all coefficient vectors $c$; the restricted orthogonality constant $\theta_{S,S'}$ (for $S+S'\le p$) is the smallest $\theta\ge0$ with $|\langle X_Tc,X_{T'}c'\rangle|\le\theta\|c\|_{\ell_2}\|c'\|_{\ell_2}$ for all disjoint $T,T'$ with $|T|\le S$, $|T'|\le S'$.

Given a tuning parameter $\lambda_p>0$, the Dantzig selector $\hat\beta$ is any solution of

$$\min_{\tilde\beta\in\mathbb R^p}\|\tilde\beta\|_{\ell_1}\quad\text{subject to}\quad\|X^*(y-X\tilde\beta)\|_{\ell_\infty}=\max_{1\le j\le p}|\langle y-X\tilde\beta,X_j\rangle|\le\lambda_p\cdot\sigma .$$

Formalization targets

Goal: Theorem 1.1

Let $S\ge1$, $3S\le p$, $\beta$ $S$-sparse, and $\delta_{2S}+\theta_{S,2S}<1$. For every $a\ge0$, with $\lambda_p=\sqrt{2(1+a)\log p}$, with probability exceeding $1-(\sqrt{\pi\log p}\cdot p^a)^{-1}$ the program has a solution and every solution satisfies

$$\|\hat\beta-\beta\|_{\ell_2}^2\le C_1^2\cdot\lambda_p^2\cdot S\cdot\sigma^2,\qquad C_1=\frac{4}{1-\delta_{2S}-\theta_{S,2S}} .$$

For $a=0$ this is $\|\hat\beta-\beta\|_{\ell_2}^2\le C_1^2\cdot(2\log p)\cdot S\cdot\sigma^2$, display (1.10) of the paper. The constant is the one the paper's proof establishes (see Formalization scope).

Milestones

1. The cone constraint (3.2): if $\|\beta+h\|_{\ell_1}\le\|\beta\|_{\ell_1}$ and $\beta$ vanishes off $T_0$, then $\|h_{T_0^c}\|_{\ell_1}\le\|h_{T_0}\|_{\ell_1}$.
2. The tube constraint (3.3): with unit-normed columns, if $|\langle z,X_j\rangle|\le\lambda_p$ for all $j$ and $\hat\beta$ is feasible, then $\|X^*X(\hat\beta-\beta)\|_{\ell_\infty}\le2\lambda_p$.
3. Lemma 3.1 (under the section’s unit-column assumption): an $\ell_2$ bound on $h$ over $T_0\cup T_1$ ($T_1$ the $S$ largest entries of $h$ off $T_0$) in terms of $\|X_{T_{01}}^TXh\|_{\ell_2}$ and $\|h\|_{\ell_1(T_0^c)}$, and $\|h\|_{\ell_2}^2\le\|h\|_{\ell_2(T_{01})}^2+S^{-1}\|h\|_{\ell_1(T_0^c)}^2$.
4. The deterministic core: with $\sigma=1$, on the event $|\langle z,X_j\rangle|\le\lambda_p$ for all $j$, every Dantzig selector satisfies $\|\hat\beta-\beta\|_{\ell_2}^2\le C_1^2\lambda_p^2S$.
5. The Gaussian tail bound: for standard normal $z$ and $Z_j=\langle z,X_j\rangle$, $\mathbb P(\sup_j|Z_j|>u)\le2p\,\varphi(u)/u$ with $\varphi(u)=(2\pi)^{-1/2}e^{-u^2/2}$.

Significance

The result. Theorem 1.1 shows that an estimator computable by linear programming reaches, up to the factor $2\log p$ and the constant $C_1^2$, the squared error $S\sigma^2$ that least squares would attain if the support of $\beta$ were known in advance, even when $p\gg n$. The factor $\log p$ is the price of not knowing the support; the paper argues (p. 5) that, apart from this factor, (1.10) is unimprovable in general. The bound is non-asymptotic, with an explicit constant and an explicit failure probability, and it holds for every $S$-sparse $\beta$ simultaneously in the sense that the good event (the noise being nearly orthogonal to every column) does not depend on $\beta$. Its deterministic part, Lemma 3.1, is reused verbatim in the proof of the paper's oracle inequality (Theorem 1.2) and became a standard tool in compressed sensing.

Formalizing it. The result is proved, and to our knowledge no machine-checked proof exists. A formalization produces a checked version of the cone-and-tube argument behind most $\ell_1$-recovery guarantees, a Lean statement of the restricted isometry machinery for noisy data, and a checked Gaussian maximal inequality usable for other high-dimensional estimators. It also settles the exact constant: the paper prints $C_1=4/(1-\delta_S-\theta_{S,2S})$, while its proof gives $\delta_{2S}$ in place of $\delta_S$.

Difficulty

Lemma 3.1 is the main obstacle. The obvious approach bounds $\|h\|_{\ell_2}$ directly through restricted isometry, and it fails because the error $h$ is not sparse: it spreads over all $p$ coordinates, and restricted isometry controls $X$ only on vectors with at most $2S$ nonzero entries. The two constraints (3.2) and (3.3) only say that $h$ is concentrated in $\ell_1$ on the $S$ coordinates of $T_0$ and that $X^*Xh$ is small coordinatewise, and turning that into an $\ell_2$ bound on all of $h$ is where the work lies. In Lean this requires bookkeeping that is routine on paper: ordering the coordinates of $h$ off $T_0$ by magnitude, with ties and a possibly incomplete last group of coordinates, and working with the span of a selected set of columns. On the probabilistic side, the tail bound needs the law of $\langle z,X_j\rangle$ (a weighted sum of independent Gaussians), a sharp Gaussian tail estimate of Mills-ratio type, and a union over $p$ events. A cruder sub-Gaussian bound $2e^{-u^2/2}$ would not give the stated failure probability.

Formalization scope

Indices are Fin n and Fin p; vectors are functions into ℝ. The norms, the column $X_j$ and the constants $\delta_S$, $\theta_{S,S'}$ are the published definitions CandesTao_Decoding_Norms and CandesTao_Decoding_RestrictedIsometry (the smallest admissible constants, via sInf), from the formalization of Candès and Tao's Decoding by Linear Programming. The noise is a family z : Fin n → Ω → ℝ on a probability space, mutually independent (iIndepFun), each coordinate with law gaussianReal 0 σ². The $\ell_\infty$ constraint is coordinatewise. A Dantzig selector is any minimizer; uniqueness is not assumed. Section 3 works with $\sigma=1$; the goal is stated for general $\sigma>0$.

Committed conventions and corrections:

• Corrected constant. Theorem 1.1 is printed with $C_1=4/(1-\delta_S-\theta_{S,2S})$, but the proof (pp. 18–19) applies Lemma 3.1, whose $\delta$ is $\delta_{2S}$. Since $\delta_S\le\delta_{2S}$, the printed constant is stronger than what is proved. The goal and the deterministic core are stated with $C_1=4/(1-\delta_{2S}-\theta_{S,2S})$.
• Domain. $1\le S$ and $3S\le p$, because $\theta_{S,2S}$ is defined only for $S+2S\le p$. This forces $p\ge3$ and $\log p>0$.
• Failure event. The probability bounded is that of the set where no Dantzig selector exists or some Dantzig selector violates the bound. A version that only constrains existing solutions, or that assumes the feasible set is nonempty, would be weaker. The bound is strict, as in the paper's "exceeding", and is on the outer measure, so no measurability of the event is assumed.
• Standing assumptions are binders: unit-normed columns, independent Gaussian noise, deterministic $X$ and $\beta$.

A trivializing formalization is excluded: the hypothesis $\delta_{2S}+\theta_{S,2S}<1$ is on the actual least constants of $X$, not on free parameters, and it is satisfiable (for instance by $X=I_p$, where both constants vanish).

Needed infrastructure: sums of independent real Gaussians (Mathlib has gaussianReal and its convolution), a Mills-ratio tail bound, a sorting-based block decomposition of a Finset, and orthogonal projection onto the span of finitely many columns. The block decomposition and the tail bound are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of Lemma 3.1.

Selected references

• E. Candès and T. Tao, The Dantzig selector: statistical estimation when p is much larger than n, Ann. Statist. 35(6) (2007), 2313–2351. arXiv:math/0506081, doi:10.1214/009053606000001523
• E. Candès and T. Tao, Decoding by linear programming, IEEE Trans. Inform. Theory 51(12) (2005), 4203–4215. arXiv:math/0502327
• P. Bickel, Y. Ritov and A. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4) (2009), 1705–1732. arXiv:0801.1095

Why the G/G/1 queue

The single-server queue with general interarrival times and general service times, written G/G/1 in Kendall's notation, is the model left when every distributional assumption is removed from the classical single-server queue. Customers arrive one at a time, wait in line in first-come, first-served order, and are served one at a time. Almost nothing about it can be computed in closed form. What survives is a recursion for the waiting times of successive customers and the integral equation of its steady state, due to Lindley (Lindley, 1952). Every exact and approximate treatment of the G/G/1 waiting time, including the bounds of the next chapter of the book, starts from that equation.

This mission is the eighth of a series formalizing Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, DOI 10.1002/9781118625651). It covers Chapter 6, "General Models and Theoretical Topics". The chapter also treats the G/E_k/1 characteristic equation (§6.1), the M/D/c queue (§6.3) and maximum-likelihood estimation for M/M/1 (§6.7), which appear here as further milestones.

Timeline. Lindley (1952) derived the recursion and the integral equation and showed that a limiting waiting-time distribution exists when the mean service time is smaller than the mean interarrival time. Loynes (1962) gave the stationary solution as a supremum over the past of a random walk, for stationary rather than independent inputs. Clarke (1957) derived the maximum-likelihood estimators for M/M/1, and Crommelin (1932) the M/D/c generating function. Chaudhry, Harris and Marchal (1990) located the roots of the G/E_k/1 characteristic equation.

Setting

The interarrival times $T^{(n)}$ are independent with common distribution $A$, the service times $S^{(n)}$ are independent with common distribution $B$, and the two sequences are independent. Both $A$ and $B$ are lifetime laws: probability distributions on $[0,\infty)$. The means are $\mathrm E[T]=1/\lambda$ and $\mathrm E[S]=1/\mu$, and the traffic intensity is $\rho=\lambda/\mu=\mathrm E[S]/\mathrm E[T]$.

The line delay $W_q^{(n)}$ of the $n$th customer satisfies Lindley's recursion

$$W_q^{(n+1)}=\max\bigl(0,\;W_q^{(n)}+S^{(n)}-T^{(n)}\bigr).$$

Write $U$ for the distribution of $S-T$ with $S\sim B$ and $T\sim A$ independent. Since $W_q^{(n)}$ is independent of $(S^{(n)},T^{(n)})$, one step of the recursion sends the distribution $\nu$ of $W_q^{(n)}$ to the distribution of $\max(0,W+U)$ with $W\sim\nu$ independent of $U$. A stationary delay distribution is a probability distribution $\nu$ that this step maps to itself; its CDF is $W_q(t)=\nu((-\infty,t])$.

Formalization targets

Goal: Lindley's equation (6.8)

If $\mathrm E[T]$ and $\mathrm E[S]$ are finite and $\rho<1$, then a stationary delay distribution exists, and the CDF of every stationary delay distribution satisfies

$$W_q(t)=\begin{cases}\displaystyle\int_{-\infty}^{t}W_q(t-x)\,dU(x) & (0\le t<\infty),\\ 0 & (t<0),\end{cases} \qquad U(x)=\int_{\max(0,x)}^{\infty}B(y)\,dA(y-x).$$

The goal consists of the existence statement and the equation together. The equation alone is close to unfolding one step of the recursion. Existence is what ties it to a queue in steady state.

Milestones

• (6.9), the CDF of $U=S-T$ as a convolution of $B$ and $A$.
• The one-step convolution (p.285): $W_q^{(n+1)}(t)=\int_{-\infty}^{t}W_q^{(n)}(t-x)\,dU(x)$ for $t\ge0$.
• (6.10)–(6.12), the Wiener–Hopf form: $W_q^-(t)+W_q(t)=\int_{-\infty}^t W_q(t-x)\,dU(x)$ for all $t$, and $\bar W_q(s)=\bar W_q^-(s)/(A^*(-s)B^*(s)-1)$ for two-sided Laplace transforms.
• The G/E_k/1 root result (p.278): the characteristic equation $z^k=A^*[k\mu(1-z)]$ has exactly one root in $(0,1)$, one in $(-1,0)$ exactly when $k$ is even, and, when $A^*=[A_1^*]^k$, exactly $k$ distinct roots in the open unit disk.
• (6.18)–(6.20), the M/D/c generating function and $p_0$ in terms of the roots of $z^c=e^{-\lambda(1-z)}$.
• (6.33), the maximum-likelihood estimators $\hat\lambda=n_a/t$, $\hat\mu=n_c/t_b$ for M/M/1.

Significance

Lindley's equation characterizes the stationary G/G/1 waiting time without any distributional assumption. The M/M/1, M/G/1 and G/M/1 waiting-time distributions of earlier chapters are its special cases. The transform relation (6.12) reduces the G/G/1 delay to a factorization problem for $A^*(-s)B^*(s)-1$. The recursion and the equation are the starting point of Kingman's bound, of heavy-traffic approximations and of simulation of single-server systems.

All of these results are classical and proved. As far as a search of the platform shows, none of them is formalized. The platform's forward-coupling mission proves convergence to a stationary workload of a continuous-time queue that it assumes to exist. It proves neither the existence of a stationary law of Lindley's discrete recursion nor Lindley's equation. The mission therefore produces a machine-checked account of the G/G/1 recursion on distributions, a Loynes-type existence theorem for it, and the Wiener–Hopf transform identity. Its definitions (lifetime laws, the law of $S-T$, the law map of the recursion, two-sided transforms) are reusable for Kingman's bound in the next mission of the series.

Difficulty

The obvious route to existence is to iterate the recursion from $W_q^{(0)}=0$ and take a limit. The distributions of $W_q^{(n)}$ from zero increase stochastically, but a limit of CDFs need not be a probability distribution: mass can escape to infinity, and it does when $\rho>1$. Ruling this out under $\rho<1$ is the whole content of the existence half. It is a statement about the entire past of the input sequences, not about one step of the recursion, and the book asserts it without argument ("In the steady state ($\rho<1$) …", p.285).

The transform identity (6.12) needs the right strip of convergence, which the book does not state. $A^*(-s)$ is finite only where the interarrival time has an exponential moment.

Formalization scope

Distributions are Mathlib measures on $\mathbb R$. $A$ and $B$ are probability measures with no mass on $(-\infty,0)$, with integrable identity where means are used. $\rho<1$ is stated as $\mathrm E[S]/\mathrm E[T]<1$ with $\mathrm E[T]>0$. Independence is encoded by product measures: $U$ is the image of $B\otimes A$ under $(s,t)\mapsto s-t$, and one step of the recursion is the image of $\nu\otimes U$ under $(w,u)\mapsto\max(0,w+u)$. Stieltjes integrals over $(-\infty,t]$ are Lebesgue integrals over the closed half-line, so the atom $W_q(0)=q_0$ is counted. Transforms take complex arguments.

The closed forms carried by the statements are the following.

• (6.8), in both of the book's forms, $\int_{-\infty}^t W_q(t-x)\,dU(x)$ and $-\int_0^\infty W_q(y)\,dU(t-y)$.
• (6.9) as an integral against the law of $T+x$.
• $U^*(s)=A^*(-s)B^*(s)$ and (6.12), for $0<\operatorname{Re}s$ with $\int e^{(\operatorname{Re}s)x}\,dA(x)<\infty$. The division is stated only where $A^*(-s)B^*(s)\ne1$.
• (6.18) and (6.19) with the denominator $1-z^ce^{\lambda(1-z)}$ cleared on $|z|\le1$, and (6.20) for $c\ge2$. The roots $z_1,\dots,z_{c-1}$ are hypotheses: distinct, $\ne1$, and exhausting the roots in the closed disk.
• (6.33) as the unique maximizer of $-\lambda t-\mu t_b+n_a\ln\lambda+n_c\ln\mu$ over $\lambda,\mu>0$.

A stationary delay distribution is a fixed point of the law map of the recursion, not an arbitrary CDF assumed to satisfy (6.8). A statement of (6.8) for "any CDF with $W_q=W_q*U$ on $[0,\infty)$" would assume its own conclusion, and is excluded. The statement for M/D/c includes existence of a steady state under $\lambda<c$ as well as the formula for every steady state.

Not formalized: §6.1.1–6.1.2 (G/PH_k/1, quasi-birth–death processes), §6.4 (semi-Markov processes, whose limit theorems the book quotes without hypotheses), §6.5 (random-order and last-come service, series representations), §6.6 (design and control), and the rest of §6.7.

Contributions are welcome on the random-walk representation of the recursion, on the existence theorem under $\rho<1$, and on the transform identities. The first two are reusable for any single-server or storage model driven by a reflected random walk.

Selected references

• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651
• D. V. Lindley, "The theory of queues with a single server", Mathematical Proceedings of the Cambridge Philosophical Society 48(2), 1952. https://doi.org/10.1017/S0305004100027638
• R. M. Loynes, "The stability of a queue with non-independent inter-arrival and service times", Mathematical Proceedings of the Cambridge Philosophical Society 58(3), 1962. https://doi.org/10.1017/S0305004100036094
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, 2nd ed., Wiley, 1971.
• A. B. Clarke, "Maximum likelihood estimates in a simple queue", Annals of Mathematical Statistics 28(4), 1957. https://doi.org/10.1214/aoms/1177706796
• M. L. Chaudhry, C. M. Harris, W. G. Marchal, "Robustness of rootfinding in single-server queueing models", ORSA Journal on Computing 2(3), 1990. https://doi.org/10.1287/ijoc.2.3.273

Strassen's Theorems and the Stochastic Ordering of Queues

Background

Chapters 1–3 of Baccelli and Brémaud's Elements of Queueing Theory compute exact quantities: Palm identities, stability criteria, PASTA, Pollaczek–Khinchin. Chapter 4 asks a different question. When you cannot compute a queue, can you at least say it is better than another one?

That requires an order on distributions. The chapter builds a family of them — integral orders — by choosing a class ℒ of test functions and declaring F ≤_ℒ G when ∫f dF ≤ ∫f dG for all f ∈ ℒ. Three matter: {i} the non-decreasing functions, giving the strong (stochastic) order; {cx} the convex functions, giving the convex order; and their intersection {icx}.

The goal

An integral order compares two distributions that need not live on the same probability space, and that is both its convenience and its difficulty. Strassen's theorems say each of these orders is secretly a statement about a coupling.

Theorem 4.2.2 (p.278), Strassen's ≤_cx theorem:

F ≤_cx G   ⟺   ∃ X ~ F, Y ~ G on one space with  E[Y | X] = X  a.s.
F ≤_icx G  ⟺   the same with  E[Y | X] ≥ X  a.s.

The convex order holds exactly when G is a martingale dilation of F — obtained by spreading each point out without moving its conditional mean. That is what makes the order usable: comparison results for queues become induction arguments on a coupling instead of analytic manipulations of convolutions of c.d.f.'s.

Its companion Theorem 4.2.1 is the ≤_st version, where the coupling is the simpler X ≤ Y a.s. In dimension one both are explicit — take X = F⁻¹(U), Y = G⁻¹(U) for a uniform U. In dimension n there is no such formula, and that is why these are Strassen's theorems. The book attributes both to Strassen (1965) and proves neither.

Why FIFO is optimal

§4.1 is a different kind of comparison: not between two queues, but between two service disciplines for the same queue. The order there is majorization ≺, which compares how spread out two vectors of the same total are.

The answer is that FIFO minimizes E⁰[f(V)] for every convex f (Property 4.1.3), and the proof is an interchange argument. Under any non-preemptive discipline that uses no information on the service times, customer k effectively receives service σ_{γ(k)} for some permutation γ; Lemma 4.1.3 shows the same queue is produced by FIFO fed with that reordered input, and that the reordering does not change the law of the input. Lemma 4.1.4 passes to the limit, which needs ρ < 1. Lemmas 4.1.1 and 4.1.2 then do the combinatorics: undoing one inversion of γ makes the waiting-time vector less spread out, so the identity permutation — FIFO — is extremal.

Feller's paradox, and what survives it

§4.4 compares time-stationary queues, and opens with a warning. T_n[P⁰] ≤_i T̃_n[P̃⁰] for every n does not imply T_n[P] ≤_i T̃_n[P̃]: Example 4.4.1, "Feller's paradox revisited", exhibits a Poisson process and a renewal process where the Palm order holds and the stationary one fails. The order does not pass from the Palm probability to the stationary one.

For ≤_cx it does. Lemma 4.4.1 is why: it expands E_P[f(N[0,x))] as a series of second differences of f against Palm expectations, and a convex f makes every coefficient non-negative. Lemma 4.4.2 handles the S-orders, built by dividing Palm integrals by the mean cycle length, and shows that the normalisation does not hide the comparison it normalises by.

Formalization scope

• Orders. ≤_i, ≤_cx, ≤_icx on distributions on ℝⁿ are integral orders over the book's test classes (§4.2.1), with the page's qualification that only test functions with well-defined integrals count. Majorization ≺ is (4.1.2) with increasing reorderings of both vectors.
• Strassen. Both theorems are stated as equivalences, with the coupling existential over the probability space. Theorem 4.2.2 carries both clauses — E[Y | X] = X for ≤_cx, E[Y | X] ≥ X for ≤_icx, as conditional expectations given σ(X) — and assumes both distributions integrable; Theorem 4.2.1 has no integrability hypothesis. A one-directional statement (the Jensen half) is not the theorem.
• The queue of §4.1.3 is constructed: a GI/GI input (i.i.d. inter-arrival and service times, independent), a single work-conserving server started empty, and any non-preemptive discipline whose choices are measurable in the information the book's σ-field 𝒢_t carries (arrivals, service times of customers already started) plus external randomisation. FIFO is one such discipline. The interchange permutations γ_n and their limit γ are built from the schedule as on pp.268–270; Lemma 4.1.4 assumes ρ = E[σ₀]/E[τ₀] < 1.
• Lemma 4.4.1 is stated with the exact second-difference series and assumes that series converges absolutely; the page states it for all f, which fails for heavy-tailed counts and sparse f.
• The S-orders test against {I-ℒ} — primitives ∫_0^t f(u, x) du of test functions — and apply only to distributions whose first coordinate is a.s. positive with a finite mean.

What this mission provides

None of it exists. Mathlib has no stochastic order, no convex order, no increasing-convex order, no majorization, no Schur-convexity and no Strassen theorem; the platform returns zero hits for q=stochastic ordering. Everything in this chapter is new substrate — and §§4.1–4.2 need nothing from Palm calculus, so this mission can be read on its own.

Motivation

Bernoulli's law of large numbers says that the relative frequency of a single event $A$ in $l$ independent trials converges in probability to $P(A)$. Statistics and learning theory need more: the probabilities of a whole class $S$ of events are judged from one and the same sample, so the frequencies must converge uniformly over the class. Uniform convergence can fail even for simple classes (all open subsets of $[0,1]$), so one needs a criterion that says when it holds and how fast.

Vapnik and Chervonenkis gave the first distribution-free answer in On the Uniform Convergence of Relative Frequencies of Events to Their Probabilities (Theory Probab. Appl. 16 (1971) 264–280, doi:10.1137/1116025). Its Theorem 2, now called the VC inequality, bounds the probability of a uniform deviation larger than $\varepsilon$ by a combinatorial quantity of the class times an exponentially small factor.

Timeline:

• 1933: Glivenko and Cantelli prove uniform almost-sure convergence of the empirical distribution function on the line (the class of rays $\{x \le a\}$).
• 1971: Vapnik and Chervonenkis publish the growth function, the VC inequality (Theorem 2), almost-sure convergence under polynomial growth (Theorem 3) and the entropy criterion (Theorem 4).
• 1972: Sauer and Shelah independently prove the polynomial bound on the growth function (the paper's Lemma 1).
• From the late 1970s: the inequality is sharpened in its constants and extended to empirical processes (Dudley, Pollard, Talagrand).

Setting

Let $(X, P)$ be a probability space and $S$ a collection of measurable events $A \subseteq X$, with probabilities $P_A$. A sample of size $l$ is a sequence $x_1, \dots, x_l$ of points of $X$ drawn independently with law $P$, so the sample has the product law $P^l$ on $X^l$. The relative frequency of $A$ in the sample is $\nu_A^{(l)} = n_A / l$, where $n_A$ is the number of sample terms in $A$. The uniform deviation is

$$\pi^{(l)} = \sup_{A \in S} \bigl|\nu_A^{(l)} - P_A\bigr|.$$

Each $A \in S$ induces in a sample $x_1, \dots, x_r$ the subsample of terms lying in $A$. The index $\Delta^S(x_1, \dots, x_r)$ is the number of different subsamples so induced (at most $2^r$), and the growth function is $m^S(r) = \max \Delta^S(x_1, \dots, x_r)$ over all samples of size $r$.

For a double sample $x_1, \dots, x_{2l}$ let $\nu'_A$ and $\nu''_A$ be the frequencies of $A$ in the two semi-samples $x_1, \dots, x_l$ and $x_{l+1}, \dots, x_{2l}$, and let

$$\rho^{(l)} = \sup_{A \in S} \bigl|\nu'_A - \nu''_A\bigr|.$$

Following the paper, $\pi^{(l)}$ and $\rho^{(l)}$ are assumed to be measurable functions of the sample for every $l$.

Formalization targets

Goal: Theorem 2 (p. 269)

For every $\varepsilon > 0$ and every $l \ge 2/\varepsilon^2$,

$$P\bigl(\pi^{(l)} > \varepsilon\bigr) \le 4\, m^S(2l)\, e^{-\varepsilon^2 l/8}.$$

The constants $4$ and $1/8$ and the growth function at $2l$ are the paper's.

Milestones, in the order of the proof

1. Lemma 2 (p. 268): for $l \ge 2/\varepsilon^2$, $P\{\rho^{(l)} \ge \varepsilon/2\} \ge \tfrac12 P\{\pi^{(l)} > \varepsilon\}$.
2. Eq. (11) (p. 270): $P\{\rho^{(l)} \ge \varepsilon/2\} = \int \frac{1}{(2l)!} \sum_{T} \theta\bigl(\rho^{(l)}(T X_{2l}) - \varepsilon/2\bigr)\, dP$, the sum over all permutations $T$ of the $2l$ positions ($\theta$ the indicator of $[0, \infty)$).
3. The $\Gamma$ estimate (p. 271): for $0 \le m \le 2l$,

$$\Gamma = \sum_{k : |2k/l - m/l| \ge \varepsilon/2} \frac{\binom{m}{k}\binom{2l-m}{l-k}}{\binom{2l}{l}} \le 2e^{-\varepsilon^2 l/8}.$$

4. The per-sample permutation bound (p. 271): for every fixed double sample, $\frac{1}{(2l)!}\sum_T \theta\bigl(\rho^{(l)}(T X_{2l}) - \varepsilon/2\bigr) \le 2\Delta^S(x_1, \dots, x_{2l})\, e^{-\varepsilon^2 l/8}$.
5. The semi-sample bound (p. 271): $P\{\rho^{(l)} \ge \varepsilon/2\} \le 2\, m^S(2l)\, e^{-\varepsilon^2 l/8}$ for every $l \ge 1$.

Further items (consequences, not milestones)

• Corollary (p. 269): if $m^S(l) \le l^n + 1$ for all $l$ and some finite $n$, then $P(\pi^{(l)} > \varepsilon) \to 0$ for every $\varepsilon > 0$.
• Theorem 3 (p. 271): under the same condition, $P(\pi^{(l)} \to 0) = 1$ for an infinite i.i.d. sequence.

Significance

The bound holds for every distribution $P$ and depends on the class only through $m^S(2l)$. Together with the paper's Theorem 1 (the growth function is either $2^r$ for every $r$ or bounded by $r^n + 1$), it shows that every class whose growth function is not identically $2^r$ enjoys uniform convergence at an exponential rate in probability and almost surely. The Glivenko–Cantelli theorem is the special case of rays on the line. The inequality underlies sample-complexity bounds for empirical risk minimization, the "finite VC dimension implies learnability" direction of the fundamental theorem of statistical learning, and the theory of empirical processes indexed by sets.

The result has been proved for more than fifty years; what is missing is a machine-checked proof of it in its original form. Formal libraries contain Hoeffding-type inequalities for independent variables and textbook uniform-convergence statements with other constants, stated for hypothesis classes and loss functions. This mission produces the 1971 statement itself, with its constants and its sequence-based index, together with the combinatorial tail bound for sampling without replacement that the paper states without proof.

Difficulty

The obvious argument applies Hoeffding's inequality to each $A \in S$ and takes a union bound. This fails as soon as $S$ is infinite, and the classes of interest are uncountable. The growth function can only enter after the probabilities $P_A$ have been removed from the event, because only then does the event depend on the finitely many subsamples that $S$ induces on a finite sample. Lemma 2 does this at the price of the condition $l \ge 2/\varepsilon^2$ and a factor $2$.

The second difficulty is combinatorial. Under a random rearrangement of a fixed double sample, the number of points of an event that fall into the first half is hypergeometric, not binomial. The paper states the required tail bound $\Gamma \le 2e^{-\varepsilon^2 l/8}$ and omits the "simple but long computation". Mathlib has no tail bound for sampling without replacement.

Formalization scope

Samples are functions Fin l → X with 0-based positions; repetitions are allowed. The subsample induced by $A$ is the set of positions {i | x i ∈ A}, so the index counts distinct sets of positions and the growth function maximizes over sequences, not finite point sets (the paper's model; the two differ when $X$ has fewer than $r$ points). The sample law is Measure.pi (fun _ : Fin l => P). The double sample is Fin (l + l) → X, read through Fin.castAdd and Fin.natAdd, and $m^S(2l)$ is growth S (2 * l). Suprema are real suprema over the events of $S$ (values in $[0, 1]$; $0$ for $S = \emptyset$). Probabilities are values in $[0, \infty]$ and the bounds enter through ENNReal.ofReal. Theorem 3 uses the infinite product Measure.infinitePi and evaluates $\pi^{(l)}$ on the first $l$ coordinates.

The measurability of $\pi^{(l)}$ (p. 265) and of $\rho^{(l)}$ (p. 268) are the paper's own assumptions and are carried as hypotheses. Without them Theorem 2 can fail for uncountable classes; replacing them by a stronger condition such as countability of $S$ would weaken the theorem.

A trivializing formalization is ruled out as follows: $\varepsilon > 0$ is stated, which forces $l \ge 1$ and so avoids the value $0/0 = 0$ of the frequency. The supremum runs over the events of $S$, not over all subsets. The index counts distinct subsamples, not sets.

Corrections of the printed text:

1. Lemma 2 is printed for $l > 2/\varepsilon^2$, but its proof concludes for $l \ge 2/\varepsilon^2$, and Theorem 2 uses $l = 2/\varepsilon^2$. The $\ge$ form is stated, which is the stronger statement.
2. The text before the permutation bound describes the averaged quantity as counting arrangements with $|\nu'_A - \nu''_A| \le \tfrac12\varepsilon$; the indicator and the index set of $\Gamma$ count those with $\ge \tfrac12\varepsilon$, which is what is stated.
3. Slips in the proof of Lemma 2 that do not affect any statement: $\varepsilon/3$ printed for $\varepsilon/2$ on p. 269, and $<$, $>$ where Chebyshev's inequality gives $\le$, $\ge$.
4. Theorem 2 prints "more then" for "more than".

Needed infrastructure:

• the invariance of Measure.pi under permutations of coordinates;
• the splitting of Fin (l + l) into two halves under the product measure;
• Chebyshev's inequality for binomial frequencies;
• a hypergeometric (sampling without replacement) tail bound.

The last two are reusable beyond this mission. Proofs of any milestone are welcome.

Selected references

• V. N. Vapnik and A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, Theory Probab. Appl. 16(2) (1971) 264–280. https://doi.org/10.1137/1116025
• W. Hoeffding, Probability inequalities for sums of bounded random variables, J. Amer. Statist. Assoc. 58 (1963) 13–30. https://doi.org/10.1080/01621459.1963.10500830
• N. Sauer, On the density of families of sets, J. Combin. Theory Ser. A 13 (1972) 145–147. https://doi.org/10.1016/0097-3165(72)90019-2
• S. Shalev-Shwartz and S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Ch. 6 and 28. https://doi.org/10.1017/CBO9781107298019