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

Direct expected spectral bound for the normalized complex range finder

Statement

Assume Countable Choice for the finite-dimensional Gaussian probability law. Let $A \in C^{m \times n}$ be fixed, let $k \geq 2$ , $p \geq 2$ be integers with $ℓ = k + p \leq \min (m, n)$ , and draw $Ω \in C^{n \times ℓ}$ with iid normalized complex Gaussian entries satisfying $E ∣ g ∣^{2} = 1$ . Let $Q$ be the exact finite-scan range-finder basis of $Ran (A Ω)$ returned by Exact Gaussian randomized range finder, and put $P = Q Q^{*}$ . Then $E ∥ (I - P) A ∥_{2} \leq \sqrt{\frac{ℓ}{p}} σ_{k + 1} + \frac{e \sqrt{ℓ}}{p} {(\sum_{j > k} σ_{j}^{2})}^{1 / 2} .$ In particular, the original approved bound with leading coefficient $1 + \sqrt{k / (p - 1)}$ follows. The algorithm and sketch width $ℓ$ are unchanged; only the analysis may use a larger SVD partition rank.

Facts & Assumptions

Given: Countable Choice, the fixed complex matrix and the stated $k, p, ℓ$ , and the normalized complex Gaussian sketch.

[F1]

Borel measurability and range correctness of the finite scan proves that the scan in Exact Gaussian randomized range finder forms $Y = A Ω$ , returns a finite-scan orthonormal basis of its actual range, and makes the orthogonal projector $P$ a Borel function of $Ω$ , including rank-deficient and empty samples.

[F2]

Fixed unitary SVD coordinates preserve the iid normalized complex Gaussian law and make disjoint row blocks independent (Orthogonal and unitary invariance of Gaussian matrix blocks).

[F3]

A wide complex Gaussian block has full row rank almost surely, and on that event its pseudoinverse is $G^{*} (G G^{*})^{- 1}$ (A wide Gaussian matrix has full row rank almost surely, Exact Frobenius moments of wide Gaussian pseudoinverses, The Moore--Penrose pseudoinverse $A^{+}$ as the solution of the four Penrose equations).

[F4]

For independent normalized complex Gaussian blocks $G_{1} \in C^{a \times ℓ}$ , $G_{2} \in C^{d \times ℓ}$ with $ℓ = a + r$ and $r \geq 2$ , and every fixed compatible $S$ , writing $C = 2 \sqrt{2} e$ , $E ∥ S G_{2} G_{1}^{†} ∥_{2}^{2} \leq C ℓ r^{- 2} (∥ S ∥_{F}^{2} + (r / 4) ∥ S ∥_{2}^{2}),$ $E ∥ S G_{2} G_{1}^{†} ∥_{2}^{2} \leq e^{2} ℓ r^{- 2} (∥ S ∥_{F}^{2} + (r / 2) ∥ S ∥_{2}^{2}) .$ This is Affine second-moment bounds for normalized complex Gaussian block products.

[F5]

SVD coordinates preserve the operator norm; the operator norm is the largest singular value and is bounded above by the Frobenius norm (Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition, The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||, The operator norm is 0 on the zero domain and otherwise equals the largest singular value, attained at a right-singular vector, Spectral and Frobenius norms are unitarily invariant, are given by singular values, and satisfy the sharp rank comparison).

[F6]

