Statistics

Motivation

Principal component analysis estimates the eigenvalues of a population covariance matrix $\Sigma$ by those of the sample covariance matrix $S$. Before random matrix theory turned to the regime where the dimension grows with the sample size, the classical question was the opposite one: the number of variables $N$ is fixed and the number of samples $M$ tends to infinity. In that regime $S\to\Sigma$ almost surely, and the next question is the size and shape of the fluctuations of the sample eigenvalues. When $\Sigma$ has a repeated eigenvalue, the sample eigenvalues near it do not fluctuate independently: they repel each other, and their joint limit law is that of the eigenvalues of a random Hermitian (or symmetric) matrix. Anderson (1963) derived these limits for real Gaussian samples.

Baik, Ben Arous and Péché (2005) study complex Gaussian samples whose covariance matrix is the identity apart from finitely many "spiked" eigenvalues, and find a phase transition for the largest sample eigenvalue $\lambda_1$ as $M,N\to\infty$ together. Their Proposition 1.1 is the fixed-dimension counterpart: with $N=k$ fixed and all population eigenvalues equal, $\lambda_1$ fluctuates on the scale $M^{-1/2}$ with the law of the largest eigenvalue of a $k\times k$ Gaussian unitary ensemble (GUE). The paper places it beside its Theorem 1.1(b), where a $k$-fold spike above the critical value $1+\gamma^{-1}$ gives the same GUE limit when $N\to\infty$. This mission formalizes Proposition 1.1.

Setting

Fix $k\ge1$ and $\ell_1>0$. A standard complex Gaussian is $g=a+ib$ with $a,b$ independent centred real Gaussians of variance $1/2$, so $\mathbb E|g|^2=1$. For each $M$, let $G=(G_{mj})$, $1\le m\le M$, $1\le j\le k$, have independent standard complex Gaussian entries (sampleLaw M k), and let the samples be $\vec y_m=\sqrt{\ell_1}\,(G_{m1},\dots,G_{mk})^{\mathsf T}$: mean zero, covariance $\Sigma=\ell_1 I_k$. The sample covariance matrix is

$$S=\frac1M\sum_{m=1}^M\vec y_m\,\vec y_m^{\,*},$$

a $k\times k$ Hermitian matrix (sampleCov), and $\lambda_1$ is its largest eigenvalue (largestEig). The general model sampleVec U ℓ G m $=U\operatorname{diag}(\sqrt{\ell})\,\vec g_m$ is specialized to $U=I$ and $\ell_j=\ell_1$, because a Hermitian matrix with all eigenvalues equal to $\ell_1$ is $\ell_1 I_k$.

Write $V(\xi)^2=\prod_{1\le i<j\le k}|\xi_i-\xi_j|^2$ (vandSq). The finite-GUE distribution (Definition 1.2) is

$$G_k(x)=\frac1{Z_k}\int_{(-\infty,x]^k}V(\xi)^2\prod_{i=1}^ke^{-\xi_i^2/2}\,d\xi,\qquad Z_k=\int_{\mathbb R^k}V(\xi)^2\prod_{i=1}^ke^{-\xi_i^2/2}\,d\xi,$$

the distribution function of the largest eigenvalue of a $k\times k$ GUE matrix. In Lean these are G k x and Z k.

Formalization targets

Goal: Proposition 1.1

For every real $x$ and every $\varepsilon>0$,

$$\lim_{M\to\infty}\mathbb P\Big((\lambda_1-\ell_1)\frac1{\ell_1}\sqrt M\le x\Big)=G_k(x),\qquad \lim_{M\to\infty}\mathbb P\big(|\lambda_1-\ell_1|>\varepsilon\big)=0 .$$

The second statement is $\lambda_1\to\ell_1$ in probability.

Milestones

With $\pi_1=\ell_1^{-1}$, $M\ge k$, and $C=\int_{(0,\infty)^k}V(y)^2\prod_je^{-M\pi_1y_j}y_j^{M-k}\,dy$:

1. (302) $\mathbb P(\lambda_1\le t)=\frac1C\int_{(0,t]^k}V(y)^2\prod_je^{-M\pi_1y_j}y_j^{M-k}\,dy$;
2. (303) $C=\prod_{j=0}^{k-1}(1+j)!(M-k+j)!\,/\,(M\pi_1)^{Mk}$;
3. (27) $Z_k=(2\pi)^{k/2}\prod_{j=1}^kj!$;
4. (304) the rescaled form of (302) after $y_j=\pi_1^{-1}(1+\xi_j/\sqrt M)$;
5. $\pi_1^{kM}M^{k^2/2}e^{kM}C\to(2\pi)^{k/2}\prod_{j=0}^{k-1}(1+j)!$ as $M\to\infty$;
6. (29) $G_1$ is the standard normal distribution function.

Significance

The proposition identifies the fixed-dimension limit of the top sample eigenvalue under a degenerate population spectrum: the $k$ sample eigenvalues near $\ell_1$, rescaled by $\sqrt M/\ell_1$, behave like a $k\times k$ GUE spectrum, and $\lambda_1$ like its maximum. For $k=1$ it reduces to the central limit theorem for the sample variance of one complex Gaussian variable, with limit $\Phi$ by (29). For general $k$ it shows that the GUE limit of the supercritical regime in Theorem 1.1(b) is already present when the dimension does not grow.

The result is proved in the paper (§5, p. 1691) by an exact computation. No machine-checked proof of it, of the complex Wishart eigenvalue density, or of the Gaussian and Laguerre cases of Selberg's integral is known to exist in Mathlib or on the platform. The formalization requires the joint eigenvalue density of a complex Wishart matrix (a Weyl-type integration formula over the unitary group), two Selberg-type integral evaluations, a Stirling asymptotic for products of factorials, and a dominated-convergence argument on $\mathbb R^k$. The first three are reusable well beyond this mission.

Difficulty

The limit itself follows from (304) and the constant asymptotics. The hard part is (302): passing from the law of the matrix $S$ to the joint law of its eigenvalues. This requires the change of variables $S=W\operatorname{diag}(\lambda)W^*$ with $W$ unitary, the Jacobian $V(\lambda)^2$, and the integration over the unitary group. A direct central limit argument for the entries of $S$ gives the Gaussian limit of $\sqrt M(S-\ell_1I)/\ell_1$ as a GUE matrix. To get from there to $\lambda_1$ one needs the continuity of the largest eigenvalue in the matrix entries and a matching normalisation, so it is a different route from the paper's. Either route requires spectral facts about Hermitian matrices that Mathlib does not yet package. The Selberg evaluations (27) and (303) are classical but have no short proof: the standard arguments use orthogonal polynomials or an induction with a Dixon–Anderson type integral.

Formalization scope

• The sample model is shared by every mission of this series:
  • the samples are mean-zero and uncentred, with $\mathbb E|g|^2=1$ per complex coordinate, and $S$ carries the factor $1/M$, as in the paper's formula (59). The density (1) "with the complex inner product", $S=\frac1NXX^*$ on p. 1645 and the centring by the sample mean on p. 1643 are printed slips that contradict (59);
  • $\lambda_1$ is the supremum of Mathlib's eigenvalues of the Hermitian matrix $S$. The events $\{\lambda_1\le t\}$ are closed, hence measurable, sets of samples.
