TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Orthogonal transformations preserve the standard normal product law

Statement

Assume the Axiom of Choice. Let $n \geq 1$ , let $Z \sim N_{n} (0, I_{n})$ have independent standard-normal coordinates, and let $U \in R^{n \times n}$ satisfy $U^{T} U = I_{n}$ . Then $U Z$ also has independent $N (0, 1)$ coordinates. Here $I_{n}$ is the identity matrix and $U$ is orthogonal.

Facts & Assumptions

Given: The Axiom of Choice, $Z \sim N_{n} (0, I_{n})$ with independent standard-normal coordinates, and an orthogonal matrix $U$ .

[A1]

The Axiom of Choice is assumed; the multivariate-normal characteristic-function and finite-Borel uniqueness suppliers below state this use explicitly. The Axiom of Choice

[A2]

The Axiom of Choice implies Countable Choice, the stated hypothesis of the continuous-map measurability and Fourier-transform suppliers. The Axiom of Countable Choice ( ${A C}_{ω}$ ) The Axiom of Choice implies countable choice

[F1]

The law $N_{n} (m, Σ)$ is the Borel law with all linear projections normal; for $Σ = I_{n}$ it is realized by independent standard-normal coordinates. Multivariate normal law, including singular covariance

[F2]

Under the Axiom of Choice, the characteristic function of $N_{n} (m, Σ)$ is $\exp (i t \cdot m - t^{T} Σ t / 2)$ . Characteristic function of a multivariate normal law

[F3]

Under Countable Choice, the Fourier transform of a finite complex Borel measure on $R^{n}$ is $\hat{μ} (ξ) = \int e^{- 2 π i x \cdot ξ} d μ (x)$ ; for the law of a Borel random vector its vector characteristic function is $E e^{i t \cdot X}$ , and substituting $ξ = - t / (2 π)$ identifies the two transforms. Fourier transform of a finite complex Borel measure Characteristic function of a multivariate normal law

[F4]

Under the Axiom of Choice, finite complex Borel measures on $R^{n}$ with equal Fourier transforms are equal. Uniqueness of finite Borel measures from their Fourier transforms

[F5]

Under Countable Choice, continuous maps between Euclidean spaces are Borel measurable, and a Borel random vector has a law by pushforward. Continuous functions on Euclidean spaces are Borel measurable Law or distribution of a random element

Proof

Given: The hypotheses in the Statement.

1.1A1A2F1F2F5algebra

Since $U^{T} U = I_{n}$ and $U$ is square, $U$ is invertible with inverse $U^{T}$ , so $U U^{T} = I_{n}$ . By [A2], Countable Choice holds. The continuous map $x \mapsto U x$ is Borel measurable by [F5], so $(U Z)^{- 1} (B) = Z^{- 1} (U^{- 1} (B))$ is measurable for every Borel $B \subseteq R^{n}$ . Thus $U Z$ is a Borel random vector and has a law by [F5]. For each $t \in R^{n}$ , [F1]–[F2] give $E e^{i t^{T} U Z} = \exp (- ∥ U^{T} t ∥^{2} / 2) = \exp (- ∥ t ∥^{2} / 2) = E e^{i t^{T} Z}$ ; the middle equality follows from $U U^{T} = I_{n}$ .

2.1step 1.1A2F3F4F5

By [A2] and [F3], the equality in step 1.1 at every $t$ is equality of the finite Borel Fourier transforms of the laws of $U Z$ and $Z$ . Both are probability measures, hence have finite total variation; [F4] therefore gives $L (U Z) = L (Z)$ .

3.1F1step 2.1∎

By [F1], the coordinates of $Z$ are independent standard normals. Equality of joint laws in step 2.1 makes the coordinate law of $U Z$ the same product law, so its coordinates are again independent $N (0, 1)$ . This use of orthogonality depends on the Gaussian product law; no claim is made for arbitrary independent coordinates.

Depends on

Used by

Dependency tree · two levels

45 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

Dmitry Panchenko, MIT 18.443 Statistics for Applications, Fall 2006, Lecture 4 (standard reference, not scraped)
Yen-Chi Chen, UW STAT 512 Lecture 8: Linear Models and Multivariate Normal Distributions (standard reference, not scraped)