Statistics

Motivation

Many statistical problems — nonparametric regression, density estimation, dimension reduction, testing — are naturally posed as optimization over a space of functions rather than a finite-dimensional parameter vector. Hilbert spaces provide the right generality: they carry an inner product and a norm, so notions of projection, orthogonality and least-squares fitting all make sense, exactly as in ordinary Euclidean space, even though the "vectors" are now functions. Reproducing kernel Hilbert spaces (RKHSs) are the particular class of function-valued Hilbert spaces that make this program computationally tractable: they are generated by a single bivariate kernel function, and every RKHS computation reduces to evaluating that kernel, never to manipulating an infinite-dimensional object directly (the "kernel trick"). Wainwright's High-Dimensional Statistics (2019), Chapter 12, develops the foundational correspondence between kernels and Hilbert spaces that makes this possible, and this mission formalizes its two central theorems.

Setting

A Hilbert space is a complete inner product space (Definitions 12.1–12.2); this mission uses Mathlib's own NormedAddCommGroup/InnerProductSpace ℝ/CompleteSpace typeclasses for this notion throughout. A linear functional $L:H\to\mathbb R$ is bounded if $|L(f)|\le M\|f\|_H$ for some $M<\infty$ and all $f\in H$; the Riesz representation theorem (Theorem 12.5) says every such functional is $L(f)=\langle f,g\rangle_H$ for a unique $g\in H$.

A bivariate function $K:X\times X\to\mathbb R$ is a positive semidefinite (PSD) kernel (Definition 12.6) if it is symmetric and every finite Gram matrix $(K(x_i,x_j))_{i,j=1}^n$ is positive semidefinite — the natural generalization of a PSD matrix to a (possibly infinite) index set $X$, with no topological structure on $X$ required. A reproducing kernel Hilbert space (RKHS) for a kernel $K$ is a Hilbert space $H$ of functions on $X$ such that, for every $x\in X$, the function $K(\cdot,x)$ belongs to $H$ and

$$\langle f, K(\cdot,x)\rangle_H = f(x) \qquad \text{for all } f\in H \tag{12.3}$$

— the reproducing property. Equivalently (Definition 12.12), $H$ is an RKHS exactly when every evaluation functional $f\mapsto f(x)$ is bounded on $H$.

Formalization targets

Goal (Theorem 12.11, the Moore-Aronszajn theorem)

Given any PSD kernel function $K$ on any set $X$, there is a Hilbert space $H$ (embedded into functions on $X$) in which $K$ satisfies the reproducing property (12.3) — and this Hilbert space is unique: any two Hilbert spaces with this property for the same $K$ are linearly isometric via an isometry intertwining their embeddings into functions on $X$.

Milestones