• The probabilities are (sampleLaw M k).real of explicit sets.
• (50) is printed without "$\le$"; the event $(\lambda_1-\ell_1)\ell_1^{-1}\sqrt M\le x$ is stated.
• (29) is printed with "erf(x)"; the standard normal distribution function is stated.
• $Z_k$ and $C$ are defined as integrals, never as their closed forms. Otherwise (27) and (303) would hold by definition.
• The goal mentions only the sample model, $\lambda_1$ and $G_k$, not $C$, the Laguerre weight or the substitution. This rules out the trivializing formalizations: the covariance is the page's $\ell_1I_k$, not a further special case, and nothing in the statement is vacuous for $k\ge1$, $\ell_1>0$.
• The milestones (302)–(304) assume $k\le M$, which the page uses implicitly through the exponent $M-k$. (304) assumes $x\ge-\sqrt M$, the range of its integration limits.

Contributions are welcome on each milestone. Particularly reusable are the complex Wishart eigenvalue density, the Gaussian and Laguerre Selberg integrals, and the measurability and continuity of eigenvalues of Hermitian matrix families.

Selected references

• J. Baik, G. Ben Arous, S. Péché, Phase transition of the largest eigenvalue for nonnull complex sample covariance matrices, Ann. Probab. 33(5) (2005), 1643–1697. https://doi.org/10.1214/009117905000000233
• T. W. Anderson, Asymptotic theory for principal component analysis, Ann. Math. Statist. 34 (1963), 122–148. https://doi.org/10.1214/aoms/1177704248
• A. T. James, Distributions of matrix variates and latent roots derived from normal samples, Ann. Math. Statist. 35 (1964), 475–501. https://doi.org/10.1214/aoms/1177703550
• I. M. Johnstone, On the distribution of the largest eigenvalue in principal components analysis, Ann. Statist. 29 (2001), 295–327. https://doi.org/10.1214/aos/1009210544
• P. J. Forrester, S. O. Warnaar, The importance of the Selberg integral, Bull. Amer. Math. Soc. 45 (2008), 489–534. https://doi.org/10.1090/S0273-0979-08-01221-4

Motivation

Suppose an unknown unit vector $s \in S^{d-1}$ is observed through exact linear measurements $Y_j = \langle X_j, s\rangle$ with independent Gaussian rows $X_j \sim N(0, I_d)$. If every pair is kept, $d$ rows determine $s$. A learner that can keep only a bounded number of bits between measurements must compress each exact real label into a state update, and the question is how many measurements this costs for a prescribed angular accuracy $\epsilon$. Exact labels make the question delicate: a real label has no built-in bit precision, so noise-based arguments do not apply.

This preprint attacks the question through a conditional information bound for a single block of observations: how much information about $s$ can a finite message formed from $k$ exact Gaussian measurements carry, beyond what an independent Gaussian projection of $s$ (revealed only to the analyst) already reveals? Iterating such a block bound over a stream gives a memory–sample lower bound.

Timeline

• 1960. Watanabe introduces total correlation as a measure of multivariate dependence; Austin (2020) develops its chain rules on general probability spaces.
• 2015. Steinhardt and Duchi prove memory and communication lower bounds for noisy sparse linear regression.
• 2016–2017. Raz proves that learning parities requires quadratic memory or exponentially many samples, and extends the branching-program method to a large class of finite learning problems.
• 2019. Sharan, Sidford and Valiant prove an $\Omega(d\log r)$ sample lower bound for Gaussian regression with tiny uniform noise, at most $d^2/4$ bits and Euclidean accuracy $d^{-r}$, in a stated range of $r$. Dagan, Kur and Shamir prove quadratic-space lower bounds for two other linear-prediction tasks.
• 2026. Two companion OpenAI preprints treat exact observations: Memory and precision in noiseless Gaussian regression (memory $Ad^2$, backward propagation of success bounds) and Replacing Gaussian observations in memory-constrained inference. The present OpenAI preprint, Posterior replicas and conditional information in Gaussian regression (dated September 27, 2026), gives multi-replica block bounds and derives the $o(d^2)$-memory consequence. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

Let $\sigma_d$ be uniform probability on $S^{d-1}$. In a block experiment the signal $S$ has law $p = f\sigma_d$ with a Borel density $0 \le f \le L$. Independently draw a $k\times d$ standard Gaussian matrix $A$ and observe $(A, AS)$. A message $W$ with values in a finite set is drawn from a measurable Markov kernel of $(A, AS)$. Finally an $\ell \times d$ standard Gaussian matrix $B$ is drawn independently of everything. The quantity of interest is the conditional mutual information

$$I(S; W \mid B, BS),$$

in nats, and $H(W)$ denotes the Shannon entropy of the message.

A finite-state learner with $M$ bits reads pairs $(X_j, Y_j)$ once, in order, keeps a state in a set of size $2^M$, may stop at any index up to a deterministic horizon $T$, and outputs a unit vector from its terminal state, stopping index and fresh randomness only. Transitions and stopping may be arbitrary measurable randomized rules of the current state and current pair; shared randomness is independent of the signal and samples.

In Lean (OAI.PosteriorReplicas), sphereLaw d is normalized surface measure, gaussianRows d k is the product of stdGaussian, signalMessageLaw p κ is the law of $(S, W)$, sideLaw ℓ appends $(B, BS)$, conditionalInformation is the relative entropy of the joint law from the conditionally independent coupling, and messageEntropy is $H(W)$. Learners are CompletedKernelLearner d M with Markov-kernel transitions on the completed observation space, wrapped in a JointKernelExperiment over a seed space $(\Omega, \rho)$.

Formalization targets

Goal: OAI.PosteriorReplicas.source_main

The goal is the conjunction of the paper's principal statements:

• Theorem 1.1 (Gaussian replica block bound). For large $d$, with $k = 2\lfloor d/16\rfloor$, $t = k+1$, $\ell = 4k$, there is an absolute $C$ with

$$I(S; W \mid B, BS) \le \frac{H(W)}{t} + Cd + C\log(2 + \log L),$$

uniformly over the prior, $L$, and the message kernel.

• Theorem 1.2 (Uniform-prior sample lower bound). There is an absolute $c > 0$ such that for every $M(d) = o(d^2)$, eventually in $d$, every learner with uniform-prior success $\Pr\{\arccos\langle \hat S, S\rangle \le \epsilon\} \ge 2/3$, $0 < \epsilon \le 1/10$, has $T \ge c\,d\log(1/\epsilon)$.
• Theorem 3.3 (the finite equal-label measure identity) and the accompanying density-version statement for projected laws.
• The alternative block comparisons: Theorem 5.1 (distance bins), Proposition 7.5 (Haar frames), Proposition 8.1 (synthetic Gaussian route) and Proposition 9.1 (Stiefel incidence).

Significance

The result. Theorem 1.2 shows that with $o(d^2)$ persistent bits, the $d\log(1/\epsilon)$ sample scale of real-valued Kaczmarz-type methods cannot be improved for exact Gaussian measurements, under the uniform prior and with an absolute constant. Theorem 1.1 is a reusable statement in its own right: the entropy of a message is divided by a factor proportional to $d$, and the dependence on the prior density bound $L$ is only doubly logarithmic, which is what allows conditioning on rare learner states.

