LemmaStatement: 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.

Uncorrelated jointly Gaussian blocks are independent

Statement

Assume the Axiom of Choice. Let $(U, V)$ be a jointly multivariate-normal real vector with finite-dimensional blocks $U \in R^{p}$ and $V \in R^{q}$ , where $p, q \geq 1$ . If $Cov (U_{i}, V_{j}) = 0$ for every $1 \leq i \leq p$ and $1 \leq j \leq q$ , then $U$ and $V$ are independent. The covariance matrix may be singular.

Facts & Assumptions

Given: AC, jointly multivariate-normal finite real vectors $U, V$ with $p, q \geq 1$ , and zero cross-covariance between every coordinate of $U$ and every coordinate of $V$ .

[A1]

The Axiom of Choice is assumed by the finite-dimensional Gaussian-law construction and its uniqueness result. The Axiom of Choice

[F1]

A law $N_{d} (m, Σ)$ is determined by its scalar normal projections, allows singular $Σ$ , and has a realization $m + Σ^{1 / 2} W$ with independent standard-normal coordinates. Multivariate normal law, including singular covariance

[F2]

Every finite-dimensional positive-semidefinite operator has a unique positive-semidefinite square root. A non-negative operator has a unique non-negative square root

[F3]

A finite independent family of random elements has product joint law; this gives independence of disjoint coordinate blocks of an independent coordinate vector. Independent random elements have product joint law

[F4]

Measurable functions applied separately to independent random elements preserve their independence. Measurable coordinatewise functions preserve independence

[F5]

The characteristic function of a multivariate-normal vector is $\exp (i t^{T} m - t^{T} Σ t / 2)$ and uniquely determines its law, including for singular covariance. Characteristic function of a multivariate normal law

[F6]

Random elements are independent exactly when probabilities of all measurable rectangles factor. Independent random elements are characterized by finite rectangle probabilities

Proof

1.1givenF2

Write the mean and covariance of $(U, V)$ in block form as $(m_{U}, m_{V})$ and $Σ = diag (Σ_{U}, Σ_{V})$ ; the off-diagonal blocks vanish by hypothesis and each diagonal block is positive semidefinite as a principal block of $Σ$ . Let $A_{U}, A_{V}$ be their positive-semidefinite square roots and put $A = diag (A_{U}, A_{V})$ . Then $A$ is positive semidefinite, $A^{2} = Σ$ , and [F2] identifies it with the unique positive-semidefinite square root of $Σ$ .

2.1A1F1F3F4F6step 1.1

By [F1], the joint law has a realization $(m_{U} + A_{U} W_{U}, m_{V} + A_{V} W_{V})$ with independent standard-normal coordinates in $W_{U}, W_{V}$ . By [F3] the full coordinate vector has product law, so rectangles in the two coordinate blocks factor into their block marginals; [F6] gives block independence. Applying [F4] to the separate block-affine maps preserves independence.

3.1A1F5F6step 2.1∎

The realization in step 2.1 and the original vector have the same multivariate-normal law by [F5]. Their joint and marginal rectangle probabilities therefore agree; the factorization established in step 2.1 transfers to the original pair, and [F6] gives independence. AC is used only through the Gaussian-law construction and uniqueness suppliers.

Depends on

Used by

Dependency tree · two levels

30 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

Rick Durrett, Probability: Theory and Examples, 5th ed., Section 3.10 (standard reference, not scraped)
J. R. Norris, Probability and Measure, Sections 8.1–8.2 (standard reference, not scraped)