For a nonnegative random variable $X$ with finite second moment, $E X \leq \sqrt{E X^{2}}$ (Jensen's inequality for expectation).

[F7]

The normalized exponential constant satisfies $e = \sum_{n \geq 0} 1 / n!$ , with factorial recurrence (The real exponential function and the number $e$ by a power series, The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ , The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, Canonical naturals are positive and strictly increasing), and $2 < e < 3$ (The elementary numerical bound $2 < e < 3$ ); for $∣ r ∣ < 1$ , $\sum_{j \geq 0} r^{j} = (1 - r)^{- 1}$ (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges).

[A1]

Countable Choice supplies the finite-dimensional Lebesgue Gaussian probability law (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

1.1givenF1F2F3F5A1choosealgebra

Choose an SVD $A = U Σ V^{*}$ and fix any deterministic analysis rank $a$ with $1 \leq a < ℓ$ . Write $V^{*} Ω = [Ω_{1}^{T} Ω_{2}^{T}]^{T}$ with the first $a$ rows in $Ω_{1}$ . By [F2] these blocks are independent normalized complex Gaussian matrices, and by [F3] $Ω_{1}$ has full row rank almost surely. In SVD coordinates set $Y = Σ V^{*} Ω$ and $C_{0} = Y Ω_{1}^{†} [I_{a} 0]$ ; then $Ran (C_{0}) \subseteq Ran (Y)$ . Since $Ω_{1} Ω_{1}^{†} = I_{a}$ , the first $a$ rows of $Σ - C_{0}$ vanish and its remaining rows are $[- T W]$ , where $T = Σ_{> a} Ω_{2} Ω_{1}^{†}$ and $W = Σ_{> a}$ . For the projector $\tilde{P}$ onto $Ran (Y)$ , $(I - \tilde{P}) C_{0} = 0$ . For any vector $z$ , the two terms in $z = \tilde{P} z + (I - \tilde{P}) z$ are orthogonal, so $∥ (I - \tilde{P}) z ∥_{2} \leq ∥ z ∥_{2}$ ; taking the unit-vector supremum shows that this projector is contractive. Thus $∥ (I - \tilde{P}) Σ ∥_{2}^{2} \leq ∥ [- T W] ∥_{2}^{2}$ . The block identity $[- T W] [- T W]^{*} = T T^{*} + W W^{*}$ and [F5] give $∥ [- T W] ∥_{2}^{2} = ∥ T T^{*} + W W^{*} ∥_{2}$ . The operator-norm triangle inequality follows by applying the vector triangle inequality to each unit vector and taking the supremum; the SVD gives $∥ T T^{*} ∥_{2} = ∥ T ∥_{2}^{2}$ and $∥ W W^{*} ∥_{2} = ∥ W ∥_{2}^{2}$ . Hence $∥ [- T W] ∥_{2}^{2} \leq ∥ T ∥_{2}^{2} + ∥ W ∥_{2}^{2} = ∥ Σ_{> a} Ω_{2} Ω_{1}^{†} ∥_{2}^{2} + σ_{a + 1}^{2}$ . Unitary invariance transfers this to $E^{2} \leq σ_{a + 1}^{2} + ∥ Σ_{> a} Ω_{2} Ω_{1}^{†} ∥_{2}^{2}$ , where $E = ∥ (I - P) A ∥_{2}$ . This uses no inverse of $Σ_{1 : a}$ and includes $rank (A) < a$ . For every draw $E \leq ∥ A ∥_{2}$ ; by [F1] it is measurable, so exceptional rank-loss sets do not change its expectation.

2.1step 1.1F6algebra

Put $σ = σ_{k + 1}$ and $R = \sum_{j > k} σ_{j}^{2}$ . If $σ = 0$ , then $R = 0$ and all tail singular values vanish, so step 1.1 with $a = k$ gives $E = 0$ almost surely. Otherwise $R \geq σ^{2} > 0$ ; set $x = R / (p σ^{2}) > 0$ and $b = σ \sqrt{ℓ / p}$ . By [F6], it suffices to prove $E E^{2} / b^{2} \leq (1 + e \sqrt{x})^{2}$ .

3.1step 1.1step 2.1F4F5F7algebra

Suppose $x \geq 1$ . Apply the second bound in [F4] to step 1.1 at $a = k$ , with oversampling $p$ . Since $∥ Σ_{> k} ∥_{2} = σ$ and $∥ Σ_{> k} ∥_{F}^{2} = R$ by [F5], $E E^{2} / b^{2} \leq p / ℓ + e^{2} (x + 1 / 2) \leq 1 + e^{2} x + e^{2} / 2 \leq (1 + e \sqrt{x})^{2} .$ The last inequality uses $e < 3 < 4$ from [F7] and $\sqrt{x} \geq 1$ .

3.2step 1.1step 2.1F4F7algebra

Suppose $1 / 7 \leq x \leq 1$ . The first bound in [F4] at $a = k$ gives $E E^{2} / b^{2} \leq 1 + C (x + 1 / 4)$ . Set $y = \sqrt{x}$ and $a_{0} = 2 \sqrt{2} - e$ . The difference $[(1 + e \sqrt{x})^{2} - (1 + C (x + 1 / 4))] / e$ is $f (y) = 2 y - a_{0} y^{2} - 1 / \sqrt{2}$ . The series in [F7] gives $27 / 10 < e < 11 / 4$ : the partial sum through $1 / 5!$ is $163 / 60 > 27 / 10$ , and the tail after $1 / 4!$ is at most $(1 / 5!) \sum_{j \geq 0} (1 / 6)^{j} = 1 / 100$ , so $e \leq 65 / 24 + 1 / 100 = 1631 / 600 < 11 / 4$ . For the tail estimate, every ratio between successive terms after $1 / 5!$ is at most $1 / 6$ by the factorial recurrence, and [F7] sums the resulting geometric majorant. The square comparisons $49 / 25 < 2 < 289 / 144$ and $7 < 64 / 9$ give $7 / 5 < \sqrt{2} < 17 / 12$ and $\sqrt{7} < 8 / 3$ . Hence $0 < a_{0} < 2 / 15$ , $1 / \sqrt{2} < 5 / 7$ , and $2 / \sqrt{7} > 3 / 4$ . The identity $f ((1 - t) u + t v) - (1 - t) f (u) - t f (v) = a_{0} t (1 - t) (u - v)^{2} \geq 0$ shows $f$ is concave on $[1 / \sqrt{7}, 1]$ . Therefore it lies above the chord joining its endpoint values, and $f (1 / \sqrt{7}) > 3 / 4 - 2 / 105 - 5 / 7 = 1 / 60 > 0$ , $f (1) > 2 - 2 / 15 - 5 / 7 = 121 / 105 > 0$ . This proves $E E^{2} / b^{2} \leq (1 + e \sqrt{x})^{2}$ throughout the region.

3.3step 1.1step 2.1F4algebra

Suppose $0 < x \leq 1 / 7$ . Let $s = ⌊ p / 4 ⌋$ , $p^{'} = p - s$ , and $a = k + s$ . Then $p^{'} \geq ⌈ 3 p / 4 ⌉ \geq 2$ , $s + 1 > p / 4$ , and $a + p^{'} = ℓ$ , so $1 \leq a < ℓ$ . Put $σ^{'} = σ_{k + s + 1}$ and $R^{'} = \sum_{j > k + s} σ_{j}^{2}$ . The first $s + 1$ terms in $R$ are at least $(σ^{'})^{2}$ , hence $(σ^{'})^{2} \leq R / (s + 1)$ ; also $R^{'} \leq R$ . Apply step 1.1 at this $a$ and the first bound in [F4] with oversampling $p^{'}$ . The same sketch and projector are used; only the deterministic SVD partition rank changes. This gives $E E^{2} \leq (σ^{'})^{2} + C ℓ (p^{'})^{- 2} (R^{'} + (p^{'} / 4) (σ^{'})^{2}) .$ Since $b^{2} = σ^{2} ℓ / p$ , $ℓ \geq p$ , and $p^{'} \geq 3 p / 4$ , division yields $E E^{2} / b^{2} \leq x [\frac{p^{2}}{ℓ (s + 1)} + \frac{C p^{2}}{(p^{'})^{2}} + \frac{C p^{2}}{4 p^{'} (s + 1)}] \leq x [4 + \frac{16}{9} C + \frac{4}{3} C] = x K^{2},$ where $K^{2} = 4 + (28 / 9) C$ . These estimates include $p = 2, 3$ , when $s = 0$ .

4.1step 3.2step 3.3F7algebra

Since $2 < 9801 / 4900$ , squaring gives $\sqrt{2} < 99 / 70$ . From this and the bound $e < 11 / 4$ proved in step 3.2, $C < 1089 / 140$ and therefore $K^{2} < 4 + (28 / 9) (1089 / 140) = 141 / 5$ . Since $441 / 64 < 7$ and $e > 27 / 10$ , we have $\sqrt{7} + e > 213 / 40$ and $(213 / 40)^{2} = 45369 / 1600 > 141 / 5$ . Thus $K < \sqrt{7} + e$ , and $x \leq 1 / 7$ implies $K \sqrt{x} \leq (\sqrt{7} + e) \sqrt{x} \leq 1 + e \sqrt{x}$ . Step 3.3 now yields $E E^{2} / b^{2} \leq (1 + e \sqrt{x})^{2}$ in the last region.

5.1step 2.1step 3.1step 3.2step 4.1algebra∎

The cases $x \geq 1$ , $1 / 7 \leq x \leq 1$ , and $0 < x \leq 1 / 7$ exhaust $x > 0$ ; the zero-tail case was handled in step 2.1. Taking square roots in steps 3.1, 3.2 and 4.1 gives $E E \leq b (1 + e \sqrt{x}) = \sqrt{ℓ / p} σ + (e \sqrt{ℓ} / p) \sqrt{R}$ . Finally $\sqrt{ℓ / p} = \sqrt{1 + k / p} \leq 1 + \sqrt{k / p} \leq 1 + \sqrt{k / (p - 1)}$ , so the original expected-error bound follows without changing its field, dimensions, constants, or sketch width.

Depends on

Used by

Expected spectral error for real and normalized complex Gaussian range finders Theorem

Dependency tree · two levels

104 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, §§9.1–10.2; the present normalized-complex moment and rank-shift argument is derived locally (standard reference, not scraped)
Martinsson and Tropp, Randomized Numerical Linear Algebra: Foundations & Algorithms, §§11.4.1–11.4.2; the present normalized-complex proof is derived locally (standard reference, not scraped)