LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generated

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.

Continuity of bivariate Gaussian feature expectations, including singular limits

Statement

Assume AC. Let $C_{n}$ be real symmetric positive-semidefinite $2 \times 2$ matrices converging entrywise to $C$ , and suppose both diagonal entries of $C_{n}$ and of $C$ are positive. Let $(U_{n}, V_{n})$ and $(U, V)$ have centered bivariate normal laws with covariance matrices $C_{n}$ and $C$ , respectively; singular covariance matrices are allowed. For every globally Lipschitz $τ : R \to R$ , $E [τ (U_{n}) τ (V_{n})] ⟶ E [τ (U) τ (V)] .$ For every bounded Borel function $g : R \to R$ , $E [g (U_{n}) g (V_{n})] ⟶ E [g (U) g (V)] .$ The second conclusion applies to any bounded measurable representative of an almost-everywhere derivative, including when the limiting pair is supported on a line.

Statement references

Jacot, Gabriel, and Hongler, Appendix A.1 and A.4, Gaussian covariance and derivative expectations in the NTK recursion

Finite Gaussian vectors are realized by a covariance square root times independent standard normals

Smooth compactly supported functions are dense in Lebesgue L²

Facts & Assumptions

Given: AC; positive limiting and approximating marginal variances; bivariate centered Gaussian vectors with the stated covariance matrices; either a globally Lipschitz feature $τ$ or a bounded Borel feature $g$ .

[A1]

AC supplies the countable and dependent choice used in the finite Gaussian-law construction (The Axiom of Choice, AC supplies countable selections and prescribed serial paths).

[F1]

The construction $C^{1 / 2} G$ , where $G$ has independent standard-normal coordinates, has centered multivariate normal law with covariance $C$ (Multivariate normal law, including singular covariance). This covariance uniquely determines the centered Gaussian law, including singular cases (Characteristic function of a multivariate normal law).

[F2]

The standard normal coordinates have a positive density and finite second moments (Standard normal and normal laws).

[F3]

Under countable choice, smooth compactly supported functions are dense in Lebesgue $L^{2}$ (Complex completeness, density, and inner product: the consumer interface).

[F4]

Cauchy–Schwarz bounds the absolute expectation of a product by the product of its marginal $L^{2}$ norms (Cauchy-Schwarz for random variables).

[F5]

Pointwise convergence under an integrable majorant passes through expectation (Dominated convergence).

Proof

technique · direct

1.1A1F1givenalgebraconstruct

Write $C_{n} = (\begin{array}{cc} v_{n} & c_{n} \\ c_{n} & w_{n} \end{array})$ and $d_{n} = \det C_{n} \geq 0$ . Since $v_{n}, w_{n} > 0$ , $tr C_{n} + 2 \sqrt{d_{n}} > 0$ . The matrix $A_{n} = (C_{n} + \sqrt{d_{n}} I_{2}) / \sqrt{tr C_{n} + 2 \sqrt{d_{n}}}$ is positive semidefinite. The identity $C_{n}^{2} - (tr C_{n}) C_{n} + d_{n} I_{2} = 0$ gives $A_{n}^{2} = C_{n}$ by expansion; the same formula defines $A$ for $C$ , and entrywise convergence gives $A_{n} \to A$ .

1.2A1F2F3givenconstruct

Fix a variance $s > \max (C_{11}, C_{22})$ . For all sufficiently large $n$ , the marginal variances of $U_{n}, V_{n}$ lie in a compact subinterval of $(0, s)$ , so their normal densities are bounded above by a common constant times the density of $N (0, s)$ . The isometry $h \mapsto h \sqrt{ϕ_{s}}$ from $L^{2} (N (0, s))$ into Lebesgue $L^{2}$ and [F3] provide bounded continuous functions $g_{k}$ with $∥ g - g_{k} ∥_{L^{2} (N (0, s))} \to 0$ . The density bound makes these approximation errors tend to zero uniformly for the marginals of all sufficiently large $n$ and for the two limiting marginals.

2.1A1F1F2step 1.1construct

Let $G = (G_{1}, G_{2})$ have independent standard-normal coordinates. The vectors $A_{n} G$ and $A G$ have centered Gaussian laws with covariances $C_{n}$ and $C$ by [F1] and step 1.1. Gaussian uniqueness in [F1] identifies their laws with those stipulated in the statement, even when singular. We may therefore compute all expectations using this coupling; $A_{n} \to A$ gives $(U_{n}, V_{n}) \to (U, V)$ almost surely.

2.2F4step 1.2

By [F4], for each such $n$ the difference between $E [g (U_{n}) g (V_{n})]$ and $E [g_{k} (U_{n}) g_{k} (V_{n})]$ is bounded by $∥ g - g_{k} ∥_{L^{2} (U_{n})} ∥ g ∥_{L^{2} (V_{n})} + ∥ g_{k} ∥_{L^{2} (U_{n})} ∥ g - g_{k} ∥_{L^{2} (V_{n})}$ , which tends to zero uniformly in sufficiently large $n$ as $k \to \infty$ by step 1.2; the same bound applies to $(U, V)$ .

3.1F2F5givenstep 2.1

If $τ$ is globally Lipschitz, then it is continuous and has at most linear growth. The matrices $A_{n}$ are bounded, so $∣ τ (U_{n}) τ (V_{n}) ∣ \leq M (1 + ∥ G ∥_{2}^{2})$ for one finite $M$ independent of all sufficiently large $n$ ; [F2] makes this majorant integrable. Almost-sure convergence in step 2.1 and [F5] prove the first expectation limit.

4.1F5step 2.1step 2.2∎

For fixed $k$ , $g_{k}$ is bounded and continuous, so step 2.1 and [F5] give $E [g_{k} (U_{n}) g_{k} (V_{n})] \to E [g_{k} (U) g_{k} (V)]$ . First take $n \to \infty$ , then $k \to \infty$ in the error bounds of step 2.2. This proves the bounded-Borel expectation limit, including singular $C$ .

Depends on

Used by

Sequential infinite-width NTK limit and finite-time lazy training dynamics Theorem

Dependency tree · two levels

42 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

Arthur Jacot, Franck Gabriel, and Clément Hongler, Neural Tangent Kernel: Convergence and Generalization in Neural Networks (standard reference, not scraped)