Formalizing it. These results appear only in an unrefereed preprint, and none has a machine-checked proof. The companion preprint Memory and precision in noiseless Gaussian regression proves a related statement for memory $Ad^2$ by a different method; the two missions share the learner model but not the block estimates. Formalizing the goal requires conditional mutual information for general (non-discrete) random variables and the exact equal-label geometry, both of which would be reusable.

Difficulty

Conditioning on one exact observation confines the signal to a lower-dimensional section of the sphere, so posterior densities with respect to $\sigma_d$ do not exist and density-based arguments fail. Bounding the information in the message by $H(W)$ alone is far too weak: a message of $d^2$ bits could then carry all relevant information. The block bound must instead account for what the analyst's independent projection already reveals, uniformly over priors with large density bounds $L$, since rare learner states produce such priors.

Formalization scope

• Vectors are EuclideanSpace ℝ (Fin d); priors are measures on the ambient space given as (sphereLaw d).withDensity f with $0 \le f \le L$.
• Messages are Markov kernels into Fin N with NeZero N; information quantities are ℝ≥0∞-valued relative entropies (klDiv), entropies use natural logarithms.
• Row counts are natural-number floors such as 2 * (d / 16), d / 8, d / 2 as in the paper.
• The streaming conjunct quantifies over all memory sequences with IsLittleO atTop M (d^2), all horizons $T$, all $0 < \epsilon \le 1/10$, all seed spaces and all JointKernelExperiments whose output kernel agrees almost surely with the run of the per-seed learner.

The goal cannot be met vacuously: block bounds are stated for every finite message kernel, and the streaming hypothesis (success at least $2/3$) is satisfiable by learners with large $T$.

A complete development needs Gaussian matrices and their projections, coarea-type identities for equal labels, conditional kernels (condKernel), relative entropy chain rules, and spherical measure estimates. Contributions that isolate one conjunct (for example Theorem 3.3 or Theorem 1.1) are welcome.

Selected references

• OpenAI, Posterior replicas and conditional information in Gaussian regression, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Posterior-replicas-and-conditional-information-in-Gaussian-regression-September-27-2026/paper.pdf
• OpenAI, Memory and precision in noiseless Gaussian regression, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/main/preprints/Memory-and-precision-in-noiseless-Gaussian-regression-September-27-2026/paper.pdf
• V. Sharan, A. Sidford, G. Valiant, Memory-Sample Tradeoffs for Linear Regression with Small Error, STOC 2019. https://doi.org/10.1145/3313276.3316403
• R. Raz, Fast Learning Requires Good Memory: A Time-Space Lower Bound for Parity Learning, 2016. https://arxiv.org/abs/1602.05161
• R. Raz, A Time-Space Lower Bound for a Large Class of Learning Problems, FOCS 2017. https://doi.org/10.1109/FOCS.2017.73
• J. Steinhardt, J. Duchi, Minimax Rates for Memory-Bounded Sparse Linear Regression, COLT 2015. https://proceedings.mlr.press/v40/Steinhardt15.html
• Y. Dagan, G. Kur, O. Shamir, Space Lower Bounds for Linear Prediction in the Streaming Model, COLT 2019. https://proceedings.mlr.press/v99/dagan19b.html
• S. Watanabe, Information Theoretical Analysis of Multivariate Correlation, IBM J. Res. Dev., 1960.
• T. Austin, Multi-variate correlation and mixtures of product measures, Kybernetika, 2020.

Motivation

Network data often come as a single observed graph, and the simplest summary of a graph is its degree sequence, the list of the numbers of neighbours of its vertices. A statistical model in which the degree sequence is a sufficient statistic is an exponential family on graphs, and the simplest such family is the β-model: each vertex $i$ carries a parameter $\beta_i$, and edges appear independently with log-odds $\beta_i+\beta_j$. The model appears in the directed case in Holland and Leinhardt (1981), in the undirected case in Park and Newman (2004) and Blitzstein and Diaconis (2011), and it is a close relative of the Bradley–Terry model for paired comparisons.

Fitting the model means solving the maximum likelihood equations. The difficulty for classical theory is that the number of parameters, $n$, equals the number of vertices: the parameter dimension grows with the sample, and standard consistency arguments for maximum likelihood do not apply. Chatterjee, Diaconis and Sly (2011) prove that, nevertheless, for parameters in a fixed bounded range the maximum likelihood estimate exists, is unique, and estimates every coordinate of $\beta$ uniformly at rate $\sqrt{\log n/n}$, with probability $1-O(n^{-2})$. This mission formalizes that result (Theorem 1.3 of the paper) and the lemmas of §4 on which its proof rests.

Setting

Let $n\ge 1$ and $\beta=(\beta_1,\dots,\beta_n)\in\mathbb R^n$. The β-model $\mathbb P_\beta$ is the law of the random simple graph $G$ on vertices $1,\dots,n$ in which, for each pair $i\ne j$, the edge $\{i,j\}$ is present with probability

$$p_{ij}=\frac{e^{\beta_i+\beta_j}}{1+e^{\beta_i+\beta_j}},$$

independently of all other edges. Write $d_1,\dots,d_n$ for the degrees of $G$. The maximum likelihood equations for an estimate $\hat\beta\in\mathbb R^n$ are

$$d_i=\sum_{j\ne i}\frac{e^{\hat\beta_i+\hat\beta_j}}{1+e^{\hat\beta_i+\hat\beta_j}},\qquad i=1,\dots,n. \tag{3}$$

The sup norm is $|x|_\infty=\max_i|x_i|$.

Two further objects enter the proof. $\mathcal D$ is the set of degree sequences of simple graphs on $n$ vertices and $\mathcal R$ the set of expected degree sequences of $\mathbb P_\beta$ as $\beta$ ranges over $\mathbb R^n$. For $d\in\mathbb R^n$ and $B\subseteq\{1,\dots,n\}$ the slack is

$$g(d,B)=\sum_{j\notin B}\min\{d_j,|B|\}+|B|(|B|-1)-\sum_{i\in B}d_i,$$

which is nonnegative for every degree sequence of a graph (the Erdős–Gallai inequalities). Finally $\varphi:\mathbb R^n\to\mathbb R^n$, $\varphi_i(x)=\log d_i-\log\sum_{j\ne i}(e^{-x_j}+e^{x_i})^{-1}$, is the map whose fixed points are the solutions of (3).

Formalization targets

Goal: Theorem 1.3

For every $L\ge 0$ there is $C(L)>0$ such that for every $n\ge 1$ and every $\beta$ with $|\beta_i|\le L$,

$$\mathbb P_\beta\Big(\exists!\,\hat\beta \text{ solving (3)},\ \ |\hat\beta-\beta|_\infty\le C(L)\sqrt{\tfrac{\log n}{n}}\Big)\ \ge\ 1-C(L)\,n^{-2}.$$

The constant depends only on $L$, and the statement holds for all $n$, small $n$ being absorbed into $C(L)$.

Milestones, in the order the proof uses them

