Alphabeta MathHow 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.
Normalization and second moments of the Gaussian matrix laws
Statement
Assume Countable Choice. The scalar and finite product densities in Standard real and normalized complex Gaussian matrix laws have total mass one. A real entry has mean zero and second moment one; a normalized complex entry has mean zero and . The image of two independent real entries under has density . These facts justify the probability laws in that definition.
Facts & Assumptions
Given: Countable Choice and the displayed density formulas in the Gaussian-law definition, initially regarded simply as functions.
Countable Choice supplies complete Euclidean Lebesgue measures with half-open-box volumes, and Borel sets are measurable. Assuming countable choice, is a sigma-algebra containing every elementary set and is a complete measure extending elementary volume Assuming countable choice, every Borel subset of is Lebesgue measurable
For supplied countably additive Borel length measures with these interval volumes, the real density has mass one, absolutely integrable mean zero, and second moment one. Gaussian density integrals for supplied length measures
Invertible real linear maps scale Lebesgue measure by the absolute determinant. A linear map of sends Lebesgue measurable sets to Lebesgue measurable sets, with when is invertible and Lebesgue null when it is not
Euclidean Lebesgue measure agrees on Borel sets with the product of its coordinate measures; Tonelli applies to nonnegative product-measurable functions on sigma-finite spaces. On Borel subsets of R^{m+n}, the product lambda_m times lambda_n agrees with lambda_{m+n} Tonelli's theorem for nonnegative measurable functions on a sigma-finite product
Increasing nonnegative measurable functions commute with integration. Monotone convergence for the integral
Proof
Restrict the measures in [F1] to Borel sets in dimensions one and two. They meet exactly the supplied-measure hypotheses of [F2]. With location zero and variance one, [F2] gives real mass one, mean zero, absolute first-moment integrability, and second moment one. No normal-law result assuming full Choice is used.
The map has determinant . By [F3], the image density is . The integral transformation follows first for indicator functions from [F3], then for simple functions and their increasing limits. Its mass is one by step 1.1 and [F4]. By the same product integration, , and both real and imaginary means vanish; their absolute integrability follows from that of .
For any positive finite number of entries, repeated [F4] factors the integral of the nonnegative Borel product density into scalar integrals, each one. All coordinate spaces are sigma-finite, being countable unions of bounded boxes. Integrating over a product of Borel entry sets similarly gives the product of their scalar probabilities, which establishes independence. The integral of the density over sets defines a countably additive probability measure: for disjoint sets, the finite sums of their density-weighted indicators increase to the density times the indicator of their union, so monotone convergence, by [F5], gives countable additivity. For zero entries use the one-point space of mass one and the empty product. Thus all finite laws in the definition are justified using only the stated Countable Choice.
Depends on
- Standard real and normalized complex Gaussian matrix laws
- Gaussian density integrals for supplied length measures
- Assuming countable choice, $\mathcal{L}(\mathbb{R}^n)$ is a sigma-algebra containing every elementary set and $\lambda_n$ is a complete measure extending elementary volume
- Assuming countable choice, every Borel subset of $\mathbb{R}^n$ is Lebesgue measurable
- A linear map $T$ of $\mathbb{R}^n$ sends Lebesgue measurable sets to Lebesgue measurable sets, with $\lambda_n(T[E])=|\det T|\,\lambda_n(E)$ when $T$ is invertible and $T[E]$ Lebesgue null when it is not
- On Borel subsets of R^{m+n}, the product lambda_m times lambda_n agrees with lambda_{m+n}
- Tonelli's theorem for nonnegative measurable functions on a sigma-finite product
- Monotone convergence for the integral
Used by
- Squared-norm concentration for real and normalized complex Gaussians Lemma
- Gaussian sketches embed a fixed subspace at the additive dimension rate Theorem
Cited to discharge well-definedness by Standard real and normalized complex Gaussian matrix laws.
Dependency tree · two levels
85 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.