LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-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.

Gaussian output initialization concentrates conditionally on the hidden features

Statement

Assume AC, DC and countable choice. Fix hidden-layer feature vectors $ϕ_{1}, \dots, ϕ_{n} \in R^{m}$ , form the matrix $Φ \in R^{n \times m}$ with rows $ϕ_{i}^{T}$ , and let the independent output-weight vector $a \sim N_{m} (0, I_{m})$ . Put $u = Φ a$ and $G = Φ Φ^{T}$ . Then for every $0 < δ < 1$ ,

$P {∥ u ∥_{2} \leq \sqrt{tr (G)} + ∥ Φ ∥_{o p} \sqrt{2 \log (1 / δ)}} \geq 1 - δ,$

where $∥ Φ ∥_{o p} = \sup_{∥ v ∥_{2} = 1} ∥ Φ v ∥_{2}$ . The probability is conditional on the fixed hidden-layer features and is over $a$ only.

Statement references

Du et al., random Gaussian output initialization and Appendix B

Facts & Assumptions

Given: AC, DC, countable choice, fixed feature vectors, and an independent standard Gaussian output vector.

[A1]

AC, DC and countable choice are assumed by the Gaussian concentration supplier. The Axiom of Choice The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain The Axiom of Countable Choice ( ${A C}_{ω}$ )

[F1]

For a standard Gaussian vector $Z$ and an $L$ -Lipschitz real function $g$ , $P {g (Z) \geq E g (Z) + r} \leq e^{- r^{2} / (2 L^{2})}$ for $L > 0, r > 0$ ; for $L = 0$ the upper-tail event is empty. Lipschitz concentration for standard Gaussian measure

[F2]

A standard multivariate normal vector has covariance identity, and a fixed linear functional has variance given by its covariance quadratic form. Multivariate normal law, including singular covariance

[F3]

Cauchy–Schwarz bounds $E ∣ X Y ∣$ by the product of the $L^{2}$ norms. Cauchy-Schwarz for random variables

[F4]

The Euclidean norm satisfies the triangle inequality and hence the reverse triangle inequality. Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation

Proof

technique · apply one-sided Gaussian concentration to the norm of a fixed linear image and bound its mean by its second moment

1.1F2F3F4givenalgebra

[F4] gives $∣ ∥ Φ a ∥_{2} - ∥ Φ b ∥_{2} ∣ \leq ∥ Φ (a - b) ∥_{2} \leq ∥ Φ ∥_{o p} ∥ a - b ∥_{2}$ , so $a \mapsto ∥ Φ a ∥_{2}$ is $∥ Φ ∥_{o p}$ -Lipschitz. Since $E [a a^{T}] = I_{m}$ by [F2], $E ∥ Φ a ∥_{2}^{2} = tr (Φ Φ^{T}) = tr (G)$ ; [F3] with $X = ∥ Φ a ∥_{2}$ and $Y = 1$ yields $E ∥ Φ a ∥_{2} \leq \sqrt{tr (G)}$ .

2.1A1F1F2step 1.1algebra∎

If $∥ Φ ∥_{o p} = 0$ , then $u = 0$ and the asserted event has probability one. Otherwise apply [F1] to $g (a) = ∥ Φ a ∥_{2}$ with $r = ∥ Φ ∥_{o p} \sqrt{2 \log (1 / δ)} > 0$ . The upper-tail probability is at most $\exp (- \log (1 / δ)) = δ$ , and the mean bound in step 1.1 gives the displayed threshold.

Depends on

Used by

Dependency tree · two levels

55 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

Simon S. Du, Jason D. Lee, Haochuan Li, Liwei Wang, and Xiyu Zhai, Gradient Descent Finds Global Minima of Deep Neural Networks, Appendix B (standard reference, not scraped)