1. The probability formula $\mathbb P_\beta(G)=e^{\sum_i\beta_id_i}/\prod_{i<j}(1+e^{\beta_i+\beta_j})$ (p. 6), with $\mathbb P_\beta$ a probability measure.
2. Theorem 1.4: $\mathrm{conv}(\mathcal D)=\overline{\mathcal R}$.
3. Lemma 4.1: if $d\in\overline{\mathcal R}$, $c_2(n-1)\le d_i\le c_1(n-1)$, and $g(d,B)\ge c_3n^2$ whenever $|B|\ge c_2^2n$, then (3) has a solution with $|\hat\beta|_\infty\le c_4(c_1,c_2,c_3)$.
4. Lemma 4.2: with probability $\ge1-2n^{-2}$ the observed degrees satisfy $c_2(n-1)\le d_i\le c_1(n-1)$ and $g(d,B)\ge(c_3-\sqrt{6\log n/n})n^2$ for $|B|\ge cn$.
5. Theorem 1.5: uniqueness of the solution of (3) and the a-priori bound $|x_0-\hat\beta|_\infty\le C|x_0-\varphi(x_0)|_\infty$.
6. The identity $(\beta-\varphi(\beta))_i=\log(\bar d_i/d_i)$, with $\bar d_i$ the expected degree of vertex $i$ (p. 21).

Significance

The theorem is a consistency result in a regime where the number of parameters is as large as the number of nodes, and it comes with a uniform rate: every vertex parameter is recovered to accuracy $O(\sqrt{\log n/n})$ simultaneously, from one graph. Existence of the MLE is itself not automatic (it fails, for instance, whenever the observed graph has an isolated vertex), so the theorem also says that the estimator is defined with high probability. The paper uses the same machinery for its graph-limit results on uniform random graphs with a given degree sequence (missions 4–5 of this series), and the β-model is the base case of a large family of exponential random graph models used in network analysis.

The result is proved in the paper; this mission produces the machine-checked version. None of the statements here is formalized on the platform or in Mathlib. Theorems 1.4 and 1.5 are the goals of missions 2 and 1 of this series and are restated here; a proof there transfers directly.

Difficulty

Standard maximum likelihood asymptotics fix the parameter dimension and let the sample size grow; here both grow together, and the ratio of squared dimension to number of observations, $n^2/\binom n2$, stays bounded, so the usual heuristic for when asymptotics apply is borderline at best. The likelihood is concave, but concavity alone gives neither existence of a maximizer (the supremum may be approached at $\beta_i=\pm\infty$) nor a bound on its size that is uniform in $n$. The central step, Lemma 4.1, is a deterministic bound on $|\hat\beta|_\infty$ that does not depend on $n$; it requires control of how the coordinates of $\hat\beta$ can spread out, expressed through a quantitative Erdős–Gallai margin. A coordinatewise argument cannot give it, because each equation of (3) involves all coordinates.

Formalization scope

Vertices are Fin n, graphs are SimpleGraph (Fin n) with the discrete σ-algebra, and $\mathbb P_\beta$ is the finite sum of point masses with the independent-edge weights $\prod_{i<j}p_{ij}^{\mathbf 1[ij\in G]}(1-p_{ij})^{\mathbf 1[ij\notin G]}$; vectors are Fin n → ℝ with Mathlib's sup norm. Probabilities are values of this measure in $[0,\infty]$, compared with $\max(0,1-Cn^{-2})$. Expected degrees are integrals against $\mathbb P_\beta$; $\mathcal R$ is not defined as the range of the right-hand side of (3), since that identification is part of the content of Theorem 1.4.

Every "constant depending only on …" is a quantifier placed before $n$: in Theorem 1.3, $C$ depends on $L$ only; in Lemma 4.1, $c_4$ is a function of $(c_1,c_2,c_3)$ alone, bounded on compact subsets of its domain, as §4 defines the phrase; in Lemma 4.2, $(C,c_1,c_2)$ on $L$ and $c_3$ on $(L,c)$. Choosing $C$ after $n$ and $\beta$ would make Theorem 1.3 trivial, since $1-Cn^{-2}<0$ for large $C$; this formalization rules that out. The paper's $L:=\max_i|\beta_i|$ is the hypothesis $|\beta_i|\le L$, and the paper's $\frac1{n^2}\inf_{B}\{\cdots\}\ge c_3$ is the bound $g(d,B)\ge c_3n^2$ for every admissible $B$ (a finite nonempty family). The phrase "there exists a unique solution $\hat\beta$ … that satisfies [the bound]" is read as: a solution exists, it is unique, and it satisfies the bound. Lemma 4.1 assumes $d\in\overline{\mathcal R}$, not $d\in\mathcal R$ (for $d\in\mathcal R$ existence would be immediate). Theorem 1.5 is stated, as in mission 1, for $n\ge3$ and $d_i>0$.

A complete development needs: the β-model as a measure and its exponential-family formula; Hoeffding's inequality for sums of independent non-identical indicators transported to $\mathbb P_\beta$ (Mathlib has Hoeffding for independent bounded variables); compactness in $\mathbb R^n$; and the results of missions 1 and 2. The β-model measure and the Erdős–Gallai slack are reusable beyond this mission. Proofs of any milestone, and of the transfer between the independent-edge and the product-space descriptions of $\mathbb P_\beta$, are welcome.

Selected references

• S. Chatterjee, P. Diaconis, A. Sly, Random graphs with a given degree sequence, Ann. Appl. Probab. 21(4), 1400–1435, 2011. arXiv:1005.1136v5. https://arxiv.org/abs/1005.1136 — https://doi.org/10.1214/10-AAP728
• P. W. Holland, S. Leinhardt, An exponential family of probability distributions for directed graphs, J. Amer. Statist. Assoc. 76, 33–50, 1981. https://doi.org/10.1080/01621459.1981.10477598
• J. Park, M. E. J. Newman, Statistical mechanics of networks, Phys. Rev. E 70, 066117, 2004. https://arxiv.org/abs/cond-mat/0405566
• J. Blitzstein, P. Diaconis, A sequential importance sampling algorithm for generating random graphs with prescribed degrees, Internet Math. 6(4), 489–522, 2011. https://doi.org/10.1080/15427951.2010.557277
• W. Hoeffding, Probability inequalities for sums of bounded random variables, J. Amer. Statist. Assoc. 58, 13–30, 1963. https://doi.org/10.1080/01621459.1963.10500830

Motivation

A degree sequence records how many neighbours each vertex of a graph has. In network statistics it is often the only summary of a graph that is observed or trusted, and the natural probability models for graphs in which "the degree sequence captures the information" are exponential families whose sufficient statistic is the degree sequence. Chatterjee, Diaconis and Sly (arXiv:1005.1136, Ann. Appl. Probab. 2011) call the resulting model the β-model and study its maximum likelihood theory and its use for sampling random graphs with a prescribed degree sequence.

For any exponential family, the first question about estimation is which values of the sufficient statistic can be matched by a parameter: the maximum likelihood equations say exactly "the expected statistic equals the observed one". Theorem 1.4 of the paper answers this for the β-model. Up to taking a closure, the expected degree sequences of the β-model fill the whole convex hull of the degree sequences. The paper notes that the result can also be derived from classical results on the mean space of exponential families (Barndorff-Nielsen 1978; Brown 1986; Wainwright and Jordan 2008, Theorem 3.3), and gives a self-contained proof in §3. Lemma 4.1 of the same paper uses Theorem 1.4 to show that the maximum likelihood estimator exists.

