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.

Affine second-moment bounds for normalized complex Gaussian block products

Statement

Assume Countable Choice for the finite-dimensional Gaussian probability law. Let $k \geq 1$ , $p \geq 2$ , $ℓ = k + p$ , and $d, a \geq 1$ be integers. Let $G_{1} \in C^{k \times ℓ}$ and $G_{2} \in C^{d \times ℓ}$ be independent matrices with iid normalized complex Gaussian entries as in Standard real and normalized complex Gaussian matrix laws, so $E ∣ g ∣^{2} = 1$ . Put $Z = G_{2} G_{1}^{†}$ , where $G_{1}^{†}$ is the Moore--Penrose pseudoinverse of The Moore--Penrose pseudoinverse $A^{+}$ as the solution of the four Penrose equations. For every fixed $S \in C^{a \times d}$ , writing $C = 2 \sqrt{2} e$ with $e = \exp (1)$ as in The real exponential function and the number $e$ by a power series, one has $E ∥ S Z ∥_{2}^{2} \leq \frac{C ℓ}{p^{2}} (∥ S ∥_{F}^{2} + \frac{p}{4} ∥ S ∥_{2}^{2}),$ $E ∥ S Z ∥_{2}^{2} \leq \frac{e^{2} ℓ}{p^{2}} (∥ S ∥_{F}^{2} + \frac{p}{2} ∥ S ∥_{2}^{2}) .$ Here $∥ \cdot ∥_{2}$ is the induced operator norm of The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv|| and $∥ \cdot ∥_{F}$ is the Frobenius norm of The Frobenius norm $∥ A ∥_{F} = (\sum_{i, j} ∣ a_{i j} ∣^{2})^{1 / 2}$ on real or complex matrices. These are coarse second-moment bounds; no sharp complex Chevet comparison is assumed. The values on the null event where $G_{1}$ loses row rank may be set to zero in these integrals.

Facts & Assumptions

Given: Countable Choice for the finite-dimensional Gaussian law; the stated independent blocks, $k \geq 1$ , $p \geq 2$ , $ℓ = k + p$ , $d, a \geq 1$ ; and a fixed compatible matrix $S$ .

[F1]

Standard real and normalized complex Gaussian matrix laws: a normalized complex Gaussian scalar has density $π^{- 1} e^{- ∣ z ∣^{2}}$ and $E ∣ z ∣^{2} = 1$ ; matrix entries have the independent product density. The finite-dimensional Lebesgue Gaussian measures use the stated The Axiom of Countable Choice ( ${A C}_{ω}$ ) assumption.

[F2]

Orthogonal and unitary invariance of Gaussian matrix blocks: left or right unitary changes preserve the normalized complex Gaussian law, and disjoint row blocks of a transformed iid matrix are independent.

[F3]

A wide Gaussian matrix has full row rank almost surely: the $k \times (k + p)$ block $G_{1}$ has row rank $k$ almost surely.

[F4]

Exact Frobenius moments of wide Gaussian pseudoinverses: on that full-row-rank event, $M = (G_{1} G_{1}^{*})^{- 1} = (G_{1}^{†})^{*} G_{1}^{†}$ , each diagonal entry of $M$ has the reciprocal $Γ (p + 1, 1)$ law, and $E tr M = k / p$ .

[F5]

The Moore--Penrose pseudoinverse $A^{+}$ as the solution of the four Penrose equations defines $G_{1}^{†}$ by the four Penrose equations, and Every finite real or complex matrix has a unique Moore--Penrose pseudoinverse gives its unique finite-dimensional real or complex value. On full row rank, Exact Frobenius moments of wide Gaussian pseudoinverses also gives $G_{1}^{†} = G_{1}^{*} (G_{1} G_{1}^{*})^{- 1}$ .

[F6]

