Random Matrix Theory

Dynamical Systems Operations Research Probability·Captain: mikedeng1

Subadditive Ergodic Theory 5: For a Stationary Sequence in a Banach Algebra with E(log‖Y₁‖)⁺ < ∞, n⁻¹ log‖Y₁⋯Y_n‖ Converges in [−∞, ∞)Research Paper

Motivation

Products of random linear operators appear wherever a system evolves by repeated application of randomly chosen linear maps: linear recursions with random coefficients, products of random matrices in statistical physics, the growth of random dynamical systems, and population models in random environments. The basic question is the exponential growth rate of the product $Y_1Y_2\cdots Y_n$ . For square matrices, Furstenberg and Kesten (Ann. Math. Statist. 31, 1960) proved that $n^{-1}\log\|Y_1\cdots Y_n\|$ converges for stationary sequences with a logarithmic moment condition.

Kingman (Subadditive ergodic theory, Ann. Probab. 1(6):883–899, 1973) showed that this limit theorem is an instance of the subadditive ergodic theorem, and that the instance needs nothing of matrices beyond the norm inequality $\|AB\|\le\|A\|\,\|B\|$ . His Theorem 6 therefore holds in an arbitrary real or complex Banach algebra, including infinite-dimensional ones such as infinite matrices with finite $\ell_1$ norm. It is the source of what later became known as the top Lyapunov exponent of a stationary random operator product.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space. A two-parameter family is a collection $x=(x_{st})$ of random variables indexed by nonnegative integers $s<t$ . Kingman's conditions (§1.1–1.2) are:

S₁: $x_{su}\le x_{st}+x_{tu}$ whenever $s<t<u$ ;
S₂: the joint distributions of $(x_{s+1,t+1})$ are the same as those of $(x_{st})$ ;
S₃: $g_t=E(x_{0t})$ is finite for every $t\ge1$ and $g_t\ge -At$ for some constant $A$ ;
S₃′: $E(x_{01}^+)<\infty$ , where $x^+=\max(x,0)$ .

A family of real random variables satisfying S₁, S₂ and S₃ is a subadditive process. Kingman's Theorem 1 (the goal of the first mission of this series) says that for a subadditive process $x_{0t}/t$ converges almost surely and in mean to a finite random variable $\xi$ with $E(\xi)=\gamma=\inf_{t\ge1}g_t/t$ .

A Banach algebra $\mathfrak B$ is a complete normed algebra over $\mathbb R$ or $\mathbb C$ whose norm satisfies $\|AB\|\le\|A\|\,\|B\|$ . A sequence $(Y_n)_{n\ge1}$ of $\mathfrak B$ -valued random elements is stationary if $(Y_{n+1})_{n\ge1}$ and $(Y_n)_{n\ge1}$ have the same joint law. The log-norm process is

x_{st}=\log\|Y_{s+1}Y_{s+2}\cdots Y_t\|\in[-\infty,\infty),\qquad s<t,

with $\log 0=-\infty$ . Expectations of $[-\infty,\infty)$ -valued variables are extended expectations $E(f)=\int f^+\,dP-\int f^-\,dP$ , defined when $\int f^+\,dP<\infty$ and possibly equal to $-\infty$ .

Formalization targets

Goal: Theorem 6 (p. 893)

If $(Y_n)$ is a stationary sequence in a real or complex Banach algebra and $E\{(\log\|Y_1\|)^+\}<\infty$ , then

\xi=\lim_{n\to\infty}n^{-1}\log\|Y_1Y_2\cdots Y_n\|

exists in $-\infty\le\xi<\infty$ with probability one, and

E(\xi)=\lim_{n\to\infty}n^{-1}E\{\log\|Y_1Y_2\cdots Y_n\|\}.

The goal fixes no constant and no ergodicity assumption: $\xi$ is in general a non-degenerate random variable.

Milestones

(1.2.7), p. 885: under S₁, S₂ and S₃′, $E(x_{st}^+)<\infty$ for all $s<t$ .
Proof of Theorem 2, p. 886: the truncation $x^{(N)}_{st}=\max(x_{st},-N(t-s))$ is a subadditive process for every positive integer $N$ .
Theorem 2, p. 885: if $x$ satisfies S₁, S₂ and S₃′ but not S₃, then $\xi=\lim x_{0t}/t$ exists with probability one in $[-\infty,\infty)$ and $E(\xi)=-\infty$ .
Proof of Theorem 6, p. 893: the log-norm process satisfies S₁, S₂ and S₃′.

Significance

Theorem 6 defines a stochastic spectral radius: if every $Y_n$ equals a fixed element $y$ , then $e^\xi$ is the spectral radius of $y$ by Gelfand's formula, and for independent $Y_n$ with common law $\pi$ the limit is a constant $\rho(\pi)$ depending only on $\pi$ . For $k\times k$ matrices the theorem reduces to the Furstenberg–Kesten theorem. Theorem 2, the extension of the subadditive ergodic theorem from S₃ to S₃′, is the form needed whenever a process can have mean growth rate $-\infty$ , as happens for products that can vanish or contract superlinearly; it is used well beyond random products.

All results here are proved on paper (Kingman 1973, building on his 1968 paper). None of them is machine-checked: Mathlib has no subadditive ergodic theorem, no Furstenberg–Kesten theorem and no random-product limit in normed algebras. The platform poses an ergodic, constant-limit form of Kingman's theorem (PalmQueueing.Ergodic.kingman_subadditive, open); this mission's Theorem 2 is a different statement (non-ergodic, conclusion $E(\xi)=-\infty$ under failure of S₃). A complete development would give the first formal proof of the Furstenberg–Kesten limit, in the generality of Banach algebras.

Difficulty

Theorem 6 is short given Theorems 1 and 2, but the obvious one-line reduction to Theorem 1 fails in two places. First, the log-norm process can take the value $-\infty$ and its means $g_t$ can be $-\infty$ or decrease superlinearly, so condition S₃ fails and Theorem 1 does not apply; the case $E(\xi)=-\infty$ is a separate theorem (Theorem 2), whose proof must exchange a limit in $t$ with a limit in an auxiliary parameter. Second, stationarity of the log-norm process (S₂) is a statement about joint laws on a path space; in a non-separable Banach algebra, multiplication need not be measurable for the product $\sigma$ -algebra on $\mathfrak B\times\mathfrak B$ , so it is not automatic that the law of $(Y_n)$ determines the joint law of the products $Y_{s+1}\cdots Y_t$ . The main dependency, Theorem 1 itself, is the subject of a separate mission and is not restated here.

Formalization scope

The Lean development fixes these conventions:

Families are functions x : ℕ → ℕ → Ω → β; only pairs $s<t$ enter any condition. S₁ is required almost surely for each triple (the weaker hypothesis); the log-norm milestone proves it at every sample point.
S₂ and stationarity are equalities of laws of the whole path (Measure.map) on the product $\sigma$ -algebra, not equality of one-dimensional marginals.
S₃′ and all positive parts are lower Lebesgue integrals; expectations that may be $-\infty$ are computed as $\int f^+ - \int f^-$ in EReal, never as Bochner integrals (which return $0$ for non-integrable functions).
$\log\|\cdot\|$ is ENNReal.log of the norm, so $\log\|0\|=-\infty$ ; Real.log 0 = 0 would replace a vanishing product's growth rate $-\infty$ by $0$ , and is ruled out.
$\mathfrak B$ is a complete unital NormedRing with NormedAlgebra 𝕜 𝔅, RCLike 𝕜. Each $Y_n$ is strongly measurable; $\mathfrak B$ is not assumed separable.
Limits are Filter.atTop on ℕ in the topology of EReal; the conclusions assert $\xi<\infty$ almost surely, $E(\xi^+)<\infty$ , and, for (2.3.5), both the existence of the limit of means and its value.

A formalization that replaces the extended logarithm by Real.log, or the extended expectation by a Bochner integral, makes the statement false or trivially different, and is excluded.

Reusable infrastructure: extended expectations of EReal-valued random variables, joint-law stationarity of sequences and two-parameter families, and the truncation lemma for S₃′ processes. Contributions toward Theorem 1 (mission 1 of this series), toward measurability of products of strongly measurable random elements, and toward the milestones in any order are welcome.

Selected references

J. F. C. Kingman, Subadditive ergodic theory, Ann. Probab. 1(6):883–899, 1973. https://doi.org/10.1214/aop/1176996798
J. F. C. Kingman, The ergodic theory of subadditive stochastic processes, J. Roy. Statist. Soc. Ser. B 30:499–510, 1968. https://doi.org/10.1111/j.2517-6161.1968.tb00749.x
H. Furstenberg and H. Kesten, Products of random matrices, Ann. Math. Statist. 31:457–469, 1960. https://doi.org/10.1214/aoms/1177705909

8 thms2 active usersReviewed

Dynamical Systems Operations Research Probability·Captain: mikedeng1

Subadditive Ergodic Theory 4: Furstenberg–Kesten — for Stationary Positive Random Matrices, n⁻¹ log [Y₁⋯Y_n]_ij Converges, Independently of i and jResearch Paper

Products of random matrices

Many systems evolve by repeated multiplication by a random linear map: the state of a linear system with randomly varying coefficients, population vectors in a random environment (Leslie models whose rates change from year to year), the transfer matrices of a disordered one-dimensional medium, and the transition operators of a Markov chain in a random environment. In each case the object of interest is the product $X_n = Y_1 Y_2 \cdots Y_n$ of random matrices and its growth as $n\to\infty$ .

The basic answer is due to Furstenberg and Kesten (Products of random matrices, Ann. Math. Statist. 31 (1960)): under a logarithmic moment condition and stationarity, $n^{-1}\log$ of the size of $X_n$ converges. Their proof was a substantial piece of analysis. In his 1973 IMS Special Invited Paper (Kingman, Subadditive ergodic theory, Ann. Probab. 1 (1973)), J. F. C. Kingman showed that for matrices with strictly positive entries the result is a short corollary of his subadditive ergodic theorem (Theorem 1 of that paper, 1968). This mission formalizes that application: Theorem 5 of the 1973 paper, §2.2, pp. 891–892.

Timeline:

1960: Furstenberg and Kesten prove convergence of $n^{-1}\log\|X_n\|$ and, for positive matrices, of $n^{-1}\log[X_n]_{ij}$ .
1968: Kingman proves the subadditive ergodic theorem (J. Roy. Statist. Soc. B 30).
1973: Kingman's survey deduces the positive-matrix theorem (Theorem 5) and the general Banach-algebra version (Theorem 6) from it.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space, $k\ge1$ , and let $Y_1, Y_2,\dots$ be random $k\times k$ real matrices. Write $[A]_{ij}$ for the $(i,j)$ th entry of a matrix $A$ , and

X_n = Y_1 Y_2\cdots Y_n \qquad (2.2.1),

the product taken left to right. The sequence $(Y_n)$ is stationary if the joint law of $(Y_2, Y_3, \dots)$ equals the joint law of $(Y_1, Y_2, \dots)$ ; this is a statement about all finite-dimensional distributions at once, and it includes the case of independent identically distributed matrices.

The proof works with the diagonal process

z_{st} = [Y_{s+1}Y_{s+2}\cdots Y_t]_{11},\qquad x_{st} = -\log z_{st}\qquad (s<t),

and with the $\ell_1$ -norm $\|A\| = \max_i \sum_j |[A]_{ij}|$ . A family $(x_{st})_{s<t}$ is a subadditive process (§1.1) if S₁: $x_{su}\le x_{st}+x_{tu}$ for $s<t<u$ ; S₂: the joint distributions of $(x_{s+1,t+1})$ equal those of $(x_{st})$ ; S₃: $g_t=E(x_{0t})$ exists and $g_t\ge -At$ for some constant $A$ .

Formalization targets

Goal: Theorem 5

Suppose the elements of the matrices $Y_n$ are strictly positive, $E|\log[Y_n]_{ij}|<\infty$ for every $n$ and every $i,j$ , and $(Y_n)$ is stationary. Then there is one finite random variable $\lambda$ such that for every $(i,j)$

\lambda = \lim_{n\to\infty} n^{-1}\log [X_n]_{ij} \qquad (2.2.2)

with probability one and in mean. The limit is random in general (it is constant when $(Y_n)$ is ergodic); the theorem asserts its existence, its finiteness and its independence of $(i,j)$ , and nothing about its value.

Milestones, in the order of the paper's proof

(2.3.1): $[AB]_{11}\ge[A]_{11}[B]_{11}$ for matrices with strictly positive entries.
$x_{st}=-\log z_{st}$ satisfies S₁ and S₂, and each $x_{st}$ has finite expectation $g_{t-s}$ .
$E\{\log\|Y_1\|\}<\infty$ and $g_n/n\ge -E\{\log\|Y_1\|\}$ for all $n\ge1$ , so S₃ holds.
The limit (2.2.2) exists, with probability one and in mean, for $i=j=1$ .
(2.2.3): for every $(i,j)$ , $P\{\liminf n^{-1}\log[X_n]_{ij}\ge\lambda\}=1$ .
For every $(i,j)$ , $P\{\limsup n^{-1}\log[X_n]_{ij}\le\lambda\}=1$ .

Significance

The limit $\lambda$ is the top Lyapunov exponent of the random product: it is the almost-sure exponential growth rate of every entry, and hence of every norm, of $X_n$ . It governs the stability of random linear recursions $v_{n}=v_{n-1}Y_n$ , the long-run growth rate of populations in random environments, and localization in one-dimensional disordered systems. Theorem 5 is the existence statement on which all of these quantitative questions rest.

The theorem has been proved since 1960, and Kingman's derivation is a classical model application of subadditive ergodic theory. To our knowledge it has no machine-checked proof: Mathlib has neither Kingman's subadditive ergodic theorem nor any limit theorem for random matrix products. This mission produces a formal statement of the result together with the formal decomposition of the proof into the steps Kingman writes down; its milestone 4 is exactly where the subadditive ergodic theorem (the goal of the companion mission Subadditive Ergodic Theory 1) is applied.

Difficulty

Milestones 1–3 are deterministic matrix inequalities plus integrability bookkeeping; the substance is elsewhere. First, milestone 4 needs the full subadditive ergodic theorem, almost-sure and in mean, for a non-ergodic stationary process: the classical Birkhoff theorem does not apply, because $\log[X_n]_{11}$ is not a sum of stationary increments. Second, passing from the diagonal entry to all entries requires controlling $n^{-1}\log[Y_n]_{1j}$ along a stationary sequence with only a first-moment hypothesis, and transporting an almost-sure statement about $X_n'=Y_2\cdots Y_{n+1}$ back to $X_n$ by stationarity, where the limit $\lambda$ is itself random. The natural shortcut — treating $\lambda$ as a constant — is only valid under ergodicity, which is not assumed.

Formalization scope

Matrices are Matrix (Fin k) (Fin k) ℝ with NeZero k; the paper's index $1$ is 0 : Fin k. The sequence is Y : ℕ → Ω → Matrix …, read only for $n\ge1$ ; Y 0 plays no role.
Products are ordered: $Y_{s+1}\cdots Y_t$ is the List.prod of [Y (s+1), …, Y t]; $X_0$ is the identity.
Stationarity is equality of the laws of $(Y_{n+2})_{n\ge0}$ and $(Y_{n+1})_{n\ge0}$ on ℕ → Fin k → Fin k → ℝ with the product σ-algebra. Independence is not assumed.
Positivity holds for every outcome; "their logarithms have finite expectations" is integrability of every $\log[Y_n]_{ij}$ , $n\ge1$ .
"Finite limit" is a real-valued lam : Ω → ℝ; "in mean" is $E|n^{-1}\log[X_n]_{ij}-\lambda|\to0$ with $\lambda$ integrable; time is $n\in\mathbb N$ with Filter.atTop. One lam serves all $(i,j)$ .
Lim inf and lim sup inequalities are stated with $\varepsilon$ : almost surely, for every $\varepsilon>0$ , eventually $n^{-1}\log[X_n]_{ij}\ge\lambda-\varepsilon$ (respectively $\le\lambda+\varepsilon$ ), which avoids the junk value of a real liminf on unbounded sequences.
Real.log 0 = 0 in Lean; the statements apply log only to entries that are strictly positive under the hypotheses, so no junk value enters. Dropping the positivity hypothesis would change the theorem, and is not an acceptable shortcut.
The S₁/S₂ vocabulary of §1.1 comes from the group's shared process module; this mission defines $g_t$ locally. The general subadditive ergodic theorem is not restated here, and milestone 4 is the object-specific statement the paper writes.

Welcome contributions: proofs of the matrix inequalities, the integrability and stationarity transfer lemmas, a formal subadditive ergodic theorem (shared with the companion mission).

Selected references

J. F. C. Kingman, Subadditive ergodic theory, Ann. Probab. 1(6):883–899, 1973. https://doi.org/10.1214/aop/1176996798
H. Furstenberg and H. Kesten, Products of random matrices, Ann. Math. Statist. 31(2):457–469, 1960. https://doi.org/10.1214/aoms/1177705909
J. F. C. Kingman, The ergodic theory of subadditive stochastic processes, J. Roy. Statist. Soc. Ser. B 30(3):499–510, 1968. https://doi.org/10.1111/j.2517-6161.1968.tb00749.x

9 thms2 active usersReviewed

Linear Optimization Operations Research Optimization+1·Captain: mikedeng1

On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming 4: For a Random Subspace, ‖Pq‖⁻∞ ≤ (log n/n)‖r‖² with Probability Tending to OneResearch Paper

Motivation

Primal–dual interior point methods follow a path of strictly feasible solutions to a linear program. Their worst case iteration bounds come from controlling a term that is quadratic in each search step. Mizuno, Todd, and Ye asked whether that term is typically much smaller than its worst case bound under a model in which a certain subspace is randomly oriented. Theorem 5 in their technical report gives a probability bound for the negative part of that term. It is a statement about one randomly oriented subspace and a fixed input vector, rather than a stochastic model for an entire algorithm run. The authors explicitly note that assigning the same random subspace model independently at successive iterations would be inconsistent with the algorithm's evolving state. Mizuno, Todd, and Ye, §6

Setting

Fix a dimension $n$ , an integer $d$ with $0\le d\le n$ , and a vector $r\in\mathbb R^n$ . Draw a random $d$ -dimensional subspace $U$ from the distribution invariant under orthogonal transformations. Let $p$ be the Euclidean orthogonal projection of $r$ onto $U$ , and put $q=r-p$ , its projection onto $U^\perp$ . The matrix $P=\operatorname{diag}(p)$ turns the vector $q$ into the coordinatewise product $Pq=(p_jq_j)_{j=1}^n$ .

For a coordinate vector $z$ , let $z^-=(\min\{z_j,0\})_{j=1}^n$ and $\|z\|^-_\infty=\|z^-\|_\infty$ . Thus $\|Pq\|^-_\infty$ records the magnitude of the largest negative coordinate of $Pq$ . An unsubscripted vector norm is always the Euclidean $\ell_2$ norm. These definitions follow the report's notation on printed pages 2 and 4. Mizuno, Todd, and Ye, §§1–2

The formal model samples an $(n-d)\times n$ matrix $G$ with independent standard normal entries and sets $U=\ker G$ . The report itself gives this construction as an example of the orthogonally invariant law. With probability one, this null space has dimension $d$ . The construction covers the endpoint cases $d=0$ and $d=n$ as well: the projection product is then zero. This probabilistic model has no linear programming data in its statement. The optimization setting explains why the quantity matters, while the result depends only on Euclidean projection geometry. Mizuno, Todd, and Ye, §6

Formalization targets

Theorem 5

For arbitrary choices $r_n\in\mathbb R^n$ and $d_n\le n$ at each dimension, the central target is

\Pr\left\{\|P_nq_n\|^-_\infty\le \frac{\log n}{n}\|r_n\|_2^2\right\} \longrightarrow 1\qquad(n\longrightarrow\infty).

The logarithm is natural. The theorem asks for the exact coefficient shown in the report, rather than only an asymptotic order. The choice of $r_n$ and $d_n$ may change with $n$ ; the result does not require a common probability space for all dimensions. Mizuno, Todd, and Ye, Theorem 5, printed p. 13

Source milestones

The mission includes Lemma 6, which identifies a beta distributed radial coordinate and a uniform spherical direction for a projected vector; the componentwise identities and inequality (18)–(19); the Gaussian norm limit (20); the Gaussian coordinate maximum limit cited in the proof; and Lemma 7, which bounds the sup norm of a rotated uniform spherical direction by $\sqrt{3\log n/n}$ with probability tending to one. Their statements, constants, and order follow printed pages 14–15 of the report. Mizuno, Todd, and Ye, §6

Significance

The result gives a precise high probability bound for the negative coordinates of the projection product. In the report this product represents the second order term of a primal–dual search direction, and a smaller value permits a larger admissible step in the relevant neighborhood analysis. The theorem therefore supplies a mathematically definite part of the paper's discussion of anticipated improved behavior. It does not by itself prove a typical iteration count: the paper does not provide a consistent random model for the sequence of subspaces visited by the algorithm. Mizuno, Todd, and Ye, §§2, 6–7

The report proves Theorem 5 and the two numbered lemmas on paper. The formalization work is to provide machine checked proofs of the random subspace representation, the beta and spherical laws, the finite dimensional Gaussian limits, and their connection to the projection bound. These results are reusable in other questions about random projections and coordinatewise estimates. The statements in this mission are open formalization targets; compilation of a statement with a proof placeholder does not count as a machine checked proof.

Difficulty

A direct norm bound on $p$ and $q$ loses the coordinate information needed for the factor $\log n/n$ . The difficult part is that the desired bound concerns the most negative coordinate of a product of two dependent projections, while the distribution is specified through a random subspace. The paper's deterministic identity (18)–(19) relates this product to an angular coordinate. The remaining probabilistic statements must control the largest coordinate of a uniformly distributed spherical vector, including the numerical constant in Lemma 7. The laws of the radial and angular coordinates also need a sound measurable construction; simply writing a mapped measure without checking the map would not establish the claimed distributions.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin n), so $\|r\|$ is the $\ell_2$ norm. Coordinate sup norms are separate definitions. A complete development needs finite dimensional inner product geometry, orthogonal projections, Gaussian product measures, beta measures, the uniform spherical law, and limits of real probabilities. The spherical law is encoded as the direction of a standard Gaussian vector. The Gaussian matrix construction fixes the invariant subspace distribution and must be connected to the stated $d$ -dimensional law almost surely.

Lemma 6 concerns $d,m\ge1$ and $n\ge2$ , where the beta parameters and the spherical direction are nondegenerate. Its angular direction is assigned zero at the zero coordinate, which has probability zero in this regime; the claimed decomposition and unit norm hold almost surely. Theorem 5 retains $d=0$ , $d=n$ , and $r=0$ . Lemma 7 is stated only for frames in dimensions at least two; finitely many smaller dimensions are assigned probability one in its limit expression. Equation (20) keeps the report's condition $\varepsilon>0$ . All limits are probabilities tending to one, never probability one at every finite $n$ .

Contributions should preserve the source's constants and all three claims of Lemma 6. A proof of the beta law alone, or a bound for a single fixed direction, does not close the corresponding target. The invariant random subspace and projection model, the Gaussian and spherical distribution facts, and the coordinate estimates are each useful independently of this mission.

Selected references

Shinji Mizuno, Michael J. Todd, and Yinyu Ye, On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming, Cornell ORIE Technical Report No. 944, 1990, revised 1991; published in Mathematics of Operations Research 18(4), 1993. DOI
Sidney I. Resnick, Extreme Values, Regular Variation, and Point Processes, Springer, 1987, pp. 42 and 71, cited in the report for the Gaussian maximum estimate. DOI

7 thms2 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

Understanding and Using Linear Programming IX: Basis Pursuit Recovers Sparse Solutions Exactly iff the Kernel Misses the CrosspolytopeTextbook

Motivation

A deep-space probe sends a vector $w\in\mathbb{R}^k$ encoded as $z=Qw\in\mathbb{R}^n$ , and up to about 8% of the transmitted numbers may be corrupted arbitrarily. Section 8.5 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer 2007, DOI 10.1007/978-3-540-30717-4) shows that decoding reduces to finding a sparse solution of an underdetermined linear system $Ax=b$ , and that under suitable conditions this sparse solution is found exactly by a single linear program. The same problem arises in signal processing (sparse representations in redundant wavelet dictionaries) and in computer tomography, and it is the core of what became known as compressed sensing.

Timeline, as recorded in the book's references:

1999: Chen, Donoho and Saunders introduce basis pursuit, minimizing the $\ell_1$ -norm subject to $Ax=b$ (SIAM J. Sci. Comput. 20).
2005: Candès, Rudelson, Tao and Vershynin prove that for every $\alpha\in(0,1)$ there is $\beta(\alpha)>0$ such that a random $\lfloor\alpha n\rfloor\times n$ matrix is exact for $\lfloor\beta n\rfloor$ -sparse vectors with probability exponentially close to 1 (FOCS 2005).
2006: Donoho, via neighborliness of centrally symmetric polytopes, obtains the constants $\alpha=0.75$ , $\beta=0.08$ used in the book, and shows that no $\lfloor 0.75n\rfloor\times n$ matrix is exact for $r>0.25n$ when $n$ is large (Discrete Comput. Geom. 35).
2006: Linial and Novik prove further upper bounds showing that these existence results are asymptotically optimal (Discrete Comput. Geom. 36).

Setting

Let $A$ be a real $m\times n$ matrix with $m<n$ and $b\in\mathbb{R}^m$ . The support of $x\in\mathbb{R}^n$ is $\operatorname{supp}(x)=\{i: x_i\ne 0\}$ . For an integer $r\ge 0$ , a sparse solution of $Ax=b$ is an $x$ with $Ax=b$ and $|\operatorname{supp}(x)|\le r$ . The $\ell_1$ -norm is $\|x\|_1=|x_1|+\dots+|x_n|$ .

Basis pursuit is the optimization problem

\text{(BP)}\qquad\text{minimize } \|x\|_1\ \text{ subject to } x\in\mathbb{R}^n,\ Ax=b,

which is equivalent to the linear program