• Theorem 12.5 (Riesz representation). Every bounded linear functional on a Hilbert space $H$ has a unique representer $g\in H$: $L(f)=\langle f,g\rangle_H$ for all $f$. Used inside the proof of Theorem 12.13 to produce the representer $R_x$ of each evaluation functional.
• Theorem 12.13 (the converse correspondence). Given any Hilbert space $H$ of functions on $X$ in which every evaluation functional is bounded, there is a unique PSD kernel $K$ satisfying the reproducing property for $H$ — completing the Moore-Aronszajn equivalence between PSD kernels and Hilbert spaces with bounded evaluation functionals.
• Theorem 12.20 (Mercer's theorem). Under compactness of $X$, continuity of $K$, and the Hilbert-Schmidt condition $\int_{X\times X}K^2\,dP\,dP<\infty$, the integral operator $T_K(f)(x)=\int_XK(x,z)f(z)\,dP(z)$ has an orthonormal eigenbasis $(\varphi_j)$ of $L^2(X;P)$ with non-negative eigenvalues $(\mu_j)$, and $K(x,z)=\sum_j\mu_j\varphi_j(x)\varphi_j(z)$, with the series converging absolutely and uniformly.

Significance

Theorem 12.11 is the theorem that makes the entire RKHS apparatus well-posed: every time a statistician writes down a kernel — linear, polynomial, Gaussian — Theorem 12.11 guarantees that a canonical Hilbert space of functions exists in which that kernel reproduces, so that optimizing over "the RKHS associated with $K$" is a well-defined problem, not merely a suggestive shorthand. Theorem 12.13's converse shows the correspondence is exact — the class of kernel-generated Hilbert spaces is exactly the class of function spaces with bounded evaluation, the class relevant to any statistical application that samples a function at finitely many points. Together, these two results are the foundation the book's own later chapters build directly on: Chapter 13's nonparametric least-squares oracle inequality, and Chapter 14's kernel density estimation, both work by optimizing over an RKHS and are only well-posed because of this correspondence. Mercer's theorem, in turn, is what connects the RKHS viewpoint back to the earlier feature-map viewpoint of Chapter 12.2.2 (Eq. 12.2): the eigenfunctions $(\sqrt{\mu_j}\varphi_j)_j$ give an explicit feature map into $\ell^2(\mathbb N)$ realizing $K$, and its expansion is what later underlies the book's discussion of kernel PCA and of RKHS balls as ellipsoids in $\ell^2(\mathbb N)$-coordinates.

Difficulty

The formalization difficulty is concentrated in getting the type of the existence-and- uniqueness claim right, not in any single hypothesis. A Hilbert space is not naturally a subtype of a fixed ambient space in Lean, so "the Hilbert space $H$" of Theorem 12.11 is formalized as an abstract type together with its own NormedAddCommGroup/InnerProductSpace ℝ/CompleteSpace instances, connected to "a space of functions on $X$" via an injective linear embedding into $X\to\mathbb R$ — and uniqueness must then be stated as an isometric equivalence between any two witnessing Hilbert spaces that respects this embedding, the faithful rendering of the book's own proof, which literally shows two candidate Hilbert spaces are equal as sets of functions. A second subtlety is keeping Theorem 12.11's hypotheses (a bare PSD kernel, no topology on $X$) cleanly separated from Mercer's theorem's additional compactness, continuity and measure-theoretic apparatus — the two theorems are frequently conflated informally, but the book is explicit that Theorem 12.11 needs none of Mercer's structure.

Formalization scope

$X$ is an unconstrained Type* for Theorem 12.5, 12.11 and 12.13 — no topology, matching the book's own generality. Mercer's theorem (Theorem 12.20) additionally requires [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] and a finite measure P, matching its own compactness/continuity/measure-theoretic hypotheses exactly, never applied outside that scope. The integral operator $T_K$ of Eq. (12.11a) is presented as an abstract linear map on Lp ℝ 2 P tied to the defining integral formula via an explicit hypothesis, rather than constructed as a def, since constructing it as a genuine well-defined operator (needing integrability and a.e.-measurability arguments) is proof content, not definitional content, and this mission's definitions file is sorry-free by convention. Mercer's orthonormal-basis index type is existentially quantified over a countable ι (∃ (ι : Type) (_ : Countable ι), ...) rather than fixed to ℕ, since L²(X;P) can be finite-dimensional for finite X (Example 12.18/12.21), where no infinite orthonormal basis exists; the uniform-convergence conjunct is correspondingly quantified over every bijection e : ℕ ≃ ι (vacuous when ι is finite, a genuine order-independent claim when ι is countably infinite). A trivializing formalization of this chapter would state only existence in Theorem 12.11 and drop uniqueness (explicitly warned against by this chapter's own brief), or state Mercer's convergence merely pointwise or in $L^2$ rather than absolutely and uniformly; this mission avoids both. Out of scope: the constructive proof detail of Theorem 12.11 (the explicit span-and-complete construction is proof content, not part of the statement), the chapter's worked kernel examples (linear, polynomial, Gaussian kernels, Examples 12.7–12.9), and the further consequences of Mercer's theorem (Corollary 12.26 on RKHS-ball ellipsoids, the feature-map connection of Eq. 12.14) — all natural follow-on work for a future mission on kernel-based nonparametric regression (Chapter 13, mission 13-nonparametric-ls), which restates whatever RKHS objects it needs locally rather than importing this mission's draft, per this book's series-wide convention.

Selected references

• Wainwright, M. J. High-Dimensional Statistics: A Non-Asymptotic Viewpoint. Cambridge University Press, 2019. Chapter 12. DOI: 10.1017/9781108627771.
• Aronszajn, N. "Theory of reproducing kernels." Transactions of the American Mathematical Society, 68(3), 1950, 337–404.
• Mercer, J. "Functions of positive and negative type, and their connection with the theory of integral equations." Philosophical Transactions of the Royal Society A, 209, 1909, 415–446.

Motivation

Chapters 2 through 8 of Wainwright's High-Dimensional Statistics build up sharp error bounds for a sequence of specific high-dimensional models — sparse linear regression via the Lasso (Chapter 7), sparse principal components (Chapter 8) — each proved from scratch with techniques tailored to that model's own penalty and loss. Chapter 9 steps back and asks what made all of those arguments work, and isolates the answer into two structural ingredients: a decomposable regularizer, whose triangle inequality is tight across a well-chosen subspace pair, and a restricted curvature condition on the loss, holding only on the cone that decomposability forces the estimation error into. Once these two ingredients are checked for a particular model, a single, already-proved oracle inequality hands back the error bound — no further optimization-theoretic argument is needed. This mission formalizes that oracle inequality itself, together with its two supporting theorems, as the reusable core the book's later chapters (nuclear-norm matrix regression in Chapter 10, graphical model selection in Chapter 11, group-sparse and overlap-group Lassos) each specialize.

Setting

Let $\Omega$ be a finite-dimensional real inner product space (e.g. $\mathbb R^d$, or a matrix space with the Frobenius inner product), and consider the regularized M-estimator

$$\hat\theta \in \operatorname*{arg\,min}_{\theta\in\Omega} \Big\{ L_n(\theta) + \lambda_n\Phi(\theta) \Big\},$$

where $L_n:\Omega\to\mathbb R$ is a convex empirical cost function, $\Phi:\Omega\to[0,\infty)$ is a norm-based regularizer, and $\lambda_n>0$ is a user-chosen regularization weight. Write $\theta^*$ for the true parameter and $\Delta:=\hat\theta-\theta^*$ for the estimation error.

A pair of subspaces $\mathcal M\subseteq\bar{\mathcal M}$ of $\Omega$ — the model subspace and its (possibly larger) closure — has an associated perturbation subspace $\bar{\mathcal M}^\perp$, the orthogonal complement of $\bar{\mathcal M}$. The regularizer $\Phi$ is decomposable with respect to $(\mathcal M,\bar{\mathcal M})$ if the triangle inequality $\Phi(\alpha+\beta)\le\Phi(\alpha)+\Phi(\beta)$ is an equality whenever $\alpha\in\mathcal M$ and $\beta\in\bar{\mathcal M}^\perp$ — the regularizer penalizes deviations away from the model subspace exactly as much as it possibly could. The canonical example is the $\ell_1$-norm with $\mathcal M=\bar{\mathcal M}$ the subspace of vectors supported on a fixed index set $S$.

Writing $\Phi^*(v):=\sup_{\Phi(u)\le 1}\langle u,v\rangle$ for the dual norm, the good event $\mathcal G(\lambda_n):=\{\Phi^*(\nabla L_n(\theta^*))\le\lambda_n/2\}$ says the regularization weight dominates the dual norm of the score function at the truth — the non-probabilistic conditioning hypothesis every result in this chapter is stated under. The subspace Lipschitz constant $\Psi(S):=\sup_{u\in S\setminus\{0\}}\Phi(u)/\|u\|$ measures the worst-case price of converting between the regularizer $\Phi$ and the error norm $\|\cdot\|$ on a subspace $S$.

Formalization targets

Goal (Theorem 9.19, "Bounds for general models")

Under (A1) $L_n$ convex, satisfying restricted strong convexity (RSC) with curvature $\kappa>0$, radius $R$ and tolerance $\tau_n^2$ — $E_n(\Delta):=L_n(\theta^*+\Delta)-L_n(\theta^*) -\langle\nabla L_n(\theta^*),\Delta\rangle \ge \frac{\kappa}{2}\|\Delta\|^2-\tau_n^2\Phi^2(\Delta)$ for $\|\Delta\|\le R$ — and (A2) $\Phi$ decomposable with respect to $(\mathcal M,\bar{\mathcal M})$: conditioned on $\mathcal G(\lambda_n)$, any optimal $\hat\theta$ satisfies

$$\text{(a)}\quad \Phi(\hat\theta-\theta^*) \le 4\big(\Psi(\bar{\mathcal M})\, \|\hat\theta-\theta^*\| + \Phi(\theta^*_{\mathcal M^\perp})\big),$$

and, whenever $\tau_n^2\Psi^2(\bar{\mathcal M})\le\kappa/64$ and $\varepsilon_n(\mathcal M,\bar{\mathcal M})\le R$,

$$\text{(b)}\quad \|\hat\theta-\theta^*\|^2 \le \varepsilon_n^2(\mathcal M,\bar{\mathcal M}) := \frac{9\lambda_n^2}{\kappa^2}\Psi^2(\bar{\mathcal M}) + \frac{8}{\kappa}\Big(\lambda_n\Phi(\theta^*_{\mathcal M^\perp}) + 16\tau_n^2\Phi^2(\theta^*_{\mathcal M^\perp})\Big).$$

Milestones

• Proposition 9.13. Under (A2) alone, conditioned on $\mathcal G(\lambda_n)$, the error $\Delta=\hat\theta-\theta^*$ lies in the cone $\mathbb C_{\theta^*}(\mathcal M,\bar{\mathcal M}):=\{\Delta\mid\Phi(\Delta_{\bar{\mathcal M}^\perp})\le 3\Phi(\Delta_{\bar{\mathcal M}})+4\Phi(\theta^*_{\mathcal M^\perp})\}$ — the purely geometric fact Theorem 9.19's curvature argument is built on.
• Corollary 9.20. When $\theta^*\in\mathcal M$ exactly, the approximation-error term of $\varepsilon_n^2$ vanishes and Theorem 9.19 collapses to $\Phi(\hat\theta-\theta^*)\le\frac{6\lambda_n}{\kappa}\Psi^2(\bar{\mathcal M})$, $\|\hat\theta-\theta^*\|^2\le\frac{9\lambda_n^2}{\kappa^2}\Psi^2(\bar{\mathcal M})$ — the form used directly against every concrete model in the rest of the book.
• Theorem 9.24. Under an alternative, gradient-based curvature condition ($\Phi^*$-curvature, Definition 9.22) and $\theta^*\in\mathcal M$, the dual-norm error is controlled directly: $\Phi^*(\hat\theta-\theta^*)\le 3\lambda_n/\kappa$.

Significance

Theorem 9.19 is the book's own claimed unifying result: as it remarks explicitly, the theorem is a deterministic implication, and every later probabilistic corollary in Parts II and III of the book is obtained by (i) checking that a specific loss/regularizer pair is decomposable with respect to a natural subspace pair for the problem at hand, (ii) certifying the RSC condition with high probability for that loss (via concentration arguments from Chapters 2–6), and (iii) choosing $\lambda_n$ large enough that the good event holds with high probability — then reading off the rate directly from $\varepsilon_n^2(\mathcal M,\bar{\mathcal M})$. Chapter 7's Lasso bound (Theorem 7.13, mission 07-sparse-linear) is exactly Corollary 9.20 specialized to $\Phi=\|\cdot\|_1$ and $\mathcal M$ the subspace of $s$-sparse vectors — but Chapter 9 proves it once, in a form that Chapter 10's nuclear-norm-regularized low-rank matrix regression (mission 10-matrix-rank), Chapter 11's graphical model selection, and the chapter's own group-Lasso and overlap-group-Lasso examples all instantiate without re-deriving the optimization argument.

Difficulty

The formalization difficulty here is almost entirely conceptual rather than syntactic: getting the two-subspace apparatus $(\mathcal M,\bar{\mathcal M})$ exactly right. The book explicitly allows $\bar{\mathcal M}$ to be a strict superset of $\mathcal M$ (needed for the nuclear norm in Chapter 10, where the naive choice $\mathcal M=\bar{\mathcal M}$ fails to be decomposable at all), so every definition and theorem in this mission is parameterized by the pair, not by a single subspace — and three genuinely different projections appear across the statements: the error vector's projection onto $\bar{\mathcal M}$ and onto $\bar{\mathcal M}^\perp$ (both keep the bar), versus the true parameter's projection onto $\mathcal M^\perp$ (the complement of the small, unbarred subspace). A further subtlety specific to this printed source: several of the book's own displayed equations for $\Psi(\cdot)$ in Theorem 9.19 and Corollary 9.20 lose the overbar on $\bar{\mathcal M}$ in PDF text extraction (a rendering artifact, not a mathematical ambiguity); resolving which subspace is meant required reading the surrounding proof text line by line, since only $\Psi(\bar{\mathcal M})$ — not $\Psi(\mathcal M)$ — is mathematically consistent with how the constant is derived and used (see MODERATION_NOTES.md).

Formalization scope

$\Omega$ is [NormedAddCommGroup Ω] [InnerProductSpace ℝ Ω] [FiniteDimensional ℝ Ω], matching the book's implicit assumption of a finite-dimensional inner-product parameter space throughout this part of the book. The regularizer's norm axioms (IsRegularizerNorm), the dual norm, and the subspace Lipschitz constant are all defined via sSup/sInf-free explicit formulas or sSup over an explicitly-described set (never an unconstrained supremum over all of $\Omega$), so no faithfulness trap from an unbounded or empty supremum arises (see MODERATION_NOTES.md's trap table). κ > 0 and λ_n > 0 are made explicit hypotheses of every theorem, matching Definition 9.15's own stated positivity of $\kappa$ and the chapter's running convention that $\lambda_n$ is a positive regularization weight — never a narrowing of the theorem's actual scope. A trivializing formalization of this chapter would either collapse the two-subspace machinery to a single subspace $\mathcal M=\bar{\mathcal M}$ (which is faithful only for the $\ell_1$/group-Lasso examples, not the general theorem, and not what Chapter 10 needs) or silently drop the second conjunct of Theorem 9.19's conclusion (part (b), the actual quantitative rate) in favor of only the qualitative part (a); this mission formalizes the full two-subspace statement and both conjuncts of the goal theorem. Out of scope: the chapter's worked examples (sparse GLMs, Corollary 9.26; group Lasso; nuclear-norm matrix regression) that specialize the goal to concrete models — Chapter 10's own mission (10-matrix-rank) restates the needed instance of this framework locally rather than importing this mission's draft, per this book's series-wide convention that no draft imports another chunk's draft. Also out of scope: the RSC-implies-restricted-eigenvalue correspondence (Example 9.16) and the $\mu_n(\Phi^*)$-based general RSC certification (Theorem 9.36, Section 9.8), both purely probabilistic results that lie outside this chapter's own deterministic core.

Selected references

• Wainwright, M. J. High-Dimensional Statistics: A Non-Asymptotic Viewpoint. Cambridge University Press, 2019. Chapter 9. DOI: 10.1017/9781108627771.
• Negahban, S. N., Ravikumar, P., Wainwright, M. J., Yu, B. "A unified framework for high-dimensional analysis of M-estimators with decomposable regularizers." Statistical Science, 27(4), 2012, 538–557.
• Tibshirani, R. "Regression shrinkage and selection via the Lasso." Journal of the Royal Statistical Society: Series B, 58(1), 1996, 267–288.

Motivation

Chapter 2's finite-hypothesis-set learning bound is uninformative the moment $H$ is infinite — $\log|H|$ diverges — yet most hypothesis sets used in practice (linear separators, neural networks, decision trees) are infinite. Chapter 3 answers the question the previous chapter's own worked example (axis-aligned rectangles, Example 2.4) leaves open: is efficient learning from a finite sample still possible for an infinite hypothesis set, and can this be shown in general rather than case by case? The chapter's answer runs through two complementary notions of complexity — Rademacher complexity, a data-dependent measure of how well a function family correlates with random noise, and the VC-dimension, a purely combinatorial measure of the number of distinct labelings a hypothesis set can realize on a finite point set — connected by Massart's lemma and Sauer's lemma, and culminating in a generalization bound that replaces $\log|H|$ with the VC-dimension $d$.

Setting

For a family $G$ of functions $Z\to[0,1]$ and a sample $S=(z_1,\dots,z_m)$, the empirical Rademacher complexity $\hat R_S(G) = \mathbb E_\sigma[\sup_{g\in G}\frac1m\sum_i\sigma_i g(z_i)]$ (Definition 3.1) measures how well $G$ fits random sign noise $\sigma$ on $S$; the Rademacher complexity $R_m(G) = \mathbb E_{S\sim D^m}[\hat R_S(G)]$ (Definition 3.2) averages this over samples. Theorem 3.3 converts a Rademacher-complexity bound directly into a generalization bound via McDiarmid's inequality. For binary hypothesis sets $H\subseteq(X\to\{-1,+1\})$, the growth function $\Pi_H(m)$ (Definition 3.6) counts the maximum number of distinct dichotomies $H$ realizes on $m$ points, and the VC-dimension $\mathrm{VCdim}(H)$ (Definition 3.10) is the largest $m$ for which $\Pi_H(m)=2^m$ (i.e. $H$ shatters some set of $m$ points). Massart's lemma (Theorem 3.7) is the purely combinatorial tool bounding the expected maximum of a sum of signed vector components by $\sqrt{\log|A|}$, and Sauer's lemma (Theorem 3.17) bounds the growth function itself, by induction on $m+d$, whenever the VC-dimension is finite.

Formalization targets

Theorem 3.3 (Rademacher generalization bound, milestone). For $G:Z\to[0,1]$ and any $\delta>0$, with probability at least $1-\delta$ over an i.i.d. sample $S$ of size $m$, for all $g\in G$: $\mathbb E[g(z)] \le \frac1m\sum_i g(z_i) + 2R_m(G) + \sqrt{\log(1/\delta)/(2m)}$.

Theorem 3.7 (Massart's lemma, milestone). For a finite $A\subseteq\mathbb R^m$ with $r=\max_{x\in A}\|x\|_2$: $\mathbb E_\sigma[\frac1m\sup_{x\in A}\sum_i\sigma_i x_i] \le r\sqrt{2\log|A|/m}$.

Theorem 3.17 (Sauer's lemma, milestone). For $H$ with $\mathrm{VCdim}(H)=d$, for all $m\in\mathbb N$: $\Pi_H(m) \le \sum_{i=0}^d\binom{m}{i}$.

Corollary 3.19 — the mission's goal. For $H\subseteq(X\to\{-1,+1\})$ with $\mathrm{VCdim}(H)=d$ and any $\delta>0$, with probability at least $1-\delta$, for all $h\in H$:

$$R(h) \le \hat R_S(h) + \sqrt{\frac{2d\log(em/d)}{m}} + \sqrt{\frac{\log(1/\delta)}{2m}}.$$

Significance

Corollary 3.19 is the chapter's answer to the question chapter 2 leaves open: it is Theorem 2.13's direct infinite-hypothesis-set generalization, replacing $\log|H|$ (undefined for infinite $H$) with the VC-dimension $d$ (finite even for many infinite hypothesis sets, such as halfspaces in $\mathbb R^k$, which have VC-dimension $k+1$). It is also the template every later margin bound in the book specializes (Chapters 5, 9, 10's SVM, multi-class and ranking margin bounds all replace this bound's uniform $\log|H|$/VC-dimension term with a scale-sensitive complexity measure derived from the same Rademacher-complexity machinery), and Sauer's lemma is independently one of the most cited results in learning theory and extremal combinatorics. No prior art on the Prove2Me platform is faithful to any of this chapter's content: RademacherSymmetrization.radS_chernoff (Aether Catalog) proves a different, Massart-optimized Chernoff bound for the empirical Rademacher complexity of a finite class — a different object (empirical vs. population) with a different bound form from Theorem 3.3/3.5 — and sauerShelah_full proves only the trivial identity sauerShelahBound k k = 2^k, not Sauer's lemma itself. A further hit, sauer_shelah (Aether Catalog, Algebra/SauerShelah.lean), does state the Sauer-Shelah bound itself (F.card ≤ ∑_{i≤d} C(n,i) for a family F of subsets of Fin n shattering no set larger than d) — checked and not reused: it is a different idiom from Theorem 3.17 as this chunk needs it, a fixed finite ambient domain Fin n with F a Finset of its subsets directly, rather than the book's own growth function Π_H(m) (a supremum over point-tuples drawn from an arbitrary, possibly infinite X, Definition 3.6) that this chunk's other items and the goal (Corollary 3.19) are built on; reusing it would require either abandoning GrowthFunction/HasVCDim (needed faithfully by the goal itself) or a nontrivial reduction lemma this mission's budget does not include, so sauer_lemma is drafted fresh against this chunk's own GrowthFunction/HasVCDim. All ten items are drafted fresh.

Difficulty

Sauer's lemma's proof is a genuine two-parameter induction (on $m+d$) with a real combinatorial construction: restricting $H$ to a sample $S$ of size $m$, then splitting the restricted family into $G_1$ (its restriction to the first $m-1$ points) and $G_2$ (the concepts whose membership in $G$ changes with the addition of the $m$-th point), with $|G_1|+|G_2|=|G|$ and $\mathrm{VCdim}(G_2) \le \mathrm{VCdim}(G)-1$ — a genuinely combinatorial argument, not a statement that unfolds by simp; a weaker restatement using only the trivial bound $\Pi_H(m)\le 2^d$ would be true but is explicitly not what Theorem 3.17 states (BRIEF.md's named trivializing formalization for this chapter). Massart's lemma needs the expectation of a supremum over a finite set of $2^m$-many sign patterns kept as an honest average, not silently replaced by a looser union bound. Corollary 3.19's own $em/d$ term inside the logarithm needs the side condition $d\le m$ carried through explicitly — Corollary 3.18's own domain restricts to $m\ge d$, and the bound is false, not merely unproved, without it (at $m<d$, $em/d$ can be smaller than $1$, making the logarithm negative).

Formalization scope

GeneralizationError/EmpiricalError are restated locally in this chunk's RademacherVC namespace (byte-identical in content to chunk 02-pac's own copies), since a draft item cannot import another chunk's draft module; this duplication is expected and will collapse once 02-pac is moderated, uploaded and listed as reusable in missions/README.md's "Published definitions" table. EmpiricalRademacherComplexity/Massart's lemma model the Rademacher signs σ as ranging over the finite type Fin m → Bool rather than a measure-theoretic i.i.d. process, so the "expectation over σ" in both is the exact finite uniform average over its 2^m outcomes — faithful and simpler than a MeasureTheory construction, since σ's distribution really is uniform on a finite set of outcomes for every finite m. GrowthFunction takes a tuple of m points (Fin m → X) rather than a size-m subset of X, a harmless generalization (repeated points never increase the dichotomy count) documented in the item's own docstring. HasVCDim is a Prop parametrized by the candidate dimension rather than a total ℕ/ℕ∞-valued function, so it does not cover the book's VCdim(H)=+\infty case (Examples 3.15-3.16); every theorem using it takes HasVCDim H d as an explicit hypothesis, matching the book's own "let H... with VCdim(H)=d." Theorem 3.3 adds an explicit measurability hypothesis on G (hGm) beyond the book's own displayed statement, needed to keep the Bochner integral ∫ z, g z ∂D from silently evaluating to 0 for a non-measurable g — this is the book's own standing assumption (footnote 3, p. 30) made an explicit hypothesis rather than an implicit one. No numerical constant in any of the four theorems is altered from the book's own; Corollary 3.19's side condition d ≤ m is kept explicit, per BRIEF.md's pitfall note.

Not formalized: Lemma 3.4 and Theorem 3.5 (the binary-classification specialization of Theorem 3.3 via the zero-one-loss identity $\hat R_S(G)=\frac12\hat R_{S_X}(H)$), Corollary 3.8 and Corollary 3.9 (the intermediate Rademacher-to-growth-function and growth-function generalization bounds), and Corollary 3.18 (the VC-dimension bound on the growth function, $\Pi_H(m)\le(em/d)^d$ for $m\ge d$) — five intermediate results in the proof chain Theorem 3.3 → Theorem 3.5 → Corollary 3.8/3.9 → Sauer's lemma → Corollary 3.18 → Corollary 3.19 that are not independently drafted as milestones, per the budget guidance to keep a chunk to a goal plus its most load-bearing 3-8 milestones rather than every numbered result on the page; the three drafted milestones (Theorem 3.3, Massart's lemma, Sauer's lemma) are the chain's three genuinely distinct proof techniques (McDiarmid's inequality, a probabilistic-maximum bound, and a combinatorial induction), and the goal theorem's own statement is Corollary 3.19 exactly as displayed, not a restatement of any intermediate corollary. Radon's theorem (Theorem 3.13, background for the hyperplane VC-dimension example) and the worked VC-dimension examples (intervals, hyperplanes, rectangles, convex polygons, sine functions) are illustrations, not general results, and are not formalized — drafting only the example computations (e.g. VCdim(hyperplanes) = d+1) instead of the general finite-H machinery is exactly the trivializing formalization this mission avoids.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 3.
• V. Vapnik, A. Chervonenkis, "On the uniform convergence of relative frequencies of events to their probabilities," Theory of Probability and its Applications 16(2), 1971, 264-280.
• N. Sauer, "On the density of families of sets," Journal of Combinatorial Theory, Series A 13(1), 1972, 145-147.

Motivation

A partially observed array with three indices appears when data record relationships among triples of objects. If its entries have a low-rank structure, one can hope to recover the full array from far fewer than $d^3$ measurements. Cai, Li, Poor and Chen study this problem when the measurements are noisy and only a random subset of entries is seen. Their result gives a statistical error bound for a concrete two-stage method: spectral initialization followed by ordinary gradient descent on a nonconvex loss. It is a known theorem, proved in the pinned preprint, rather than an open conjecture.

Setting

The unknown symmetric order-three tensor is $T^\star\in\mathbb R^{d\times d\times d}$. It has a CP decomposition $T^\star=\sum_{s=1}^r(u_s^\star)^{\otimes3}$, where the nonzero columns $u_s^\star$ form $U^\star\in\mathbb R^{d\times r}$. Each unordered triple of coordinates is sampled independently with probability $p$; its six permutations share one sampling decision. On a sampled triple the observation is $T^\star_{ijk}+E_{ijk}$, with symmetric, centered, independent sub-Gaussian noise of variance at most $\sigma^2$. The observed tensor $T$ vanishes outside the sampled set $\Omega$.

For a candidate factor matrix $U=[u_1,\ldots,u_r]$, the objective is

$$f(U)=\frac{1}{6p}\left\|P_\Omega\!\left(\sum_{s=1}^r u_s^{\otimes3}-T\right)\right\|_F^2.$$

Algorithm 2 obtains a leading $r$-dimensional eigenspace from an off-diagonal Gram matrix of the mode-one unfolding of $p^{-1}T$. Algorithm 3 uses Gaussian restarts, leading singular vectors, and greedy pruning to turn that subspace into a factor matrix $U^0$. Algorithm 1 then applies the gradient step to $f$. Eigenvalue ties, leading singular-vector choices, and pruning ties can produce several admissible executions; the result concerns every execution.

Incoherence $\mu$ measures how evenly the tensor and factors spread across coordinates and how nearly orthogonal distinct factors are. The condition number $\kappa$ is the ratio of the largest to smallest factor norm. Write $\lambda^\star_{\min}=\min_s\|u_s^\star\|_2^3$ and $\lambda^\star_{\max}=\max_s\|u_s^\star\|_2^3$. Distances $\operatorname{dist}_F$, $\operatorname{dist}_\infty$, and $\operatorname{dist}_{2,\infty}$ minimize their respective matrix norms over permutations of the $r$ columns.

Formalization targets

The goal is Theorem 2.4, in the bounded-rank, bounded-incoherence, bounded-condition-number regime. Under its printed sampling, noise, restart, threshold and step-size conditions, for every $0\le t\le d^5$ it asserts, with probability at least $1-\delta$,

$$\operatorname{dist}_F(U^t,U^\star)\le\left(C_1\rho^t+C_2\frac{\sigma}{\lambda^\star_{\min}}\sqrt{\frac{d\log d}{p}}\right)\|U^\star\|_F,$$ $$\operatorname{dist}_\infty(U^t,U^\star)\le\operatorname{dist}_{2,\infty}(U^t,U^\star)\le\left(C_3\rho^t+C_4\frac{\sigma}{\lambda^\star_{\min}}\sqrt{\frac{d\log d}{p}}\right)\|U^\star\|_{2,\infty}.$$

The rate is fixed to $\rho=1-\lambda_{\min}^{\star,4/3}\eta/5$, consistent with the paper's local-convergence lemmas. Milestones formalize the gradient identity (36), local Hessian bounds (Lemma 5.1), spectral-subspace recovery (Lemma 5.7), factor retrieval (Theorem 5.9), and the paper's general-parameter recovery theorem (Theorem 2.8). The latter makes the dependence on $\mu$ and $r$ explicit.

Significance

The inequalities give two guarantees at once: geometric reduction of initialization error and an explicit noise floor. The $2,\infty$ bound controls the error in each coordinate row, which a Frobenius estimate alone does not supply. Together with the tensor-entry corollaries in the paper, they explain the accuracy of this practical nonconvex method under random subsampling. The authors also specify how the sample probability, noise level, rank and incoherence interact, so the result can be compared to other tensor-completion methods.

This mission asks for a machine-checked version of the known result. Its published ψ₂ norm definition is reused; the paper-specific tensor model, spectral initialization relations, loss and gradient iteration are new. The theorem statements compile with sorry, so none of their proofs is claimed as machine checked here. Proofs of the listed milestones, the main theorem, and faithful auxiliary concentration results are welcome; the paper's numerical experiments are outside this formalization.

Difficulty

The gradient loss is nonconvex, so global convexity cannot justify the iteration bound. The local Hessian estimate applies only near $U^\star$ in both Frobenius and rowwise norm. A Frobenius estimate alone cannot establish the rowwise condition at every iteration. The spectral initializer must also select individual factors from a subspace despite nearly tied eigenvalues and noisy tensor contractions. These are the points where a direct appeal to standard smooth-gradient-descent theory stops short of the stated result.

Formalization scope

Coordinates are Fin d and Fin r, with zero-based indexing; the PDF uses one-based indices. All logarithms are natural. Tensor and matrix norms are explicit finite-coordinate Euclidean norms. Minima over permutations range over all permutations of Fin r, and maxima in the incoherence parameters range over the indices specified by Definition 2.1. Sampling is on sorted triples, then extended by symmetry. The probability model is a single probability space carrying the sampling indicators, noise variables and Gaussian restarts, jointly independent; the paper leaves some cross-family independence implicit. Noise has mean zero, variance at most $\sigma^2$, and ψ₂ norm at most $\sigma$ using the published extended-nonnegative norm. The last bound makes the paper's sub-Gaussian scale explicit.

The statements use $d\ge d_0\ge2$, $r\ge1$, nonzero true factor columns, $0<p\le1$, and $\sigma\ge0$. Theorems 2.8 and 5.9 use $r\ge2$ and round their real-valued restart count up to a natural number; this handles the boundary where $\log r=0$. Theorem 2.4 places its claimed absolute error constants before the rank and incoherence bounds and all instance data. Probability is expressed as the outer measure of the bad event, since admissible-execution predicates quantify over choices and need not be measurable. Each good event explicitly asserts that an admissible execution exists before requiring the bounds for every execution; otherwise a failed pruning run would make a universal claim vacuous.

The remaining reusable infrastructure includes concentration for symmetric sampled tensors, finite-dimensional spectral perturbation with ties, and derivative estimates for the cubic factor map. The paper's leave-one-out iteration lemmas and their auxiliary estimators are not included in this initial milestone list; they remain natural contributions toward the full proof.

Selected references

• C. Cai, G. Li, H. V. Poor and Y. Chen, Nonconvex Low-Rank Tensor Completion from Noisy Data, arXiv:1911.04436v2, 2021; published in Operations Research 70(2), 2022. Preprint.
• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Definition 2.5.6 for the ψ₂ norm. Publisher DOI.

Motivation

A decision maker who asks several experts for the probability of a one-off event (an election result, a geopolitical outcome, a product launch) has to turn $K$ reported probabilities into one. Simple averages are known to be under-confident when the experts hold different information, and over-confident when they share noise. Model-based aggregators correct for this. The event is a one-off, however, so there is no history from which to estimate the model's parameters, and the aggregate has to come from a single cross-section of $K$ predictions. Satopää (SSRN 3769945, 2021; Operations Research 70(6), 2022, doi:10.1287/opre.2021.2224) answers this with a Bayesian aggregator whose prior carries no tuning parameters. That only makes sense if the resulting posterior is a genuine probability distribution. This mission formalizes the theorem that guarantees it.

Setting

A binary event is $Y = \mathbf 1(I_0 > 0)$, where $I_0$ is a latent Gaussian variable. The common prior is $p_0 = \mathbb P(Y=1) = \Phi(\mu_0)$, where $\Phi$ is the standard normal distribution function and $\mu_0 \in \mathbb R$. There are $K \ge 2$ forecasters. Forecaster $k$ holds evidence $I_k$, and in addition irrational noise $N_k$. They report $p_k = \Phi(P_k)$; the real number $P_k$ is the probit prediction, and $\mathbf P = (P_1,\dots,P_K) \in \mathbb R^K$.

Under exchangeability and Gaussianity, the model has three parameters $\theta = (\delta,\gamma,\rho)$: $\gamma = \operatorname{Var}(I_k)$ is the information each forecaster holds, $\rho = \operatorname{Cov}(I_j,I_k)$ the information two forecasters share, and $\delta - \gamma = \operatorname{Var}(N_k)$ the noise. The evidence $(I_0, I_1,\dots,I_K)$ has covariance matrix

$$\Sigma = \begin{pmatrix} 1 & \gamma \mathbf 1_K' \\ \gamma\mathbf 1_K & (\gamma-\rho)I_K + \rho J_K\end{pmatrix},$$

where $I_K$ is the identity and $J_K$ the all-ones matrix. The parameter space is

$$\mathcal P(K) = \Big\{(\delta,\gamma,\rho) : \max\Big\{0,\tfrac{K\gamma^2-\gamma}{K-1}\Big\} \le \rho < \gamma \le \delta\Big\}.$$

The probit predictions are Gaussian, $\mathbf P \sim \mathcal N_K\big(\mathbf 1_K \mu_0/\sqrt{1-\gamma},\ \Lambda_{22}\big)$ with $\Lambda_{22} = [(\delta-\rho)I_K + \rho J_K]/(1-\gamma)$. The likelihood $\pi(\mathbf P\mid p_0,\theta)$ is this density. The two eigenvalues of $\Lambda_{22}$ are

$$\eta_1 = \frac{\delta+(K-1)\rho}{1-\gamma},\qquad \eta_2 = \frac{\delta-\rho}{1-\gamma},$$

and the sufficient statistics are $\bar P = \frac1K\sum_k P_k$ and $S_P = \frac1K\sum_k P_k^2 - \bar P^2$.

The prior family is

$$\pi(\theta;a,b) \propto \eta_1^{-(a+1/2)}\,\eta_2^{-(b+1/2)}\,(1-\gamma)^{-(a+5/2)},\qquad a,b>0.$$

It contains the Jeffreys prior $\pi(\theta;1,1/2)$, which is proportional to the square root of the determinant of the Fisher information $\mathcal I(\theta)$, and the independence Jeffreys prior $\pi(\theta;1/2,1/2)$.

Formalization targets

Goal: Theorem 3.3 (iii), propriety of the posterior

For every $K\ge2$, $\mu_0\in\mathbb R$, $a,b>0$ and $\mathbf P\in\mathbb R^K$ with $P_j \ne P_k$ for some $j\ne k$ and $\bar P\ne\mu_0$,

$$0 < \int_{\mathcal P(K)} \pi(\mathbf P\mid p_0,\theta)\,\pi(\theta;a,b)\,d\theta < \infty .$$

The statement holds for the whole family, not only for the two Jeffreys priors.

Milestones, in attack order

1. The proof of Theorem 2.1: $\Sigma \succ 0$ if and only if $(K\gamma^2-\gamma)/(K-1) < \rho < \gamma$.
2. Theorem 2.1: $\Sigma\succ0$, $\rho\ge0$ and $\delta\ge\gamma$ imply $\theta\in\mathcal P(K)$.
3. $\det\Lambda_{22} = \eta_1\eta_2^{K-1}$.
4. $(\mathbf P - m)'\Lambda_{22}^{-1}(\mathbf P - m) = K\,[S_P/\eta_2 + (\bar P - \mu_0/\sqrt{1-\gamma})^2/\eta_1]$, where $m = \mathbf 1_K\mu_0/\sqrt{1-\gamma}$.
5. Theorem 3.2: the spectrum of $\Lambda_{22}$ is $\{\eta_1,\eta_2\}$, and

$$\pi(\mathbf P\mid p_0,\theta) = \frac{1}{\sqrt{(2\pi)^K\eta_1\eta_2^{K-1}}}\exp\Big\{-\frac K2\Big[\frac{S_P}{\eta_2} + \frac{(\bar P - \mu_0/\sqrt{1-\gamma})^2}{\eta_1}\Big]\Big\}.$$

6. $|\mathcal I(\theta)| = \mu_0^2(K-1)K^3 / \big(16(1-\gamma)^7\eta_1^3\eta_2^2\big)$.
7. Theorem 3.3 (i): the Jeffreys prior exists if and only if $p_0\ne 0.5$, and then it equals $\pi(\theta;1,1/2)$ up to a constant.
8. With $S_1 = \sum_k (P_k-\mu_0)^2$ and $S_2 = \sum_{i,k}(P_k-\mu_0)(P_i-\mu_0)$: $KS_1 \ge S_2$, and $KS_1 > S_2$ as soon as two $P_k$ differ.
9. The inverse gamma normalizer $\int_0^\infty x^{-(s+1)}e^{-c/x}\,dx = \Gamma(s)c^{-s}$ for $s,c>0$.

Significance

The result. An objective prior "may not have a finite integral and hence may not represent an actual probability distribution. Inference, however, is valid as long as the resulting posterior distribution is proper" (p. 16). Theorem 3.3 (iii) gives conditions on the data under which the likelihood tames the prior's mass near the boundary of $\mathcal P(K)$: the forecasters do not all agree, and their mean probit differs from $\mu_0$. The revealed aggregator of the paper is defined through this posterior, so its MCMC implementation and every application in §4 rest on this theorem.

Formalizing it. The result has a published, informal proof. No part of it has been machine-checked. The mission adds a machine-checked statement of the model (parameter space, likelihood as a Gaussian density, the prior family, the Fisher information) and of the steps the proof relies on. A complete solution also corrects a slip in the printed proof: the posterior display on p. 40 centres the predictions at $\mu_0$, while the likelihood (6) centres them at $\mu_0/\sqrt{1-\gamma}$. The formal statement uses the likelihood as defined.

Difficulty

The integral is over a three-dimensional region whose boundary is curved, $\rho = (K\gamma^2-\gamma)/(K-1)$, and the integrand degenerates in several directions at once: $\gamma \uparrow 1$, $\delta-\rho\downarrow0$, $\delta+(K-1)\rho\downarrow0$, and $\delta\to\infty$. A bound that treats the parameters one at a time fails, because the prior's singularity in $\eta_1$ is integrable only after the exponential factor in $(\bar P - \mu_0/\sqrt{1-\gamma})^2/\eta_1$ is used. That factor depends on $\gamma$ through the mean, and the printed argument handles the dependence with a mis-centred posterior. Showing that the likelihood written with $\det\Lambda_{22}$ and $\Lambda_{22}^{-1}$ coincides with its closed form needs the spectral structure of compound-symmetric matrices, which Mathlib does not package.

Formalization scope

• $\theta$ is a function $\mathrm{Fin}\,3\to\mathbb R$ with $\theta_0 = \delta$, $\theta_1 = \gamma$, $\theta_2 = \rho$, so $d\theta$ is Lebesgue measure on $\mathbb R^3$.
• $\mathcal P(K)$ is as printed, with $\le$ at the lower bound on $\rho$. The boundary is a null set.
• $K \ge 2$ is a hypothesis of every theorem.
• The data are the probits $\mathbf P\in\mathbb R^K$ and $\mu_0\in\mathbb R$, not the probabilities, and $p_0 = \Phi(\mu_0)$.
• The likelihood is the Gaussian density with determinant and matrix inverse, through the published definition DKFAsymptotics.gaussianPDF.
• "Proper" means that the Lebesgue integral in $[0,\infty]$ of likelihood times prior over $\mathcal P(K)$ is strictly positive and finite.
• The Fisher information is the expectation of score products, computed with derivatives and Bochner integrals. These operations return $0$ on degenerate inputs, and such inputs do not occur on $\mathcal P(K)$.

A formalization in which the likelihood is defined by the closed form (6), or in which the integral ranges over a bounded box, would make the goal a different and easier statement. The likelihood here is the Gaussian density, and the domain is all of $\mathcal P(K)$.

A complete development needs:

• compound-symmetric matrices: determinant, inverse, spectrum;
• Gaussian Fisher information;
• Gamma-function integrals;
• a change of variables to $(\lambda_1, \lambda_2, z)$ on $\mathcal P(K)$.

The compound-symmetric matrix lemmas and the inverse gamma integral are reusable well beyond this paper. Contributions to either are welcome, as are alternative proofs of the goal.

Not formalized: Theorem 3.3 (ii), the independence Jeffreys prior, whose derivation drops cross-block factors inside its proportionalities. Its prior is still covered by the goal at $(a,b) = (1/2,1/2)$. Also not formalized: Propositions 2.2 and 3.1, and the empirical §4.

Selected references

• V. A. Satopää, Regularized Aggregation of One-off Probability Predictions, SSRN working paper 3769945 (version of 2021-08-10); published in Operations Research 70(6), 2022. https://ssrn.com/abstract=3769945, https://doi.org/10.1287/opre.2021.2224
• H. Jeffreys, An invariant form for the prior probability in estimation problems, Proceedings of the Royal Society A 186, 1946. https://doi.org/10.1098/rspa.1946.0056
• L. Malagò and G. Pistone, Information geometry of the Gaussian distribution in view of stochastic optimization, Proceedings of the 2015 ACM Conference on Foundations of Genetic Algorithms XIII, pp. 150–162, 2015. https://doi.org/10.1145/2725494.2725510
• K. Dobbin and R. Simon, Sample size determination in microarray experiments for class comparison and prognostic classification, Biostatistics 6(1):27–38, 2005 (supplementary material, Theorem 2: inverse of a compound-symmetric matrix). https://doi.org/10.1093/biostatistics/kxh015

Motivation

Characterizing the state $\rho$ of an $n$-qubit device is a basic task in quantum computing and simulation. Full quantum state tomography reconstructs $\rho$ completely, but it needs a number of measurements exponential in $n$ (Haah et al., 2017; O'Donnell–Wright, 2016). In practice one usually wants only a list of properties, such as the expectation values $\operatorname{tr}(O_1\rho),\dots,\operatorname{tr}(O_M\rho)$ of observables (fidelities with target states, entanglement witnesses, local energies). Aaronson's shadow tomography (Aaronson, 2018) showed that $M$ such properties can be learned from a number of copies polylogarithmic in $M$, but with collective measurements across many copies that are far beyond present hardware.

Huang, Kueng and Preskill (arXiv:2002.08953, Nature Physics 16, 2020) gave a procedure that uses only single-copy randomized measurements: rotate $\rho$ by a random unitary from a fixed ensemble, measure in the computational basis, and store the outcome classically. From these records, called classical shadows, a median-of-means estimator predicts all $M$ properties at once. Their Theorem 1 bounds the number of measurements by $O(\log M)$ times a state-independent norm of the observables. The method has since become a standard tool for benchmarking and for estimating many observables in experiments.

Setting

Fix $n$ qubits. Computational-basis labels are bit strings $b \in \{0,1\}^n$, and operators are $2^n\times 2^n$ complex matrices. A state is a positive semidefinite matrix of trace one.

A measurement primitive $\mathcal U$ (Definition 1) is a finite ensemble of unitaries $U_i$ drawn with probabilities $w_i$. One snapshot of $\rho$ draws $i$ with probability $w_i$, applies $\rho\mapsto U_i\rho U_i^\dagger$, and measures, obtaining $b$ with probability $\langle b|U_i\rho U_i^\dagger|b\rangle$ (S1). The primitive is tomographically complete if any two distinct states $\sigma\ne\rho$ give different outcome probabilities $\langle b|U_i\sigma U_i^\dagger|b\rangle\ne\langle b|U_i\rho U_i^\dagger|b\rangle$ for some $b$ and some $i$ of positive weight.

The measurement channel (S2) is the linear map

$$\mathcal M(X)=\sum_i w_i\sum_{b}\langle b|U_iXU_i^\dagger|b\rangle\,U_i^\dagger|b\rangle\langle b|U_i ,$$

and the classical shadow of the outcome $(i,b)$ is $\hat\rho=\mathcal M^{-1}(U_i^\dagger|b\rangle\langle b|U_i)$ (S3). For an observable $O$ the single-shadow prediction is $\hat o=\operatorname{tr}(O\hat\rho)$. The shadow norm (S7) is

$$\|O\|_{\mathrm{shadow}}=\max_{\sigma\ \text{state}}\Big(\sum_i w_i\sum_b\langle b|U_i\sigma U_i^\dagger|b\rangle\,\langle b|U_i\mathcal M^{-1}(O)U_i^\dagger|b\rangle^2\Big)^{1/2},$$

and $O_0=O-\frac{\operatorname{tr}(O)}{2^n}\mathbb I$ is the traceless part of $O$.

The median-of-means prediction (S12) takes $NK$ independent snapshots, splits them into $K$ batches of $N$, averages $\operatorname{tr}(O\hat\rho_j)$ within each batch, and outputs the median $\hat o(N,K)$ of the $K$ batch means.

Formalization targets

Goal: Theorem 1 (p. 13)

For Hermitian $O_1,\dots,O_M$, $\epsilon,\delta\in(0,1]$ and integers

$$K\ge 2\log\frac{2M}{\delta},\qquad N\ge\frac{34}{\epsilon^2}\max_{1\le i\le M}\big\|O_{i,0}\big\|_{\mathrm{shadow}}^2,\quad N\ge1,$$

the median-of-means predictions from $NK$ independent classical shadows satisfy

$$\Pr\Big[\,|\hat o_i(N,K)-\operatorname{tr}(O_i\rho)|\le\epsilon\ \text{ for all } 1\le i\le M\,\Big]\ \ge\ 1-\delta .$$

Milestones

1. Tomographic completeness makes $\mathcal M$ invertible (p. 11).
2. $\operatorname{tr}(\hat\rho)=1$ and $\mathbb E[\hat\rho]=\rho$ (p. 11).
3. $\mathbb E[\hat o]=\operatorname{tr}(O\rho)$, (S5).
4. $\mathcal M^{-1}$ is self-adjoint for the trace pairing (p. 12).
5. Lemma 1: $\operatorname{Var}[\hat o]\le\|O_0\|_{\mathrm{shadow}}^2$, (S6).
6. The median-of-means guarantee: for $N\ge34\sigma^2/\epsilon^2$, $\Pr[|\hat\mu(N,K)-\mathbb E X|\ge\epsilon]\le2e^{-K/2}$ (p. 13).
7. The per-observable bound $\Pr[|\hat o_i(N,K)-\operatorname{tr}(O_i\rho)|\ge\epsilon]\le\delta/M$ (p. 13).

The constants $34$, $2$ and $2M/\delta$ are the paper's own. Remark 1 of the paper says they are chosen for simplicity, not tightness.

Significance

Theorem 1 gives a sample complexity $NK=O\big(\log(M)\max_i\|O_{i,0}\|^2_{\mathrm{shadow}}/\epsilon^2\big)$. It grows only logarithmically in the number of properties and does not depend on the dimension $2^n$ except through the shadow norm. For random global Clifford measurements the shadow norm is at most $3\operatorname{tr}(O_0^2)$. For random single-qubit Pauli measurements it is at most $4^{k}\|O\|_\infty^2$ for an observable acting on $k$ qubits (Propositions 1–3 of the paper). These instantiations are what make the protocol useful for fidelity estimation and for local observables. The theorem also separates two independent ingredients, a state-independent variance bound and a generic median-of-means concentration bound, and each is reusable.

The result is proved in the paper. As far as the platform's corpus shows, it has not been machine-checked. This mission produces a formal statement of the protocol and its guarantee, and its definitions (measurement channel, classical shadow, shadow norm) can be reused for the Clifford and Pauli instantiations and for the paper's quadratic-function estimator (Theorem 4).

Difficulty

The linear-algebra layer is elementary but has to be set up carefully. The channel must be shown invertible from completeness on states alone. Its inverse must be shown trace-preserving and self-adjoint, and the variance has to be rewritten as an expectation of squared diagonal entries.

The probabilistic layer is where the naive argument fails. Chebyshev's inequality on a single empirical mean gives a sample size proportional to $1/\delta$, not $\log(1/\delta)$. Applying Hoeffding's inequality to the number of failing batches gives exponent $2K(1/2-1/34)^2\approx0.44K$. That is weaker than $K/2$, so it does not reach the stated constant $2e^{-K/2}$. The bound needs the relative-entropy form of the Chernoff bound for a binomial tail, which Mathlib does not provide in this form. The median also has to be related to a count of deviating batch means without sign or tie errors.

Formalization scope

• Model. Operators are Matrix (Fin n → Fin 2) (Fin n → Fin 2) ℂ. States are the published WildeQIT.IsDensityOperator.
• Ensemble. The ensemble is finite: a published WildeQIT.FinDist of weights and a family in Matrix.unitaryGroup. The paper's ensemble is general, but both of its examples are finite with uniform weights. "$U\in\mathcal U$" in completeness means positive weight.
• Channel and inverse. $\mathcal M$ is a genuine $\mathbb C$-linear endomorphism and $\mathcal M^{-1}$ is Ring.inverse of it. Every statement using $\mathcal M^{-1}$ assumes tomographic completeness.
• Real parts. Predictions and targets are real parts of traces, which are real for Hermitian observables.
• Shadow norm. The maximum in (S7) is a real supremum over the nonempty, compact set of states, of a function bounded above.
• Probability. The $NK$ snapshots are modelled exactly. Probabilities are finite sums over all $K\times N$ outcome arrays of the product of single-snapshot probabilities $w_i\langle b|U_i\rho U_i^\dagger|b\rangle$, and batch $k$ is row $k$ of the array. The median-of-means milestone is stated for general real random variables in Mathlib's measure-theoretic language (independence, identical distribution, $L^2$).
• Median. The median is the lower median.
• Parameters. $N$ and $K$ are natural numbers at least the printed real values. $N\ge1$, $\epsilon>0$, $\delta>0$ and $M\ge1$ are added, because at $\epsilon=0$ or $\delta=0$ the printed values are undefined.

Theorem 1 must not be restated about an abstract estimator with a variance bound; that is milestone 6. The goal is about the median of means of classical shadows of a concrete primitive, with the shadow norm of (S7). Tomographic completeness is satisfiable non-trivially: the three single-qubit Pauli bases form a complete primitive, so the goal's hypotheses are not vacuous.

Needed infrastructure: elementary facts about the trace pairing and diagonal entries of $U X U^\dagger$; finite product measures, or direct finite-sum manipulations; Chebyshev's inequality; a binomial Chernoff bound in relative-entropy form; and order-statistic facts about the median. The binomial tail bound and the median-of-means lemma are independent of quantum information and reusable elsewhere. Contributions to any milestone are welcome. The Clifford and Pauli shadow-norm computations are natural follow-up work on top of these definitions.

Selected references

• H.-Y. Huang, R. Kueng, J. Preskill, Predicting many properties of a quantum system from very few measurements, Nature Physics 16, 1050–1057 (2020); arXiv:2002.08953v2. https://arxiv.org/abs/2002.08953
• S. Aaronson, Shadow tomography of quantum states, STOC 2018; SIAM J. Comput. 49 (2020). https://arxiv.org/abs/1711.01053
• J. Haah, A. W. Harrow, Z. Ji, X. Wu, N. Yu, Sample-optimal tomography of quantum states, IEEE Trans. Inf. Theory 63 (2017). https://arxiv.org/abs/1508.01797
• R. O'Donnell, J. Wright, Efficient quantum tomography, STOC 2016. https://arxiv.org/abs/1508.01907
• M. R. Jerrum, L. G. Valiant, V. V. Vazirani, Random generation of combinatorial structures from a uniform distribution, Theoret. Comput. Sci. 43 (1986), 169–188. https://doi.org/10.1016/0304-3975(86)90174-X
• A. S. Nemirovsky, D. B. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley (1983). (Jerrum–Valiant–Vazirani and Nemirovsky–Yudin are the paper's references [41, 55] for median of means.)

Motivation

Best subset selection fits a linear model using at most $k$ of $p$ available predictors: it minimizes the residual sum of squares $\|y-X\beta\|^2$ over all $\beta$ with at most $k$ nonzero coordinates. It is the classical benchmark for sparse regression, and mixed-integer optimization has made it computable at scales that used to be out of reach (Bertsimas, King & Mazumder, 2016). When the signal-to-noise ratio is low, however, best subsets overfits, and Mazumder, Radchenko & Dedieu propose to add a shrinkage penalty $\lambda\|\beta\|_q$ ($q\in\{1,2\}$) to it. Their oracle inequalities for the penalized estimators hold for a fixed model size $k$, and the practitioner still has to choose $k$.

§3.5 of the paper removes that choice. It replaces the cardinality constraint with BIC-type penalties that depend on the candidate model size, and Theorem 5 shows that the resulting estimators satisfy oracle inequalities for the expected prediction error over all of $\mathbb R^p$, with no condition on the design beyond the normalization of its columns. This mission formalizes Theorem 5 and the steps of its printed proof.

Setting

We observe $y=f^*+\epsilon\in\mathbb R^n$. The mean $f^*\in\mathbb R^n$ is deterministic and unknown, and $\epsilon$ has independent $N(0,\sigma^2)$ entries with $\sigma>0$. The design $X\in\mathbb R^{n\times p}$ is deterministic, with $p\ge1$ and columns of unit Euclidean norm. The prediction error of an estimate $\hat\beta$ is $\|f^*-X\hat\beta\|^2$. For $\beta\in\mathbb R^p$, $\|\beta\|$ is the Euclidean norm, $\|\beta\|_1=\sum_j|\beta_j|$, and $\|\beta\|_0$ is the number of nonzero coordinates.

For nonnegative tuning parameters $a$ and $b$, the data-dependent penalties are

$$\lambda_\beta=a\sqrt{\|\beta\|_0\log(ep/\|\beta\|_0)},\qquad \mu_\beta=b\log(ep/\|\beta\|_0),$$

with the convention $0\cdot\infty=0$, so the empty model is not penalized. The BIC-type estimators are

$$\hat\beta^B_2\in\arg\min_{\beta}\ \|y-X\beta\|^2+\lambda_\beta\|\beta\|+\mu_\beta\|\beta\|_0,\qquad \hat\beta^B_1\in\arg\min_{\beta}\ \|y-X\beta\|^2+\lambda\|\beta\|_1+\mu_\beta\|\beta\|_0,$$

where $\lambda\ge0$ is a fixed number. Both are unconstrained problems. Solving them is equivalent to solving the constrained problems with $\|\beta\|_0\le k$ for each $k$ and then choosing $k$ by the penalty. A minimizer exists but need not be unique.

The proof works on events of the noise vector. For an integer $s$ and $\delta_0\in(0,1]$ the event $G'_s$ requires

$$\epsilon^\top Xu\le\sigma\sqrt{5s\log(ep/s)+3\log(1/\delta_0)}\,\|Xu\|\qquad\text{for every }u\text{ with }\|u\|_0\le s .$$

Formalization targets

Goal: Theorem 5 (p. 21)

There exist universal constants $a_0,b_0,c_0$ such that, if $a\ge a_0\sigma$ or $b\ge b_0\sigma^2$,

$$\mathbb E\|f^*-X\hat\beta^B_2\|^2\lesssim\inf_{\beta\in\mathbb R^p}\Big[\|f^*-X\beta\|^2+\lambda_\beta\|\beta\|+\mu_\beta\|\beta\|_0\Big]+\sigma^2,$$

and, if $\lambda\ge c_0\sigma\sqrt{\log(ep)}$ or $b\ge b_0\sigma^2$,

$$\mathbb E\|f^*-X\hat\beta^B_1\|^2\lesssim\inf_{\beta\in\mathbb R^p}\Big[\|f^*-X\beta\|^2+\lambda\|\beta\|_1+\mu_\beta\|\beta\|_0\Big]+\sigma^2 .$$

Here $\lesssim$ hides one universal multiplicative constant. The constants are not specified, so the goal records the shape of the bound and is not invalidated by later improvements of the constants.

Milestones (proof of Theorem 5, B.13, and B.5)

1. (51): the deterministic basic inequality for $\hat\beta^B_2$.
2. (54): for $a\gtrsim\sigma$, with probability at least $1-\delta_0/2$, $\|f^*-X\hat\beta\|^2+\mu_{\hat\beta}\|\hat\beta\|_0\lesssim\|f^*-X\beta\|^2+\lambda_\beta\|\beta\|+\sigma^2\log(1/\delta_0)+\mu_\beta\|\beta\|_0$.
3. The union bound over model sizes: with $G=\bigcap_{s=1}^pG'_s$, where $G'_s$ is taken at $\delta_0=(s/[ep])^s\epsilon_0$, we have $P(G^c)\le\epsilon_0$.
4. (55): for $b\gtrsim\sigma^2$, the analogue of (54) with probability at least $1-\epsilon_0$.
5. (56): under either condition, the high-probability oracle inequality with $\inf_\beta$ and $\sigma^2\log(1/\delta_0)$.
6. The tail-to-expectation step of B.5: if $W\le\kappa\log(1/\delta_0)$ with probability at least $1-\delta_0/2$, then $\mathbb EW^+\le\kappa/2$.
7. (58): the high-probability counterpart of (56) for $\hat\beta^B_1$.

Significance

The result. Theorems 2 and 3 of the paper give oracle inequalities only over the sparsity class $\{\|\beta\|_0\le k\}$ for a $k$ fixed in advance. Theorem 5 makes the model size data-driven. Its bounds hold over all of $\mathbb R^p$ and need no restricted-eigenvalue or sparse-eigenvalue condition on $X$. Corollary 6 of the paper deduces from it that the estimators attain the error rates of Corollaries 3 and 4 while selecting models of the same order as the true model size. The paper also notes that the slow-rate bound for $\hat\beta^B_1$ with $b=0$ is a bound for the Lasso.

Formalizing it. Theorem 5 is a published result with a printed proof (Supplement B.13). The proof is written up to unspecified universal constants, and it defers two steps to other parts of the paper ("repeating the argument after inequality (32)" and "repeating the argument in the proof of Corollary 3"). A formal proof makes every constant and every deferred step explicit. No part of the paper has been machine-checked, to the best of our search.

Difficulty

The argument is long rather than deep. The obvious first attempt fixes the selected model size $\hat k=\|\hat\beta\|_0$ and applies a high-probability bound for that size. This fails because $\hat k$ is random and depends on $\epsilon$, so a bound for each fixed $s$ says nothing about the random $\hat k$. The noise term must be controlled simultaneously over all model sizes, at a total failure probability that does not grow with $p$. The second obstacle is the passage from high-probability bounds, which hold for every $\delta_0$ and grow like $\log(1/\delta_0)$, to a bound in expectation. That passage needs the high-probability statement with a constant that is uniform in $\delta_0$.

Formalization scope

• Representation. Vectors are Fin n → ℝ and Fin p → ℝ, and the design is a Matrix (Fin n) (Fin p) ℝ.

  • The norms $\|\cdot\|$, $\|\cdot\|_1$ and $\|\cdot\|_0$ are explicit definitions (l2, l1, l0), because Mathlib's norm on Fin m → ℝ is the sup norm.
  • The noise law is the product of $n$ centred Gaussians with variance $\sigma^2$ (noiseLaw).
  • Logarithms are natural, and $e=\exp(1)$.

• Model. The standing hypotheses are:

  • unit-norm columns of $X$;
  • $\sigma>0$ and $p\ge1$;
  • $a,b\ge0$, and $\lambda\ge0$ for $\hat\beta^B_1$.

  The quantities $X$, $f^*$, $\sigma$, $a$, $b$, $\lambda$ and the penalties are inputs. The randomness is the law of $\epsilon$ alone, and $y=f^*+\epsilon$.

• Estimators are argmin predicates IsBIC2, IsBIC1: "$\hat\beta$ minimizes the objective over all of $\mathbb R^p$". Every statement holds for every minimizer.

  • In Theorem 5 an estimator is a measurable map $y\mapsto\hat\beta(y)$ that is a minimizer for every $y$, and the bound is claimed for every such selection.
  • The expectation is a lower Lebesgue integral in $[0,\infty]$, so a non-integrable error cannot make the bound vacuous.

• Constants.

  • "$\lesssim$" is one universal constant $C>0$, quantified before every other parameter.
  • "$\inf_\beta[\dots]$" is written as "for every $\beta$".
  • "With probability at least $1-\delta$" is the existence of a measurable event of probability at least $1-\delta$ on which the inequality holds.
  • The constants $a_0$, $b_0$ and $c_0$ carry no sign, as on the page.

• Correction. Theorem 1 of the paper states $P(G_s)\ge1-\delta_0$ for an event with coefficient $1$ on $\log(1/\delta_0)$. That bound is false for small $\delta_0$ (already for $n=p=s=1$). The union bound here uses the corrected event $G'_s$ with coefficient $3$, which inside $\lesssim$ changes nothing downstream.

• Ruled out. None of the following counts as a formalization of the goal:

  • an arbitrary or non-measurable selection of the minimizer;
  • a Bochner integral, which is $0$ for a non-integrable error;
  • a constant that depends on $n$, $p$, $\delta_0$ or the design;
  • a fixed $\delta_0$ or $\epsilon_0$.

• Not formalized here. The fixed-$k$ oracle inequalities (Theorems 2 and 3), the noise events of Theorem 1, the lower bound (Theorem 4), Corollaries 1–6 and the numerical study are not part of this mission. Some of them are the subjects of the other missions of this series. The proof of Theorem 5 needs the probability bounds for the events $F$ and $G'_s$ of Theorem 1 and the deterministic arguments of Theorems 2 and 3. A solver may prove them here or import them once they are published.

• Contributions welcome.

  • Gaussian chi-square tail bounds (Laurent–Massart);
  • the bound for the sorted-$\ell_1$ event $F$ (Bellec, Lecué & Tsybakov);
  • the existence of measurable selections of the argmin;
  • the layer-cake step.

  These are reusable well beyond this paper.

Selected references

• R. Mazumder, P. Radchenko, A. Dedieu, Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low, arXiv:1708.03288v4, 2022; Operations Research, 2023. https://arxiv.org/abs/1708.03288
• D. Bertsimas, A. King, R. Mazumder, Best subset selection via a modern optimization lens, Annals of Statistics 44(2), 2016. https://doi.org/10.1214/15-AOS1388
• P. C. Bellec, G. Lecué, A. B. Tsybakov, Slope meets Lasso: improved oracle bounds and optimality, Annals of Statistics 46(6B), 2018. https://doi.org/10.1214/17-AOS1670
• B. Laurent, P. Massart, Adaptive estimation of a quadratic functional by model selection, Annals of Statistics 28(5), 2000. https://doi.org/10.1214/aos/1015957395
• L. Birgé, P. Massart, Gaussian model selection, Journal of the European Mathematical Society 3, 2001. https://doi.org/10.1007/s100970100031