The Beta function is $B (u, v) = \int_{0}^{1} t^{u - 1} (1 - t)^{v - 1} d t$ for $u, v > 0$ (Euler's real Beta integral), and the Beta--Gamma identity is $B (u, v) = Γ (u) Γ (v) / Γ (u + v)$ (The real Beta--Gamma identity). Euler integration and the functional equation for $Γ$ are The real Gamma function by Euler's integral and The real Gamma functional equation $Γ (s + 1) = s Γ (s)$ .

[F7]

For integer $q \geq 1$ , $t \mapsto ∣ t ∣^{q}$ is convex by Absolute real powers are Borel measurable and convex, so Jensen for expectation gives $E X \leq (E X^{q})^{1 / q}$ for $X \geq 0$ with finite $q$ th moment (Jensen's inequality for expectation). The finite Jensen inequality for convex functions on Euclidean convex sets is Finite Jensen inequality for convex functions on $R^{n}$ , and the finite arithmetic--geometric mean inequality is The arithmetic mean, geometric mean inequality.

[F8]

Nonnegative product-measurable functions may be integrated in either order by Tonelli's theorem for nonnegative measurable functions on a sigma-finite product.

[F9]

Matrices admit SVDs, the operator norm is attained at a unit right singular vector and equals the largest singular value (Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition, The operator norm is 0 on the zero domain and otherwise equals the largest singular value, attained at a right-singular vector, The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||). The Frobenius norm is the Euclidean norm of the entry list, equals the square root of the sum of squared singular values, and dominates the operator norm (The Frobenius norm $∥ A ∥_{F} = (\sum_{i, j} ∣ a_{i j} ∣^{2})^{1 / 2}$ on real or complex matrices, Spectral and Frobenius norms are unitarily invariant, are given by singular values, and satisfy the sharp rank comparison).

[F10]

The factorial is the recursively defined natural product (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ); in real arithmetic natural numbers are read through the canonical embedding $ι$ (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, Canonical naturals are positive and strictly increasing). Also $e = \exp (1)$ with $\exp (x) = \sum_{n \geq 0} x^{n} / n!$ (The real exponential function and the number $e$ by a power series). The natural logarithm is the inverse of the positive real exponential, is strictly increasing, obeys the product and quotient laws, and satisfies $\log^{'} (x) = 1 / x$ (The natural logarithm as the inverse of the exponential function, Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm, The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t).

[F11]

A continuous function on a closed interval is Riemann integrable (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion); an integrable derivative is evaluated by The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ . Integrals are additive over subintervals and monotone in their integrands (For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ , If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ ), using the oriented convention The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ . The finite-sum convention and splitting laws are Finite sums and finite products, by recursion and Laws of finite sums and finite products.

[F12]

Under Countable Choice, a $C^{1}$ diffeomorphism between open subsets of $R^{n}$ changes variables in nonnegative Lebesgue integrals by its absolute Jacobian (A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions).

[F13]

Polar coordinates decompose Lebesgue measure on $R^{n}$ as $r^{n - 1} d r d σ$ for nonnegative Borel functions (Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma).

[F14]

The shape-rate Gamma law with shape $a > 0$ and rate $b > 0$ has density $b^{a} u^{a - 1} e^{- b u} / Γ (a)$ on $u > 0$ ; in particular, $Γ (a, 1)$ has density $u^{a - 1} e^{- u} / Γ (a)$ (Shape-rate Gamma distribution). This matches the scale- $1$ notation in Exact Frobenius moments of wide Gaussian pseudoinverses.

[A1]

Assume the Axiom of Countable Choice as required by the finite-dimensional Gaussian law [F1], the Gamma density normalization in [F14], and the Lebesgue integration suppliers [F12] and [F13] (The Axiom of Countable Choice ( ${A C}_{ω}$ )). No stronger choice principle is used.

Proof

1.1givenF2F3F4F5A1algebra

On the full-row-rank event of [F3], set $M = (G_{1} G_{1}^{*})^{- 1}$ . For a fixed unit $v \in C^{k}$ , choose a unitary $U_{0}$ with $U_{0} e_{1} = v$ . By [F2], $U_{0}^{*} G_{1}$ has the same law as $G_{1}$ , and its inverse Gram matrix is $U_{0}^{*} M U_{0}$ ; hence $v^{*} M v$ has the same law as $M_{11}$ . The Moore--Penrose formula in [F4] gives $∥ G_{1}^{†} v ∥_{2}^{2} = v^{*} M v$ , so [F4] makes this variance $1 / U$ for $U \sim Γ (p + 1, 1)$ . The formula in [F4] also gives $G_{1} G_{1}^{†} = I_{k}$ , hence $G_{1}^{†} v \neq 0$ . Conditional on $G_{1}$ , a row of $G_{2} G_{1}^{†} v$ is a fixed linear functional of one isotropic normalized complex Gaussian row. Completing $G_{1}^{†} v / ∥ G_{1}^{†} v ∥_{2}$ to a unitary basis and using [F2] shows that this functional is a normalized complex Gaussian with variance $v^{*} M v$ ; the $d$ rows are conditionally independent. The full-row-rank set is open because it is the union of the nonzero-minor sets. On this set the inverse formula in [F4] is continuous; setting $Z = 0$ on its null complement therefore gives a Borel version, equal almost surely to the stated product. This justifies the expectations without changing their values.

2.1step 1.1F1F6F8F12F13F14A1algebra

Apply [F13] in $R^{2}$ to the radial density $π^{- 1} e^{- ∣ z ∣^{2}}$ from [F1]. Since this is a probability density, $1 = π^{- 1} σ (S^{1}) \int_{0}^{\infty} e^{- r^{2}} r d r$ ; substitution $u = r^{2}$ by [F12] makes the integral $Γ (1) / 2 = 1 / 2$ by [F6], so $σ (S^{1}) = 2 π$ . Applying [F13] to the indicator of ${z : ∣ z ∣^{2} \in E}$ for a Borel set $E \subseteq (0, \infty)$ , and again substituting $u = r^{2}$ , gives $P (∣ g ∣^{2} \in E) = \int_{E} e^{- u} d u$ . Thus the squared modulus is $Γ (1, 1)$ . For independent $X \sim Γ (r, 1)$ and $Y \sim Γ (s, 1)$ , the map $(x, y) \mapsto (t = x + y, w = x / (x + y))$ is a $C^{1}$ diffeomorphism from $(0, \infty)^{2}$ to $(0, \infty) \times (0, 1)$ , with inverse $(t, w) \mapsto (t w, t (1 - w))$ and inverse Jacobian determinant $t$ . By [F12], their joint density in these coordinates is $t^{r + s - 1} e^{- t} w^{r - 1} (1 - w)^{s - 1} / (Γ (r) Γ (s))$ . Integrating in $w$ by Tonelli [F8] and applying the Beta--Gamma identity [F6] gives the $Γ (r + s, 1)$ density in $t$ . Finite induction therefore makes the squared norm of $j$ independent normalized complex Gaussian coordinates $Γ (j, 1)$ . Euler integration [F6] gives its $q$ th moment $Γ (j + q) / Γ (j)$ and gives $E U^{- q} = Γ (p + 1 - q) / Γ (p + 1)$ for $U \sim Γ (p + 1, 1)$ when $0 < q < p + 1$ . Integrating first over $G_{2}$ and then $G_{1}$ by [F8], for each fixed unit $v \in C^{k}$ and $1 \leq j \leq d$ this yields $E ∥ P_{j} Z v ∥_{2}^{2 q} = \frac{Γ (j + q) Γ (p + 1 - q)}{Γ (j) Γ (p + 1)},$ where $P_{j}$ keeps the first $j$ rows.

3.1step 2.1F1F2F6F8F9F12A1choosealgebra

Define $P_{0} Z = 0$ . On an auxiliary finite product probability space, let $h \in C^{k}$ have iid normalized complex Gaussian coordinates, independent of $(G_{1}, G_{2})$ , and put $v = h / ∥ h ∥_{2}$ when $h \neq 0$ and $v = e_{1}$ when $h = 0$ ; the latter event has probability zero by [F1]. The law of $v$ is unitary invariant by [F2]. For $k = 1$ , $E ∣ v_{1} ∣^{2 q} = 1$ . For $k \geq 2$ , $X = ∣ h_{1} ∣^{2}$ and $Y = \sum_{i = 2}^{k} ∣ h_{i} ∣^{2}$ are independent with laws $Γ (1, 1)$ and $Γ (k - 1, 1)$ by step 2.1. The change $s = X + Y$ , $t = X / (X + Y)$ is a $C^{1}$ diffeomorphism with Jacobian $s$ and factors the joint density into a $Γ (k, 1)$ density in $s$ and a Beta $(1, k - 1)$ density in $t$ by [F12]. Thus [F6] gives $c_{k} (q) : = E ∣ v_{1} ∣^{2 q} = \frac{Γ (k) Γ (q + 1)}{Γ (k + q)},$ which also equals $1$ when $k = 1$ . For each fixed $Z$ , choose a unit right singular vector $u$ of $P_{j} Z$ for its largest singular value (possible by [F9]). Its SVD gives $∥ P_{j} Z v ∥_{2}^{2} \geq ∥ P_{j} Z ∥_{2}^{2} ∣ u^{*} v ∣^{2}$ . Average over the auxiliary $v$ ; unitary invariance replaces $u$ by $e_{1}$ , so the left side is at least $c_{k} (q) ∥ P_{j} Z ∥_{2}^{2 q}$ after raising to power $q$ . Integrate over $Z$ by [F8] and use step 2.1, then divide by $c_{k} (q) > 0$ , to obtain $E ∥ P_{j} Z ∥_{2}^{2 q} \leq \frac{Γ (j + q) Γ (k + q) Γ (p + 1 - q)}{Γ (j) Γ (k) Γ (q + 1) Γ (p + 1)} .$ The eigenvector is selected only for each fixed finite matrix in this pointwise inequality; no measurable eigenvector is used.

4.1step 3.1F2F4F6F7F8A1algebra

The law of $Z$ is left-unitary invariant by [F2], since left multiplication acts only on $G_{2}$ . Conditional coordinate second moments give $E_{G_{2}} ∥ G_{2} G_{1}^{†} ∥_{F}^{2} = d ∥ G_{1}^{†} ∥_{F}^{2}$ ; [F4] and [F8] therefore give $E ∥ Z ∥_{F}^{2} = d k / p < \infty$ . For integer $1 \leq q \leq p$ , apply Jensen [F7] to the nonnegative variable $∥ P_{j} Z ∥_{2}^{2}$ and use step 3.1. The Gamma functional equation [F6] then gives $E ∥ P_{j} Z ∥_{2}^{2} \leq {[\frac{(k)_{q} (j)_{q}}{q! (p)_{↓ q}}]}^{1 / q},$ where $(b)_{q} = b (b + 1) \dots (b + q - 1)$ and $(p)_{↓ q} = p (p - 1) \dots (p - q + 1)$ .

5.1step 4.1F6F7F10F11algebra

By AM--GM [F7], $(k)_{q}^{1 / q} \leq k + (q - 1) / 2$ and $(j)_{q}^{1 / q} \leq j + (q - 1) / 2$ . We also have $(q!)^{1 / q} \geq q / e$ : for $q = 1$ this is immediate since the first two terms of the defining series give $e > 1$ ; for $q \geq 2$ , on each $[r - 1, r]$ with $2 \leq r \leq q$ , monotonicity of $\log$ in [F10] gives $\int_{r - 1}^{r} \log t d t \leq \log r$ . Additivity and monotonicity of integration [F11] yield $\int_{1}^{q} \log t d t \leq \sum_{r = 2}^{q} \log r = \log (q!)$ , the last equality following by induction from the product law in [F10]. The primitive $t \log t - t$ has derivative $\log t$ by [F10], and $\log$ is integrable on $[1, q]$ by [F11], so the fundamental theorem gives $\int_{1}^{q} \log t d t = q \log q - q + 1$ . Hence $\log (q!) \geq q \log q - q + 1 \geq q \log (q / e)$ , because $\log e = 1$ and the quotient law holds by [F10]. Since $\log$ is strictly increasing and both arguments are positive, $q! \geq (q / e)^{q}$ . Finally, pair the first and last, second and penultimate, and so on among the $q$ factors of $(p)_{↓ q}$ . Each complete pair has product $(p - i) (p - q + 1 + i) = p (p - q + 1) + i (q - 1 - i) \geq p (p - q + 1) .$ If $q$ is odd, the unpaired middle factor is $p - (q - 1) / 2$ , and ${(p - \frac{q - 1}{2})}^{2} = p (p - q + 1) + \frac{(q - 1)^{2}}{4} \geq p (p - q + 1) .$ Thus $(p)_{↓ q}^{1 / q} \geq \sqrt{p (p - q + 1)}$ .

6.1step 4.1step 5.1A1algebra

Take $q = ⌈ p / 2 ⌉$ in step 4.1. Then $q \geq p / 2$ , $p - q + 1 \geq p / 2$ , and $(q - 1) / 2 \leq p / 4$ . Step 5.1 gives, for $1 \leq j \leq d$ , $E ∥ P_{j} Z ∥_{2}^{2} \leq C ℓ p^{- 2} (j + p / 4), C = 2 \sqrt{2} e .$ Indeed, the denominator in step 5.1 is at least $(q / e) \sqrt{p (p - q + 1)} \geq p^{2} / (2 \sqrt{2} e)$ , while $k + (q - 1) / 2 \leq k + p / 4 \leq ℓ$ and $j + (q - 1) / 2 \leq j + p / 4$ . This proves the displayed half-order bound. For $q = p$ , $(p)_{↓ p} = p!$ , so step 5.1 bounds both denominator roots by $p / e$ and their product from below by $(p / e)^{2}$ . The numerator factors are at most $k + p / 2 \leq ℓ$ and $j + p / 2$ . Substitution into step 4.1 gives $E ∥ P_{j} Z ∥_{2}^{2} \leq e^{2} ℓ p^{- 2} (j + p / 2) .$ Both bounds also hold at $j = 0$ because $P_{0} Z = 0$ .

7.1step 4.1step 6.1F2F7F9A1constructalgebra∎

If $S = 0$ , both claims hold. Otherwise set $σ = ∥ S ∥_{2} > 0$ and diagonalize $S^{*} S$ by [F9] as $W^{*} diag (σ^{2} w_{1}, \dots, σ^{2} w_{d}) W$ , where $0 \leq w_{i} \leq 1$ . The Frobenius singular-value formula in [F9] gives $∥ S ∥_{F}^{2} = tr (S^{*} S) = σ^{2} \sum_{i} w_{i}$ , hence $\sum_{i} w_{i} = ∥ S ∥_{F}^{2} / σ^{2}$ . For $w \in [0, 1]^{d}$ , define $f (w) = E ∥ diag (\sqrt{w_{i}}) Z ∥_{2}^{2}$ . It is finite because $0 \leq w_{i} \leq 1$ and operator norm is bounded by Frobenius norm in [F9], so $f (w) \leq E ∥ Z ∥_{F}^{2} < \infty$ by step 4.1. It is convex because for every fixed unit vector $u$ , $∥ diag (\sqrt{w_{i}}) Z u ∥_{2}^{2} = \sum_{i} w_{i} ∣ (Z u)_{i} ∣^{2}$ is linear in $w$ , and taking the unit-vector maximum and then expectation preserves convexity. It is invariant under coordinate permutations by the row-unitary invariance of $Z$ from [F2]. For each subset $J \subseteq {1, \dots, d}$ put $λ_{J} = \prod_{i \in J} w_{i} \prod_{i \notin J} (1 - w_{i})$ . These are nonnegative, sum to $\prod_{i} (w_{i} + 1 - w_{i}) = 1$ , and satisfy $\sum_{J ∋ i} λ_{J} = w_{i}$ ; hence the convex combination of indicator vectors is $w$ and its mean cardinality is $\sum_{i} w_{i}$ . Finite Euclidean Jensen [F7] gives $f (w) \leq \sum_{J} λ_{J} f (1_{J})$ . By permutation invariance and step 6.1, $f (1_{J}) = E ∥ P_{∣ J ∣} Z ∥_{2}^{2} \leq h (∣ J ∣)$ for each of the two affine bounds $h (j)$ there. Since $h$ is affine, $f (w) \leq \sum_{J} λ_{J} h (∣ J ∣) = h (\sum_{i} w_{i})$ ; this includes every endpoint $w_{i} = 0$ or $1$ and never uses a row count above $d$ . Finally, left-unitary invariance and the diagonalization of $S^{*} S$ give $E ∥ S Z ∥_{2}^{2} = E ∥ diag (σ \sqrt{w_{i}}) W Z ∥_{2}^{2} = σ^{2} f (w)$ . Substitution of each affine $h$ proves both asserted inequalities.

Depends on

Used by

Direct expected spectral bound for the normalized complex range finder Lemma

Dependency tree · two levels

179 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, §10.1 and Appendix A.1; standard Gaussian block context, with the present normalized-complex estimates derived locally (standard reference, not scraped)
Martinsson and Tropp, Randomized Numerical Linear Algebra: Foundations & Algorithms, §11.4.2; real Gaussian rangefinder context, with the present normalized-complex estimates derived locally (standard reference, not scraped)