Setting

Fix $n\ge 0$ and the vertex set $\{1,\dots,n\}$. A graph $G$ is undirected and simple: no loops and no multiple edges. Its degree sequence is $d(G)=(d_1,\dots,d_n)\in\mathbb R^n$, and

$$\mathcal D=\{d(G):\ G\text{ a simple graph on }n\text{ vertices}\}$$

is the finite set of all degree sequences. Its convex hull $\operatorname{conv}(\mathcal D)$ is a polytope in $\mathbb R^n$.

For $\beta\in\mathbb R^n$, the β-model $\mathbb P_\beta$ is the law of the random graph in which each pair $\{i,j\}$, $i\neq j$, is an edge with probability

$$p_{ij}=\frac{e^{\beta_i+\beta_j}}{1+e^{\beta_i+\beta_j}},$$

independently of all other pairs. The expected degree sequences form the set

$$\mathcal R=\big\{\big(\mathbb E_\beta[d_1],\dots,\mathbb E_\beta[d_n]\big):\ \beta\in\mathbb R^n\big\}.$$

Two functions on $\mathbb R^n$ appear in the proof. The first is $g=(g_1,\dots,g_n)$ with

$$g_i(x)=\sum_{j\neq i}\frac{e^{x_i+x_j}}{1+e^{x_i+x_j}}.$$

The second is, for each $y\in\mathbb R^n$,

$$f_y(x)=\sum_{i=1}^n x_iy_i-\log\prod_{1\le i<j\le n}\big(1+e^{x_i+x_j}\big).$$

The Lean development names these objects betaModel, D, R, g and fy in the namespace GivenDegreeSeq.MeanPolytope.

Formalization targets

Goal: Theorem 1.4 (p. 8)

$$\operatorname{conv}(\mathcal D)=\overline{\mathcal R}\qquad\text{for every }n.$$

The statement fixes no constants. The closure cannot be dropped: for $n\ge2$ the degree sequence $0$ of the empty graph lies in $\mathcal D$ but not in $\mathcal R$, because every expected degree is positive.

Milestones, in the order the proof uses them

1. The probability formula (p. 6): $\mathbb P_\beta$ is a probability measure, and

$$\mathbb P_\beta(\{G\})=\frac{e^{\sum_i\beta_id_i}}{\prod_{i<j}(1+e^{\beta_i+\beta_j})}.$$

2. Expected degrees (p. 15): $\mathbb E_x[d_i]=g_i(x)$, so $\mathcal R=g(\mathbb R^n)$.
3. The easy inclusion (p. 15): $\overline{\mathcal R}\subseteq\operatorname{conv}(\mathcal D)$.
4. A uniform bound (p. 16): $f_y(x)\le 0$ for all $y\in\operatorname{conv}(\mathcal D)$ and $x\in\mathbb R^n$.
5. Smoothness (p. 16): $f_y$ is twice differentiable and $\nabla^2 f_y$ is uniformly bounded.
6. Lemma 3.1 (pp. 14–15): if $f$ is twice differentiable, $M=\sup f<\infty$ and $\|\nabla^2 f\|_{\mathrm{op}}\le C$, then

$$|\nabla f(x)|^2\le 2C\big(M-f(x)\big),$$

and $\nabla f(x_k)\to0$ along some sequence. 7. The gradient (p. 16): $\nabla f_y(x)=y-g(x)$.

Significance

The theorem describes the mean space of the β-model. Its interior contains every degree sequence that lies strictly inside the polytope, and for these sequences maximum likelihood estimation is well posed. The paper's consistency result (Theorem 1.3) and the existence part of Lemma 4.1 start from this description. The polytope $\operatorname{conv}(\mathcal D)$ is studied in its own right; its extreme points are the degree sequences of threshold graphs (Mahadev and Peled 1995).

Theorem 1.4 is proved, and as far as this mission's authors know it is not machine-checked anywhere. Formalizing it means turning the paper's short proof into a complete argument. That includes the steps the page dismisses as easy: the exponential-family formula for the independent-edge law, the expectation computation, the Hessian bound for $f_y$, and the passage from a sequence of approximate critical points to the closure. Lemma 3.1, a descent-type gradient bound for a function bounded above, is a general fact of real analysis and is independent of graphs.

Difficulty

The inclusion $\overline{\mathcal R}\subseteq\operatorname{conv}(\mathcal D)$ is direct: an expectation is an average. The reverse inclusion is the content. For $y$ in the interior of the polytope, one would like to find $x$ with $g(x)=y$ by maximizing the concave function $f_y$. For $y$ on the boundary of the polytope, however, $f_y$ need not attain its supremum. So the argument cannot rely on the existence of a maximizer, and it has to produce points $x_k$ with $g(x_k)\to y$ without ever solving $g(x)=y$. Compactness arguments on $\beta$ fail for the same reason: the relevant sequences $x_k$ are unbounded.

Formalization scope

• Graphs and measure. Vertices are Fin n, so the paper's vertex $i$ is the index $i-1$. Graphs are SimpleGraph (Fin n), a finite type. Its σ-algebra is Mathlib's SimpleGraph.instMeasurableSpace, under which every set of graphs on Fin n is measurable.
• The law and its expectations. $\mathbb P_\beta$ is the finite sum of Dirac masses weighted by the independent-edge product over pairs $i<j$. $\mathcal R$ is defined through Bochner expectations under $\mathbb P_\beta$, not as the range of $g$. Defining $\mathcal R$ as $g(\mathbb R^n)$ would erase the link to the probability model and is ruled out.
• Vector spaces. $\mathcal D$ and $\mathcal R$ are subsets of Fin n → ℝ, whose product topology is the Euclidean topology, so the closure is unambiguous. Gradients and Hessians are taken on EuclideanSpace ℝ (Fin n). There "twice differentiable" means that $f$ and its Fréchet derivative are differentiable, and the Hessian norm is the norm of the second Fréchet derivative, which equals the $L^2$ operator norm of the Hessian matrix.
• No size hypothesis. The goal holds for every $n$; for $n\le1$ both sides are $\{0\}$.
• Readings of the page.
  • On p. 15 the paper prints $\log\sum_{1\le i<j\le n}(1+e^{x_i+x_j})$ in $f_y$. The formalization uses $\log\prod$, the only reading under which "taking logs, we get $f_d(x)\le0$" and $\nabla f_y=y-g$ hold. The milestone text keeps the printed version.
  • The "Lemma 11" of p. 16 is Lemma 3.1.
  • The probability-measure property of $\mathbb P_\beta$ is stated as a conjunct of milestone 1.
  • The differentiability of $f_y$ is stated alongside the Hessian bound in milestone 5.

Contributions of any milestone are welcome. Lemma 3.1 and the gradient identity are self-contained calculus. The probability formula and the expected-degree identity are finite computations on graphs.

Selected references

