LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Exact bias and noise decomposition of isotropic prediction risk

Statement

Let $n, p \geq 1$ , let $X \in R^{n \times p}$ and $β \in R^{p}$ be deterministic, and let $ε \in R^{n}$ and $z_{0} \in R^{p}$ be independent of one another and of $X$ , with $E ε = 0$ , $Cov (ε) = σ^{2} I_{n}$ , $E z_{0} = 0$ , and $Cov (z_{0}) = I_{p}$ . Set $y = X β + ε$ , $\hat{β} = X^{+} y$ , $S = X^{T} X / n$ , and $R (X) : = E_{ε, z_{0}} [(z_{0}^{T} (\hat{β} - β))^{2} ∣ X] .$ Then $R (X) = ∥ (I_{p} - X^{+} X) β ∥_{2}^{2} + σ^{2} tr ((X^{T} X)^{+}) = ∥ (I_{p} - X^{+} X) β ∥_{2}^{2} + \frac{σ^{2}}{n} tr (S^{+}) .$

Statement references

Ridgeless minimum-norm least-squares regression

The Moore--Penrose pseudoinverse $A^{+}$ as the solution of the four Penrose equations

Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition

Facts & Assumptions

Given: $X, β, ε, z_{0}$ and their moment and independence assumptions from the Statement.

[A1]

The noise is independent of $X$ , centered, and has covariance $σ^{2} I_{n}$ , so these are also its conditional first and second moments given $X$ .

[A2]

The test vector is independent of $(X, ε)$ , centered, and has covariance $I_{p}$ , so its conditional second moment given $(X, ε)$ is $I_{p}$ .

[F1]

Every finite real matrix has a singular value decomposition (Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition).

[F2]

The Moore--Penrose pseudoinverse exists uniquely and satisfies the four Penrose equations (The Moore--Penrose pseudoinverse $A^{+}$ as the solution of the four Penrose equations, Every finite real or complex matrix has a unique Moore--Penrose pseudoinverse).

Proof

1.1givenF1F2algebra

Write a rank- $q$ singular value decomposition $X = U_{q} D_{q} V_{q}^{T}$ with positive diagonal $D_{q}$ . The four Penrose equations and uniqueness [F2] give $X^{+} = V_{q} D_{q}^{- 1} U_{q}^{T}$ , $I_{p} - X^{+} X = I_{p} - V_{q} V_{q}^{T}$ , and $X^{+} (X^{+})^{T} = V_{q} D_{q}^{- 2} V_{q}^{T} = (X^{T} X)^{+}$ ; the last equality follows by checking the four equations for $X^{T} X = V_{q} D_{q}^{2} V_{q}^{T}$ . The same decomposition gives $S^{+} = n (X^{T} X)^{+}$ .

1.2givenA2algebra

For any fixed $v \in R^{p}$ , [A2] gives $E [(z_{0}^{T} v)^{2} ∣ X, ε] = v^{T} I_{p} v = ∥ v ∥_{2}^{2}$ . Taking $v = \hat{β} - β$ and then expectation over $ε$ reduces $R (X)$ to $E_{ε} [∥ \hat{β} - β ∥_{2}^{2} ∣ X]$ .

2.1givenA1step 1.1step 1.2algebra∎

Put $Q = I_{p} - X^{+} X$ . From the definition of $\hat{β}$ , $\hat{β} - β = - Q β + X^{+} ε$ . Expanding the squared norm, the cross term has conditional expectation zero by [A1], and the noise term is $E_{ε} [∥ X^{+} ε ∥_{2}^{2} ∣ X] = σ^{2} tr (X^{+} (X^{+})^{T}) = σ^{2} tr ((X^{T} X)^{+}),$ using step 1.1. Combining with step 1.2 and the scaling identity in step 1.1 proves the two displayed risk formulas.

Depends on

Used by

Dependency tree · two levels

12 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Hastie, Montanari, Rosset and Tibshirani, Surprises in High-Dimensional Ridgeless Least Squares Interpolation (standard reference, not scraped)