\text{(BP}'\text{)}\qquad\text{minimize } u_1+\dots+u_n\ \text{ subject to } Ax=b,\ -u\le x\le u,\ u\ge 0 .

The matrix $A$ is BP-exact for $r$ if for every $b\in\mathbb{R}^m$ : whenever $Ax=b$ has a solution $\tilde x$ with at most $r$ nonzero components, $\tilde x$ is the unique optimal solution of (BP). The crosspolytope is $B^n_1=\{x:\|x\|_1\le 1\}$ , the kernel of $A$ is $L=\{x: Ax=0\}$ , and $L+z=\{\ell+z:\ell\in L\}$ . For $z$ with $\|z\|_1=1$ , the cone at $z$ is $C_z=\{t(x-z): t\ge 0,\ x\in B^n_1\}$ , and $L$ is good for $z$ if $(L+z)\cap B^n_1=\{z\}$ .

Formalization targets

Goal: Lemma 8.5.4 (reformulation of BP-exactness)

For $m<n$ and $r\le m$ :

A \text{ is BP-exact for } r\iff \forall z\in\mathbb{R}^n\ \text{with}\ \|z\|_1=1,\ |\operatorname{supp}(z)|\le r:\quad (L+z)\cap B^n_1=\{z\}.

This is the book's geometric characterization of exact recovery, and the statement on which the known probabilistic proofs are built.

Milestones

Observation 8.5.1: $Ax=b$ has at most one sparse solution for every $b$ if and only if every $2r$ or fewer columns of $A$ are linearly independent.
The remark after it (p. 169): under $m<n$ , that column condition forces $m\ge 2r$ .
Equivalence of (BP) and (BP′) (p. 170): in every optimal solution of (BP′), $u_i=|x_i|$ ; and $x$ is optimal for (BP) iff $(x,|x|)$ is optimal for (BP′).
From the proof of Lemma 8.5.4 (p. 173): if $Az=b$ , the solution set of $Ax=b$ is exactly $L+z$ .
From "Intuition for BP-exactness" (p. 174): for $\|z\|_1=1$ and $|\operatorname{supp}(z)|\le r$ , $L$ is good for $z$ iff $L\cap C_z=\{0\}$ .

Further draft item: Theorem 8.5.2

With $m=\lfloor 0.75n\rfloor$ , $r=\lfloor 0.08n\rfloor$ and $A$ an $m\times n$ matrix of independent $N(0,1)$ entries, there is a constant $c>0$ such that for every $n$

\Pr[A \text{ is BP-exact for } r]\ \ge\ 1-e^{-cm}.

The book states this without proof. It is included as a separate theorem, not a milestone of the goal.

Significance

Lemma 8.5.4 converts an algorithmic property, that an $\ell_1$ linear program returns a prescribed sparse vector for every right-hand side, into a purely geometric property of the kernel of $A$ relative to the low-dimensional faces of the crosspolytope. With milestone 5 it becomes the statement that $L$ avoids a finite family of cones, which is where union bounds over faces and estimates for random subspaces enter. Observation 8.5.1 separates what is information-theoretically possible (uniqueness of sparse solutions) from what is computationally achievable by linear programming; finding a sparse solution directly is NP-hard in general. Theorem 8.5.2 is the quantitative payoff: a fixed fraction of arbitrary gross errors can be corrected by solving one linear program.

All of these results are proved in the literature; Lemma 8.5.4, Observation 8.5.1 and the milestones are elementary, and Theorem 8.5.2 rests on Donoho's polytope-neighborliness analysis. The platform has a related formalization of Wainwright's restricted nullspace property (Theorem 7.8 of High-Dimensional Statistics, namespace HighDimStat.SparseLinear), which fixes a support set $S$ rather than characterizing exactness for all $r$ -sparse vectors through the crosspolytope. A machine-checked proof of Theorem 8.5.2 with the constants $0.75$ and $0.08$ is, to our knowledge, not available anywhere; it would require substantial Gaussian and high-dimensional geometry infrastructure.

Difficulty

For the goal and milestones the difficulty is bookkeeping, not ideas: the scaling between a sparse solution $\tilde x$ and the boundary point $\tilde x/\|\tilde x\|_1$ , the case $\tilde x=0$ , and the fact that BP-exactness quantifies over all right-hand sides $b$ while the geometric side quantifies over boundary points of the crosspolytope.

Theorem 8.5.2 is of a different order. A union bound over the $\binom{n}{r}2^r$ faces of dimension $r-1$ reduces it to bounding the probability that a random $(n-m)$ -dimensional subspace meets one cone $C_F$ nontrivially, and getting that probability small enough to beat the combinatorial factor with the stated numerical constants is the hard part. Rough asymptotic estimates do not give $0.08$ at $\alpha=0.75$ .

Formalization scope

Vectors are functions Fin n → ℝ (the book's indices $1,\dots,n$ become $0,\dots,n-1$ ) and matrices are Matrix (Fin m) (Fin n) ℝ. The $\ell_1$ -norm is written out as $\sum_i|x_i|$ , since Mathlib's norm on Fin n → ℝ is the sup norm. The support is a Finset of indices. Optimality in (BP) and (BP′) is stated against every feasible point; no infimum is taken, so an empty or unbounded feasible set cannot create a spurious optimum. "Every $2r$ or fewer columns" ranges over finsets of distinct column indices, column $j$ being Aᵀ j. The hypotheses $m<n$ and $r\le m$ of Lemma 8.5.4 are kept as on the page, although the equivalence does not use them; $m<n$ is also the standing assumption of §8.5 needed for $m\ge 2r$ .

In Theorem 8.5.2 the random matrix has the product law of independent gaussianReal 0 1 entries, the constant $c>0$ is quantified before $n$ , and measurability of the BP-exact event is part of the conclusion, so the bound concerns a genuine probability rather than an outer measure.

A trivializing formalization is ruled out: BP-exactness requires uniqueness among all minimizers for every right-hand side, not just optimality of $\tilde x$ , and the crosspolytope condition is an equality of sets, not an inclusion that $z$ alone would satisfy.

All definitions live in one module (MatousekLP.SparseRecovery.BasisPursuit); the $\ell_1$ and support vocabulary is reusable for later sparse-recovery missions. Contributions are welcome on every milestone, on the goal, and on the infrastructure towards Theorem 8.5.2 (Gaussian measures on matrix spaces, measurability of the BP-exact event, the face structure of the crosspolytope).

Selected references

J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.5. https://doi.org/10.1007/978-3-540-30717-4
S. S. Chen, D. L. Donoho and M. A. Saunders, Atomic decomposition by basis pursuit, SIAM J. Sci. Comput. 20(1), 1999, 33–61. https://doi.org/10.1137/S1064827596304010
E. J. Candès, M. Rudelson, T. Tao and R. Vershynin, Error correction via linear programming, Proc. 46th IEEE FOCS, 2005, 295–308. https://doi.org/10.1109/SFCS.2005.5464411
D. L. Donoho, High-dimensional centrally symmetric polytopes with neighborliness proportional to dimension, Discrete Comput. Geom. 35, 2006, 617–652. https://doi.org/10.1007/s00454-005-1220-0
N. Linial and I. Novik, How neighborly can a centrally symmetric polytope be?, Discrete Comput. Geom. 36, 2006, 273–281. https://doi.org/10.1007/s00454-006-1235-1

7 thms2 active usersReviewed

Completed

Linear algebra Numerical Analysis Probability·Captain: mikedeng1

Randomized Algorithms for Estimating the Trace of an Implicit Symmetric Positive Semi-Definite Matrix V: Sample Bound for the Mixed Unit Vector Trace EstimatorResearch Paper

Motivation

Many computations in numerical linear algebra, statistics and computational physics need the trace of a matrix $A$ that is never formed explicitly: $A$ may be an inverse, a matrix function $f(B)$ , or a product of large operators, and the only affordable access is a routine that returns $Av$ or $v^TAv$ for a given vector $v$ . Monte Carlo trace estimators handle this setting: draw random vectors $z$ and average the quadratic forms $z^TAz$ , each of which costs one matrix–vector product.

Avron and Toledo (J. ACM 2011) compare such estimators by the number of samples $M$ that guarantee relative error $\epsilon$ with probability $1-\delta$ , and by the number of random bits each sample consumes. Hutchinson's estimator (Hutchinson 1990) and the Gaussian estimator need $\Omega(n)$ random bits per sample. Section 8 of the paper studies two estimators that sample only from the $n$ standard basis vectors and so need about $\log_2 n$ bits per sample, which allows the samples to be generated in advance. The plain version has a sample bound that depends on how uneven the diagonal of $A$ is; the mixed version first multiplies $A$ on both sides by a random orthogonal mixing matrix of the kind introduced by Ailon and Chazelle (2006) for the fast Johnson–Lindenstrauss transform and used by Avron, Maymounkov and Toledo (2010) in least-squares solvers. This mission formalizes the resulting sample bound, Theorem 8.4.

Setting

Let $n \ge 1$ , let $A \in \mathbb{R}^{n\times n}$ be symmetric positive semi-definite, and let $e_1,\ldots,e_n$ be the standard basis of $\mathbb{R}^n$ .

A random variable $T$ is an $(\epsilon,\delta)$ -approximator of $\mathrm{trace}(A)$ if

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

(Definition 4.1).

The unit vector estimator with $M$ samples is

U_M = \frac{n}{M}\sum_{i=1}^M z_i^TAz_i,

where $z_1,\ldots,z_M$ are independent uniform random samples from $\{e_1,\ldots,e_n\}$ (Definition 3.4). Each term $z_i^TAz_i$ is a diagonal entry of $A$ chosen uniformly at random. Its behaviour is governed by

r_D(A) = \frac{n\cdot\max_i A_{ii}}{\mathrm{trace}(A)},

which lies between $1$ and $n$ .

A random mixing matrix is $\mathcal F = FD$ , where the seed $F$ is a fixed orthogonal $n\times n$ matrix and $D$ is diagonal with i.i.d. Rademacher entries, $\Pr(D_{ii}=\pm1) = 1/2$ (Definition 3.5). The seed enters through

\eta = \max_{i,j}|F_{ij}|^2,

which satisfies $1/n \le \eta \le 1$ ; normalized DFT and Hadamard matrices attain $\eta = 1/n$ , DCT and DHT matrices have $\eta = 2/n$ (p. 8:5).

The mixed unit vector estimator is

T_M = \frac{n}{M}\sum_{i=1}^M z_i^T\mathcal F A\mathcal F^T z_i,

with $z_1,\ldots,z_M$ as above, independent of $D$ (Definition 3.6). It is the unit vector estimator applied to $\mathcal FA\mathcal F^T$ , whose trace equals $\mathrm{trace}(A)$ .

Formalization targets

Goal: Theorem 8.4

For every orthogonal seed $F$ , every symmetric positive semi-definite $A$ , every $\epsilon > 0$ , $\delta \in (0,1)$ and every $M \ge 1$ ,

M \ \ge\ 2n^2\eta^2\epsilon^{-2}\ln(4/\delta)\ln^2(4n^2/\delta) \quad\Longrightarrow\quad T_M \text{ is an } (\epsilon,\delta)\text{-approximator of } \mathrm{trace}(A).

Milestones

Lemma 8.1. For symmetric $A$ , $\mathrm{E}(U_1) = \mathrm{trace}(A)$ and $\mathrm{Var}(U_1) = n\sum_{i}A_{ii}^2 - \mathrm{trace}^2(A)$ .
Theorem 8.2. $U_M$ is an $(\epsilon,\delta)$ -approximator of $\mathrm{trace}(A)$ whenever

M \ge \tfrac12\epsilon^{-2}\ln(2/\delta)\,r_D^2(A).

Lemma 8.3. For $U \in \mathbb{R}^{n\times m}$ with orthonormal columns and $\delta > 0$ , with probability at least $1-\delta$ ,

|(\mathcal FU)_{ij}| \le \sqrt{2\eta\ln(2mn/\delta)} \quad\text{for all } i,j.

Proof of Theorem 8.4, p. 8:13. With probability at least $1-\delta/2$ over $D$ , $0 \le (\mathcal FA\mathcal F^T)_{jj} \le 2\eta\ln(4n^2/\delta)\,\mathrm{trace}(A)$ for all $j$ , and hence

r_D(\mathcal FA\mathcal F^T) \le 2n\eta\ln(4n^2/\delta).

Significance

Theorem 8.2 alone shows that the unit vector estimator can need order $n^2$ samples: when the trace is concentrated on one diagonal entry, $r_D(A) = n$ . Theorem 8.4 removes the dependence on $A$ entirely. For a Fourier-type seed with $\eta = \Theta(1/n)$ the bound becomes $O(\epsilon^{-2}\ln(1/\delta)\ln^2(n/\delta))$ samples for every positive semi-definite $A$ , while each sample still costs about $\log_2 n$ random bits, and the $n$ bits of $D$ are drawn once. Among the estimators of the paper this is the only one with both an $A$ -independent sample bound and logarithmic randomness per sample (Table I, p. 8:5). Lemma 8.3 is a standalone statement about randomized orthogonal transforms that is used well beyond trace estimation, in the analysis of subsampled randomized Hadamard transforms, sketching-based least squares, and fast Johnson–Lindenstrauss embeddings.

All results of the mission are proved in the literature: Lemma 8.3 in the cited works, the rest in the paper. As far as the platform's catalogue shows, none has a machine-checked proof. The mission produces checked statements of the paper's Section 8 with their exact constants, a probability model for random sign matrices and uniform basis-vector sampling that other randomized linear-algebra missions can reuse, and, once proved, a checked instance of Hoeffding's inequality applied to a concrete estimator.

Difficulty

The obvious argument for Theorem 8.4 applies Theorem 8.2 to $\mathcal FA\mathcal F^T$ . That matrix is random, so Theorem 8.2, which is a statement about a fixed matrix, cannot be applied directly: the proof must condition on $D$ , use that the samples $z_i$ are independent of $D$ , and combine a failure event over $D$ with a conditional failure event over the $z_i$ , each with probability at most $\delta/2$ . The second difficulty is Lemma 8.3: each entry $(\mathcal FU)_{ij} = \sum_k F_{ik}D_{kk}U_{kj}$ is a Rademacher sum whose coefficient vector has squared norm at most $\eta$ , and the bound needs a sub-Gaussian tail for such sums together with a union bound over all $mn$ entries. Bounding the diagonal of $\mathcal FA\mathcal F^T$ through the diagonal of $A$ alone does not work: each mixed diagonal entry depends on all entries of $A$ , including the off-diagonal ones.

Formalization scope

Everything is over $\mathbb{R}$ . The paper allows complex unitary seeds; since the estimator uses the transpose $\mathcal F^T$ , the mission takes $F$ real orthogonal ( $F^TF = I$ ). Matrices are Matrix (Fin n) (Fin n) ℝ, "symmetric positive semi-definite" is Matrix.PosSemidef, and $n \ge 1$ is assumed throughout. The sample spaces are explicit product measures: indices $k_1,\ldots,k_M$ uniform on Fin n with $z_i = e_{k_i}$ , the diagonal of $D$ with the $n$ -fold Rademacher product law, and, for $T_M$ , the product of the two, which makes $D$ and the $z_i$ independent as the paper assumes implicitly. Probabilities are Measure.real. $\eta$ and $\max_i A_{ii}$ are maxima over finite nonempty index sets; $r_D$ uses real division, whose value at $\mathrm{trace}(A) = 0$ is irrelevant because a positive semi-definite matrix with zero trace is $0$ . The sample-count thresholds are exactly the paper's constants.

Deviations from the page, all recorded in the items' Formalization Notes: Definition 3.4 and Theorem 8.2 are stated for positive semi-definite rather than positive definite $A$ (the proof uses only $A_{ii} \ge 0$ ); Table I's entry $8\epsilon^{-2}\ln(4n^2/\delta)\ln(4/\delta)$ for the mixed estimator, which disagrees with Theorem 8.4, is not used; the proof of Theorem 8.4 prints the conditional failure probability as " $\le 1-\delta/2$ " where $\delta/2$ is meant, and no statement copies it; Remark 8.5 ("for some small $C$ ") has no pinned constant and is not stated.

A formalization in which $D$ is an arbitrary orthogonal diagonal matrix, the $z_i$ are correlated with $D$ , or the law of the estimator is assumed rather than constructed would make the goal either false or a restatement of its hypotheses; the product-measure model rules this out.

Needed infrastructure: Hoeffding's inequality for bounded i.i.d. sums (in Mathlib as sub-Gaussian moment generating function bounds), a sub-Gaussian tail for Rademacher linear combinations, conditioning on one factor of a product measure, and the spectral theorem for real symmetric matrices. The Rademacher sign model and the random-mixing-matrix entry bound are reusable beyond this mission. Proofs of any milestone, and alternative arguments for Lemma 8.3, are welcome.

Selected references

H. Avron and S. Toledo, Randomized algorithms for estimating the trace of an implicit symmetric positive semi-definite matrix, J. ACM 58(2), Article 8, 2011. https://doi.org/10.1145/1944345.1944349
N. Ailon and B. Chazelle, Approximate nearest neighbors and the fast Johnson–Lindenstrauss transform, STOC 2006. https://doi.org/10.1145/1132516.1132597
H. Avron, P. Maymounkov and S. Toledo, Blendenpik: Supercharging LAPACK's least-squares solver, SIAM J. Sci. Comput. 32(3), 2010. https://doi.org/10.1137/090767911
M. F. Hutchinson, A stochastic estimator of the trace of the influence matrix for Laplacian smoothing splines, Comm. Statist. Simulation Comput. 19(2), 1990. https://doi.org/10.1080/03610919008812866
W. Hoeffding, Probability inequalities for sums of bounded random variables, J. Amer. Statist. Assoc. 58, 1963. https://doi.org/10.1080/01621459.1963.10500830

10 thms2 active usersReviewed

Completed

Linear algebra Numerical Analysis Probability·Captain: mikedeng1

Randomized Algorithms for Estimating the Trace of an Implicit Symmetric Positive Semi-Definite Matrix III: Sample Bound for Normalized Rayleigh-Quotient Trace EstimatorsResearch Paper

Motivation

Many computations in numerical linear algebra, statistics and computational physics need the trace of a matrix $A$ that is never formed explicitly: $A$ may be an inverse, a matrix function $f(B)$ , or a product of large operators, and the only affordable access is a routine that returns $Av$ for a given vector $v$ . Examples include log-determinants and the generalized cross-validation criterion in statistics, counting eigenvalues in an interval, and charge densities in electronic-structure computations. Monte Carlo trace estimators handle this setting: draw random vectors $z$ , and average the quadratic forms $z^TAz$ , each of which costs one matrix–vector product.

Hutchinson (1990) introduced the estimator with Rademacher vectors and computed its variance. Avron and Toledo (J. ACM 2011) replaced variance statements with sample bounds: how many samples $M$ guarantee relative error $\epsilon$ with probability $1-\delta$ . Section 6 of their paper proves one such bound for an entire class of estimators at once, the normalized Rayleigh-quotient trace estimators, which contains Hutchinson's estimator and the unit vector estimator. This mission formalizes that bound (Theorem 6.1).

Setting

Let $A \in \mathbb{R}^{n\times n}$ be symmetric positive semi-definite, with eigenvalues $0 \le \lambda_1 \le \cdots \le \lambda_n$ and rank $\mathrm{rank}(A)$ . Write $\lambda_n$ for the largest eigenvalue and

\kappa_f(A) = \frac{\text{largest nonzero eigenvalue of }A}{\text{smallest nonzero eigenvalue of }A},

defined for $A \ne 0$ ; it is the condition number of $A$ on its range.

A normalized Rayleigh-quotient trace estimator of $A$ with $M$ samples is

R_M = \frac1M\sum_{i=1}^M z_i^TAz_i,

where $z_1,\ldots,z_M$ are independent random vectors in $\mathbb{R}^n$ with $z_i^Tz_i = n$ and $\mathrm{E}(z_i^TAz_i) = \mathrm{trace}(A)$ for each $i$ (Definition 3.2). The vectors need not be identically distributed. Hutchinson's vectors ( $\pm1$ entries, i.i.d. uniform) and the vectors $\sqrt n\,e_k$ with $k$ uniform are instances.

A random variable $T$ is an $(\epsilon,\delta)$ -approximator of $\mathrm{trace}(A)$ if

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

(Definition 4.1).

Formalization targets

Goal: Theorem 6.1, in the form its proof establishes

For every nonzero symmetric positive semi-definite $A$ , every $\epsilon>0$ , $\delta\in(0,1)$ , and every normalized Rayleigh-quotient estimator $R_M$ of $A$ ,

M \ \ge\ \frac{\ln(2/\delta)\cdot n^2\,\kappa_f^2(A)}{2\,\mathrm{rank}^2(A)\,\epsilon^2} \quad\Longrightarrow\quad R_M \text{ is an } (\epsilon,\delta)\text{-approximator of } \mathrm{trace}(A).

Milestones (the displayed steps of the proof, p. 8:10)

$\mathrm{trace}(A)\,\kappa_f(A) \ge \mathrm{rank}(A)\,\lambda_n$ .
For every $z$ with $z^Tz = n$ : $\ 0 \le z^TAz \le \lambda_n z^Tz = n\lambda_n \le \frac{n}{\mathrm{rank}(A)}\mathrm{trace}(A)\,\kappa_f(A)$ .
For every $t>0$ :

\Pr(|R_M-\mathrm{trace}(A)| \ge t) \le 2\exp\left(-\frac{2M^2\mathrm{rank}^2(A)t^2}{M n^2\mathrm{trace}^2(A)\kappa_f^2(A)}\right).

For every $\epsilon>0$ :

\Pr(|R_M-\mathrm{trace}(A)| \ge \epsilon\,\mathrm{trace}(A)) \le 2\exp\left(-\frac{2M\mathrm{rank}^2(A)\epsilon^2}{n^2\kappa_f^2(A)}\right).

Significance

The result is distribution-free within the class: it needs only normalization and unbiasedness, so it covers Hutchinson's estimator, the unit vector estimator and any future normalized scheme with one argument. For well-conditioned matrices of full or nearly full rank the required number of samples is $O(\epsilon^{-2}\ln(1/\delta))$ , independent of $n$ . For ill-conditioned matrices the bound degrades with $\kappa_f^2(A)$ , which is the reason the paper proves sharper estimator-specific bounds in Sections 7 and 8; Theorem 6.1 is the baseline those results are compared against (Table I, p. 8:5).

The theorem is proved in the paper. No machine-checked version of it, or of any sample bound for trace estimators, is known to exist. The formalization adds a precise statement of the class of estimators on a general probability space, a corrected threshold (see below), and a Lean development that connects Mathlib's spectral theorem for symmetric matrices with its Hoeffding inequality for independent bounded variables.

Difficulty

Each step is short on paper; the work is in the interfaces. The eigenvalue inequality of milestone 1 requires relating the number of nonzero eigenvalues (with multiplicity) to $\mathrm{rank}(A)$ and handling the maximum and minimum over the nonzero spectrum. Milestone 2 is the Rayleigh-quotient bound $z^TAz \le \lambda_n z^Tz$ , which is a consequence of the spectral decomposition rather than a one-line identity. Milestone 3 applies Hoeffding's inequality to summands that are bounded only almost surely, are not identically distributed, and whose mean is fixed by hypothesis rather than computed; the two-sided bound must be assembled from two one-sided tails, and the event $|R_M - \mathrm{trace}(A)| \ge t$ must be rescaled to a statement about the sum $\sum_i z_i^TAz_i$ . A naive attempt that fixes a particular distribution for the $z_i$ (Rademacher, say) proves a different, narrower theorem and does not settle the goal.

Formalization scope

Matrices and spectrum. $A$ is Matrix (Fin n) (Fin n) ℝ with A.PosSemidef and A ≠ 0; eigenvalues are Mathlib's IsHermitian.eigenvalues. $\lambda_n$ is lambdaMax (the maximum eigenvalue) and $\kappa_f(A)$ is kappaF (maximum over minimum of the finite set of nonzero eigenvalues); both are Finset.max'/min'/sup' of nonempty finite sets. $\kappa_f(0)$ is a placeholder, and every statement assumes $A \ne 0$ .
Probability model. A general probability space $(\Omega, P)$ and random vectors z : Fin M → Ω → Fin n → ℝ satisfying IsNormalizedRayleighSample P A z: each $z_i$ measurable, the family mutually independent (iIndepFun), $z_i^Tz_i = n$ almost surely, and $\int z_i^TAz_i\,dP = \mathrm{trace}(A)$ . The estimator is universally quantified over this class. Unbiasedness is required for the given $A$ only, as on the page. Probabilities are P.real of events; $M \ge 1$ is a natural number and $1/M$ is (M : ℝ)⁻¹.
Correction of the printed statement. Theorem 6.1 and Table I print the threshold $\tfrac12\epsilon^{-2}n^{-2}\mathrm{rank}^2(A)\ln(2/\delta)\kappa_f^2(A)$ . The last display of the proof gives $\ln(2/\delta)\,n^2\kappa_f^2(A)/(2\,\mathrm{rank}^2(A)\epsilon^2)$ , with the exponents of $n$ and $\mathrm{rank}(A)$ swapped. The printed version is false: for $n=2$ , $A=e_1e_1^T$ , $z=\sqrt2\,e_k$ with $k$ uniform and $\epsilon=\delta=1/2$ it admits $M=1$ , while $R_1\in\{0,2\}$ . The goal states the proof's threshold.
Indexing slip. The proof writes $0=\lambda_1=\cdots=\lambda_k$ with $k=n-\mathrm{rank}(A)+1$ and $\kappa_f(A)=\lambda_n/\lambda_k$ , which would make $\lambda_k=0$ ; milestone 1 states the inequality with $\kappa_f$ as defined, not the indexing.
Non-trivialization. The hypotheses of the class are satisfiable (by the unit vector and Hutchinson estimators), $A\ne0$ excludes the degenerate $\kappa_f(0)$ , and all divisions in the statements have positive denominators, so no statement holds vacuously or through a junk value.
Reusable parts. A proof of milestone 2 is a general Rayleigh-quotient bound for symmetric matrices; milestone 3 is a two-sided Hoeffding bound for independent, almost surely bounded, non-identically distributed summands, useful well beyond this mission. Contributions welcome: proofs of any milestone, and a sorry-free instance showing a concrete estimator (e.g. $\sqrt n\,e_k$ ) satisfies IsNormalizedRayleighSample.

Selected references

H. Avron and S. Toledo, Randomized algorithms for estimating the trace of an implicit symmetric positive semi-definite matrix, Journal of the ACM 58(2), Article 8, 2011. https://doi.org/10.1145/1944345.1944349
M. F. Hutchinson, A stochastic estimator of the trace of the influence matrix for Laplacian smoothing splines, Communications in Statistics – Simulation and Computation 19(2), 433–450, 1990. https://doi.org/10.1080/03610919008812866
W. Hoeffding, Probability inequalities for sums of bounded random variables, Journal of the American Statistical Association 58(301), 13–30, 1963. https://doi.org/10.1080/01621459.1963.10500830

8 thms2 active usersReviewed

Convex Optimization Machine Learning Probability+1·Captain: mikedeng1

The Power of Convex Relaxation: Near-Optimal Matrix Completion I: Exact Nuclear-Norm Recovery with Quadratic Dependence on the RankResearch Paper

Motivation

Matrix completion asks to recover a low-rank matrix from a small random subset of its entries. It models collaborative filtering (a ratings matrix with most entries missing), sensor-network localization from partial distance matrices, and system identification. The natural estimator, the matrix of least rank that agrees with the observations, is NP-hard to compute in general. Candès and Recht (Found. Comput. Math. 2009) proposed to replace the rank by the nuclear norm (the sum of the singular values), its convex envelope, and proved that this convex program recovers the matrix exactly from $O(n^{6/5} r \log n)$ random entries under incoherence assumptions.

Candès and Tao (IEEE Trans. Inf. Theory 2010) sharpened the sample size to within logarithmic factors of the information-theoretic minimum $n r\log n$ . This mission formalizes their first result, Theorem 1.1, whose proof is a direct moment computation, together with the lemmas on which that proof rests.

Timeline:

2009, Candès–Recht: exact recovery from $m \gtrsim \mu_0 n^{6/5} r \log n$ entries.
2010, Candès–Tao (this paper): $m \gtrsim \mu^4 n r^2 (\log n)^2$ (Theorem 1.1, general-rank form) and $m \gtrsim \mu^2 n r \log^6 n$ (Theorem 1.2), plus a lower bound of order $n r \log n$ for every method (Theorem 1.7).
2011, Gross (IEEE Trans. Inf. Theory) and Recht (JMLR): $m \gtrsim \mu_0 n r \log^2 n$ by the "golfing scheme", with a different proof.

Setting

Let $M \in \mathbb R^{n\times n}$ have rank $r$ and singular value decomposition $M = \sum_{k=1}^r \sigma_k u_k v_k^*$ with $\sigma_k > 0$ and orthonormal $u_k$ , $v_k$ . Write $P_U = \sum_k u_k u_k^*$ , $P_V = \sum_k v_k v_k^*$ and $E = \sum_k u_k v_k^*$ . The matrix obeys the strong incoherence property with parameter $\mu > 0$ if, for all indices $a, a', b, b'$ ,

\Bigl|\langle e_a, P_U e_{a'}\rangle - \tfrac{r}{n}1_{a=a'}\Bigr| \le \mu\tfrac{\sqrt r}{n},\qquad \Bigl|\langle e_b, P_V e_{b'}\rangle - \tfrac{r}{n}1_{b=b'}\Bigr| \le \mu\tfrac{\sqrt r}{n},\qquad |E_{ab}| \le \mu\tfrac{\sqrt r}{n}.

For a set $\Omega \subset [n]\times[n]$ of observed positions, the nuclear-norm program is

\text{minimize } \|X\|_* \quad \text{subject to } X_{ab} = M_{ab}\ \ ((a,b)\in\Omega). \qquad \text{(I.3)}

In the uniform model $\Omega$ is a uniformly random $m$ -subset of $[n]\times[n]$ ; in the Bernoulli model each entry is included independently with probability $p = m/n^2$ .

The proof works with the tangent space $T$ at $M$ and its projection $\mathcal P_T(X) = P_UX + XP_V - P_UXP_V$ , the sampling projection $\mathcal P_\Omega$ , and the centered operators $\mathcal Q_\Omega = p^{-1}\mathcal P_\Omega - \mathcal I$ and $\mathcal Q_T = \mathcal P_T - \rho'\mathcal I$ , where $\rho = r/n$ and $\rho' = 2\rho - \rho^2$ . The candidate certificate $Y$ of (III.10) is the matrix of least Frobenius norm with $\mathcal P_\Omega(Y) = Y$ and $\mathcal P_T(Y) = E$ .

Formalization targets

Goal: Theorem 1.1, general-rank form (I.11)

There is an absolute constant $C$ such that, for every strongly incoherent $M$ of rank $r$ and every $m \le n^2$ ,

m \ge C\mu^4 n r^2(\log n)^2 \implies \Pr_{\text{uniform}}\bigl[M \text{ is the unique solution of (I.3)}\bigr] \ge 1 - n^{-3}.

Milestones

Lemma 3.1: a matrix $Y$ supported on $\Omega$ with $\mathcal P_T(Y) = E$ and $\|\mathcal P_{T^\perp}(Y)\| < 1$ , together with injectivity of $\mathcal P_\Omega$ on $T$ , certifies that $M$ is the unique solution (already proved on the platform).
Lemma 5.1 (exponent bound): $|J|+|K|-|Q|-|\Omega| \le -|Q'|+1$ for every admissible pair.
Lemma 5.2 (pair counting): at most $(Cj(k+1))^{2j(k+1)+q}$ strongly admissible pairs have $|Q'| = q$ .
Theorem 3.4 (moment bound I): with $A = (\mathcal Q_\Omega\mathcal Q_T)^k\mathcal Q_\Omega(E)$ and $r_\mu = \mu^2 r$ ,

\mathbb E\operatorname{trace}(A^*A)^j \le (Cj(k+1))^{2j(k+1)}\, n\,(n r_\mu^2/m)^{j(k+1)}.

Corollary 3.5: under the goal's sampling condition and the Bernoulli model, with probability at least $1-n^{-3}$ , $\mathcal P_\Omega$ is injective on $T$ and $\|\mathcal P_{T^\perp}(Y)\| \le 1/2$ .

The Bernoulli-to-uniform transfer (at most doubling the failure probability) is already on the platform and is included as a supporting item.

Significance

Theorem 1.1 shows that a tractable convex program recovers every strongly incoherent matrix of bounded rank from $O(n(\log n)^2)$ random entries, while Theorem 1.7 of the same paper shows that no method can succeed with fewer than order $n\log n$ . The gap is a single logarithmic factor. The result also requires nothing of the singular values, only of the singular vectors.

The theorem is proved in the literature, and later work improved the rank dependence (Theorem 1.2 of the same paper, and the golfing-scheme results of Gross and Recht). As far as is known, none of these results has a machine-checked proof. The mission produces a formal version of the full moment-method argument. Its combinatorial core, the admissible-pair calculus of Sections IV–V, is a self-contained counting problem for closed paths in a grid and is reusable for other trace-moment bounds of random operators. The Candès–Recht mission on the platform already supplies the deterministic duality step (Lemma 3.1) and the model transfer.

Difficulty

The obvious route bounds the Neumann series $\sum_k \|(\mathcal Q_\Omega\mathcal P_T)^k\mathcal Q_\Omega(E)\|$ term by term with noncommutative Khintchine inequalities and decoupling. That is how the earlier $n^{6/5}$ bound was obtained, and it degrades as $k$ grows because the indicator variables in the higher terms are strongly coupled. The moment method replaces these tools by an exact expansion of $\mathbb E\operatorname{trace}(A^*A)^j$ as a sum over "spider" configurations of paths in $[n]\times[n]$ . The difficulty moves into combinatorics. Configurations have to be grouped by admissible pairs, the exponent of $n$ has to be matched against the powers of $1/p$ (Lemma 5.1), and the configurations have to be counted with enough precision that the sum over $q$ converges (Lemma 5.2). A naive count of pairs gives $(2j(k+1))^{4j(k+1)}$ , which is too large by a square.

Formalization scope

Square case. Theorem 1.1 is printed for $n_1\times n_2$ matrices, but the paper proves only the square case (Section I-H: "we shall work exclusively with square matrices"). Every statement is for Matrix (Fin n) (Fin n) ℝ.
General rank. The goal and Corollary 3.5 are stated in the general-rank form (I.11), $m \ge C\mu^4 n r^2(\log n)^2$ . The paper states this form explicitly on p. 2055, and the proof of Corollary 3.5 derives it as (III.26). For $r = O(1)$ it is the printed Theorem 1.1 and the printed Corollary 3.5.
Constants. Every constant ("numerical constant $C$ ", $c_0$ , and $O(M)^M := (CM)^M$ ) is an existential absolute constant quantified before $n$ , $r$ , $m$ , $M$ , $\mu$ , $j$ , $k$ and $q$ . A constant allowed to depend on $n$ or $M$ would make (I.11) unsatisfiable for large $C$ and the goal vacuous; that formalization is ruled out.
Standing assumptions. The paper assumes $n \ge C'$ and $m \ge 2nr$ (I.22) throughout. In the goal and in Corollary 3.5 they are absorbed by $C$ , since strong incoherence forces $\mu \ge 1$ . Theorem 3.4 carries $2nr \le m$ explicitly. Theorem 3.4 omits $r = O(1)$ and (I.10), since Section V uses only its own proviso $m \ge n r_\mu^2$ . Every statement also carries $m \le n^2$ , without which the uniform model is empty.
Probability. The uniform model is the platform's successProb (a ratio of finite counts). The Bernoulli model uses bernoulliEventProb and bernoulliExpectation with $p = m/n^2$ . The logarithm is natural, and the failure probability is written 1 / n^3.
Recovery. "Unique solution of (I.3)" is IsUniqueMinimizer: every other matrix that agrees with $M$ on $\Omega$ has strictly larger nuclear norm. Stating recovery conditionally on the existence of a certificate would reduce the goal to Lemma 3.1; the goal instead bounds the probability of recovery itself.
Admissible pairs. The index $i \in [j]$ is 0-based, the cyclic successor is finRotate, and the lexicographic order is compared through positions. Pair values are counted in Fin (2j(k+1)+1), which contains every admissible value, so the count is exact and finite.
New definitions. centeredTangentProjection ( $\mathcal Q_T$ ), momentMatrix ( $A$ ), and the admissible-pair calculus. Strong incoherence (A1–A2) is the shared definition CandesTao.Shared.StrongIncoherence, used by this mission and by the companion mission II. The $\mathcal Q_T$ definition is drafted independently in mission II.

Contributions are welcome on any milestone. Lemmas 5.1 and 5.2 are finite combinatorics and need no analysis. Theorem 3.4 additionally needs the expansion (IV.4) of the trace moment and the moment bounds for centered Bernoulli variables of Section IV-C. Corollary 3.5 also uses Theorem 3.2 (Rudelson selection estimate) and Lemma 3.3 (replacing $\mathcal P_T$ by $\mathcal Q_T$ ), which are milestones of the companion mission The Power of Convex Relaxation: Near-Optimal Matrix Completion II.

Selected references

E. J. Candès and T. Tao, The Power of Convex Relaxation: Near-Optimal Matrix Completion, IEEE Trans. Inf. Theory 56(5):2053–2080, 2010. https://doi.org/10.1109/TIT.2010.2044061
E. J. Candès and B. Recht, Exact Matrix Completion via Convex Optimization, Found. Comput. Math. 9(6):717–772, 2009. https://doi.org/10.1007/s10208-009-9045-5
D. Gross, Recovering Low-Rank Matrices From Few Coefficients in Any Basis, IEEE Trans. Inf. Theory 57(3):1548–1566, 2011. https://doi.org/10.1109/TIT.2011.2104999
B. Recht, A Simpler Approach to Matrix Completion, J. Mach. Learn. Res. 12:3413–3430, 2011. https://jmlr.org/papers/v12/recht11a.html

14 thms2 active usersReviewed

Completed

Machine Learning Optimization Probability+1·Captain: mikedeng1

High-Dimensional Probability X: Exact Sparse RecoveryTextbook

Motivation

Compressed sensing asks a question that looks impossible at first: can a signal $x\in\mathbb R^n$ be reconstructed exactly from far fewer than $n$ linear measurements $y=Ax\in\mathbb R^m$ , $m\ll n$ ? Classical linear algebra says no — an underdetermined system has infinitely many solutions. But if $x$ is known in advance to be sparse (most of its coordinates are zero), the extra structure makes recovery possible: solving the convex program that minimizes the $\ell_1$ norm of a candidate solution, subject to matching the measurements, recovers $x$ exactly, for a measurement matrix $A$ with a suitable geometric property. This idea, developed by Candès, Romberg, Tao and Donoho in the mid-2000s, underlies modern MRI acceleration, single-pixel cameras, and sparse signal processing generally.

The chapter isolates the exact geometric property a measurement matrix needs — the restricted isometry property (RIP) — and proves, purely by linear algebra with no probability involved, that RIP alone is sufficient for exact recovery by $\ell_1$ minimization. (A companion result, outside this mission, shows random sub-gaussian matrices satisfy RIP with high probability once $m$ is large enough, which is what makes the deterministic guarantee here practically useful; this mission formalizes the deterministic half.)

Setting

For a vector $v$ indexed by a finite set, write $\|v\|_0$ for its number of non-zero coordinates (so $v$ is $s$ -sparse if $\|v\|_0\le s$ ), $\|v\|_1:=\sum_i|v_i|$ for its $\ell_1$ norm, and $\|v\|_2:=\sqrt{\sum_i v_i^2}$ for its Euclidean norm.

An $m\times n$ matrix $A$ satisfies the restricted isometry property (RIP) with parameters $\alpha,\beta,s$ if

\alpha\|v\|_2 \;\le\; \|Av\|_2 \;\le\; \beta\|v\|_2 \qquad\text{for every } s\text{-sparse } v\in\mathbb R^n,

i.e. $A$ acts as an approximate isometry on every $s$ -sparse vector — equivalently (the book's own Exercise 10.5.9), the singular values of every $m\times s$ column-submatrix of $A$ lie in $[\alpha,\beta]$ .

Given a matrix $A$ and measurements $y=Ax$ for an unknown sparse $x$ , the exact-recovery program is

\text{minimize } \|x'\|_1 \quad\text{subject to}\quad y = Ax'.

Formalization targets

Goal (Theorem 10.5.10, RIP implies exact recovery)

\exists\,\hat x = x \quad\text{whenever}\quad \hat x \text{ solves the exact-recovery program for } y=Ax,

precisely: suppose $A$ satisfies RIP with parameters $\alpha,\beta,(1+\lambda)s$ where $\lambda>(\beta/\alpha)^2$ ; then for every $s$ -sparse $x$ , every $\hat x$ that is feasible ( $A\hat x=Ax$ ) and $\ell_1$ -optimal among feasible vectors satisfies $\hat x=x$ . No constant here is hard-coded beyond the book's own explicit threshold $\lambda>(\beta/\alpha)^2$ — the weakest stable form of the claim.

Significance

RIP isolates exactly the geometric mechanism that makes $\ell_1$ -minimization work for sparse recovery: once a matrix is known to satisfy it, exact recovery is a deterministic, provable consequence with no appeal to randomness, no failure probability, and no measurement-count formula to verify beyond the RIP parameters themselves. This clean separation — a purely geometric sufficient condition (RIP), proved separately (in the book's Theorem 10.5.11, outside this mission) to hold with high probability for random sub-gaussian matrices — is the template compressed sensing theory follows throughout: geometric/deterministic guarantee first, probabilistic verification that random constructions meet it second. The theorem is one of the two standard routes (with the direct probabilistic argument of Theorem 10.5.1) to the chapter's central claim that $m=O(s\log n)$ measurements suffice to recover any $s$ -sparse signal in $\mathbb R^n$ — exponentially fewer than the $n$ measurements a naive linear-algebraic argument would need.

The result itself, and the RIP framework, are classical and well-established (Candès-Tao 2005). This mission formalizes the deterministic linear-algebra core of the argument — the statement infrastructure (RIP, sparsity, the exact-recovery program stated as an explicit optimization problem) and the goal theorem — for a solver to close with a proof.

Difficulty

The natural first idea for showing $\hat x=x$ is to try to bound the recovery error $h:=\hat x-x$ directly using $\|Ah\|_2$ (which vanishes, since both $x$ and $\hat x$ are feasible) together with RIP applied to $h$ itself — but $h$ need not be sparse at all: it is the difference of two sparse-ish vectors and can have full support. The actual argument decomposes $h$ 's support into blocks by descending magnitude (the support $I_0$ of $x$ , then the $\lambda s$ largest remaining coordinates $I_1$ , then the next $\lambda s$ , and so on), applies RIP only to the leading block $I_{0,1}=I_0\cup I_1$ (which genuinely has bounded sparsity $\le(1+\lambda)s$ ), and separately bounds the contribution of every later block using the fact that $\hat x$ is $\ell_1$ -optimal (so $\|h_{I_0^c}\|_1\le\|h_{I_0}\|_1$ , the "cone constraint"): each later block's $\ell_2$ norm is controlled by the $\ell_1$ mass of the previous block divided by its size. This is a genuinely multi-step argument combining a purely geometric fact (RIP on one bounded-sparsity block) with a purely combinatorial one (the magnitude-sorted decomposition), and the "obvious" idea of applying RIP to $h$ as a whole does not typecheck, since RIP says nothing about vectors with more than $(1+\lambda)s$ non-zero entries.

Formalization scope

Vectors are plain functions ι → ℝ on a finite index type, not EuclideanSpace ℝ ι: the latter's fixed $\ell_2$ norm instance cannot also host the $\ell_1$ norm the program's objective needs, so both norms (L2Norm, L1Norm) are defined directly by their defining sums on the same underlying type. Sparsity (Sparsity) takes a real-valued threshold s : ℝ, matching that the RIP parameter $(1+\lambda)s$ used by the goal theorem is a real number even at integer base sparsity. A solution $\hat x$ "of the program" is formalized as an explicit argmin membership — feasibility (A.mulVec xhat = A.mulVec x) conjoined with optimality over the exact feasible set (∀ x', A.mulVec x' = A.mulVec x → l1Norm xhat ≤ l1Norm x') — never "there exists an estimator such that", the trivialization risk this chapter's own triage brief flags explicitly (shared with Chapter 3's Max-Cut): an existential reading would prove a different, strictly weaker statement. The conclusion is stated for every such $\hat x$ , not one witness, matching that RIP forces uniqueness.

This mission covers Theorem 10.5.10 only, as the sole item; the probabilistic goal Theorem 10.5.1 (exact recovery for random sub-gaussian measurement matrices, which needs Theorem 10.5.10 together with a separate probabilistic argument, Theorem 10.5.11, that random matrices satisfy RIP), and the Lasso guarantee (Theorem 10.6.1), are both left out for lack of session time: each would need a fresh probabilistic apparatus (independent isotropic sub-gaussian random rows, a failure-probability bound) built from scratch in this chapter's own sub-namespace, with no reusable published definition from an earlier chunk. L2Norm, L1Norm, Sparsity and RIP are reusable by any later chapter or mission needing sparse vectors or the restricted isometry property; solvers' contributions are welcome on completing the proof of Theorem 10.5.10 itself (the magnitude-sorted support decomposition sketched under Difficulty above), and, beyond this mission's current scope, on Theorem 10.5.11 and Theorem 10.5.1.

Selected references

E. J. Candès, T. Tao, Decoding by linear programming, IEEE Transactions on Information Theory 51 (2005), 4203–4215. https://doi.org/10.1109/TIT.2005.858979
D. L. Donoho, Compressed sensing, IEEE Transactions on Information Theory 52 (2006), 1289–1306. https://doi.org/10.1109/TIT.2006.871582
R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 10. https://doi.org/10.1017/9781108231596

5 thms2 active usersReviewed

Completed

Machine Learning Probability Statistics·Captain: mikedeng1

High-Dimensional Probability VII: Slepian's Inequality for Gaussian ProcessesTextbook

Motivation

A Gaussian process is a family $(X_t)_{t\in T}$ of jointly Gaussian real random variables indexed by an arbitrary set $T$ — not necessarily time. The canonical example is $X_t = \langle g, t\rangle$ for $t$ ranging over a subset $T\subseteq\mathbb R^n$ and $g$ a standard Gaussian vector in $\mathbb R^n$ ; this single family already encodes questions as varied as the operator norm of a random matrix, the size of a random projection, and the metric complexity of a convex body. In every one of these applications the object of interest reduces to the same quantity: $E\sup_{t\in T} X_t$ , the expected supremum of the process.

Bounding $E\sup_{t\in T} X_t$ directly is hard — computing it exactly is possible only in special cases, such as the reflection principle for Brownian motion. Slepian's inequality (David Slepian, 1962) sidesteps this by comparison: if a second Gaussian process $(Y_t)_{t\in T}$ has matching variances and at-least-as-large pairwise increments as $(X_t)_{t\in T}$ , then $Y$ 's supremum stochastically dominates $X$ 's. This turns a hard direct estimate into a search for a simpler comparison process — the technique that Sudakov and Fernique later sharpened by dropping the equal-variance hypothesis (Theorem 7.2.11), and that Sudakov used to derive a purely geometric lower bound on $E\sup_{t\in T}X_t$ from the covering numbers of $(T,d)$ (Theorem 7.4.1, Sudakov's minoration inequality). Together these results are the entry point to the theory of Gaussian width and generic chaining that occupies the rest of the book (Chapters 7–9, 11), and they underlie sharp bounds on random matrices (Section 7.3), random projections (Chapter 9), and high-dimensional geometry more broadly (Adler and Taylor, Random Fields and Geometry, Springer, 2007; Talagrand, Upper and Lower Bounds for Stochastic Processes, Springer, 2014).

Setting

Fix a probability space $(\Omega,\mathcal F,P)$ . A random process indexed by a set $T$ is a family $(X_t)_{t\in T}$ of real random variables on $\Omega$ . It is a Gaussian process if every finite linear combination $\sum_{t\in T_0} a_t X_t$ ( $T_0\subseteq T$ finite, $a_t\in \mathbb R$ ) is a (possibly degenerate) normal random variable — equivalently, every finite marginal $(X_t)_{t\in T_0}$ is a multivariate Gaussian vector. A process is mean zero if $EX_t = 0$ for every $t$ .

For a mean zero process, the increments $d(t,s) := \lVert X_t - X_s\rVert_{L^2} = (E(X_t - X_s)^2)^{1/2}$ always define a (pseudo)metric on $T$ — the canonical metric — turning the otherwise unstructured index set into a metric space. For a metric space $(T,d)$ and $\varepsilon

0 $, the **covering number**$ N(T,d,\varepsilon) $is the smallest cardinality of a finite subset$ N\subseteq T $such that every point of$ T $is within$ \varepsilon $of some point of$ N $(an$ \varepsilon $-net);$ N(T,d,\varepsilon) := \infty$ if no finite net exists.

Because $T$ need not be countable, $\sup_{t\in T} X_t(\omega)$ need not be a measurable function of $\omega$ . Following the book's own convention, every quantity built from this supremum — $E\sup_{t\in T}X_t$ and $P\{\sup_{t\in T}X_t\ge\tau\}$ — is instead defined through the process's finite-dimensional marginals: as the supremum, over finite nonempty $T_0\subseteq T$ , of $E\max_{t\in T_0}X_t$ (respectively $P\{\max_{t\in T_0}X_t\ge\tau\}$ ). This sidesteps the measurability question entirely, at the cost of the quantity possibly being $+\infty$ .

Formalization targets

Slepian's inequality (Theorem 7.2.1, goal)

Let $(X_t)_{t\in T}$ and $(Y_t)_{t\in T}$ be mean zero Gaussian processes with $EX_t^2 = EY_t^2$ and $E(X_t-X_s)^2 \le E(Y_t-Y_s)^2$ for all $t,s\in T$ . Then for every $\tau\in\mathbb R$ ,

P\{\sup_{t\in T} X_t \ge \tau\} \le P\{\sup_{t\in T} Y_t \ge \tau\},

and consequently $E\sup_{t\in T} X_t \le E\sup_{t\in T} Y_t$ .

Sudakov-Fernique's inequality (Theorem 7.2.11, milestone)

Under only the increment hypothesis $E(X_t-X_s)^2 \le E(Y_t-Y_s)^2$ (no equal-variance hypothesis),

E\sup_{t\in T} X_t \le E\sup_{t\in T} Y_t.

This is the weaker-hypothesis, strictly more applicable form: it is what Sudakov's minoration inequality and the sharp Gaussian random matrix bound of Section 7.3 both invoke.

Sudakov's minoration inequality (Theorem 7.4.1, milestone)

Let $(X_t)_{t\in T}$ be a mean zero Gaussian process with canonical metric $d$ . For every $\varepsilon\ge 0$ at which $N(T,d,\varepsilon)=:N$ is finite,

E\sup_{t\in T} X_t \ge c\,\varepsilon\,\sqrt{\log N}

for an absolute constant $c>0$ . This is the weakest, most stable form of the bound: it names no numerical value for $c$ , so it survives any later sharpening of the constant.

Slepian's inequality, finite-dimensional case (Theorem 7.2.9, milestone)

The vector-indexed special case of Theorem 7.2.1 ( $T$ finite), proved first by Gaussian interpolation and then extended to the general index set.

Significance

The results themselves. Slepian's inequality is the founding comparison theorem for Gaussian processes; Sudakov-Fernique's inequality is its practically indispensable generalization, used routinely to bound suprema of Gaussian processes without needing to track variances explicitly. Sudakov's minoration inequality is the first bridge from the probability of a Gaussian process to the metric geometry of its index set, complementing Dudley's upper bound (Chapter 8) and together giving matching bounds — up to a logarithmic factor, and exactly in many cases of interest — on $E\sup_{t\in T}X_t$ purely from the covering numbers of $(T,d)$ . Downstream, this machinery gives the sharp bound $E\lVert A\rVert \le \sqrt m + \sqrt n$ on Gaussian random matrices (Section 7.3), underlies the Gaussian width used throughout convex geometry and compressed sensing (Chapters 9, 11), and bounds the covering numbers of polytopes and other convex sets (Corollary 7.4.4).

Formalizing it. All three inequalities are proved by the book (Gaussian interpolation and integration by parts for Slepian/Sudakov-Fernique; a direct application of Sudakov-Fernique to a well-chosen comparison process for Sudakov's minoration), so this mission's work is formalizing the statements faithfully and precisely — including the finite-marginal convention needed to make $E\sup_{t\in T}X_t$ and $P\{\sup_{t\in T}X_t\ge\tau\}$ meaningful for an uncountable index set without begging the underlying measurability question. The Gaussian interpolation technique itself (Lemmas 7.2.3, 7.2.5, 7.2.7) is not part of this mission's formalization scope; it is the proof method for the milestones and belongs to solvers closing them.

Difficulty

The obvious first idea — bound $E\sup_t X_t$ by controlling each $X_t$ separately, e.g. via a union bound over a net — throws away exactly the structure Slepian-type comparisons exploit: the joint Gaussianity across $t$ , not marginal tail behavior at each fixed $t$ . A union bound needs a net and a modulus of continuity to begin with; Slepian's and Sudakov-Fernique's inequalities need neither — they compare two processes directly through their covariance structure, which is what makes the technique (Gaussian interpolation: continuously deform the covariance of one process into the other's, and track how a smooth, nearly-indicator functional behaves along the path) work with no assumption on $T$ beyond the two hypotheses stated. The genuine difficulty is the smooth-interpolation argument itself — showing that $E f(Z(u))$ is monotone in $u$ for the right choice of test function $f$ — which is exactly the part left as a milestone for solvers to formalize, not sketched here per the mission format's own rule against proof ideas.

Formalization scope

$E\sup_{t\in T}X_t$ (ProcessESup) is valued in EReal, not ℝ: the finite-marginal supremum a real-valued definition would silently default to the junk value $0$ when the set of finite-marginal expectations is unbounded above — exactly the case the book itself records as $E\sup_{t\in T}X_t=\infty$ (Exercise 7.4.2, a non-relatively-compact index set). P\{\sup_{t\in T}X_t\ge\tau\} (ProcessTailProb) stays real-valued, since it is always bounded in $[0,1]$ and so carries no such risk. Both are defined through finite nonempty subsets of $T$ , per the book's own footnote to Section 7.2; no separability, continuity, or countability assumption is placed on $T$ itself.

Gaussianity is Mathlib's ProbabilityTheory.IsGaussianProcess — every finite restriction of the process has a Gaussian law — which is definitionally the book's Definition 7.1.10 ("every finite linear combination is Gaussian"); mean-zero is stated as an explicit hypothesis alongside it. Integrability of every quantity appearing under an expectation is not stated as a separate hypothesis: Fernique's theorem (already in Mathlib for general Gaussian measures) guarantees a Gaussian process has finite moments of every order, exactly as the book takes for granted.

Sudakov's minoration inequality (Theorem 7.4.1) is formalized for the case the book's own proof actually covers — $N(T,d,\varepsilon)$ finite, taken as a hypothesis = (N : ℕ) rather than as a case split inside the conclusion — since the book itself defers the infinite-covering-number case to a separate, unproved exercise (7.4.2). This keeps $T$ fully general (still possibly uncountable) at every fixed $\varepsilon$ where the net is finite, which rules out a trivializing reading of the theorem: nothing here forces $T$ itself to be finite or countable, only the covering number at the scale $\varepsilon$ in play, which is the book's own hypothesis.

Definitions reusable beyond this mission: ProcessESup, ProcessTailProb, CanonicalMetric, and CoveringNumber are exactly the substrate Chapters 8 ("Dudley's Integral Inequality"), 9 ("The Matrix Deviation Inequality"), and 11 ("Dvoretzky-Milman's Theorem") need for Gaussian width and generic chaining; per this series' plan those missions restate them locally (drafts cannot import another draft's definitions), using this chunk's forms as the faithful reference. Contributions closing the Gaussian-interpolation machinery (Lemmas 7.2.3–7.2.8) as a reusable definitions layer, beyond what any one milestone needs, are welcome.

Selected references

Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018. https://www.math.uci.edu/~rvershyn/papers/HDP-book/HDP-book.pdf
D. Slepian, "The one-sided barrier problem for Gaussian noise", Bell System Technical Journal 41 (1962), 463–501.
V. N. Sudakov, "Gaussian random processes and measures of solid angles in Hilbert space", Soviet Mathematics Doklady 12 (1971), 412–415.
X. Fernique, "Regularité des trajectoires des fonctions aléatoires gaussiennes", in École d'Été de Probabilités de Saint-Flour IV-1974, Springer Lecture Notes in Mathematics 480 (1975), 1–96.
M. Talagrand, Upper and Lower Bounds for Stochastic Processes: Modern Methods and Classical Problems, Springer, 2014.

11 thms2 active usersReviewed

Completed

Machine Learning Probability Statistics·Captain: mikedeng1

High-Dimensional Probability II: Concentration Inequalities for Sums of Independent Random VariablesTextbook

Motivation

The central limit theorem tells us that a normalized sum of independent random variables converges in distribution to a Gaussian. For applications — bounding the failure probability of a randomized algorithm, controlling the error of a Monte Carlo estimator, proving a generalization bound in learning theory — a limiting distribution is not enough: what is needed is a single, explicit, non-asymptotic inequality that holds for every fixed sample size $N$ , not merely as $N \to \infty$ . Hoeffding's inequality (Wassily Hoeffding, 1963) and Bernstein's inequality (Sergei Bernstein, 1920s–1940s, in the form used here due to Vadim Bennett and later authors) are the two archetypal answers: both give an explicit Gaussian-type tail bound for a weighted sum of independent random variables, valid for every $N$ , with all constants made explicit. They are the workhorses behind concentration of measure, high-dimensional statistics, and the non-asymptotic analysis of randomized algorithms; a textbook trying to reach the Johnson–Lindenstrauss lemma, random matrix norms, or the restricted isometry property has to pass through this chapter first, because every one of those results is itself an application of a weighted-sum concentration inequality to a specific choice of random variables.

The central limit theorem's own error term is the obstruction that direct concentration inequalities are built to avoid: the Berry–Esseen theorem (Andrew C. Berry, 1941; Carl-Gustav Esseen, 1942) bounds the normal approximation's error at order $1/\sqrt N$ , which is too slow to recover a genuinely exponential tail bound for finite $N$ . Hoeffding's and Bernstein's inequalities are proved instead by a direct argument — bounding the moment generating function of the sum and optimizing a Markov/Chernoff exponential tilt — that never invokes the central limit theorem or its error term at all.

The sub-gaussian and sub-exponential norms

Fix a probability space $(\Omega, \mathcal F, P)$ . For a real random variable $X$ on $(\Omega, \mathcal F, P)$ , define its sub-gaussian norm

\|X\|_{\psi_2} := \inf\{t > 0 : \mathbb E \exp(X^2/t^2) \text{ is finite and } \le 2\}

and its sub-exponential norm

\|X\|_{\psi_1} := \inf\{t > 0 : \mathbb E \exp(|X|/t) \text{ is finite and } \le 2\}.

In both definitions, the requirement that the exponential moment be finite (i.e. that the moment-generating integrand be integrable), and not merely satisfy " $\le 2$ " as a bare inequality, is essential: without it a moment that is genuinely infinite for a given $t$ would vacuously count as " $\le 2$ " under the Bochner integral's convention that a non-integrable function integrates to $0$ , and every random variable — however heavy-tailed — would trivially have norm $0$ . $X$ is called sub-gaussian (respectively sub-exponential) when this infimum is over a nonempty set, i.e. when some finite $t$ makes the moment finite and at most $2$ . These are genuine norms (up to the identification of almost-surely-equal random variables) on the vector space of random variables for which they are finite, and they are the natural non-asymptotic yardsticks for tail heaviness: $\|X\|_{\psi_2} < \infty$ characterizes a Gaussian-type tail $P\{|X| \ge t\} \le 2\exp(-ct^2/\|X\|_{\psi_2}^2)$ , while $\|X\|_{\psi_1} < \infty$ characterizes an exponential-type tail $P\{|X| \ge t\} \le 2\exp(-ct/\|X\|_{\psi_1})$ . Every bounded random variable — in particular every Bernoulli or Rademacher (symmetric Bernoulli) random variable — is sub-gaussian, and the square of a sub-gaussian random variable is sub-exponential; a genuinely sub-exponential (not sub-gaussian) example is the squared coordinate $g_i^2$ of a standard Gaussian vector, or the exponential distribution itself.

Formalization targets

Goal — Theorem 2.8.2 (Bernstein's inequality, weighted sum). Let $X_1, \dots, X_N$ be independent, mean-zero, sub-exponential random variables on $(\Omega, \mathcal F, P)$ , and let $a = (a_1, \dots, a_N) \in \mathbb R^N$ . Then, for every $t \ge 0$ ,

P\Bigl\{\Bigl|\sum_{i=1}^N a_i X_i\Bigr| \ge t\Bigr\} \;\le\; 2\exp\left[-c\min\left(\frac{t^2}{K^2\|a\|_2^2}, \frac{t}{K\|a\|_\infty}\right)\right],

where $K = \max_i \|X_i\|_{\psi_1}$ and $c > 0$ is an absolute constant that does not depend on $N$ , the $X_i$ , $a$ , or $t$ .

The goal is deliberately the weighted and sub-exponential form, the weakest of the chapter's results that is still stable under the improvements a solver might find: it neither fixes $a_i \equiv 1$ (the unweighted Theorem 2.8.1, a special case) nor restricts to the lighter sub-gaussian tail (Theorem 2.6.3, which follows from a strictly stronger hypothesis). Both weaker theorems, plus Hoeffding's and Chernoff's inequalities, are included as milestones because Bernstein's own proof is built directly from them.

Significance

The result itself. Bernstein's inequality is the two-tail-regime concentration bound: a sub-gaussian tail $\exp(-ct^2/(K\|a\|_2)^2)$ near the mean, transitioning to a heavier sub-exponential tail $\exp(-ct/(K\|a\|_\infty))$ far from it, exactly the behavior one should expect from a mixture of light-tailed terms with one heavy-tailed outlier. It underlies the concentration of quadratic forms (Chapter 6's Hanson–Wright inequality controls $\sum \varepsilon_i \varepsilon_j$ -type terms, which are themselves products of sub-gaussians and hence sub-exponential by Lemma 2.7.7), and it is the standard tool for bounding empirical-process suprema whose summands are not bounded but merely light-tailed.

Formalizing it. No formalization of Bernstein's inequality — in either the weighted or unweighted, or sub-gaussian or sub-exponential form — exists yet on Prove2Me (GET /theorems?q=Bernstein and q=sub-exponential return no relevant hits, checked 2026-09-17). What this mission produces is not just the statement but the machinery underneath it: a working Orlicz-norm treatment of $\psi_1$ and $\psi_2$ that a later mission (the Hanson–Wright inequality, or any future chapter that needs sub-exponential concentration) can build on directly.

Difficulty

The obvious first idea — squaring both sides and applying Chebyshev, as one does to prove the weak law of large numbers — gives only a polynomial tail bound decaying like $1/N$ , far too weak to be useful (this is exactly the point made by the chapter's opening discussion of the coin-tossing example, comparing the linear decay from Chebyshev against the target exponential decay). The central limit theorem promises the right shape of tail asymptotically but, per Berry–Esseen, with an error of order $1/\sqrt N$ that swamps any exponential gain for large deviations — the CLT approximation is simply not valid in the tail regime the inequality needs. The actual argument instead controls the moment generating function of the full sum directly and optimizes an exponential (Chernoff) tilt; this is why the sub-gaussian and sub-exponential norms — MGF-control objects, not moment or tail objects per se — are the right technical vehicle, even though Proposition 2.5.2 and 2.7.1 show all these characterizations are equivalent up to constants. The min of two terms in Bernstein's exponent is not an artifact of a loose proof: it reflects a genuinely two-regime tail (Gaussian near the mean, exponential in the far tail), and collapsing it to a single term in either direction would either be false (dropping the exponential term) or needlessly weak (dropping the Gaussian term, which is what a naive union bound over the worst single term would give).

Formalization scope

Random variables are ℝ-valued functions on an explicit probability space (Ω, mΩ, P) (Ω : Type, MeasurableSpace Ω, P : Measure Ω, [IsProbabilityMeasure P]), matching the book's setup throughout. Independence is Mathlib's ProbabilityTheory.iIndepFun, and tail probabilities are stated with P.real, Mathlib's ℝ-valued measure evaluation, which corresponds directly to the book's $P\{\cdot\}$ .

Both Orlicz norms are defined locally, as genuine infima matching Definitions 2.5.6 and 2.7.5 verbatim (subgaussianNorm, subexponentialNorm, each sInf {t > 0 : Integrable (fun ω => E[...]) P ∧ E[...] ≤ 2}), rather than reused from Mathlib's HasSubgaussianMGF (Mathlib.Probability.Moments.SubGaussian). The Integrable conjunct is not optional dressing: Mathlib's Bochner integral of a non-integrable function is 0 by convention, so a bare E[...] ≤ 2 (without asserting integrability) would be satisfied by every t for which the moment is actually infinite, collapsing the sub-gaussian norm of a standard Gaussian (and, symmetrically, the sub-exponential norm of any heavy-tailed variable) to 0 — a trivializing formalization the mission was moderated to rule out. The same Integrable conjunct appears in every moment hypothesis (general_hoeffding, bernstein_unweighted, bernstein_weighted): ∃ s > 0, Integrable (...) P ∧ ∫ ... ≤ 2, so that the hypothesis is not satisfied vacuously by non-integrable exponential moments either. HasSubgaussianMGF bounds the moment generating function directly with a variance-proxy parameter $\sigma^2$ (E exp(tX) ≤ exp(c t²/2)), which is a different object definitionally from the Orlicz $\psi_2$ norm — equivalent up to a constant factor by the book's own Proposition 2.5.2, but not interchangeable without restating that equivalence — and Mathlib has no sub-exponential analogue at all. Since the goal theorem and two of its milestones need the sub-exponential norm, one consistent convention (the book's own Orlicz norms) is used for both $\psi_1$ and $\psi_2$ throughout the mission, rather than mixing Mathlib's MGF-based sub-gaussian convention with a locally defined sub-exponential one.

Every occurrence of the book's " $c$ is an absolute constant" is formalized as a genuine existential quantifier fixed before the random variables, the vector a, and t are introduced: ∃ c : ℝ, 0 < c ∧ ∀ ..., P.real {...} ≤ 2 * Real.exp (-(c * ...)). No numeral is substituted for c anywhere; a solver's proof may use any positive constant it can establish, exactly mirroring the book's own non-constructive existence claims. The trivializing formalization this rules out is fixing c to a specific small numeral (which would be a strictly stronger, easier, and unfaithful claim) or, in the other direction, weakening the statement by allowing c to depend on N, the $X_i$ , a, or t (which would make the theorem vacuous, since any such bound trivially holds for a small enough $c$ depending on the instance).

Chernoff's inequality (Theorem 2.3.1) needs no Orlicz norm — Bernoulli parameters $p_i$ are given directly via P.real {X i = 1} = p i ∧ P.real {X i = 0} = 1 - p i, and the conclusion uses Real.rpow (^ on ℝ → ℝ → ℝ) for the real exponent $t$ in $(e\mu/t)^t$ . Hoeffding's inequality for symmetric Bernoulli variables (Theorem 2.2.2) is likewise self-contained, needing only the two-point probability hypothesis defining the Rademacher distribution.

Selected references

W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, Journal of the American Statistical Association 58(301), 1963. https://doi.org/10.2307/2282952
S. Bernstein, The Theory of Probabilities, Gastehizdat Publishing House, Moscow, 1946 (Russian; the inequality is due to Bernstein's earlier 1920s–1930s work, this textbook states the modern sub-exponential form following later expositions).
A. C. Berry, The Accuracy of the Gaussian Approximation to the Sum of Independent Variates, Transactions of the American Mathematical Society 49(1), 1941. https://doi.org/10.2307/1990053
C.-G. Esseen, On the Liapunoff Limit of Error in the Theory of Probability, Arkiv för Matematik, Astronomi och Fysik A28, 1942.
R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 2. https://doi.org/10.1017/9781108231596

7 thms2 active usersReviewed

Completed

Machine Learning Probability Statistics·Captain: mikedeng1

High-Dimensional Probability I: Approximate Carathéodory's TheoremTextbook

Motivation

Many arguments in high-dimensional geometry, statistics and computer science need to approximate a point of a convex set by an average of a handful of extreme points, rather than represent it exactly. The classical Carathéodory theorem (1907) answers the exact question: every point of the convex hull of a set $T \subseteq \mathbb{R}^n$ is a convex combination of at most $n+1$ points of $T$ . That bound is tight and grows with the dimension $n$ , which makes it useless whenever $n$ is large — exactly the regime of interest in high-dimensional probability.

B. Maurey's empirical method — an unpublished 1980–81 result reported by G. Pisier, "Remarques sur un résultat non publié de B. Maurey," Séminaire d'Analyse Fonctionnelle 1980–1981 — and later applied by B. Carl to bound covering numbers of operators between Banach spaces (Inequalities of Bernstein-Jackson-type and the degree of compactness of operators in Banach spaces, Ann. Inst. Fourier 35(3), 1985, 79–118), replaces the exact question with an approximate one and removes the dimension dependence entirely: to approximate $x$ to accuracy $\varepsilon$ , the number of points needed depends only on $\varepsilon$ , never on $n$ . Vershynin's High-Dimensional Probability opens with this result as its "Appetizer," using it to illustrate the book's central theme — that randomness is a tool for constructing deterministic combinatorial objects — before any probabilistic machinery has been introduced.

Setting

A convex combination of finitely many points $z_1, \dots, z_m \in \mathbb{R}^n$ is a sum $\sum_{i=1}^m \lambda_i z_i$ with $\lambda_i \ge 0$ and $\sum_i \lambda_i = 1$ . The convex hull $\operatorname{conv}(T)$ of a set $T \subseteq \mathbb{R}^n$ is the set of all convex combinations of all finite collections of points of $T$ . The diameter of $T$ is $\operatorname{diam}(T) = \sup\{\|s-t\|_2 : s, t \in T\}$ , the Euclidean norm throughout.

The classical Carathéodory theorem states that every $x \in \operatorname{conv}(T)$ is a convex combination of at most $n+1$ points of $T$ — with $n+1$ generally unavoidable, attained by a simplex. The question this mission answers is different: given that we are willing to approximate $x$ rather than represent it exactly, and willing to use only combinations with equal coefficients $1/k$ (an average of $k$ points, with repetition allowed), how large must $k$ be as a function of the desired accuracy?

Formalization targets

Goal — Theorem 0.0.2, Approximate Carathéodory's theorem

\text{diam}(T) \le 1,\ x \in \operatorname{conv}(T),\ k \in \mathbb{Z}_{>0} \ \Longrightarrow\ \exists\, x_1,\dots,x_k \in T:\quad \left\| x - \frac{1}{k}\sum_{j=1}^{k} x_j \right\|_2 \le \frac{1}{\sqrt{k}}.

The quantifiers are exactly this order: for every bounded $T$ , every point of its convex hull, and every target $k$ , such an averaging set exists. This is the weakest stable statement carrying the theorem's content — the number of points $k$ does not depend on the dimension $n$ , and the coefficients are forced to be uniform — and it is the form the corollary below invokes directly.

Milestone — Corollary 0.0.4, Covering polytopes by balls

P = \operatorname{conv}(T),\ |T| = N,\ \operatorname{diam}(P) \le 1,\ \varepsilon > 0 \ \Longrightarrow\ \exists\, C,\ |C| \le N^{\lceil 1/\varepsilon^2 \rceil}:\quad P \subseteq \bigcup_{c \in C} \overline{B}(c, \varepsilon).

This is a direct application of the goal to computational geometry's covering problem: how many balls of radius $\varepsilon$ are needed to cover a polytope, and where should they be centered.

Significance

The result itself. The approximate Carathéodory theorem is the prototype of a dimension-free approximation result: whenever a set is bounded, a fixed number of points (depending only on the target accuracy, not the ambient dimension) suffices to approximate any point of its convex hull. This is what makes possible dimension-independent covering-number bounds such as Corollary 0.0.4, which in turn are the starting point for the book's later treatment of entropy, packing and generic chaining (Chapters 4, 7–8). The technique generalizes far beyond $\mathbb{R}^n$ : it underlies covering-number bounds for operators between Banach spaces (Carl's original application) and is a recurring device in learning theory for bounding the size of an $\varepsilon$ -net of a hypothesis class.

Formalizing it. Both results are elementary and already fully proved in the literature; no open mathematical content remains. What this mission contributes is a machine-checked, faithful Lean statement of Maurey's construction and its corollary, phrased over Mathlib's existing convex-hull and metric-diameter machinery, so that later missions in this series (concentration inequalities, Johnson–Lindenstrauss, chaining) can build on a verified base case of "probability constructs a deterministic covering," and so that the empirical method itself becomes a reusable, linked component on the platform. The proof of the goal (via the probabilistic argument sketched by the book: interpret a convex combination as a probability distribution, average $k$ i.i.d. samples, and bound the variance) is left open for solvers.

Difficulty

The identity that makes the proof work — averaging $k$ independent copies of a random vector concentrates around its mean at rate $1/\sqrt{k}$ in mean-square — is a two-line computation once the convex combination is reinterpreted probabilistically. The step that is easy to miss is this reinterpretation itself: nothing in the statement mentions probability, so the "obvious" attack of manipulating the convex-combination weights directly, or trying to construct $x_1,\dots,x_k$ by some explicit combinatorial recipe, does not see a path to a bound independent of $n$ . The probabilistic argument produces the points non-constructively, via an averaging/existence argument (the expected squared distance is small, so some realization achieves it) rather than an explicit formula — a solver has to introduce a probability space and a random vector that does not appear anywhere in the formal statement to be proved.

Formalization scope

Both results are stated over EuclideanSpace ℝ (Fin n) for an explicit dimension n : ℕ, so ‖·‖ is the Euclidean norm and Mathlib's Metric.diam is used directly for $\operatorname{diam}(T) = \sup\{\|s-t\|_2\}$ . The convex hull is Mathlib's convexHull ℝ T; by Mathlib's convexHull_eq, this already coincides with the book's own definition of a convex combination of finitely many points of $T$ , so no bespoke convex-combination definition is introduced — this mission needs no supporting definitions of its own. In the corollary, "a polytope $P$ with $N$ vertices" is formalized, following the book's own proof, as $P = \operatorname{conv}(T)$ for a finite vertex set $T$ with $\#T = N$ , rather than via a separate Polytope structure (which Mathlib does not provide and the book's argument does not need). The covering bound $N^{\lceil 1/\varepsilon^2\rceil}$ is an exponent, not a product with $N$ — matching the book's own proof, which counts the $N^k$ ordered $k$ -tuples of vertices with repetition, $k := \lceil 1/\varepsilon^2\rceil$ ; the typeset " $N\lceil 1/\varepsilon^2\rceil$ " in the corollary statement is the same juxtaposition-as-exponent notation the proof uses for " $N^k$ " one line earlier.

A trivializing formalization is ruled out explicitly: the goal must hold for every integer $k > 0$ and every $x \in \operatorname{conv}(T)$ , not merely some convenient choice — e.g. $k = 1$ together with $x \in T$ trivially satisfies the inequality but proves nothing about the theorem's actual content, that a fixed, dimension-independent $k$ works uniformly over all points of the hull. The formal statement quantifies $T$ , then $x$ , then $k$ , and only then asserts existence of the $x_1,\dots,x_k$ , exactly in that order.

Classical Carathéodory (Theorem 0.0.1, stated for context in the source but not used by either formalized result's proof) is not drafted here: Mathlib already proves the corresponding statement via affine independence (Caratheodory.eq_pos_convex_span_of_mem_convexHull, Analysis/Convex/Caratheodory.lean), from which the book's " $n+1$ points" bound follows via AffineIndependent.card_le_finrank_succ. It is not added as a kind: reference milestone because no corresponding theorem is yet published on the Prove2Me platform to point at (checked 2026-09-17: GET /theorems?q=Caratheodory returns only unrelated tropical-convexity results), and re-drafting existing Mathlib content as a new platform theorem would duplicate rather than reuse it.

Selected references

R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, DOI 10.1017/9781108231596, Appetizer (pp. 1–5).
G. Pisier, "Remarques sur un résultat non publié de B. Maurey," Séminaire d'Analyse Fonctionnelle (Maurey–Schwartz), 1980–1981, exposé no. 5. numdam.org/item/SAF_1980-1981____A5_0
B. Carl, "Inequalities of Bernstein-Jackson-type and the degree of compactness of operators in Banach spaces," Annales de l'Institut Fourier, 35(3), 1985, 79–118. numdam.org/item/AIF_1985__35_3_79_0

2 thms2 active usersReviewed

Operations Research Probability Statistics·Captain: mikedeng1

The Risk of Expected Utility Under Parameter Uncertainty I: Closed-Form Out-of-Sample Utility Variance of the Shrinkage Mean-Variance PortfolioResearch Paper

Why out-of-sample utility risk matters

A portfolio chosen from historical returns can look attractive in the data used to construct it and deliver a different result when evaluated under the population return distribution. The gap is driven by estimation error in both the mean return and covariance matrix. A mean of future utility values describes average performance, but it does not describe how much that utility varies across possible estimation samples. Lassance, Martín-Utrera and Simaan study this variation for a portfolio that blends an estimated mean-variance choice with an estimated global-minimum-variance choice. Their closed-form variance makes the sampling risk of that blend an explicit function of market and sample parameters. The source for this mission is the authors’ SSRN manuscript, version dated August 18, 2023, including its Internet Appendix; appendix pages are cited as IA pages.

The market and the estimated portfolio

There are $N$ risky stocks. Their excess-return vector has population mean $\mu\in\mathbb R^N$ and positive-definite population covariance $\Sigma\in\mathbb R^{N\times N}$ . The investor has risk aversion $\gamma>0$ . A portfolio is a vector of weights $w$ whose entries sum to one. Its population mean-variance utility is

U(w)=w^\top\mu-\frac{\gamma}{2}w^\top\Sigma w.

Write $e$ for the vector of ones. The global-minimum-variance portfolio and its variance are $w_g=\Sigma^{-1}e(e^\top\Sigma^{-1}e)^{-1}$ and $\sigma_g^2=(e^\top\Sigma^{-1}e)^{-1}$ . Its mean is $\mu_g=\mu^\top\Sigma^{-1}e\,\sigma_g^2$ . The population matrix $B=\Sigma^{-1}(I-ew_g^\top)$ maps the mean vector to a zero-cost portfolio. The variance of that portfolio is $\psi^2=\mu^\top\Sigma^{-1}\mu-\mu_g^2/\sigma_g^2$ . These quantities are computed from $\mu$ and $\Sigma$ ; they are not independent inputs. These definitions are equations (3)–(7) of the manuscript.

The investor observes $T$ independent return vectors $r_1,\ldots,r_T$ , each with multivariate Gaussian law $\mathcal N(\mu,\Sigma)$ . The sample mean is $\hat\mu=T^{-1}\sum_t r_t$ , and the sample covariance is $\hat\Sigma=T^{-1}\sum_t(r_t-\hat\mu)(r_t-\hat\mu)^\top$ . Replacing the population parameters in $w_g$ and $B$ by these estimates gives the sample GMV portfolio $\hat w_g$ and the sample zero-cost portfolio $\hat w_z=\hat B\hat\mu$ . The estimated mean-variance portfolio is $\hat w^\star=\hat w_g+\gamma^{-1}\hat w_z$ . At shrinkage intensity $\kappa\in[0,1]$ , the portfolio under study is $\hat w^\star(\kappa)=(1-\kappa)\hat w_g+\kappa\hat w^\star$ . Its out-of-sample utility, $U(\hat w^\star(\kappa))$ , is evaluated using population $\mu$ and $\Sigma$ . It is random because the weights depend on the sample. These choices are fixed by equations (9)–(12) and Assumption 2 of the manuscript.

Formalization targets

The goal is Proposition 1, equations (13)–(19). Under $N\ge2$ and $T>N+7$ , it asserts that the utility has a finite second moment and that

\mathbb V[U(\hat w^\star(\kappa))] =\mathbb V[U(\hat w_g)]+\Delta(\kappa),\qquad \Delta(\kappa)=a_1\kappa^4+a_2\kappa^3+a_3\kappa^2+a_4\kappa.

The coefficients $a_1,\ldots,a_4$ and $\mathbb V[U(\hat w_g)]$ are the exact rational expressions in $T,N,\gamma,\sigma_g^2,\psi^2$ on pp. 14–15 of the manuscript. In particular, the result covers every $\kappa\in[0,1]$ , including the sample GMV portfolio at $\kappa=0$ and the sample mean-variance portfolio at $\kappa=1$ .

The milestones follow the quantities named in the authors’ proof, Section IA.10. Equation (IA43) gives the covariance matrix of the random weights, and (IA44) gives the variance of their population mean return. The jointly distributed mean-return and return-variance pair in (IA45)–(IA48) supplies the setting for two auxiliary moment identities, (IA53) and (IA57). Equations (IA49), (IA59), and (IA60) give the first and second moments needed for return variance and mean return; (IA68) gives their covariance. All are statements from the Internet Appendix, pp. IA35–IA39.

What the result supplies

The expression tells an investor how the sampling risk of utility changes with the shrinkage intensity, sample size, stock count, risk aversion, and the two population variance parameters. The later comparison of variance-minimizing, mean-maximizing, and robustness-maximizing intensities uses this formula. Without Proposition 1, those comparisons have no explicit OOSU risk function to analyze. The result is already proved in the paper; this mission asks for its Lean proof and for reusable formal statements of the associated Gaussian portfolio and moment identities. No machine-checked proof of this paper’s proposition is included in the draft.

Where the difficulty lies

The sample covariance is random and its inverse appears in the estimated weights. Taking the variance of utility therefore involves inverse-covariance terms and moments beyond those needed for expected utility. The requirement $T>N+7$ is tied to existence of the fourth negative moment of a chi-squared variable in (IA57). A direct calculation that replaces random weights by their population counterparts loses the dependence on the estimation sample. A calculation from separate marginal laws also does not determine the covariance between mean return and return variance; the representation in (IA47)–(IA48) describes them jointly.

Formalization scope

The Lean market uses vectors Fin N → ℝ, matrices indexed by Fin N, and returns in EuclideanSpace ℝ (Fin N) to use Mathlib’s multivariate Gaussian law. The sample has Fin T observations on a probability space. Its covariance divisor is exactly $T$ , as in (9). The standing assumptions are $N\ge2$ , $T>N+7$ , $\Sigma\succ0$ , $\gamma>0$ , and independent, identically distributed Gaussian returns. Every theorem about a variance or covariance explicitly asserts finite second moments; expectation statements explicitly assert integrability. The source’s finite-variance convention is thereby represented without Lean’s default value for a nonintegrable variance.

The left side of the goal is the probability-theory variance of utility under the sampling law. It is not defined by the closed formula. Likewise $\sigma_g^2$ , $\mu_g$ , and $\psi^2$ are computed from the market; independence is part of the sampling hypothesis. In the auxiliary representation, the chi-squared law is the squared norm of independent standard normals. The zero-degree cases and footnote 6’s $N=2,3$ rules are encoded explicitly. Mathlib’s matrix inverse and real division are total operations; their values on singular sample covariances or zero denominators do not alter the distributions because those events have probability zero under the stated assumptions. Contributions establishing the sample-covariance distribution, the joint representation, the negative moments, and the final variance identity are within scope and can support other Gaussian portfolio results.

Selected references

N. Lassance, A. Martín-Utrera, and M. Simaan, The Risk of Expected Utility under Parameter Uncertainty, authors’ SSRN manuscript dated August 18, 2023, subsequently in Management Science (2024). SSRN 3855546; DOI 10.1287/mnsc.2023.00178.

12 thms1 active userReviewed

Probability Statistics·Captain: mikedeng1

Change-Point Detection in Dynamic Networks with Missing Links III: The Dyadic-Grid Matrix CUSUM Test Detects an Unknown Change Time Above Energy 4(1+ϵ)(6ω_n/T)^{1/2} + C log(4n log₂T/(α∧β))/√TResearch Paper

Detecting a change in a partially observed network

Many networks are recorded as a sequence of snapshots: contact networks in epidemiology, communication graphs, brain connectivity measured over time, trade or transport links. A basic statistical question is whether the law generating the snapshots changed at some point. Two features make the question hard in practice. The networks are often sparse, so each snapshot carries little information. And links are missing: a pair of vertices is observed only with some probability, so an absent edge may mean "no link" or "not sampled".

Enikeeva and Klopp (arXiv:2106.14470, Operations Research, 2025) give minimax bounds for this testing problem. They treat both a known change time (Theorems 1 and 2) and an unknown change time (Theorem 3). This mission formalizes the unknown-time case, where the test scans a dyadic grid of candidate times. Two companion missions formalize the known-time upper bound (Theorem 1) and the lower bound (Theorem 2).

Setting

There are $n$ vertices and $T$ time points. At time $t$ the statistician observes a symmetric matrix $Y^t\in\{0,1\}^{n\times n}$ with zero diagonal, $Y^t_{ij}=\Omega^t_{ij}A^t_{ij}$ . Here $A^t$ is the adjacency matrix of the network and $\Omega^t$ records which pairs were sampled. The entries $Y^t_{ij}$ , $i<j$ , are independent over pairs and times, and

Y^t_{ij}\sim\mathrm{Bernoulli}\big((\Pi\odot\Theta^t)_{ij}\big),

where $\Theta^t\in[0,1]^{n\times n}$ is the connection-probability matrix (symmetric, zero diagonal), $\Pi$ is the sampling matrix (symmetric, entries in $(0,1]$ , unit diagonal), and $\odot$ is the entrywise product.

The sparsity level $\omega_n$ bounds the expected observed degree: $(\Theta,\Pi)\in\mathcal S_n(\omega_n)$ when $\|\Pi\odot\Theta\|_{1,\infty}=\max_j\sum_i|(\Pi\odot\Theta)_{ij}|\le\omega_n$ .

Under the null hypothesis $\Theta^t=\Theta^0$ for all $t$ . Under the alternative there is $\tau\in\mathcal D_T=\{1,\dots,T-1\}$ with $\Theta^t=\Theta^0$ for $t\le\tau$ and $\Theta^t=\Theta^0+\Delta\Theta^\tau$ for $t>\tau$ . Both parameter pairs lie in $\mathcal S_n(\omega_n)$ , and the jump has energy at least $R$ :

q(\tau/T)\,\|\Pi\odot\Delta\Theta^\tau\|_{2\to2}\ge R,\qquad q(x)=\sqrt{x(1-x)},

where $\|\cdot\|_{2\to2}$ is the spectral norm. A test $\psi$ maps the data to $\{0,1\}$ . Its type I error $\alpha(\psi)$ is the largest rejection probability over the null class. Its type II error $\beta(\psi,R)$ is the largest acceptance probability over all $\tau\in\mathcal D_T$ and all alternatives of energy at least $R$ .

The Matrix CUSUM at time $t$ contrasts the averages before and after $t$ :

Z_T(t)=\sqrt{\frac{t(T-t)}{T}}\Big(\frac1t\sum_{s=1}^tY^s-\frac1{T-t}\sum_{s=t+1}^TY^s\Big),\qquad1\le t\le T-1.

The dyadic grid is $\mathcal T=\{2^k\}\cup\{T-2^k\}$ , $0\le k\le\lfloor\log_2(T/2)\rfloor$ . Fix $\epsilon\in(0,1/2]$ . The test (14) of the paper rejects when

\max_{t\in\mathcal T}\|Z_T(t)\|_{2\to2}>H_{\alpha,n,T}=2\sqrt2(1+\epsilon)\sqrt{\omega_n}+C_\epsilon\log\frac{4n\log_2(T)}{\alpha}.

Formalization targets

Goal: Theorem 3

For every $\epsilon\in(0,1/2]$ there are constants $C_\epsilon>0$ and $C$ , depending only on $\epsilon$ , such that for all $n\ge1$ , $T\ge2$ , $\omega_n\ge0$ and $\alpha,\beta\in(0,1)$ : if

R\ \ge\ 4(1+\epsilon)\Big(\frac{6\omega_n}{T}\Big)^{1/2}+\frac{C}{\sqrt T}\log\Big(\frac{4n\log_2(T)}{\alpha\wedge\beta}\Big),

then the grid test with threshold $H_{\alpha,n,T}$ has $\alpha(\psi_{n,T})\le\alpha$ and $\beta(\psi_{n,T},R)\le\beta$ .

Milestones

the signal-plus-noise decomposition $Z_T(t)=-\mu^\tau_T(t)\,\Pi\odot\Delta\Theta^\tau+\xi(t)$ and the maximum $\mu^\tau_T(\tau)=\sqrt T\,q(\tau/T)$ , display (7);
the grid facts $\mathcal T\subseteq\mathcal D_T$ and $|\mathcal T|\le2\log_2T$ ;
the grid captures signal: for every $\tau\in\mathcal D_T$ some $t\in\mathcal T$ has $\mu^\tau_T(t)\ge\sqrt T\,q(\tau/T)/\sqrt3$ ;
Proposition 11, the Bandeira–van Handel bound for symmetric random matrices with independent bounded entries;
Lemma 12, the noise bound for the CUSUM at a fixed time;
Lemma 5 (level) and Lemma 6 (power above $4\sqrt6(1+\epsilon)(\omega_n/T)^{1/2}+\frac{\sqrt3C_\epsilon}{\sqrt T}(\log\frac{4n\log_2T}\alpha+\log\frac{2n}\beta)$ ).

Significance

Theorem 3 shows that not knowing the change time costs at most a constant factor and a $\log\log T$ term in the detection energy. Together with the lower bound of Theorem 2, which is of order $(\omega_n/T)^{1/2}$ , this makes the grid test rate-optimal when $\omega_n$ grows at least polylogarithmically in $n$ (Remark 3 of the paper). The statistic depends on the data only through spectral norms of $O(\log T)$ CUSUM matrices, so it is cheap to compute. The threshold needs only the degree bound $\omega_n$ , which can be estimated from the observed degrees.

The paper's proof is complete on paper apart from one step noted below. No part of it is machine-checked. Formalizing it produces a checked finite model of Bernoulli network data with missing links, a reusable Matrix CUSUM, and a precise statement of a Bandeira–van Handel type bound for symmetric matrices with independent bounded entries. That bound is a standard tool in random-matrix statistics and is not yet available in Mathlib or on the platform.

Difficulty

The level of the test is a union bound over the grid combined with a high-probability bound on $\|\xi(t)\|_{2\to2}$ at a fixed time. The hard part is that bound, Lemma 12. A matrix Bernstein inequality gives a leading term $\sigma\sqrt{\log(n/\delta)}$ , which is too large. The statement needs the sharp form $2\sqrt2(1+\epsilon)\sigma+C_\epsilon\log(2n/\delta)$ , where the variance proxy $\sigma$ enters without a logarithmic factor. Proposition 11 supplies this only for matrices whose entries are bounded by $\sigma_*$ . The entries of $\xi(t)$ are sums over time and are only bounded by about $\sqrt{\log(n/\delta)}$ with high probability. The paper applies Proposition 11 "given the event" $\{\|\xi(t)\|_\infty\le\sigma_*\}$ , but conditioning on that event destroys centring and independence, so a truncation argument is missing there.

The power analysis is elementary once Lemma 12 is available. Its one subtlety is that the change time ranges over all of $\mathcal D_T$ , while the test inspects only the grid.

Formalization scope

Data and probability. Only $Y$ is modelled; the latent $A^t,\Omega^t$ are integrated out. An observation is a Boolean function of a 0-based time index and of a pair $i<j$ . Probabilities are finite sums of products of Bernoulli weights, so every test is measurable and no measure theory enters the model. Proposition 11 is the only measure-theoretic statement.
Classes. The sampling class carries the paper's standing assumptions $\Pi_{ii}=1$ , $\Pi_{ij}>0$ . The errors are real suprema of sets of probabilities; an empty alternative has type II error $0$ .
Spectral norm. $\|\cdot\|_{2\to2}$ is the published HighDimProb.RandomMatrices.matrixOpNorm.
Grid and test. $\lfloor\log_2(T/2)\rfloor$ is Nat.log 2 (T / 2). " $\max_{t\in\mathcal T}\|Z_T(t)\|>H$ " is " $\exists t\in\mathcal T$ , $\|Z_T(t)\|>H$ ". The threshold uses the real $\log_2T$ .
Constants. $C_\epsilon$ and $C$ are quantified existentially before $n,T,\omega_n,\alpha,\beta,R$ . A version with the constants chosen after $n$ or $T$ would be trivial, because huge constants silence the test or empty the alternative. The goal does not assume Lemma 12's conclusion. Lemmas 5 and 6 take it as a hypothesis, and Lemma 12 states that it is satisfiable. The test ranges over all functions of the data, and the alternative over all $\tau\in\mathcal D_T$ .
Disclosed additions and corrections. The theorems assume $n\ge1$ , $T\ge2$ and $\omega_n\ge0$ , which the paper leaves implicit. Proposition 11 assumes $m\ge1$ and $c_\epsilon>0$ . Independence in Proposition 11 and Lemma 12 refers to the entries with $i\le j$ ( $i<j$ ) of a symmetric matrix. The grid statement is the inequality $|\mathcal T|\le2\log_2T$ : the printed equality $|\mathcal T|=2+2\lfloor\log_2(T/2)\rfloor$ fails when the two halves overlap, as at $T=4$ . Lemma 5 is stated with " $\le\alpha$ ", as its proof concludes, rather than the printed "less than $\alpha$ ". The grid-signal milestone is stated as an existence claim, because the printed choice $\tau/2\le t^*<\tau$ has no solution at $\tau=1$ .

Welcome contributions: a proof of Proposition 11, or of any sharp spectral-norm bound that implies it; a rigorous proof of Lemma 12, repairing the conditioning step; and the elementary grid lemmas.

Selected references

F. Enikeeva and O. Klopp, Change-point detection in dynamic networks with missing links, Operations Research, 2025; arXiv:2106.14470v2. https://arxiv.org/abs/2106.14470
A. S. Bandeira and R. van Handel, Sharp nonasymptotic bounds on the norm of random matrices with independent entries, Annals of Probability 44(4), 2016. https://doi.org/10.1214/15-AOP1025
H. Liu, C. Gao and R. J. Samworth, Minimax rates in sparse, high-dimensional change point detection, Annals of Statistics 49(2), 2021. https://doi.org/10.1214/20-AOS1994

12 thms1 active userReviewed

Probability Statistics·Captain: mikedeng1

Change-Point Detection in Dynamic Networks with Missing Links II: At a Known Time the Matrix CUSUM Test Has Level α and Type II Error ≤ β Above Energy 4√2(1+ϵ)(ω_n/T)^{1/2} + C log(n/(α∧β))/√TResearch Paper

Motivation

Networks observed over time, such as communication graphs, contact networks and financial exposure graphs, often change structure abruptly. Change-point detection asks whether the law of the network changed during the observation window. In practice not every pair of nodes is observed at every time: links are missing because of sampling, privacy or measurement failure. Enikeeva and Klopp (arXiv:2106.14470, published in Operations Research, 2025) give the minimax detection boundary for this problem in a sparse inhomogeneous random graph model with missing links, for a change at a known time and at an unknown time.

This mission formalizes the upper bound at a known time (their Theorem 1): a test based on the spectral norm of a matrix-valued CUSUM statistic has level $\alpha$ and type II error at most $\beta$ as soon as the change is a constant multiple of $(\omega_n/T)^{1/2}$ plus a logarithmic term. The companion missions of this series formalize the matching lower bound (Theorem 2) and the unknown-time test (Theorem 3).

Setting

There are $n$ vertices and $T$ snapshots. At time $t$ the network has a symmetric, zero-diagonal connection-probability matrix $\Theta^t\in[0,1]^{n\times n}$ , and each pair $i<j$ is sampled independently with probability $\Pi_{ij}>0$ , where the sampling matrix $\Pi$ is symmetric with $\Pi_{ii}=1$ . What is observed is $Y^t\in\{0,1\}^{n\times n}$ , symmetric with zero diagonal, whose entries $Y^t_{ij}$ , $i<j$ , are independent Bernoulli variables with success probability $(\Pi\odot\Theta^t)_{ij}$ , independent over $t$ ; $\odot$ is the entrywise product.

The column-wise norm $\|M\|_{1,\infty}=\max_j\sum_i|M_{ij}|$ measures the largest expected observed degree. The null class is

\mathcal S_n(\omega_n)=\{(\Theta,\Pi):\ \Theta\in\mathcal C^0_n,\ \Pi\in\mathcal C_n,\ \|\Pi\odot\Theta\|_{1,\infty}\le\omega_n\}.

A change at time $\tau\in\{1,\dots,T-1\}$ replaces $\Theta^b=\Theta^0$ by $\Theta^a=\Theta^0+\Delta\Theta^\tau$ after time $\tau$ . With $q(x)=\sqrt{x(1-x)}$ and the spectral norm $\|\cdot\|_{2\to2}$ , the change-point energy is $q(\tau/T)\|\Pi\odot\Delta\Theta^\tau\|_{2\to2}$ , and the alternative class $\mathcal W^\tau_{n,T}(\omega_n,r)$ collects the pairs in $\mathcal S_n(\omega_n)$ whose energy is at least $r$ .

A test $\psi$ maps the data to $\{0,1\}$ . Its type I error $\alpha(\psi)$ is the supremum over the null class of the probability of rejecting, and its type II error $\beta(\psi,R)$ is the supremum over $\mathcal W^\tau_{n,T}(\omega_n,R)$ of the probability of accepting.

The Matrix CUSUM is

Z_T(t)=\sqrt{\frac{t(T-t)}{T}}\Big(\frac1t\sum_{s=1}^tY^s-\frac1{T-t}\sum_{s=t+1}^TY^s\Big),\qquad 1\le t\le T-1,

and the test at the known time $\tau$ is

\psi^\tau_{n,T}(Y)=\mathbf 1\big\{\|Z_T(\tau)\|_{2\to2}>H_{\alpha,n}\big\},\qquad H_{\alpha,n}=2\sqrt2(1+\epsilon)\sqrt{\omega_n}+C_\epsilon\log(2n/\alpha),

with $\epsilon\in(0,1/2]$ and $C_\epsilon$ a constant depending only on $\epsilon$ .

Formalization targets

Goal: Theorem 1

For every $\epsilon\in(0,1/2]$ there are constants $C_\epsilon>0$ and $C$ , depending only on $\epsilon$ , such that for all $n\ge1$ , $1\le\tau\le T-1$ , $\omega_n\ge0$ and $\alpha,\beta\in(0,1)$ : if

R_{n,\tau}\ge4\sqrt2(1+\epsilon)\Big(\frac{\omega_n}{T}\Big)^{1/2}+\frac{C}{T^{1/2}}\log\Big(\frac{n}{\alpha\wedge\beta}\Big),

then $\alpha(\psi^\tau_{n,T})\le\alpha$ and $\beta(\psi^\tau_{n,T},R_{n,\tau})\le\beta$ . The constants are existential and are not pinned to particular values; the statement asserts the shape of the boundary.

Milestones

Display (7): $Z_T(t)=-\mu^\tau_T(t)\,\Pi\odot\Delta\Theta^\tau+\xi(t)$ , with $\xi(t)$ the CUSUM of the centred observations, and $\max_t\mu^\tau_T(t)=\mu^\tau_T(\tau)=\sqrt T\,q(\tau/T)$ .
Proposition 11 (Bandeira and van Handel): for a symmetric $m\times m$ matrix $W$ with independent centred entries bounded by $\sigma_*$ ,

\mathbb P\{\|W\|_{2\to2}\ge2\sqrt2(1+\epsilon)\sigma+x\}\le m\,e^{-x^2/(c_\epsilon\sigma_*^2)}.

Lemma 12: with probability larger than $1-\delta$ ,

\|\xi(t)\|_{2\to2}\le2\sqrt2(1+\epsilon)\sqrt{\tfrac{t(T-t)}{T}}\Big[\tfrac1{t^2}\sum_{s\le t}\|B^s\|_{1,\infty}+\tfrac1{(T-t)^2}\sum_{s>t}\|B^s\|_{1,\infty}\Big]^{1/2}+C_\epsilon\log\tfrac{2n}{\delta}.

Lemma 3: the test has type I error at most $\alpha$ .
Lemma 4: under $R_{n,\tau}\ge4\sqrt2(1+\epsilon)(\omega_n/T)^{1/2}+C_\epsilon T^{-1/2}(\log(2n/\alpha)+\log(2n/\beta))$ the type II error is at most $\beta$ .

Significance

Theorem 1 is the upper half of the minimax detection boundary for a change at a known time. Together with Theorem 2 of the same paper (a lower bound of order $(\omega_n/T)^{1/2}$ ) it shows that, up to the logarithmic term, the CUSUM test in spectral norm is rate-optimal, and that missing links enter only through the observed degree bound $\omega_n=\max\|\Pi\odot\Theta\|_{1,\infty}$ . The same noise bound (Lemma 12) drives the unknown-time test of Theorem 3.

The result is proved in the paper; no machine-checked version exists. Formalizing it produces a checked finite-sample statement with explicit leading constant $4\sqrt2(1+\epsilon)$ , a reusable formal Bernoulli network model with missing links, and, through Proposition 11, a formal statement of the Bandeira–van Handel tail bound, which is used well beyond change-point problems. The printed proof of Lemma 12 applies Proposition 11 after conditioning on the event $\{\|\xi(t)\|_\infty\le\sigma_*\}$ , which destroys centring and independence; a complete proof needs a truncation argument that the paper does not give.

Difficulty

Under the null the CUSUM is pure noise, so both errors reduce to a high-probability bound on $\|\xi(t)\|_{2\to2}$ whose leading term is exactly $2\sqrt2(1+\epsilon)\sqrt{\omega_n}$ after rescaling. Matrix Bernstein inequalities give a bound with an extra $\sqrt{\log n}$ factor on the leading term, which is too weak for the stated threshold; the sharp constant requires the Bandeira–van Handel inequality, whose proof goes through moment comparisons for random matrices with non-identically distributed entries. The entries of $\xi(t)$ are themselves sums over time with coefficients up to order $\sqrt T$ in aggregate, so the boundedness hypothesis of Proposition 11 does not hold directly and must be recovered with probability bounds. Finally, the level and the power must hold for the same threshold constant $C_\epsilon$ , uniformly in $n$ , $T$ , $\tau$ and the parameters.

Formalization scope

An observation is a function from the $T$ snapshots and the pairs $i<j$ to Booleans; time is 0-based in Lean (snapshot $s$ is the paper's $s+1$ ). The latent adjacency and sampling matrices are integrated out: only $Y$ is modelled, by its exact product-Bernoulli law, and probabilities are finite sums over the finite observation space, so every test is measurable. Tests are Boolean-valued (true rejects). The sampling class carries the paper's standing assumptions $\Pi_{ii}=1$ and $\Pi_{ij}>0$ . Errors are real suprema over sets contained in $[0,1]$ ; an empty alternative class has type II error $0$ . The spectral norm is the published HighDimProb.RandomMatrices.matrixOpNorm. Proposition 11 alone uses measure theory, with independence of the entries on and above the diagonal and an added (implicit) $m\ge1$ .

Disclosed readings: (24) prints $\kappa_n$ , which is read as $\omega_n$ as in the proof; Lemma 12's matrices are the symmetric, zero-diagonal centred observations of the model; Lemmas 3 and 4 take " $C_\epsilon$ is a constant of Lemma 12" (with $C_\epsilon>0$ ) as a hypothesis, stated as a predicate. The goal does not assume that predicate: it asserts the existence of $C_\epsilon$ and $C$ , both chosen before $n$ , $T$ , $\tau$ , $\omega_n$ , $\alpha$ , $\beta$ and $R$ , so neither constant can be tuned to the instance, and tests range over all functions of the data. Choosing huge constants does not trivialize the goal, since for large $T$ the energy condition is met by nonempty alternatives that the test must detect.

The development needs: the product-Bernoulli law of the network, the Matrix CUSUM algebra, the Bandeira–van Handel inequality, and a truncation argument for Lemma 12. The Setting and Proposition 11 are reusable for the unknown-time test and for spectral methods on random graphs. Proofs of any milestone, and alternative routes to Lemma 12, are welcome.

Selected references

F. Enikeeva and O. Klopp, Change-point detection in dynamic networks with missing links, Operations Research, 2025; arXiv:2106.14470v2. https://arxiv.org/abs/2106.14470
A. S. Bandeira and R. van Handel, Sharp nonasymptotic bounds on the norm of random matrices with independent entries, Annals of Probability 44(4), 2016. https://doi.org/10.1214/15-AOP1025
Yu. I. Ingster and I. A. Suslina, Nonparametric Goodness-of-Fit Testing under Gaussian Models, Springer, 2003. https://doi.org/10.1007/978-0-387-21580-8

9 thms1 active userReviewed

Completed

Numerical Analysis Probability·Captain: tc

Gaussian Random Matrices III: Extreme Singular Values and ConcentrationTextbook

Motivation

A tall $N\times n$ matrix with independent standard normal entries is, with high probability, a near-isometry: all its singular values lie in $[\sqrt N-\sqrt n,\ \sqrt N+\sqrt n]$ up to Gaussian fluctuations. This is Gordon's theorem together with Gaussian concentration (Vershynin 2012, Theorem 5.32 and Corollary 5.35), the non-asymptotic counterpart of the Bai–Yin law and the model result for the whole theory of non-asymptotic random matrices. In randomized numerical linear algebra the same two ingredients give the expected spectral norm of $S\Gamma T$ (Halko–Martinsson–Tropp 2011, Proposition 10.1 (10.2)), its second moment (Tropp–Webber 2023, Lemma B.1), and the lower tail of $\sigma_{\min}$ of a Gaussian sketch, which controls the inverse moments $\mathbb E\,\sigma_{\min}^{-2p}$ that appear in the analysis of sketching algorithms with rank truncation. None of these results is available in Mathlib; this mission proves them.

Setting

A standard Gaussian matrix $A\in\mathbb R^{N\times n}$ has independent $\mathcal N(0,1)$ entries; its law is $\gamma_{N,n}$ . Its extreme singular values are

s_{\min}(A)=\inf_{\|x\|_2=1}\|Ax\|_2,\qquad s_{\max}(A)=\sup_{\|x\|_2=1}\|Ax\|_2=\|A\|,

the infimum and supremum over the unit sphere of $\mathbb R^n$ ( $n\ge1$ ); $\|A\|$ is the spectral norm. For a wide matrix $G\in\mathbb R^{k\times t}$ , $k\le t$ , the usual $\sigma_{\min}(G)$ is $s_{\min}(G^{\mathsf T})$ . The Frobenius norm is $\|A\|_F=(\sum_{i,j}A_{ij}^2)^{1/2}$ ; a function $h$ on matrices is $L$ -Lipschitz if $|h(X)-h(Y)|\le L\|X-Y\|_F$ . A chi-square variable with $d$ degrees of freedom is $\chi_d^2=\sum_{i=1}^d g_i^2$ for independent standard normals $g_i$ . The letter $e$ denotes Euler's number.

Formalization targets

Goal — deviation of the extreme singular values (Vershynin, Corollary 5.35)

For every $t\ge0$ , with probability at least $1-2e^{-t^2/2}$ ,

\sqrt N-\sqrt n-t\ \le\ s_{\min}(A)\qquad\text{and}\qquad s_{\max}(A)\ \le\ \sqrt N+\sqrt n+t .

This is the goal because it is the statement users of Gaussian matrices quote: a quantitative near-isometry with explicit sub-Gaussian deviations. It follows from the expectation bounds (Gordon) and concentration, both of which are milestones.

Milestones

Gaussian concentration for Lipschitz functions of a Gaussian matrix: $\mathbb P\{h(G)\ge\mathbb E h(G)+Lt\}\le e^{-t^2/2}$ (HMT Proposition 10.3; Vershynin Proposition 5.34).
Gordon–Chevet bound. $\mathbb E\|S\Gamma T\|\le\|S\|\|T\|_F+\|S\|_F\|T\|$ (HMT Proposition 10.1 (10.2), A.2) and its second-moment form $(\mathbb E\|S\Gamma T\|^2)^{1/2}\le\|S\|\|T\|_F+\|S\|_F\|T\|$ (Tropp–Webber Lemma B.1).
Gordon's theorem. $\sqrt N-\sqrt n\le\mathbb E s_{\min}(A)\le\mathbb E s_{\max}(A)\le\sqrt N+\sqrt n$ (Vershynin Theorem 5.32).
One-sided tail of $s_{\min}$ . $\mathbb P\{s_{\min}(A)\le\sqrt N-\sqrt n-u\}\le e^{-u^2/2}$ for $u\ge0$ (Davidson–Szarek Theorem II.13; one-sided form of Vershynin Corollary 5.35).
Chi-square lower tail. $\mathbb P\{\chi_d^2\le u\}\le(eu/d)^{d/2}$ for $0\le u\le d$ (Dasgupta–Gupta Lemma 2.2).
Small-ball bound for $s_{\min}$ . $\mathbb P\{s_{\min}(A)\le s\}\le n\bigl(\frac{e\,ns^2}{N-n+1}\bigr)^{(N-n+1)/2}$ for $s\ge0$ , $ns^2\le N-n+1$ , from the invertibility-via-distance lemma of Rudelson–Vershynin (Lemma 3.5), rotational invariance and the chi-square lower tail.

Significance

The results. Gordon's theorem is sharp: $\mathbb E s_{\min}$ and $\mathbb E s_{\max}$ are pinned to within $O(1)$ of the Bai–Yin limits for every $N,n$ . Gaussian concentration upgrades it to tail bounds with the optimal sub-Gaussian rate, and the Chevet-type bound is the same mechanism for $S\Gamma T$ , where it yields the expected spectral error of the randomized SVD. The small-ball bound covers the other regime, $s\to0$ , with polynomial decay of the exact order $N-n+1$ ; together the two tails make every negative moment $\mathbb E s_{\min}(A)^{-2p}$ , $2p<N-n+1$ , finite and explicitly bounded, which is what the early-truncated analysis needs.

Formalizing them. Mathlib has the standard Gaussian measure on finite-dimensional inner product spaces but neither Gaussian concentration for Lipschitz functions, nor Slepian's or Gordon's comparison inequalities, nor any result on singular values of random matrices. These are foundational pieces of high-dimensional probability whose formalization would be reused far beyond this series.

Difficulty

The upper bound in Gordon's theorem is proved by Slepian's comparison lemma for the Gaussian process $(u,v)\mapsto\langle Au,v\rangle$ on $S^{n-1}\times S^{N-1}$ , and the lower bound by Gordon's minimax comparison inequality for $\max_v\min_u\langle Au,v\rangle$ ; both require a theory of Gaussian processes indexed by continuous parameter sets, or at least a discretization argument with careful limits. Gaussian concentration (Tsirelson–Ibragimov–Sudakov) is usually proved through the Gaussian logarithmic Sobolev inequality or the Ornstein–Uhlenbeck semigroup, with a smoothing step to pass from smooth to Lipschitz functions. Both are long developments with no Mathlib support. The elementary alternatives do not reach the stated constants: an $\varepsilon$ -net argument bounds $\mathbb E\|A\|$ by $C(\sqrt N+\sqrt n)$ with $C>1$ , and a union bound over rows for the small-ball estimate is exactly how the stated bound is obtained, but it needs the fact that the distance from a Gaussian vector to a fixed $(n-1)$ -dimensional subspace is a $\chi_{N-n+1}$ variable, which again rests on rotational invariance.

Formalization scope

Matrices are sampled from the product measure $\gamma_{N,n}$ on arrays. $s_{\min}$ is sMin, the real infimum over the unit sphere of $\mathbb R^n$ ; $n\ge1$ is assumed so the sphere is nonempty, and $N\ge n$ is not assumed for Gordon's theorem (for $N<n$ one has $s_{\min}=0$ and the lower bound is trivial, as in the source). $s_{\max}$ is Mathlib's $\ell_2$ operator norm. Expectation bounds are stated together with integrability of their integrands, so the Lean convention that non-integrable functions integrate to $0$ cannot trivialize them. Probabilities are measures in $[0,\infty]$ compared with $\operatorname{ofReal}$ of the real bound; the goal's lower bound $1-2e^{-t^2/2}$ uses truncated subtraction and is vacuous for $t\le\sqrt{2\log2}$ , exactly as in the source. Gaussian concentration is stated with $L>0$ and $t\ge0$ , which the sources leave implicit (for $L=0$ or $t<0$ the event has probability one). Results that the sketching literature states for wide $k\times t$ matrices are stated here for tall $N\times n$ matrices via $\sigma_{\min}(G)=s_{\min}(G^{\mathsf T})$ , with $(N,n)=(t,k)$ .

Welcome contributions: Gaussian concentration for Lipschitz functions on $\mathbb R^d$ (any proof), Slepian's and Gordon's inequalities, the $1$ -Lipschitz property of $s_{\min}$ and $s_{\max}$ , the chi-square Chernoff bounds, and the law of the distance from a Gaussian vector to a subspace.

Selected references

N. Halko, P.-G. Martinsson, J. A. Tropp, Finding structure with randomness: probabilistic algorithms for constructing approximate matrix decompositions, SIAM Review 53(2), 217–288, 2011. https://arxiv.org/abs/0909.4061
J. A. Tropp, R. J. Webber, Randomized algorithms for low-rank matrix approximation: design, analysis, and applications, 2023. https://arxiv.org/abs/2306.12418
R. Vershynin, Introduction to the non-asymptotic analysis of random matrices, in Compressed Sensing: Theory and Applications, Cambridge University Press, 2012. https://arxiv.org/abs/1011.3027
L. Isserlis, On a formula for the product-moment coefficient of any order of a normal frequency distribution in any number of variables, Biometrika 12, 134–139, 1918. https://doi.org/10.1093/biomet/12.1-2.134
S. Dasgupta, A. Gupta, An elementary proof of a theorem of Johnson and Lindenstrauss, Random Structures & Algorithms 22, 60–65, 2003. https://doi.org/10.1002/rsa.10073
M. Rudelson, R. Vershynin, The Littlewood–Offord problem and invertibility of random matrices, Advances in Mathematics 218, 600–633, 2008. https://arxiv.org/abs/math/0703503
Y. Chen, J. Dongarra, Condition numbers of Gaussian random matrices, SIAM J. Matrix Anal. Appl. 27(3), 603–620, 2005. https://doi.org/10.1137/040616413
A. Edelman, Eigenvalues and condition numbers of random matrices, SIAM J. Matrix Anal. Appl. 9(4), 543–560, 1988. https://doi.org/10.1137/0609045
Y. Gordon, Some inequalities for Gaussian processes and applications, Israel J. Math. 50, 265–289, 1985. https://doi.org/10.1007/BF02759761
K. R. Davidson, S. J. Szarek, Local operator theory, random matrices and Banach spaces, Handbook of the Geometry of Banach Spaces, Vol. 1, 317–366, 2001. https://doi.org/10.1016/S1874-5849(01)80010-3
M. Ledoux, The Concentration of Measure Phenomenon, AMS Mathematical Surveys and Monographs 89, 2001. https://doi.org/10.1090/surv/089

Shared definitions: the items of this mission import Definitions.Def_GaussianMatrix_basic, a draft of Mission I; submit that proposal first so the import resolves at compile time.

Series: I. Rotation Invariance and Moment Identities · II. Inverse Moments of the Pseudoinverse · III. Extreme Singular Values and Concentration. All three missions share the definition bundle GaussianMatrix_basic, published with Mission I, and the namespace GaussianMatrix.

8 thms1 active userReviewed

Numerical Analysis Probability·Captain: tc

Gaussian Random Matrices II: Inverse Moments of the PseudoinverseTextbook

Motivation

The expected error of the randomized SVD with a $k\times(k+p)$ Gaussian test matrix is $\bigl(1+\tfrac{k}{p-1}\bigr)^{1/2}$ times the optimal error (Halko–Martinsson–Tropp 2011, Theorem 10.5). The factor $\tfrac{k}{p-1}$ is $\mathbb E\|G^{\dagger}\|_F^2$ for a $k\times(k+p)$ standard Gaussian matrix $G$ : the quality of every Gaussian sketching method is governed by inverse moments of a Gaussian matrix — moments of its pseudoinverse, equivalently of the inverse of the Wishart matrix $GG^{\mathsf T}$ . The expected spectral error uses $\mathbb E\|G^{\dagger}\|$ instead (Tropp–Webber 2023, Lemmas B.2–B.3), and deviation bounds use tail estimates for both norms (HMT Proposition 10.4). None of these inverse moments is available in Mathlib. This mission proves them.

Setting

A standard Gaussian matrix $G\in\mathbb R^{r\times k}$ has independent $\mathcal N(0,1)$ entries; its law is $\gamma_{r,k}$ . Throughout, $G$ is wide or square, $r\le k$ , so that $GG^{\mathsf T}\in\mathbb R^{r\times r}$ is almost surely invertible; $GG^{\mathsf T}$ is a Wishart matrix with $k$ degrees of freedom and $(GG^{\mathsf T})^{-1}$ is inverse-Wishart.

The pseudoinverse of a full-row-rank matrix is $G^{\dagger}=G^{\mathsf T}(GG^{\mathsf T})^{-1}$ . Its norms are determined by the inverse Wishart matrix:

\|G^{\dagger}\|_F^2=\operatorname{tr}(GG^{\mathsf T})^{-1},\qquad \|G^{\dagger}\|^2=\|(GG^{\mathsf T})^{-1}\|=\sigma_{\min}(G)^{-2},

where $\|\cdot\|_F$ is the Frobenius norm, $\|\cdot\|$ the spectral norm (largest singular value) and $\sigma_{\min}(G)$ the smallest of the $r$ singular values of $G$ . The letter $e$ denotes Euler's number.

Formalization targets

Goal — Tropp–Webber inverse spectral moment (Lemma B.3)

For integer $1\le p\le18$ and $k\ge r+2p$ ,

\Bigl(\mathbb E\,\bigl\|(GG^{\mathsf T})^{-1}\bigr\|^p\Bigr)^{1/p}\le\frac{e^2(k+r)}{2(k-r)^2}.

The case $p=1$ is $\mathbb E\|G^{\dagger}\|^2\le e^2(k+r)/(2(k-r)^2)$ , the spectral inverse moment at the heart of expected spectral-norm error bounds. It is the goal because it is the one inverse moment that is not an exact formula: its proof passes through Edelman's bound on the density of $\lambda_{\min}(GG^{\mathsf T})$ and an explicit integration, and it implies the expectation bound of HMT Proposition 10.2 by Jensen's inequality.

Milestones

Inverse-Wishart mean. $\mathbb E(GG^{\mathsf T})^{-1}=\frac{1}{k-r-1}I_r$ for $r\le k-2$ (Tropp–Webber Lemma B.2).
Frobenius inverse moment. $\mathbb E\|G^{\dagger}\|_F^2=\frac{r}{k-r-1}$ for $k-r\ge2$ (HMT Proposition 10.2 (10.3) and A.5).
Second-order inverse-Wishart moments. $\mathbb E\|G^{\dagger}\|_F^4=\frac{r^2(k-r)-2r(r-1)}{(k-r)(k-r-1)(k-r-3)}$ and $\mathbb E\|(GG^{\mathsf T})^{-1}\|_F^2=\frac{r(k-1)}{(k-r)(k-r-1)(k-r-3)}$ for $r\le k-4$ (Tropp–Webber Lemma B.2).
Chen–Dongarra tail. $\mathbb P\{\|G^{\dagger}\|>t\}\le\frac{1}{\sqrt{2\pi(k-r+1)}}\bigl(\frac{e\sqrt k}{k-r+1}\bigr)^{k-r+1}t^{-(k-r+1)}$ for $k\ge r\ge2$ , $t>0$ (HMT Proposition A.3).
Expected spectral norm of the pseudoinverse. $\mathbb E\|G^{\dagger}\|\le\frac{e\sqrt k}{k-r}$ for $r\ge2$ , $k\ge r+1$ (HMT Proposition 10.2 (10.4) and A.4).
Frobenius tail. $\mathbb P\{\|G^{\dagger}\|_F^2>\frac{12r}{k-r}t\}\le4t^{-(k-r)/2}$ for $k-r\ge4$ , $t\ge1$ (HMT Theorem A.6).

Significance

The results. Combined with the second-moment identity and block independence of Mission I, the Frobenius inverse moment gives the expected Frobenius error of the randomized SVD and of generalized Nyström; the spectral inverse moment gives the expected spectral error and the core-noise bounds of truncated sketching methods; the two tail bounds give the large-deviation statements of HMT §10.3. The second-order inverse-Wishart moments quantify the variance of $\|G^{\dagger}\|_F^2$ , which Tropp–Webber use for concentration of the randomized SVD error.

Formalizing them. The inverse-Wishart mean and the second-order moments are classical multivariate-statistics formulas (Muirhead; von Rosen) with no Mathlib counterpart. The Chen–Dongarra tail requires the exact distribution of $\sigma_{\min}$ , or at least Edelman's density bound; the Frobenius tail is HMT's own argument through the bidiagonal (Householder) model of a Gaussian matrix and chi-square moment estimates. Every statement here is a proved theorem in the literature; none has a machine-checked proof.

Difficulty

There is no Wishart distribution in Mathlib. The direct approach — compute the density of $GG^{\mathsf T}$ and integrate — needs the Wishart density, a change of variables on the cone of positive-definite matrices, and the matrix-variate gamma function. The classical route to the mean avoids this: by rotational invariance $(GG^{\mathsf T})^{-1}$ has the same law as $Q(GG^{\mathsf T})^{-1}Q^{\mathsf T}$ for every orthogonal $Q$ , so its mean is a multiple of the identity, and the trace is $\sum_i 1/\chi^2_{k-r+1}$ -type quantities whose means are elementary; making "the diagonal entries of $(GG^{\mathsf T})^{-1}$ are reciprocals of $\chi^2_{k-r+1}$ variables" rigorous requires the Gram–Schmidt (QR) decomposition of a Gaussian matrix and the independence of its factors. The spectral inverse moment needs a lower-tail bound for $\lambda_{\min}(GG^{\mathsf T})$ of the exact order $t^{(k-r+1)/2}$ ; a union bound over rows loses a factor $r$ and does not give the stated constant. The naive attempt to bound $\mathbb E\|G^{\dagger}\|^2$ by $\mathbb E\|G^{\dagger}\|_F^2$ loses a factor $r$ as well.

Formalization scope

$G$ is sampled from the product measure $\gamma_{r,k}$ on arrays; $(\cdot)^{-1}$ is Mathlib's total matrix inverse, equal to $0$ on the null set where $GG^{\mathsf T}$ is singular, and $G^{\dagger}$ is defined as $G^{\mathsf T}(GG^{\mathsf T})^{-1}$ (pinvR). Every inequality is stated together with integrability of its integrand, so the Lean convention that a non-integrable function integrates to $0$ cannot make a bound vacuous; identities with nonzero right-hand sides force integrability on their own but are also stated with it. The inverse-Wishart mean is stated entrywise. Tail bounds are inequalities between a measure in $[0,\infty]$ and $\operatorname{ofReal}$ of the real bound. Real powers with non-integer exponents are Mathlib's rpow; all bases are positive under the hypotheses. The spectral norm is Mathlib's $\ell_2$ operator norm. The sizes follow Tropp–Webber ( $G\in\mathbb R^{r\times k}$ ); HMT's $k\times(k+p)$ and $m\times n$ conventions are translated in each item's source field.

Welcome contributions: a Wishart/inverse-Wishart library (QR decomposition of a Gaussian matrix, Bartlett decomposition, chi-square moments $\mathbb E\,\Xi^{-q}=\Gamma(k/2-q)/(2^q\Gamma(k/2))$ ), and the distribution of $\sigma_{\min}$ of a Gaussian matrix (Edelman).

Selected references

N. Halko, P.-G. Martinsson, J. A. Tropp, Finding structure with randomness: probabilistic algorithms for constructing approximate matrix decompositions, SIAM Review 53(2), 217–288, 2011. https://arxiv.org/abs/0909.4061
J. A. Tropp, R. J. Webber, Randomized algorithms for low-rank matrix approximation: design, analysis, and applications, 2023. https://arxiv.org/abs/2306.12418
R. Vershynin, Introduction to the non-asymptotic analysis of random matrices, in Compressed Sensing: Theory and Applications, Cambridge University Press, 2012. https://arxiv.org/abs/1011.3027
L. Isserlis, On a formula for the product-moment coefficient of any order of a normal frequency distribution in any number of variables, Biometrika 12, 134–139, 1918. https://doi.org/10.1093/biomet/12.1-2.134
S. Dasgupta, A. Gupta, An elementary proof of a theorem of Johnson and Lindenstrauss, Random Structures & Algorithms 22, 60–65, 2003. https://doi.org/10.1002/rsa.10073
M. Rudelson, R. Vershynin, The Littlewood–Offord problem and invertibility of random matrices, Advances in Mathematics 218, 600–633, 2008. https://arxiv.org/abs/math/0703503
Y. Chen, J. Dongarra, Condition numbers of Gaussian random matrices, SIAM J. Matrix Anal. Appl. 27(3), 603–620, 2005. https://doi.org/10.1137/040616413
A. Edelman, Eigenvalues and condition numbers of random matrices, SIAM J. Matrix Anal. Appl. 9(4), 543–560, 1988. https://doi.org/10.1137/0609045
Y. Gordon, Some inequalities for Gaussian processes and applications, Israel J. Math. 50, 265–289, 1985. https://doi.org/10.1007/BF02759761
K. R. Davidson, S. J. Szarek, Local operator theory, random matrices and Banach spaces, Handbook of the Geometry of Banach Spaces, Vol. 1, 317–366, 2001. https://doi.org/10.1016/S1874-5849(01)80010-3
M. Ledoux, The Concentration of Measure Phenomenon, AMS Mathematical Surveys and Monographs 89, 2001. https://doi.org/10.1090/surv/089

Shared definitions: the items of this mission import Definitions.Def_GaussianMatrix_basic, a draft of Mission I; submit that proposal first so the import resolves at compile time.

Series: I. Rotation Invariance and Moment Identities · II. Inverse Moments of the Pseudoinverse · III. Extreme Singular Values and Concentration. All three missions share the definition bundle GaussianMatrix_basic, published with Mission I, and the namespace GaussianMatrix.

13 thms1 active userReviewed

Completed

Numerical Analysis Probability·Captain: tc

Gaussian Random Matrices I: Rotation Invariance and Moment IdentitiesTextbook

Motivation

Randomized algorithms for low-rank approximation — the randomized SVD of Halko, Martinsson and Tropp (HMT 2011), generalized Nyström, randomized subspace iteration, one-pass sketching (Tropp–Webber 2023) — multiply the input matrix by a random test matrix $\Omega$ with independent standard normal entries. Every error bound for these methods rests on a small number of facts about such standard Gaussian matrices: they are invariant under rotations, disjoint blocks of a rotated copy are independent, and the second and fourth moments of a linearly transformed Gaussian matrix are given by explicit formulas. These facts are classical, but none of them is available in Mathlib, so a Lean development of randomized numerical linear algebra currently has to carry every one of them as an explicit hypothesis of its main theorems. This mission removes those hypotheses.

Setting

For $p,m\in\mathbb N$ , a standard Gaussian matrix of size $p\times m$ is a random matrix $\Gamma\in\mathbb R^{p\times m}$ whose $pm$ entries are independent $\mathcal N(0,1)$ random variables. Its law, written $\gamma_{p,m}$ , is the product measure $\bigotimes_{i<p}\bigotimes_{j<m}\mathcal N(0,1)$ on real $p\times m$ arrays.

For a real matrix $A$ , $\|A\|_F^2=\sum_{i,j}A_{ij}^2$ is the squared Frobenius norm; $\operatorname{rank}A$ is the dimension of its column space. A matrix $V_1\in\mathbb R^{n\times k}$ has orthonormal columns when $V_1^{\mathsf T}V_1=I_k$ ; a square such matrix is orthogonal. For $t\ge1$ , a matrix $S\in\mathbb R^{n\times t}$ with independent $\mathcal N(0,1/t)$ entries is written $S=t^{-1/2}\Omega$ with $\Omega\sim\gamma_{n,t}$ , so that $SS^{\mathsf T}=\tfrac1t\Omega\Omega^{\mathsf T}$ is an unbiased sketch of the identity.

Formalization targets

Goal — Gaussian approximate matrix multiplication

For fixed $M\in\mathbb R^{a\times n}$ , $N\in\mathbb R^{b\times n}$ and $S\in\mathbb R^{n\times t}$ with independent $\mathcal N(0,1/t)$ entries,

\mathbb E\,\bigl\|MSS^{\mathsf T}N^{\mathsf T}-MN^{\mathsf T}\bigr\|_F^2=\frac{\|M\|_F^2\|N\|_F^2+\|MN^{\mathsf T}\|_F^2}{t}\le\frac2t\|M\|_F^2\|N\|_F^2 .

This is the exact mean-squared error of the sketched product $MSS^{\mathsf T}N^{\mathsf T}$ as an estimator of $MN^{\mathsf T}$ , a direct consequence of Isserlis' pairing formula for Gaussian fourth moments. It is the goal because it is the one fourth-moment computation the series needs and because every other identity in the mission is a step towards it.

Milestones

Rotational invariance. $U\Gamma V\sim\gamma_{p,m}$ for orthogonal $U\in\mathbb R^{p\times p}$ , $V\in\mathbb R^{m\times m}$ (HMT §10.1).
Blocks of a rotated Gaussian matrix. For $V_1\in\mathbb R^{n\times k}$ with orthonormal columns, $V_1^{\mathsf T}\Omega\sim\gamma_{k,t}$ ; for orthonormal $V_1,V_2$ with $V_1^{\mathsf T}V_2=0$ , the blocks $V_1^{\mathsf T}\Omega$ and $V_2^{\mathsf T}\Omega$ are independent (HMT, proof of Theorem 10.5).
Second moment. $\mathbb E\|S\Gamma T\|_F^2=\|S\|_F^2\|T\|_F^2$ (HMT Proposition 10.1 (10.1); Tropp–Webber Lemma B.1).
Fourth moment. $\mathbb E\|S\Gamma T\|_F^4=(\|S\|_F^2\|T\|_F^2)^2+2\|S^{\mathsf T}S\|_F^2\|TT^{\mathsf T}\|_F^2$ , the Isserlis formula for the Gaussian quadratic form $\operatorname{tr}(\Gamma^{\mathsf T}S^{\mathsf T}S\,\Gamma\,TT^{\mathsf T})$ ; its special case $\mathbb E\|\Omega\|_F^4=(kt)^2+2kt$ is the chi-square second moment (HMT Proposition A.8).
Full rank. $\operatorname{rank}\Gamma=\min\{p,m\}$ almost surely (HMT, proof of Theorem 10.5 and Proposition A.5).

Significance

The results. Rotational invariance and block independence are the mechanism behind every conditioning argument in randomized linear algebra: writing the right singular vectors of the input as $[V_1\ V_2]$ , the sketch splits into independent standard Gaussian blocks $\Omega_1=V_1^{\mathsf T}\Omega$ and $\Omega_2=V_2^{\mathsf T}\Omega$ , and one may condition on $\Omega_1$ while treating $\Omega_2$ as fresh. The second-moment identity then turns the deterministic range-finder bound $\|\Sigma_2\Omega_2\Omega_1^{\dagger}\|_F$ into $\|\Sigma_2\|_F^2\,\mathbb E\|\Omega_1^{\dagger}\|_F^2$ , and the approximate-multiplication identity gives the one-pass error terms. Almost-sure full rank is what makes $\Omega_1^{\dagger}$ a genuine pseudoinverse.

Formalizing them. Mathlib has the one-dimensional Gaussian measure, product measures, independence of coordinate projections, and (recently) the standard Gaussian measure on a finite-dimensional inner product space together with its invariance under linear isometries. None of the matrix-level statements above is in Mathlib. Once proved here they are reusable by every later mission in the series and by any formalization of randomized low-rank approximation, whose expectation-level inputs (e.g. $\mathbb E\|\Sigma_2\Omega_2\Omega_1^{\dagger}\|_F^2=\frac{k}{t-k-1}\|\Sigma_2\|_F^2$ ) follow from these milestones together with the inverse moments of Mission II.

Difficulty

Rotational invariance is not a computation with densities on $\mathbb R^{pm}$ that Mathlib supports out of the box: the clean route is through characteristic functions or through the basis-independence of the standard Gaussian on an inner product space, transported along the linear isometry $\Gamma\mapsto U\Gamma V$ of $\mathbb R^{p\times m}$ with the Frobenius inner product. Independence of the blocks requires identifying $[V_1\ V_2]^{\mathsf T}\Omega$ with a product measure and then projecting onto disjoint coordinate sets, with a completion of $[V_1\ V_2]$ to an orthogonal matrix when $k+r<n$ . The moment identities are finite computations, but the fourth-moment identity needs the Gaussian moments $\mathbb E g^4=3$ , $\mathbb E g^2=1$ organized through Isserlis' pairing formula over a four-fold sum of indices; the obvious entrywise expansion produces $O((pm)^4)$ terms that must be collapsed symbolically. Almost-sure full rank is the statement that the zero set of a nonzero polynomial ( $\det$ of a maximal square submatrix) is Lebesgue-null, which must be established for the product Gaussian measure.

Formalization scope

The sample space is the function type $\mathbb R^{p}\to\mathbb R^{m}\to\mathbb R$ with the product $\sigma$ -algebra; a sample is viewed as a matrix through the identity map $\mathrm{of}$ . Expectations are real Bochner integrals: for an identity with a nonzero right-hand side this forces integrability, and the integrands here are polynomials in Gaussian entries. Laws are stated as equalities of pushforward measures; independence is Mathlib's IndepFun. Dimensions may be $0$ ; all statements remain true in that case. The hypothesis $V_1^{\mathsf T}V_1=I_k$ silently forces $k\le n$ (vacuous otherwise), which matches the source.

The definition bundle GaussianMatrix_basic supplies the law $\gamma_{p,m}$ , $\|\cdot\|_F^2$ , $\|\cdot\|_F$ , the spectral norm (Mathlib's $\ell_2$ operator norm), the smallest singular value and the pseudoinverse $G^{\dagger}=G^{\mathsf T}(GG^{\mathsf T})^{-1}$ ; it is shared by the whole series. Welcome contributions: the Gaussian integration-by-parts and Isserlis lemmas for finite index sets, the identification of $\gamma_{p,m}$ with Mathlib's stdGaussian on the Frobenius inner product space, and the "polynomial zero sets are null" lemma for product measures.

Selected references

N. Halko, P.-G. Martinsson, J. A. Tropp, Finding structure with randomness: probabilistic algorithms for constructing approximate matrix decompositions, SIAM Review 53(2), 217–288, 2011. https://arxiv.org/abs/0909.4061
J. A. Tropp, R. J. Webber, Randomized algorithms for low-rank matrix approximation: design, analysis, and applications, 2023. https://arxiv.org/abs/2306.12418
R. Vershynin, Introduction to the non-asymptotic analysis of random matrices, in Compressed Sensing: Theory and Applications, Cambridge University Press, 2012. https://arxiv.org/abs/1011.3027
L. Isserlis, On a formula for the product-moment coefficient of any order of a normal frequency distribution in any number of variables, Biometrika 12, 134–139, 1918. https://doi.org/10.1093/biomet/12.1-2.134
S. Dasgupta, A. Gupta, An elementary proof of a theorem of Johnson and Lindenstrauss, Random Structures & Algorithms 22, 60–65, 2003. https://doi.org/10.1002/rsa.10073
M. Rudelson, R. Vershynin, The Littlewood–Offord problem and invertibility of random matrices, Advances in Mathematics 218, 600–633, 2008. https://arxiv.org/abs/math/0703503
Y. Chen, J. Dongarra, Condition numbers of Gaussian random matrices, SIAM J. Matrix Anal. Appl. 27(3), 603–620, 2005. https://doi.org/10.1137/040616413
A. Edelman, Eigenvalues and condition numbers of random matrices, SIAM J. Matrix Anal. Appl. 9(4), 543–560, 1988. https://doi.org/10.1137/0609045
Y. Gordon, Some inequalities for Gaussian processes and applications, Israel J. Math. 50, 265–289, 1985. https://doi.org/10.1007/BF02759761
K. R. Davidson, S. J. Szarek, Local operator theory, random matrices and Banach spaces, Handbook of the Geometry of Banach Spaces, Vol. 1, 317–366, 2001. https://doi.org/10.1016/S1874-5849(01)80010-3
M. Ledoux, The Concentration of Measure Phenomenon, AMS Mathematical Surveys and Monographs 89, 2001. https://doi.org/10.1090/surv/089

Series: I. Rotation Invariance and Moment Identities · II. Inverse Moments of the Pseudoinverse · III. Extreme Singular Values and Concentration. All three missions share the definition bundle GaussianMatrix_basic, published with Mission I, and the namespace GaussianMatrix.

8 thms1 active userReviewed

Graph Theory Probability·Captain: mikedeng1

Spectral Statistics of Erdős–Rényi Graphs I: Local Semicircle Law: Local Semicircle Law for the Sparse Noncentered Matrix A = H + f|e⟩⟨e| Down to Spectral Scale η ≈ 1/NResearch Paper

Motivation

The adjacency matrix of an Erdős–Rényi random graph contains a large deterministic mean as well as random fluctuations. The mean affects the largest eigenvalue, while the centered fluctuations determine much of the remaining spectrum. A local spectral law must describe both pieces at a resolution fine enough to distinguish eigenvalues within a narrow energy window. Erdős, Knowles, Yau and Yin established such estimates for a broader class of sparse symmetric matrices and their noncentered rank-one deformations in Spectral statistics of Erdős–Rényi graphs I. This mission formalizes the paper's Theorem 2.9, with the centered-matrix law and eleven intermediate results of the paper as milestones.

The paper treats the graph matrix through a model that also allows other sparse distributions. Its parameters $q_N$ and $f_N$ separate sparsity from the size of the deterministic mean. That separation matters: the normalized resolvent trace can obey a local semicircle law even when the deformation produces a distinguished top eigenvalue. The formal target therefore concerns the deformed matrix itself, rather than replacing it with the centered matrix.

Setting

For each size $N$ , let $H_N=(h_{ij})$ be a real symmetric random matrix. Entries indexed by the upper triangle are independent, centered, and have variance $1/N$ . Their higher moments obey

\mathbf E|h_{ij}|^p\le\frac{C^p}{Nq_N^{p-2}},\qquad 3\le p\le(\log N)^{A_0\log\log N}.

The sparsity parameter $q_N$ lies between $(\log N)^{3\xi_N}$ and $C\sqrt N$ , and the logarithmic parameter satisfies $1+a_0\le\xi_N\le A_0\log\log N$ , with $a_0>0$ and $A_0\ge10$ . Define $e_N=N^{-1/2}(1,\ldots,1)$ and the noncentered matrix $A_N=H_N+f_N|e_N\rangle\langle e_N|$ , where $0\le f_N\le N^C$ . The projection $|e_N\rangle\langle e_N|$ has every entry equal to $1/N$ . These are Definitions 2.1 and 2.2 of the source paper, pp. 5–6.

For a complex number $z=E+i\eta$ with $\eta>0$ , the resolvents are $G(z)=(H_N-zI)^{-1}$ and $\widetilde G(z)=(A_N-zI)^{-1}$ . Their normalized traces are $m(z)=N^{-1}\operatorname{Tr}G(z)$ and $\widetilde m(z)=N^{-1}\operatorname{Tr}\widetilde G(z)$ . The comparison object is the semicircle density $\rho_{\mathrm{sc}}(x)=(2\pi)^{-1}\sqrt{[4-x^2]_+}$ and its Stieltjes transform $m_{\mathrm{sc}}(z)=\int_{\mathbb R}\rho_{\mathrm{sc}}(x)/(x-z)\,dx$ . Put $\kappa_E=\bigl||E|-2\bigr|$ and $D=\{E+i\eta:|E|\le\Sigma,\ 0<\eta\le3\}$ for a fixed $\Sigma\ge3$ . These definitions appear in Section 2, pp. 7–9.

An $N$ -dependent event has $(\xi,\nu)$ -high probability when its failure probability is at most $\exp[-\nu(\log N)^{\xi_N}]$ for all sufficiently large $N$ . The spectral estimates below refer to single events on which the claimed bound holds at every $z\in D$ simultaneously.

Formalization targets

Main goal: the local law for A

Theorem 2.9 assumes $\xi_N\sim(A_0/2)\log\log N$ and $q_N\ge(\log N)^{C_1\xi_N}$ . Its first conclusion is that, with $(\xi,\nu)$ -high probability, every $z=E+i\eta\in D$ satisfies

|\widetilde m(z)-m_{\mathrm{sc}}(z)|\le(\log N)^{C_2\xi_N}\left(\min\left\{\frac1{q_N^2\sqrt{\kappa_E+\eta}},\frac1{q_N}\right\}+\frac1{N\eta}\right).

Under the additional bound $f_N\le C_0\sqrt N$ , its second conclusion controls every entry at every $z\in D$ :

|\widetilde G_{ij}(z)-\delta_{ij}m_{\mathrm{sc}}(z)|\le(\log N)^{C_2\xi_N}\left(\frac1{q_N}+\sqrt{\frac{\operatorname{Im}m_{\mathrm{sc}}(z)}{N\eta}}+\frac1{N\eta}\right).

The constants $C_1,C_2$ are universal and positive. The probability exponent $\nu>0$ may depend on the fixed parameters named in the theorem. Both conclusions, including the extra condition on $f_N$ in the second, are retained from Theorem 2.9, pp. 9–10.

Milestones

The milestones follow the paper's own sequence of numbered results.

Properties of $m_{\mathrm{sc}}$ (Lemma 3.2): $|m_{\mathrm{sc}}|\sim1$ , $|1-m_{\mathrm{sc}}^2|\sim\sqrt{\kappa_E+\eta}$ , and the size of $\operatorname{Im}m_{\mathrm{sc}}$ inside and outside the spectrum.
Resolvent identities for minors (Lemma 3.4) and the self-consistent equation $G_{ii}=1/(-z-m_{\mathrm{sc}}-([v]-\Upsilon_i))$ (Lemma 3.10); both are deterministic.
Large deviation bounds for linear and quadratic forms in independent variables with the sparse moment decay (Lemma 3.8 (ii)).
The weak local semicircle law for $H$ (Theorem 3.1) on $D_L=\{|E|\le\Sigma,\ (\log N)^LN^{-1}\le\eta\le3\}$ , $L\ge8\xi$ .
Fluctuation averaging (Lemma 4.1 (4.2)): the average $[Z]=N^{-1}\sum_iZ_i$ of the fluctuation terms is much smaller than each $Z_i$ .
The a priori norm bound $\|H\|\le2+(\log N)^\xi q^{-1/2}$ (Lemma 4.3) and the strong local law for $H$ (Theorem 2.8, the analogue of the goal for $f=0$ ).
Interlacing of the eigenvalues of $H$ and $A$ (Lemma 6.1) and the near-orthogonality $\sum_{\alpha\ne N}|\langle v_\alpha,e\rangle|^2=O(f^{-2})$ of $e$ to the non-top eigenvectors of $A$ (Corollary 6.7).
The trace comparison $|\widetilde\Lambda-\Lambda|\le\pi/(N\eta)$ (Lemma 7.1), which yields the first conclusion of the goal from Theorem 2.8.
Entrywise control of $\widetilde G$ on the event $\widetilde\Omega(\eta)$ that $\widetilde\Lambda_d+\widetilde\Lambda_o\le(\log N)^{-\xi}$ on the line $\operatorname{Im}z=\eta$ : the off-diagonal bound $\widetilde\Lambda_o\le C\Phi$ (Proposition 7.6 (7.14)) and the diagonal bounds of Lemma 7.7, with $\Phi=(\log N)^\xi/q+(\log N)^{2\xi}(\sqrt{\operatorname{Im}\widetilde m/(N\eta)}+1/(N\eta))$ .

Significance

The trace estimate gives quantitative control over spectral mass at local scales, including near the edges $E=\pm2$ . The entrywise estimate says more: each resolvent entry is close to the diagonal semicircle approximation with an error that records both sparsity and finite-size effects. The paper's later results derive density-of-states and eigenvector statements from these local controls. Those consequences are outside this mission's goal.

The intended formal development supplies reusable definitions of sparse symmetric ensembles, high-probability events, semicircle transforms, and complex resolvents, followed by exact statements of the paper's estimates. Mathlib contains no local semicircle law, for Wigner or for sparse matrices, and no Stieltjes transform of the semicircle distribution; the local law, the large deviation bounds and the interlacing lemma are each reusable beyond this paper.

Difficulty

The deterministic rank-one comparison controls the normalized trace but does not by itself control each entry of $\widetilde G$ . The entrywise estimate must account for the deformation and for fluctuations caused by sparse entries. Near the spectral edges, the stability scale of the semicircle transform changes with $\kappa_E+\eta$ ; a bound that is uniform in the bulk does not automatically retain the paper's edge behavior. The theorem also asks for one event covering a continuum of $z$ values, so a collection of separate fixed- $z$ probability bounds has the wrong quantifier order. These are substantive parts of Sections 3–7, beyond algebraic manipulation of resolvents.

Formalization scope

Lean represents all $H_N$ on one probability space and takes their entries to be real, symmetric, measurable random variables, independent in the upper triangle. Conditions involving $\log\log N$ and the moments hold for all sufficiently large $N$ ; this avoids impossible small- $N$ parameter bounds and matches the asymptotic theorem. The moment order $p$ is real, as in the paper. Each finite expectation has an explicit integrability condition. A single positive constant $C$ is used for the moment, sparsity, and deformation bounds: replacing several fixed constants by their maximum preserves all three inequalities.

Matrix indices use Fin N rather than the paper's $1,\ldots,N$ . The resolvent is a complex matrix formed by coercing the real matrix before subtracting $zI$ . Every result that uses it restricts $\eta>0$ eventually or explicitly; its inverse at a singular input is never used to make a claim. The semicircle transform is defined by the paper's integral, and $\sqrt{4-x^2}$ uses Lean's nonnegative square root, implementing the positive part. The high-probability predicate evaluates the measure of arbitrary sets, so it can state the intersection over all $z$ without a separate measurability assumption on that intersection. Positive $q_N$ and positive square-root arguments follow eventually from the model and $z\in D$ .

The deterministic Lemmas 3.2, 3.4, 3.10, 6.1 and 7.1 are stated for every real symmetric matrix and every $z$ with $\eta>0$ (Lemma 3.2 on $D$ ); the paper's $D_L$ is contained there. Minors keep the original index names, and $G^{(\mathbb T)}_{kl}$ is only used for $k,l\notin\mathbb T$ . $Z_i$ is the explicit expression of (3.15). Ordered eigenvalues are the sorted roots of the characteristic polynomial. Statements the paper makes "for fixed $z$ " (Lemmas 4.1, 7.7, Proposition 7.6) are uniform in $z$ : one threshold $N_0$ serves every $z$ . The unnamed constants $C$ , $\nu$ , $K$ are chosen after the fixed parameters and before the random matrices; the universal $C_1,C_2$ come first.

Trivializing encodings are ruled out: every resolvent is taken at $\eta>0$ , so the junk inverse of a singular matrix never enters; the model is satisfiable (independent Rademacher signs divided by $\sqrt N$ with $q_N=\sqrt N$ and $\xi_N=(A_0/2)\log\log N$ satisfy it for large $N$ ); each event of the goal is one intersection over all $z\in D$ , not a family of pointwise bounds; the constants appear in the paper's order; and the goal is about $A=H+f|e\rangle\langle e|$ with $f$ allowed to be large, so it does not reduce to Theorem 2.8.

Part (iii) of Lemma 3.8 is not a milestone: the printed (3.22) omits the diagonal variance term $(N^{-2}\sum_i|B_{ii}|^2)^{1/2}$ , without which it fails for Rademacher variables with $q\asymp\sqrt N$ . Contributions of proofs of any milestone, and of the missing groundwork (Stieltjes transforms of measures, Schur complements of resolvents, moment bounds for sums of independent variables), are welcome.

Selected references

L. Erdős, A. Knowles, H.-T. Yau and J. Yin, Spectral statistics of Erdős–Rényi graphs I: Local semicircle law, Annals of Probability 41(3B), 2013, pp. 2279–2375. arXiv:1103.1919v5; DOI:10.1214/11-AOP734.

16 thms1 active userReviewed

Information Theory Probability Statistics·Captain: mikedeng1

Universality in Polytope Phase Transitions and Message Passing Algorithms 2: State Evolution, Empirical Averages of Polynomial AMP Iterates Converge to Gaussian ExpectationsResearch Paper

Motivation

Approximate message passing (AMP) is an iterative method for large systems with random matrices. At each step, every coordinate receives a weighted combination of nonlinear messages from all other coordinates, together with a correction for dependence created by earlier steps. For symmetric random matrices, the correction makes a simple description of the high-dimensional iterates possible: a finite collection of covariance matrices predicts their limiting distributions. Bayati, Lelarge and Montanari prove this state evolution statement for polynomial AMP on a broad class of independent sub-Gaussian matrix entries, rather than only Gaussian entries (paper, §§1.2–1.3). It gives a precise distributional account of an algorithm whose coordinates are coupled at every iteration.

The paper has three distinct headline results. Its Theorem 3 compares AMP moments under two matrix laws with equal entry variances, and its Theorem 2 concerns projected cross-polytopes. This mission targets Theorem 4, which identifies the limit of empirical averages of AMP iterates with a Gaussian expectation. The companion missions address the other results; the statements here use their own copy of the paper's AMP model because draft definitions cannot yet be imported across proposals (paper, pp. 5, 8–9).

Setting

For each size $N$ , let $A(N)$ be a random symmetric $N\times N$ matrix with zero diagonal. Its entries above the diagonal are independent, centered, and sub-Gaussian at scale $C/N$ . Each coordinate $i$ carries a polynomial map $f^i(\cdot;t):\mathbb R^q\to\mathbb R^q$ at iteration $t$ and an initial vector $x_i^0$ . Their coefficients have degree at most $d$ and a uniform bound $C$ . The AMP orbit is

x_i^{t+1}=\sum_j A_{ij}f^j(x_j^t;t) -\sum_j A_{ij}^{2}Jf^j(x_j^t;t)f^i(x_i^{t-1};t-1).

The second sum is the Onsager memory term; it is absent at $t=0$ . Here $Jf^j$ is the Jacobian, so its product with the preceding $q$ -vector is another $q$ -vector. The initial vectors obey an exponential bound on their squared Euclidean norms. These assumptions form the paper's $(C,d)$ -regularity condition (Definitions 2–4, pp. 6–7).

A converging sequence has a fixed finite set of classes $a\in[k]$ . Coordinate $i$ belongs to $C_a^N$ for one class $a$ , whose proportion approaches $c_a\in(0,1)$ . A symmetric nonnegative matrix $W$ specifies entry variances: if $i\in C_a^N$ and $j\in C_b^N$ , then $\mathbb E A_{ij}^2=W_{ab}/N$ . Independent labels $Y(i)$ have class-dependent laws $P_a$ , each a finite mixture of Gaussian laws that may be degenerate. The polynomial maps have the common form $f^i(x;t)=g(x,Y(i),a,t)$ for $i\in C_a^N$ (Definition 5, pp. 8–9).

The empirical second moments of $g(x_i^0,Y(i),a,0)$ converge in probability to a prescribed positive semidefinite matrix $\widehat\Sigma_a^0$ . For $t\ge1$ , state evolution defines

\Sigma_a^t=\sum_b c_bW_{ab}\widehat\Sigma_b^{t-1},\qquad \widehat\Sigma_a^t=\mathbb E\big[g(Z_a^t,Y_a,a,t)g(Z_a^t,Y_a,a,t)^{\mathsf T}\big],

where $Z_a^t\sim\mathcal N(0,\Sigma_a^t)$ is independent of $Y_a\sim P_a$ . The index $t-1$ in the first formula and $t$ in the second are essential (equations (1.9)–(1.11), p. 9).

Formalization targets

Coordinate moments and concentration

For a nonnegative multi-index $m$ and a coordinate sequence eventually in class $a$ , Proposition 4 identifies the Gaussian limit of each moment. Proposition 5 says the variance of the class-average monomial tends to zero:

\mathbb E[(x_{i(N)}^t)^m]\longrightarrow\mathbb E[(Z_a^t)^m],\qquad \operatorname{Var}\!\left(\frac1{|C_a^N|}\sum_{i\in C_a^N}(x_i^t)^m\right)\longrightarrow0.

The diagonal two-time identity (4.4) is another milestone: $\Sigma_a^{t,t}$ has four blocks, each equal to $\Sigma_a^t$ . These are the paper's stated intermediate targets (pp. 15, 30, 32).

Main goal: Theorem 4

For $t\ge1$ , class $a$ , and every locally Lipschitz function $\psi$ with $|\psi(x,y)|\le K(1+\|x\|_2^2+\|y\|_2^2)^K$ for some $K$ , prove convergence in probability:

\frac1{|C_a^N|}\sum_{j\in C_a^N}\psi(x_j^t,Y(j)) \longrightarrow \mathbb E[\psi(Z_a^t,Y_a)].

The target covers polynomial-growth test functions, including functions beyond monomials. The expectation on the right is under the product law of the Gaussian state and the independent class label (Theorem 4, p. 9).

Significance

The theorem assigns a computable asymptotic distribution to each class of AMP coordinates at every fixed positive iteration time. It can be used to evaluate empirical observables without tracking the full coupled $N$ -dimensional random trajectory. The class weights and variance profile permit heterogeneous coordinates, while the sub-Gaussian assumption covers more matrix laws than a Gaussian-only statement (paper, Introduction and Theorem 4).

The paper proves this result. The mission's Lean statements are compilation-checked targets, with proofs still to be formalized. A completed development would establish the measure-theoretic meaning of the covariance recursion and its Gaussian expectations, as well as the moment and concentration claims needed for the empirical limit. The polynomial representation, random-matrix regularity predicate, and Gaussian transport are reusable for other AMP results from the same paper.

Difficulty

The matrix $A(N)$ is reused at every AMP iteration, so a new coordinate is correlated with earlier coordinates and with the matrix entries that produced them. A direct independent-summand argument for its Gaussian limit is unavailable. The memory term is tuned to this dependence, and any formal proof must account for its exact Jacobian and squared-entry form. Passing from individual moments to empirical averages also requires control of correlations between different coordinates. The target allows locally Lipschitz functions with polynomial growth, so convergence for a fixed monomial alone does not finish the job (paper, §4.7).

Formalization scope

Vectors in $\mathbb R^q$ are functions Fin q → ℝ; squared Euclidean norms are explicit sums of coordinate squares. Polynomials use bounded real coefficient arrays as in (4.10), with an explicit Jacobian. Fin N uses zero-based indices. The orbit stores the current and preceding iterates and omits the memory term at $t=0$ . A single probability space carries all sizes; matrix entries, labels, coefficients, and initial vectors have explicit measurability and independence conditions.

The paper's displayed sub-Gaussian formula conflicts with its stated $C/N$ scale, so the model uses the scale required by its moment estimates and imposes the moment-generating bound for all real arguments. Its initial exponential bound is read almost surely at every size, which ensures the expectations used by the paper are well-defined. Label-dependent polynomial coefficients are measurable. The full label vector is independent of the matrix and initial vectors; this makes explicit the independence needed for Theorem 4's Gaussian-label product law. Independence of the induced polynomial coefficients alone would not imply it when $g$ ignores part of a label. The initial covariance limit is entrywise convergence in probability; finite-dimensional equivalence makes this the same matrix convergence. Class averages divide by the class cardinality, even though that expression has Lean's default value at an empty class for a small $N$ . Positive limiting class fractions make those finite exceptions irrelevant.

Gaussian laws live on Mathlib's Euclidean space and are transported to coordinate vectors. Theorems explicitly assert positive semidefiniteness or integrability where a non-PSD covariance, non-integrable expectation, or non-square-integrable variance could otherwise give a default value. The source's $Y(i)$ in (1.12) is read as $Y(j)$ , its summation index, and its final covariance as $\Sigma_a^t$ . The Gaussian covariance is computed by the recursion above; it is not defined from the proposed limit. Contributions establishing moment bounds, covariance positivity, Gaussian integrability, the three milestones, or the full Theorem 4 are within scope.

Selected references

M. Bayati, M. Lelarge and A. Montanari, Universality in polytope phase transitions and message passing algorithms, Annals of Applied Probability 25(2), 2015, 753–822. arXiv:1207.7321v2; DOI:10.1214/14-AAP1010.

12 thms1 active userReviewed

Convex Optimization Discrete Geometry Information Theory+1·Captain: mikedeng1

Universality in Polytope Phase Transitions and Message Passing Algorithms 3: Projected Cross-Polytopes Have Weak Neighborliness ρ∗(δ) for Sub-Gaussian Matrices with a Gaussian ComponentResearch Paper

Why this phase transition matters

Sparse recovery asks when a vector with few nonzero coordinates can be reconstructed from fewer linear measurements than unknowns. A related geometric question asks how many faces of a high-dimensional cross-polytope survive a random linear projection. The two questions meet at the same threshold: uniqueness of a minimum-one-norm solution corresponds to a face of the projected cross-polytope. For Gaussian measurement matrices this threshold was known before the work of Bayati, Lelarge and Montanari, from Donoho's face-counting analysis (Donoho 2006); the same curve was later identified as the transition of approximate message passing (Donoho, Maleki and Montanari 2009). Their 2015 paper establishes the same weak-neighborliness curve for a broader class of independent sub-Gaussian entries with a nonzero Gaussian component. The result addresses the universality question posed for these projections: does the asymptotic transition depend on the full entry distribution or only on broad features of the matrix law?

The mathematical theorem is established in that paper. This mission records its statement in Lean and leaves the machine-checked proof open. The relevant statement is Theorem 2 on page 5 of the pinned arXiv version 2, rather than a claim about every random projection without a Gaussian component.

Polytopes, faces, and random matrices

The cross-polytope $C_n$ is the unit ball for the coordinate one-norm in $\mathbb R^n$ :

C_n=\left\{x\in\mathbb R^n:\sum_{i=1}^n|x_i|\leq1\right\}.

For an $m\times n$ matrix $A$ , the projected polytope $AC_n$ consists of all $Ax$ with $x\in C_n$ . Write $F(Q;\ell)$ for the number of nonempty faces of $Q$ whose affine dimension is $\lfloor\ell\rfloor$ . The weak neighborliness level $\rho\in(0,1)$ of a random sequence $Q_n\subseteq\mathbb R^{m(n)}$ means that, for every $\xi>0$ , the ratio $F(Q_n;m(n)\rho(1-\xi))/F(C_n;m(n)\rho(1-\xi))$ converges in probability to one, while the analogous ratio with $1+\xi$ converges in probability to zero. Both limits belong to the definition; the first alone would record only survival below a candidate threshold.

The matrices have $m(n)=\lfloor n\delta\rfloor$ rows for a fixed sampling ratio $\delta\in(0,1)$ . Within each matrix, the entries are independent, centered, unit-variance, and sub-Gaussian with one scale factor independent of $n$ . They also admit a decomposition $A(n)=\widetilde A(n)+\nu_0G(n)$ , where $\nu_0>0$ and the entries of $G(n)$ are independent standard normal variables, jointly independent of $\widetilde A(n)$ . The theorem imposes no independence between matrices with different values of $n$ Bayati–Lelarge–Montanari, Theorem 2.

Formalization targets

Let $\phi$ and $\Phi$ be the density and distribution function of a standard normal random variable. The paper defines its phase boundary through a positive parameter $\alpha$ :

f_\delta(\alpha)=\frac{2\phi(\alpha)}{\alpha+2\bigl(\phi(\alpha)-\alpha\Phi(-\alpha)\bigr)},\qquad f_\rho(\alpha)=1-\frac{\alpha\Phi(-\alpha)}{\phi(\alpha)}.

Footnote 3 states that $f_\delta$ decreases from one to zero on the nonnegative half-line, so each $\delta\in(0,1)$ has exactly one positive parameter. The goal, Theorem 2, says that whenever $f_\delta(\alpha)=\delta$ , the sequence $A(n)C_n$ has weak neighborliness $f_\rho(\alpha)$ in probability. The Lean theorem spells out this parameter relation; it does not apply an inverse function at an argument outside a proved range.

The milestone list covers the two scalar results identifying the boundary, a deterministic condition for exact recovery, and the compressed-sensing transition. With $Z$ standard normal and $u_+=\max(u,0)$ , the scalar function is

G_\varepsilon(\alpha)=\varepsilon(1+\alpha^2)+2(1-\varepsilon)\mathbb E[(Z-\alpha)_+^2].

Lemma 8 gives its unique positive minimizer and its minimum value. Lemma 9 relates that minimum to both sides of the boundary. The scalar state evolution $\sigma_{t+1}^2=\mathsf F(\sigma_t^2,\alpha\sigma_t)$ , with $\mathsf F(\sigma^2,\theta)=\delta^{-1}\mathbb E\{[\eta(X+\sigma Z;\theta)-X]^2\}$ and $\eta(u;\theta)=\operatorname{sign}(u)(|u|-\theta)_+$ soft thresholding, has slope $G_\varepsilon(\alpha)/\delta$ at the origin and is concave (Lemma 7). Lemma 10 shows that a two-time correlation map $\mathcal F_{\alpha,\varepsilon}$ satisfies $\mathcal F_{\alpha,\varepsilon}(Q)>Q$ on $[0,1)$ . Theorem 10, cited from Bürgisser and Cucker, bounds the probability that a Gaussian-perturbed rectangular matrix has a small least singular value:

\mathbb P\{\sigma_N(B+\nu G)\le\nu z\}\le(a_1z)^{M-N+1}.

Lemma 5 gives a recovery condition based on an approximate dual certificate and singular-value bounds. Theorem 8 states that minimum-one-norm recovery succeeds with probability tending to one below the boundary and fails with probability tending to one above it Bayati–Lelarge–Montanari, pp. 39–41, 60–61.

What a formal proof would establish

The goal would certify that the same face-count transition applies to every entry law in the stated class, including laws that are not identically distributed across the matrix. The conclusion is geometric: it counts faces of an actual projected one-norm ball. The recovery milestone provides a second way to state the threshold for sparse signals. Together they make the normalization and the two sides of the transition explicit, so future variants can compare their assumptions and conclusions with a fixed formal statement.

No machine-checked proof of Theorem 2 or of the selected milestones is known. The declarations are open Lean statements over explicit definitions. A complete development would formalize the known argument in the paper, including the probabilistic estimates and the bridge from recovery probabilities to face counts. Sharper results that remove the Gaussian component would be separate theorems with their own hypotheses.

Where the difficulty lies

The count of surviving faces depends on many supports and sign patterns simultaneously. Matching means and variances of matrix entries does not make their finite-dimensional face counts equal. Likewise, controlling recovery for one fixed signal does not immediately control the fraction of all faces. Near the boundary, exact recovery also requires uniform singular-value information for many column submatrices. These are the points where elementary concentration for a single entry or a single support is insufficient. The source paper treats the geometric statement and the recovery transition under a Gaussian-component condition; a proof that silently assumes full Gaussianity would miss its universality claim.

Formalization scope

Vectors are functions on Fin n, and every one-norm is an explicit sum of absolute values. The squared Euclidean norm is a sum of coordinate squares; the default norm on Fin n → ℝ is not used for it. Face counts reuse the published Grunbaum2003.faceCount definition, with dimension $\lfloor\ell\rfloor$ for nonnegative $\ell$ ; negative dimensions have zero nonempty faces. The two limits in weak neighborliness use convergence in measure, which expresses convergence in probability here. The printed lower ratio has a zero denominator for $\xi>1$ , so that limit is stated for $0<\xi\leq1$ . Ratios at small $n$ may involve zero denominators, but the asymptotic assertion concerns arbitrarily large $n$ .

Theorem 2 uses variance one and an $N(0,1)$ Gaussian component. Theorem 8 instead uses variance $1/m(n)$ and an $N(0,1/m(n))$ component, exactly as printed. Sub-Gaussianity uses Mathlib's moment-generating-function predicate for all real parameters; this is the operative two-sided reading of the paper's stated scale condition. The scalar Gaussian expectation in $G_\varepsilon$ is accompanied by an explicit integrability conclusion in Lemma 8, excluding Lean's zero value for a nonintegrable integral. The restricted least singular value is the infimum of output norms on unit column vectors. This gives zero when a wide submatrix has a kernel and is the bound needed by Lemma 5. The state-evolution map is written as a function of $\sigma^2$ , and its derivative at $0$ is a right derivative. In Lemma 10 the law of $X_\infty$ is the three-atom mixture on $\{0,+\infty,-\infty\}$ , with the split of the mass $\varepsilon$ between the two infinite atoms left free. The page's clause $\mathcal F'_{\alpha,\varepsilon}(1)<1$ is stated for $\alpha>\alpha_*(\varepsilon)$ , since the derivative equals $1$ at $\alpha=\alpha_*$ . Theorem 10 quantifies $\nu>0$ and $z>0$ , which the page leaves implicit.

The random-matrix predicates require measurability, independence within each $n$ , the stated marginal laws, and independence of $G(n)$ from $\widetilde A(n)$ . They leave the matrix law otherwise arbitrary. The weak-neighborliness predicate contains both face-ratio limits and $0<\rho<1$ ; neither the goal nor a milestone defines the threshold by assuming its conclusion. A full proof needs reusable facts about Gaussian integrals, independence of finite arrays, random face counts, restricted singular values, and the relation between projected faces and unique one-norm recovery. Contributions establishing those facts or closing any of the listed theorem statements are within scope.

Selected references

Mohsen Bayati, Marc Lelarge and Andrea Montanari, Universality in polytope phase transitions and message passing algorithms, Annals of Applied Probability 25(2), 2015. arXiv:1207.7321v2
David L. Donoho, High-dimensional centrally symmetric polytopes with neighborliness proportional to dimension, Discrete & Computational Geometry 35, 617–652, 2006. MR2225676
David L. Donoho, Arian Maleki and Andrea Montanari, Message-passing algorithms for compressed sensing, Proceedings of the National Academy of Sciences 106, 18914–18919, 2009. doi:10.1073/pnas.0909892106
Peter Bürgisser and Felipe Cucker, Smoothed analysis of Moore–Penrose inversion, SIAM Journal on Matrix Analysis and Applications 31, 2769–2783, 2010. MR2740632

16 thms1 active userReviewed

Linear algebra Probability·Captain: mikedeng1

User-Friendly Tail Bounds for Sums of Random Matrices III: The Matrix Chernoff Inequality for Sums of Independent Positive-Semidefinite Random MatricesResearch Paper

Motivation

The classical Chernoff bound controls the probability that a sum of independent, nonnegative, uniformly bounded random variables deviates from its mean, with exponentially small tails governed by the Kullback–Leibler divergence between two Bernoulli laws. Many problems in numerical linear algebra, graph sparsification, compressed sensing and randomized algorithms instead require control of a sum of independent random matrices: the smallest singular value of a random matrix with independent columns, the spectrum of a sampled Laplacian, or the conditioning of a random submatrix. For these, what matters is not a scalar sum but the extreme eigenvalues of a random positive-semidefinite matrix.

Ahlswede and Winter (2002) introduced a matrix version of the Laplace transform method and proved a matrix Chernoff bound for identically distributed summands. Tropp's paper (arXiv:1004.4389, Found. Comput. Math. 2012) replaced the Golden–Thompson step of their argument with Lieb's concavity theorem, obtaining a master tail bound for independent sums, and derived from it matrix Chernoff, Bernstein and Azuma inequalities that require no identical distribution and lose only a dimensional factor. This mission formalizes the matrix Chernoff inequalities of §5 of that paper.

Timeline:

2002, Ahlswede–Winter: matrix Laplace transform method; matrix Chernoff bound for i.i.d. summands via Golden–Thompson.
2010, Oliveira: a variant of the Laplace transform method used in Proposition 3.1 of the paper.
2010–2012, Tropp: master tail bound via Lieb's theorem (Theorem 3.6), and Theorem 5.1 / Corollary 5.2 for independent, non-identical psd summands.

Setting

All matrices are $d\times d$ complex matrices with $d\ge1$ . For a self-adjoint (Hermitian) matrix $A$ , $\lambda_{\max}(A)$ and $\lambda_{\min}(A)$ are its algebraically largest and smallest eigenvalues. The semidefinite order $A\preccurlyeq B$ means that $B-A$ is positive semidefinite (psd). Functions of a self-adjoint matrix are defined spectrally: if $A = Q\Lambda Q^*$ then $f(A) = Qf(\Lambda)Q^*$ ; this gives the matrix exponential $e^A$ and, on positive-definite matrices, the matrix logarithm $\log A$ .

A random matrix is a measurable map $X:\Omega\to\mathbb C^{d\times d}$ on a probability space $(\Omega,\mathcal F,\mathbb P)$ , and its expectation $\mathbb E X$ is taken entrywise. The matrix moment generating function of $X$ is $\theta\mapsto\mathbb E\,e^{\theta X}$ .

The objects of the mission are independent random Hermitian matrices $X_1,\dots,X_n$ that are almost surely psd contractions: $X_k\succcurlyeq0$ and $\lambda_{\max}(X_k)\le1$ . Their average expectation has extreme eigenvalues

\bar\mu_{\min} = \lambda_{\min}\Big(\frac1n\sum_{k=1}^n\mathbb E X_k\Big),\qquad \bar\mu_{\max}=\lambda_{\max}\Big(\frac1n\sum_{k=1}^n\mathbb E X_k\Big),

and the binary information divergence is

\mathrm D(a\,\|\,u) = a(\log a-\log u)+(1-a)(\log(1-a)-\log(1-u)),\qquad a,u\in[0,1].

In Lean these are lambdaMax, lambdaMin, mexp, mlog, mean and binDiv in the namespace MatrixTail.Chernoff.

Formalization targets

Goal: Theorem 5.1 (Matrix Chernoff I)

\mathbb P\Big\{\lambda_{\min}\Big(\tfrac1n\textstyle\sum_k X_k\Big)\le\alpha\Big\}\le d\,e^{-n\,\mathrm D(\alpha\|\bar\mu_{\min})}\quad(0\le\alpha\le\bar\mu_{\min}),

\mathbb P\Big\{\lambda_{\max}\Big(\tfrac1n\textstyle\sum_k X_k\Big)\ge\alpha\Big\}\le d\,e^{-n\,\mathrm D(\alpha\|\bar\mu_{\max})}\quad(\bar\mu_{\max}\le\alpha\le1).

Milestones

Theorem 3.6 (master tail bound): for every $\theta>0$ at which the mgfs exist, $\mathbb P\{\lambda_{\max}(\sum_kX_k)\ge t\}\le e^{-\theta t}\operatorname{tr}\exp(\sum_k\log\mathbb E\,e^{\theta X_k})$ .
Corollary 3.9: the same with the mgfs under one logarithm, $d\cdot\exp(-\theta t+n\log\lambda_{\max}(\frac1n\sum_k\mathbb E\,e^{\theta X_k}))$ .
Lemma 5.8 (Chernoff mgf): $\mathbb E\,e^{\theta X}\preccurlyeq\mathbf I+(e^\theta-1)\mathbb E X$ for a random psd contraction $X$ .
Display (5.1): $\mathbb P\{\lambda_{\max}(\sum_kX_k)\ge t\}\le d\exp(-\theta t+n\log(1+(e^\theta-1)\bar\mu_{\max}))$ .
Display (5.2): $\mathbb P\{\lambda_{\min}(\sum_kX_k)\le t\}\le d\exp(\theta t+n\log(1-(1-e^{-\theta})\bar\mu_{\min}))$ .

Further statement

Corollary 5.2 (Matrix Chernoff II), the form usually quoted: with $\lambda_{\max}(X_k)\le R$ , $\mu_{\min},\mu_{\max}$ the extreme eigenvalues of $\sum_k\mathbb E X_k$ ,

\mathbb P\{\lambda_{\min}(\textstyle\sum_kX_k)\le(1-\delta)\mu_{\min}\}\le d\Big[\tfrac{e^{-\delta}}{(1-\delta)^{1-\delta}}\Big]^{\mu_{\min}/R},\quad \mathbb P\{\lambda_{\max}(\textstyle\sum_kX_k)\ge(1+\delta)\mu_{\max}\}\le d\Big[\tfrac{e^{\delta}}{(1+\delta)^{1+\delta}}\Big]^{\mu_{\max}/R}.

Significance

Theorem 5.1 matches the strongest scalar Chernoff bound for independent, non-identical Bernoulli trials, up to the factor $d$ , which cannot be removed (coupon collector, Remark 5.6). Corollary 5.2 is the version used in applications: lower bounds on the smallest singular value of matrices with independent columns (Remark 5.4), spectral sparsification, column subset selection and random sampling of matrices. Remark 5.5 derives from it the expectation bound $\mathbb E\lambda_{\max}(\sum_kX_k)\le C\max\{\mu_{\max},R\log d\}$ .

The results are proved in the paper, from Lieb's concavity theorem. As far as is known, no machine-checked proof of a matrix Chernoff inequality exists in Lean or Mathlib. A formalization yields a reusable statement for the random-matrix and randomized-numerical-linear-algebra literature, and the milestones (the master bound, the single-logarithm corollary and the semidefinite mgf bound) are reusable beyond this mission.

Difficulty

The scalar Chernoff argument uses $\mathbb E\,e^{\theta(X+Y)}=\mathbb E\,e^{\theta X}\,\mathbb E\,e^{\theta Y}$ for independent $X,Y$ . For matrices $e^{A+B}\neq e^Ae^B$ unless $A$ and $B$ commute, so the trace of the mgf of a sum does not factor. The Golden–Thompson inequality handles two summands but does not extend to three, which is why the Ahlswede–Winter bound needed identical distributions. The master bound (Theorem 3.6) requires Lieb's concavity theorem, which has no counterpart in Mathlib. Corollary 3.9 in addition needs operator concavity of the matrix logarithm, and Lemma 5.8 needs the transfer of a scalar inequality to the semidefinite order through the spectral calculus.

Formalization scope

Matrices are Matrix (Fin d) (Fin d) ℂ with [NeZero d]; the semidefinite order is Mathlib's MatrixOrder (A ≤ B ↔ (B − A).PosSemidef). exp and log of a matrix are the continuous functional calculus cfc. $\lambda_{\max}$ , $\lambda_{\min}$ are sSup/sInf of the real spectrum. Expectation is entrywise. Random matrices are measurable with respect to the Borel σ-algebra on matrices, independence is iIndepFun, and the probability measure is a probability measure. The summands are Hermitian for every outcome; "psd" and " $\lambda_{\max}\le1$ " hold almost surely. The sequence has $n\ge1$ terms wherever an average $1/n$ appears. An infimum over $\theta>0$ is stated as a bound for every admissible $\theta>0$ ; integrability of $e^{\theta X_k}$ is a hypothesis only in Theorem 3.6 and Corollary 3.9, where the summands are unbounded. In Lean $\log 0=0$ , so at the boundary values $\bar\mu\in\{0,1\}$ the divergence is finite where the paper's is $+\infty$ ; this only weakens the stated bound.

A formalization in which $d=0$ (empty spectrum, $\lambda_{\max}=0$ ) or $n=0$ (the average $1/0=0$ ) were allowed, or in which the range of $\alpha$ were dropped, would state a different, partly false theorem; these cases are excluded.

A complete development needs Lieb's theorem or another route to the master bound, operator concavity of the logarithm, the spectral mapping theorem and the transfer rule for the functional calculus on Hermitian matrices, monotonicity of the trace exponential, and the scalar optimization in $\theta$ . Contributions of any of these as stand-alone lemmas are welcome.

Selected references

J. A. Tropp, User-Friendly Tail Bounds for Sums of Random Matrices, arXiv:1004.4389v7 (2011); Found. Comput. Math. 12 (2012) 389–434. https://arxiv.org/abs/1004.4389, https://doi.org/10.1007/s10208-011-9099-z
R. Ahlswede, A. Winter, Strong converse for identification via quantum channels, IEEE Trans. Inform. Theory 48 (2002) 569–579. https://doi.org/10.1109/18.985947
E. H. Lieb, Convex trace functions and the Wigner–Yanase–Dyson conjecture, Adv. Math. 11 (1973) 267–288. https://doi.org/10.1016/0001-8708(73)90011-X
R. I. Oliveira, Sums of random Hermitian matrices and an inequality by Rudelson, Electron. Commun. Probab. 15 (2010) 203–212. https://arxiv.org/abs/1004.3821

8 thms1 active userReviewed

Completed

Linear algebra Probability·Captain: tc

An Introduction to Matrix Concentration Inequalities Ch 8: Lieb’s ConcavityTextbook

Prove Lieb’s concavity theorem (Theorem 8.1.1, also stated as Theorem 3.4.1): for fixed Hermitian H, the function A ↦ tr exp(H + log A) is concave on positive-definite matrices. This is the deterministic foundation of Chapter 3’s probabilistic argument.

Milestones follow the book’s route through generalized Klein, relative-entropy nonnegativity, variational trace formulas, operator Jensen, matrix perspectives, and joint convexity of relative entropy. Logarithm and trace-exponential monotonicity are included as reusable comparisons. The domain allows noncommuting positive-definite matrices without trace normalization.

Source: Tropp, January 2015 version, Chapter 8. Lean statements compile; proofs remain open.

Shared definitions: Chapter 3; submit that draft first.

Series: Ch. 3 | Ch. 4 | Ch. 5 | Ch. 6 | Ch. 7 | Ch. 8.

12 thms1 active userReviewed

Completed

Linear algebra Probability·Captain: tc

An Introduction to Matrix Concentration Inequalities Ch 4: Gaussian and Rademacher SeriesTextbook

Control the spectral norm of a matrix series with independent standard Gaussian or Rademacher coefficients. The goal is Theorem 4.1.1, including its variance identity, expected-norm estimate, and tail bound for rectangular complex matrices.

Milestones are the Gaussian and Rademacher matrix mgf/cgf estimates (Lemmas 4.6.2–3) and the Hermitian series bound (Theorem 4.6.1). The formulation keeps the source’s constants, both coefficient laws, and the zero-variance case. The shared Chapter 3 tools connect these transform estimates to concentration.

Source: Tropp, January 2015 version, Chapter 4. Lean statements compile; proofs remain open.

Shared definitions: Chapter 3; submit that draft first.

Series: Ch. 3 | Ch. 4 | Ch. 5 | Ch. 6 | Ch. 7 | Ch. 8.

10 thms1 active userReviewed

Completed

Linear algebra Probability·Captain: tc

An Introduction to Matrix Concentration Inequalities Ch 7: Intrinsic DimensionTextbook

Replace ambient matrix dimension by intrinsic dimension, the ratio of trace to spectral norm. The goal is intrinsic Matrix Bernstein (Theorem 7.3.1). Intrinsic Matrix Chernoff (Theorem 7.2.1) is a second major target within the mission.

Supporting milestones include the generalized Laplace bound, intrinsic-dimension trace estimate, block-diagonal identities, Hermitian Bernstein, and the expected-norm corollary. The statements retain the source’s constants, threshold restrictions, and matrix-valued mean or variance bounds. Nonzero proxies keep intrinsic dimension well-defined; the expectation constant is universal.

Source: Tropp, January 2015 version, Chapter 7. Lean statements compile; proofs remain open.

Shared definitions: Chapter 3; submit that draft first.

Series: Ch. 3 | Ch. 4 | Ch. 5 | Ch. 6 | Ch. 7 | Ch. 8.

17 thms1 active userReviewed

Completed

Linear algebra Probability·Captain: tc

An Introduction to Matrix Concentration Inequalities Ch 6: Matrix BernsteinTextbook

Control the spectral norm of a sum of independent, centered, bounded rectangular random matrices. The goal is Matrix Bernstein (Theorem 6.1.1), including the variance identity and both expected-norm and tail estimates.

Milestones cover Hermitian dilation, variance additivity, the bounded-summand mgf/cgf estimate (Lemma 6.6.2), and Hermitian Bernstein (Theorem 6.6.1). Chapter 3 supplies the general Laplace-transform machinery. The formulation uses the Euclidean operator norm, preserves the one-sided eigenvalue assumption in the Hermitian result, and includes deterministic zero sums.

Source: Tropp, January 2015 version, Chapter 6. Lean statements compile; proofs remain open.

Shared definitions: Chapter 3; submit that draft first.

Series: Ch. 3 | Ch. 4 | Ch. 5 | Ch. 6 | Ch. 7 | Ch. 8.

14 thms1 active userReviewed

Random Matrix Theory

Missions

Subadditive Ergodic Theory 5: For a Stationary Sequence in a Banach Algebra with E(log‖Y₁‖)⁺ < ∞, n⁻¹ log‖Y₁⋯Y_n‖ Converges in [−∞, ∞)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6 (p. 893)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Subadditive Ergodic Theory 4: Furstenberg–Kesten — for Stationary Positive Random Matrices, n⁻¹ log [Y₁⋯Y_n]_ij Converges, Independently of i and jResearch Paper

Products of random matrices

Setting

Formalization targets

Goal: Theorem 5

Milestones, in the order of the paper's proof

Significance

Difficulty

Formalization scope

Selected references

On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming 4: For a Random Subspace, ‖Pq‖⁻∞ ≤ (log n/n)‖r‖² with Probability Tending to OneResearch Paper

Motivation

Setting

Formalization targets

Theorem 5

Source milestones

Significance

Difficulty

Formalization scope

Selected references

Understanding and Using Linear Programming IX: Basis Pursuit Recovers Sparse Solutions Exactly iff the Kernel Misses the CrosspolytopeTextbook

Motivation

Setting

Formalization targets

Goal: Lemma 8.5.4 (reformulation of BP-exactness)

Milestones

Further draft item: Theorem 8.5.2

Significance

Difficulty

Formalization scope

Selected references

Randomized Algorithms for Estimating the Trace of an Implicit Symmetric Positive Semi-Definite Matrix V: Sample Bound for the Mixed Unit Vector Trace EstimatorResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 8.4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Randomized Algorithms for Estimating the Trace of an Implicit Symmetric Positive Semi-Definite Matrix III: Sample Bound for Normalized Rayleigh-Quotient Trace EstimatorsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6.1, in the form its proof establishes

Milestones (the displayed steps of the proof, p. 8:10)

Significance

Difficulty

Formalization scope

Selected references

The Power of Convex Relaxation: Near-Optimal Matrix Completion I: Exact Nuclear-Norm Recovery with Quadratic Dependence on the RankResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1.1, general-rank form (I.11)

Milestones

Significance

Difficulty

Formalization scope

Selected references

High-Dimensional Probability X: Exact Sparse RecoveryTextbook

Motivation

Setting

Formalization targets

Goal (Theorem 10.5.10, RIP implies exact recovery)

Significance

Difficulty