• S. Chatterjee, P. Diaconis, A. Sly, Random graphs with a given degree sequence, Ann. Appl. Probab. 21(4) (2011), 1400–1435. https://arxiv.org/abs/1005.1136 (v5), https://doi.org/10.1214/10-AAP728
• O. Barndorff-Nielsen, Information and Exponential Families in Statistical Theory, Wiley, Chichester, 1978. MR0489333, https://mathscinet.ams.org/mathscinet-getitem?mr=0489333
• L. D. Brown, Fundamentals of Statistical Exponential Families with Applications in Statistical Decision Theory, IMS Lecture Notes–Monograph Series 9, 1986. MR0882001, https://mathscinet.ams.org/mathscinet-getitem?mr=0882001
• M. J. Wainwright, M. I. Jordan, Graphical models, exponential families, and variational inference, Found. Trends Mach. Learn. 1 (2008), 1–305. https://doi.org/10.1561/2200000001
• N. V. R. Mahadev, U. N. Peled, Threshold Graphs and Related Topics, Ann. Discrete Math. 56, North-Holland, 1995. MR1417258, https://mathscinet.ams.org/mathscinet-getitem?mr=1417258

Motivation

The $\beta$-model is the simplest exponential random graph model in which every vertex has its own parameter. It was studied by Holland and Leinhardt (1981) in the directed case and by Park and Newman (2004) and Blitzstein and Diaconis (2011) in the undirected case, and it is a close relative of the Bradley–Terry model for paired comparisons. Its sufficient statistic is the degree sequence of the observed graph, so fitting the model to data means solving a system of $n$ nonlinear equations in $n$ unknowns, one per vertex, where $n$ can be in the thousands.

Chatterjee, Diaconis and Sly (arXiv:1005.1136, Ann. Appl. Probab. 21 (2011)) give a simple iteration for this system and prove that it converges geometrically fast whenever a solution exists, at a rate that does not deteriorate with the number of vertices, and that it detects when no solution exists. The same estimate is then used in the paper's consistency theorem for the maximum likelihood estimator (Theorem 1.3) and in its graph-limit theorem (Theorem 1.1). This mission formalizes that algorithmic result, Theorem 1.5, together with the chain of numbered displays in Section 2 that proves it.

Setting

Let $n\ge 3$ and label the vertices $1,\dots,n$. For $\beta=(\beta_1,\dots,\beta_n)\in\mathbb R^n$, the $\beta$-model puts an edge between distinct vertices $i$ and $j$ independently with probability

$$p_{ij}(\beta)=\frac{e^{\beta_i+\beta_j}}{1+e^{\beta_i+\beta_j}}.$$

Given an observed graph with degrees $d_1,\dots,d_n$, the maximum likelihood estimate $\hat\beta$ must satisfy the ML equations

$$d_i=\sum_{j\ne i}\frac{e^{\hat\beta_i+\hat\beta_j}}{1+e^{\hat\beta_i+\hat\beta_j}},\qquad i=1,\dots,n.\tag{3}$$

The sup norm of $x\in\mathbb R^n$ is $|x|_\infty=\max_i|x_i|$. For $i\ne j$ put $r_{ij}(x)=1/(e^{-x_j}+e^{x_i})$, and define the map $\varphi:\mathbb R^n\to\mathbb R^n$ by

$$\varphi_i(x)=\log d_i-\log\sum_{j\ne i}r_{ij}(x).$$

Starting from any $x_0\in\mathbb R^n$, the fixed-point iteration is $x_{k+1}=\varphi(x_k)$. The fixed points of $\varphi$ are exactly the solutions of (3).

For an $n\times n$ matrix $A=(a_{ij})$, the $L^\infty$ operator norm is $|A|_\infty=\max_i\sum_j|a_{ij}|$. For $\delta>0$, the class $\mathcal L_n(\delta)$ consists of the matrices with $|A|_\infty\le 1$, $a_{ii}\ge\delta$ and $a_{ij}\le-\delta/(n-1)$ for $i\ne j$. For $x,y\in\mathbb R^n$, $J(x,y)$ is the matrix with entries $J_{ij}(x,y)=\int_0^1\frac{\partial\varphi_i}{\partial x_j}(tx+(1-t)y)\,dt$.

Formalization targets

Goal: Theorem 1.5

There are functions $\Theta(a,b)\in[0,1)$ and $C(a,b)$, $C$ continuous, independent of $n$ and $d$, such that for every $n\ge3$ and every $d\in(0,\infty)^n$: if (3) has a solution $\hat\beta$, then $\hat\beta=\varphi(\hat\beta)$, it is the unique solution of (3), and for all $x_0$ and $k$

$$|x_k-\hat\beta|_\infty\le\Theta(|\hat\beta|_\infty,|x_0|_\infty)^{\lfloor k/2\rfloor}|x_0-\hat\beta|_\infty,\qquad |x_0-\hat\beta|_\infty\le C(|\hat\beta|_\infty,|x_0|_\infty)\,|x_0-x_1|_\infty;$$

and if (3) has no solution, then every orbit $\{x_k\}$ is unbounded.

Milestones, in the order the proof uses them

1. p. 9: $\varphi(x)=x$ if and only if $x$ solves (3).
2. (6)–(7), p. 12: on $|x|_\infty\le K$, $-\frac{e^{2K}}{n-1}\le\frac{\partial\varphi_i}{\partial x_j}\le-\frac{e^{-4K}}{2(n-1)}$ for $i\ne j$, and $\frac12e^{-4K}\le\frac{\partial\varphi_i}{\partial x_i}\le e^{2K}$.
3. (8), pp. 12–13: $\varphi(x)-\varphi(y)=J(x,y)(x-y)$; off-diagonal partials are negative, diagonal ones positive, and every row of the Jacobian has absolute sum $1$.
4. Lemma 2.1, p. 11: for $A,B\in\mathcal L_n(\delta)$,

$$|AB|_\infty\le 1-\frac{2(n-2)\delta^2}{n-1}.$$

5. (9), p. 13: with $K$ the largest of $|x|_\infty,|y|_\infty,|\varphi(x)|_\infty,|\varphi(y)|_\infty$ and $\delta=\frac12e^{-4K}$,

$$|\varphi(\varphi(x))-\varphi(\varphi(y))|_\infty\le\Big(1-\frac{2(n-2)\delta^2}{n-1}\Big)|x-y|_\infty,$$

and $|\varphi(x)-\varphi(y)|_\infty\le|x-y|_\infty$. 6. (10), p. 13: a single $\theta=\Theta(|\hat\beta|_\infty,|x_0|_\infty)\in[0,1)$, continuous in its arguments, with $|x_{k+3}-x_{k+2}|_\infty\le\theta|x_{k+1}-x_k|_\infty$ and $|x_{k+2}-\hat\beta|_\infty\le\theta|x_k-\hat\beta|_\infty$.

Significance

The theorem turns an implicit statistical object, the MLE of an $n$-parameter model, into the limit of an explicit iteration with three guarantees: a convergence rate that depends on the size of the parameters but not on $n$; an a posteriori error bound in terms of the computable step $|x_0-x_1|_\infty$; and a certificate of non-existence. The uniqueness of the MLE comes out of the same estimate. In the paper, the a priori bound $|x_0-\hat\beta|_\infty\le C|x_0-x_1|_\infty$ is the device that proves consistency of the MLE (Theorem 1.3, applied with $x_0=\beta$), and the two-step contraction is reused in the proof of the graph-limit theorem.

