LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Real scaled-Gaussian spectral and Frobenius product bounds

Statement

Assume Countable Choice for the finite-dimensional Gaussian probability law. Let $a, r, s, b$ be positive integers, let $S \in R^{a \times r}$ and $T \in R^{s \times b}$ be fixed, and let $G \in R^{r \times s}$ have independent standard real Gaussian entries. Then $E ∥ S G T ∥_{F}^{2} = ∥ S ∥_{F}^{2} ∥ T ∥_{F}^{2}, E ∥ S G T ∥_{2} \leq ∥ S ∥_{2} ∥ T ∥_{F} + ∥ S ∥_{F} ∥ T ∥_{2} .$ The spectral estimate in this lemma is real-field only.

Facts & Assumptions

Given: Countable Choice for the finite Gaussian law, and fixed compatible real matrices $S, T$ and an iid standard real Gaussian matrix $G$ .

[F1]

The entries of $G$ are independent standard real Gaussians (Standard real and normalized complex Gaussian matrix laws).

[F2]

Finite centered Gaussian families whose increment variances are ordered have ordered expected maxima (Finite Gaussian increment comparison).

[F3]

For an integrable real random variable $X$ and a convex real function $φ$ on an interval containing its almost-everywhere range, Jensen's inequality applies when $φ (X)$ is integrable or nonnegative (Jensen's inequality for expectation).

[F4]

Almost-everywhere convergence under one integrable absolute majorant permits passage of expectations to the limit (Dominated convergence).

[A1]

Countable Choice supplies the Lebesgue measures for the finite Gaussian expectations (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

1.1givenF1A1algebra

Write $(S G T)_{α β} = \sum_{i = 1}^{r} \sum_{j = 1}^{s} S_{α i} G_{i j} T_{j β}$ . Expanding gives $E ∥ S G T ∥_{F}^{2} = \sum_{α = 1}^{a} \sum_{β = 1}^{b} \sum_{i, u = 1}^{r} \sum_{j, v = 1}^{s} S_{α i} T_{j β} S_{α u} T_{v β} E (G_{i j} G_{u v})$ . Independence, zero means, and unit variances give $E (G_{i j} G_{u v}) = 1_{i = u} 1_{j = v}$ , so this reduces to $\sum_{α, β, i, j} S_{α i}^{2} T_{j β}^{2} = (\sum_{α, i} S_{α i}^{2}) (\sum_{j, β} T_{j β}^{2}) = ∥ S ∥_{F}^{2} ∥ T ∥_{F}^{2}$ .

1.2givenF1algebra

For unit vectors $x \in R^{a}, y \in R^{b}$ , set $u = S^{T} x$ , $v = T y$ , $U = ∥ u ∥$ , $V = ∥ v ∥$ , and define centered Gaussian processes $X_{x y} = u^{T} G v + z U V$ and $Y_{x y} = V g^{T} u + U h^{T} v$ , where $z \in R$ , $g \in R^{r}$ , and $h \in R^{s}$ are independent standard real Gaussian variables/vectors, independent of $G$ . For a second pair $(x^{'}, y^{'})$ , write $u^{'} = S^{T} x^{'}$ , $v^{'} = T y^{'}$ , $U^{'} = ∥ u^{'} ∥$ , $V^{'} = ∥ v^{'} ∥$ , $c = u^{T} u^{'}$ , and $d = v^{T} v^{'}$ . At each index both processes have variance $2 U^{2} V^{2}$ , and their cross-covariances are $Cov (X_{x y}, X_{x^{'} y^{'}}) = c d + U U^{'} V V^{'}$ and $Cov (Y_{x y}, Y_{x^{'} y^{'}}) = c V V^{'} + U U^{'} d$ . The difference is $(U U^{'} - c) (V V^{'} - d) \geq 0$ by Cauchy–Schwarz; subtracting twice the covariance from the sum of the two variances gives $E (X_{x y} - X_{x^{'} y^{'}})^{2} \leq E (Y_{x y} - Y_{x^{'} y^{'}})^{2}$ .

2.1step 1.2F2F3F4A1algebra

Apply [F2] to increasing finite subsets of normalized rational vectors in the product of unit spheres. They are dense; both sample paths are continuous, and their absolute suprema are bounded by $∥ S ∥_{2} ∥ T ∥_{2} (∥ G ∥_{F} + ∣ z ∣)$ for $X$ and $∥ T ∥_{2} ∥ S g ∥_{2} + ∥ S ∥_{2} ∥ T^{T} h ∥_{2}$ for $Y$ . These bounds are integrable because independence and unit coordinate variances give $E ∥ G ∥_{F}^{2} = r s$ , $E z^{2} = 1$ , $E ∥ S g ∥_{2}^{2} = ∥ S ∥_{F}^{2}$ , and $E ∥ T^{T} h ∥_{2}^{2} = ∥ T ∥_{F}^{2}$ . Dominated convergence [F4] passes the finite comparisons to the full spheres. For fixed $G$ , $z \mapsto \sup_{x, y} (u^{T} G v + z U V)$ is convex with integrable growth, so Jensen [F3] gives $E_{z} \sup_{x, y} X_{x y} \geq \sup_{x, y} E_{z} X_{x y} = \sup_{x, y} u^{T} G v = ∥ S G T ∥_{2}$ .

3.1step 2.1F1F3algebra∎

For every unit $x, y$ , $Y_{x y} \leq ∥ T ∥_{2} ∥ S g ∥_{2} + ∥ S ∥_{2} ∥ T^{T} h ∥_{2}$ . Taking suprema and expectations, [F3] applied to the convex square gives $E ∥ S g ∥_{2} \leq (E ∥ S g ∥_{2}^{2})^{1 / 2} = ∥ S ∥_{F}$ and $E ∥ T^{T} h ∥_{2} \leq ∥ T ∥_{F}$ . Combining with step 2.1 proves the spectral estimate.

Depends on

Used by

Expected spectral error of the real Gaussian range finder Theorem

Dependency tree · two levels

26 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

Halko, Martinsson, and Tropp, Finding Structure with Randomness, Proposition 10.1 and Appendix A.1 (standard reference, not scraped)
S. Chevet, Séries de variables aléatoires gaussiennes..., Lemma 3.1 (standard reference, not scraped)