The result is proved in the paper; no machine-checked proof of it is known. The work here is to formalize the known proof. The matrix inequality of Lemma 2.1 and the derivative bounds (6)–(7) are self-contained and can be attacked independently of the iteration.

Difficulty

The obvious approach is to show that $\varphi$ is a contraction and apply Banach's fixed-point theorem. This fails: every row of the Jacobian of $\varphi$ has absolute sum exactly $1$, so $\varphi$ is only non-expansive in the sup norm, never strictly contracting. Contraction appears only for the two-step map $\varphi\circ\varphi$, through the sign pattern of the Jacobian (positive diagonal, uniformly negative off-diagonal), and only on bounded sets, with a factor that tends to $1$ as the norms grow. A second difficulty is uniformity: the factor must be bounded away from $1$ independently of $n$, which needs $(n-2)/(n-1)\ge\frac12$, hence $n\ge3$. For the converse, there is no fixed point to anchor the orbit, so boundedness of the orbit has to be converted into convergence before a fixed point exists.

Formalization scope

• Vertices are Fin n $=\{0,\dots,n-1\}$; vectors are Fin n → ℝ, whose Mathlib norm is the sup norm $|x|_\infty$. Matrix norms are the explicit maximal absolute row sum.
• The degrees $d_i$ are arbitrary positive reals. This is a generalization of the page (degrees of a graph), and it is all the proof uses; positivity is required because $\log d_i$ is junk in Lean at $0$.
• $n\ge3$ is a hypothesis of the goal and of (10). It is not on the page but is necessary: for $n=2$, (3) reads $d_1=d_2=p_{12}$, whose solutions form a line, so uniqueness fails, and the factor in Lemma 2.1 equals $1$.
• Partial derivatives are Fréchet derivatives applied to unit vectors; $J(x,y)$ uses the interval integral over $[0,1]$.
• "Geometrically fast, with rate depending only on $(|\hat\beta|_\infty,|x_0|_\infty)$" is stated with the function $\Theta$ quantified before $n$, $d$, $\hat\beta$ and $x_0$, and "$C$ is a continuous function of the pair" likewise. A version that chooses the rate after fixing $n$, $d$ and $x_0$ is strictly weaker and nearly says only that a convergent sequence converges; it is not the target.
• "A divergent subsequence" is stated as unboundedness of $\{|x_k|_\infty\}$, which is equivalent for sequences in $\mathbb R^n$.
• The paper's remark that $\theta$ is "uniformly bounded away from 1 on subsets of $\mathbb R^n\times\mathbb R^n$" holds only on bounded subsets; it is not stated separately, and its quantitative content is (10).

Needed infrastructure: calculus of $\varphi$ (derivatives of $\log$ of a sum of exponentials), the integral form of the mean value theorem for maps $\mathbb R^n\to\mathbb R^n$, and elementary matrix-norm estimates. The class $\mathcal L_n(\delta)$ and Lemma 2.1 are reusable for other diagonally dominant iterations. Proofs of any milestone are welcome, in any order.

Selected references

• S. Chatterjee, P. Diaconis and A. Sly, Random graphs with a given degree sequence, Ann. Appl. Probab. 21(4), 1400–1435, 2011. arXiv:1005.1136v5, DOI 10.1214/10-AAP728
• P. W. Holland and S. Leinhardt, An exponential family of probability distributions for directed graphs, J. Amer. Statist. Assoc. 76, 33–65, 1981. DOI 10.1080/01621459.1981.10477598
• J. Park and M. E. J. Newman, Statistical mechanics of networks, Phys. Rev. E 70, 066117, 2004. arXiv:cond-mat/0405566
• J. Blitzstein and P. Diaconis, A sequential importance sampling algorithm for generating random graphs with prescribed degrees, Internet Mathematics 6(4), 489–522, 2011. DOI 10.1080/15427951.2010.557277

Motivation

The Lasso fits a linear model by least-norm regression with an $\ell^1$ penalty, and its most used property is that it returns sparse coefficient vectors: many features receive weight exactly zero. Most sparsity guarantees for the Lasso are statistical. They assume a generative model and an incoherence or irrepresentability condition on the design, and conclude that the support is recovered (Tropp 2006; Zhao and Yu 2006).

Xu, Caramanis and Mannor (arXiv:0811.1790v1, 2008; IEEE Trans. Inf. Theory 56(7), 2010) show that the Lasso's $\ell^1$-regularized regression problem is exactly a robust regression problem in which each feature column is perturbed independently within a norm ball (their Theorem 1; mission 1 of this series). Section IV of the paper uses this robust view to give a sparsity criterion that needs no generative model: a feature gets zero weight if some allowable perturbation makes it irrelevant. This mission formalizes that criterion, Theorem 5, together with the more general Theorem 5′ it specializes, and the geometric consequence Theorem 6.

Setting

Fix integers $n, m$. The data are the features $a_1,\dots,a_m \in \mathbb R^n$, the columns of a matrix $A$, and a response $b \in \mathbb R^n$. For $x\in\mathbb R^m$, $Ax = \sum_i x_i a_i$. A disturbance $\Delta A = (\delta_1,\dots,\delta_m)$ perturbs column $i$ to $a_i + \delta_i$.

Given radii $c_1,\dots,c_m \ge 0$, the feature-wise uncoupled uncertainty set is

$$\mathcal U = \{(\delta_1,\dots,\delta_m) \mid \|\delta_i\|_2 \le c_i,\ i = 1,\dots,m\}.$$

For a set $\mathcal V$ of disturbances, the robust objective is

$$R_{A,\mathcal V}(x) = \max_{\Delta A\in\mathcal V}\|b - (A+\Delta A)x\|_2,$$

and the robust regression problem is $\min_{x\in\mathbb R^m} R_{A,\mathcal V}(x)$. It has a solution supported on $I \subseteq \{1,\dots,m\}$ if some minimizer $x^*$ has $x^*_j = 0$ for all $j \in I^c = \{1,\dots,m\}\setminus I$.

For a disturbance $\Delta A$, $\Delta A^I$ agrees with $\Delta A$ on the features in $I$ and is zero elsewhere, and $\mathcal U^I = \{\Delta A^I \mid \Delta A \in \mathcal U\}$. Given numbers $l_j$ for $j\notin I$, the enlarged set of Theorem 5′ is

$$\tilde{\mathcal U} = \{(\delta_1,\dots,\delta_m) \mid \|\delta_i\|_2 \le c_i,\ i \in I;\ \|\delta_j\|_2 \le c_j + l_j,\ j\notin I\}.$$

In Lean these are uncertaintySet c, restrictedSet c I, enlargedSet c l I, robustObjective a b V x, IsRobustSolution and HasSolutionSupportedOn, all in the namespace RobustRegLasso.Sparsity.

Formalization targets

Goal: Theorem 5 (p. 8)

If there is a disturbance $\Delta\tilde A^{I^c}\in\mathcal U$ that is zero on the features in $I$ and such that

$$\min_{x\in\mathbb R^m}\Big\{\max_{\Delta\tilde A^I\in\mathcal U^I}\|b-(A+\Delta\tilde A^{I^c}+\Delta\tilde A^I)x\|_2\Big\}$$

has a solution supported on $I$, then $\min_x R_{A,\mathcal U}(x)$ has a solution supported on $I$.

Milestones (proof order)

1. First display of the proof of Theorem 5′ (p. 9). If $x^*_j = 0$ off $I$ and $\tilde a_i = a_i$ on $I$, then $R_{A,\tilde{\mathcal U}}(x^*) = R_{A,\mathcal U}(x^*) = R_{\tilde A,\mathcal U}(x^*)$, and also $R_{\tilde A,\tilde{\mathcal U}}(x^*) = R_{A,\mathcal U}(x^*)$.
2. Second display of the proof of Theorem 5′ (p. 9). If $\|a_j-\tilde a_j\|_2 \le l_j$ off $I$ and $a_i = \tilde a_i$ on $I$, then $\{A+\Delta A \mid \Delta A\in\mathcal U\}\subseteq\{\tilde A+\Delta A\mid\Delta A\in\tilde{\mathcal U}\}$, hence $R_{\tilde A,\tilde{\mathcal U}} \ge R_{A,\mathcal U}$ pointwise.
3. Theorem 5′ (pp. 8–9). If $x^*$ minimizes $R_{A,\mathcal U}$ and $x^*_j = 0$ off $I$, then $x^*$ minimizes $R_{\tilde A,\tilde{\mathcal U}}$ for every $\tilde A$ with $\|\tilde a_j - a_j\|_2\le l_j$ off $I$ and $\tilde a_i = a_i$ on $I$.
4. Theorem 6, conclusion corrected (p. 10). With $c_i = c$ for all $i$: if every unit $v\in\operatorname{span}(\{a_i, i\in I\}\cup\{b\})$ has $v^\top a_j\le c$ for all $j\notin I$, then some optimal solution of $\min_x R_{A,\mathcal U}(x)$ vanishes off $I$.

Theorem 5 is Theorem 5′ applied to the perturbed matrix $A + \Delta\tilde A^{I^c}$ with radii $c_j = 0$ off $I$, $l_j = c_j$ and $\tilde A = A$.

Significance

The result separates sparsity from statistics. Theorem 5 asks only that the features outside $I$ can be made irrelevant by a perturbation within the uncertainty budget; it involves no noise model and no probability. Theorem 6 turns this into an incoherence-type condition: features that lie within $c$ of being orthogonal to the response and to the relevant features receive zero weight. Because the robust problem over $\mathcal U$ is the $\ell^1$-regularized regression $\min_x \|b-Ax\|_2 + \sum_i c_i|x_i|$ (Theorem 1), these are sparsity statements about that Lasso-type problem. The same argument gives the paper's further results on angular separation and nearly dependent features, which it defers to a companion report.

These results are proved in the paper; none of them has a machine-checked proof on Prove2Me or, to our knowledge, elsewhere. The mission formalizes the known proof. It also records a correction: Theorem 6 as printed claims that every optimal solution vanishes off $I$, which is false (a two-dimensional counterexample is in the milestone's statement); the proof gives existence of one such solution, and that is what is posed.

Difficulty

The proof of Theorem 5′ is short, and the work is in the bookkeeping. The obvious attempt treats "max" as a real supremum and compares values directly; it has to know that each uncertainty set is nonempty and that the residual is bounded on it, and the enlarged set $\tilde{\mathcal U}$ is nonempty only because $l_j \ge \|\tilde a_j - a_j\|_2 \ge 0$. The two equalities of the first display require reassigning the columns outside $I$ of a disturbance (to zero, or to a feasible value) without changing the residual at $x^*$, which works only because $x^*_j = 0$ there. The specialization of Theorem 5′ to Theorem 5 changes the radius vector and the base matrix at the same time, and needs $\mathcal U^I$ to coincide with the feature-wise set whose radii are $c_i$ on $I$ and $0$ off it. Theorem 6 additionally needs the equivalence of the robust problem with an $\ell^1$-regularized problem, an orthogonal projection onto a span, and the existence of a minimizer of a coercive (or, for $c = 0$, least-squares) objective.

Formalization scope

• Features are a family a : Fin m → EuclideanSpace ℝ (Fin n); a disturbance is δ : Fin m → EuclideanSpace ℝ (Fin n); $A+\Delta A$ is the family a + δ. Index sets are Finset (Fin m) (0-based). The loss is the $\ell^2$ norm, as stated in the paper (which remarks that any norm works).
• "max" over a set of disturbances is the supremum in EReal (⨆ δ ∈ V). With nonnegative radii every set used is nonempty and bounded, so the value is a finite, attained real number; no junk value of a real sSup can make a statement vacuous. "Optimal solution" means a minimizer of this objective over all of $\mathbb R^m$; existence of a minimizer is assumed where the paper assumes it (Theorem 5′) and concluded where the paper concludes it (Theorems 5, 6).
• Radii $c_i \ge 0$ are hypotheses (the paper's standing convention). $l_j \ge 0$ is not assumed: it follows from $\|\tilde a_j - a_j\|_2 \le l_j$.
• Corrected printed typos: $I\subseteq\{1,\dots,n\}$ on p. 8 is read with $m$; the inequality after "For an arbitrary $x'$" is posed with $A$ and $\tilde A$ exchanged, as the inclusion and the final display require; Theorem 6's "any optimal solution" becomes "some optimal solution", and "$I\subset$" becomes $I\subseteq$.
• The robust objective is the supremum over the set, never its closed form $\|b-Ax\|_2+\sum_i c_i|x_i|$; with that definition the problem would no longer be a robust problem and Theorems 5 and 5′ would be about a different function.
• The definitions here restate objects of mission 1 of this series (the set (2) and $Ax$). The interpretation through a generative model (p. 9) and the results deferred to the companion report are not formalized. Contributions of proofs of any milestone, and of a local proof of Theorem 1 for use in Theorem 6, are welcome.

Selected references

• H. Xu, C. Caramanis, S. Mannor, Robust Regression and Lasso, arXiv:0811.1790v1, 2008; IEEE Transactions on Information Theory 56(7), 2010. https://arxiv.org/abs/0811.1790v1, https://doi.org/10.1109/TIT.2010.2048503
• R. Tibshirani, Regression shrinkage and selection via the lasso, Journal of the Royal Statistical Society B 58(1), 1996. https://doi.org/10.1111/j.2517-6161.1996.tb02080.x
• J. A. Tropp, Just relax: convex programming methods for identifying sparse signals in noise, IEEE Transactions on Information Theory 52(3), 2006. https://doi.org/10.1109/TIT.2005.864420
• P. Zhao, B. Yu, On model selection consistency of Lasso, Journal of Machine Learning Research 7, 2006. https://jmlr.org/papers/v7/zhao06a.html
• L. El Ghaoui, H. Lebret, Robust solutions to least-squares problems with uncertain data, SIAM Journal on Matrix Analysis and Applications 18(4), 1997. https://doi.org/10.1137/S0895479896298130