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.

Jointly Gaussian blocks with zero cross-covariance are independent, including singular blocks

Statement

Assume AC. Let $(U_{1}, U_{2})$ be a jointly multivariate-normal vector with mean $(m_{1}, m_{2})$ and covariance $(\begin{array}{cc} S & 0 \\ 0 & T \end{array}),$ where $S$ and $T$ are allowed to be singular positive-semidefinite matrices. Then the random vectors $U_{1}$ and $U_{2}$ are independent.

Facts & Assumptions

Given: AC and a finite-dimensional jointly Gaussian vector with the block covariance in the Statement.

[F1]

A multivariate-normal law with positive-semidefinite covariance exists, may be realized as its mean plus the covariance square root times independent standard-normal coordinates, and allows singular covariance. Multivariate normal law, including singular covariance.

[F2]

The nonnegative square root of a finite-dimensional nonnegative operator exists and is unique. A non-negative operator has a unique non-negative square root.

[F3]

Disjoint groups of an independent sigma-algebra family remain independent. Disjoint groups of an independent sigma-algebra family remain independent.

[F4]

Measurable functions of independent random elements remain independent. Measurable coordinatewise functions preserve independence.

[F5]

The multivariate-normal characteristic function uniquely determines its law, including for singular covariance. Characteristic function of a multivariate normal law.

[A1]

AC holds for the multivariate-normal construction. The Axiom of Choice.

Proof

Given: The hypotheses in the Statement.

1.1F2algebra

Let $S^{1 / 2}$ and $T^{1 / 2}$ be the nonnegative square roots from [F2]. The block matrix $A = diag (S^{1 / 2}, T^{1 / 2})$ is nonnegative and satisfies $A^{2} = diag (S, T)$ , so uniqueness in [F2] makes $A$ the nonnegative square root of the joint covariance. This argument also applies when either block is singular.

2.1A1F1F3F4step 1.1

By [A1] and [F1], the joint law is the law of $(m_{1}, m_{2}) + A Z$ for a vector $Z$ with independent standard-normal coordinates. Partition those coordinates into vectors $Z_{1}, Z_{2}$ of the matching dimensions. Their sigma-algebras are independent by [F3], and the separate affine maps $m_{1} + S^{1 / 2} Z_{1}$ and $m_{2} + T^{1 / 2} Z_{2}$ remain independent by [F4]. Hence the coordinate blocks of the constructed vector are independent.

3.1A1F5step 2.1∎

Any jointly multivariate-normal vector with the stated mean and covariance has this constructed law by the uniqueness clause of [F5]. Independence is a property of the joint law, so $U_{1}$ and $U_{2}$ are independent.

Remarks

No inverse of $S$ or $T$ is used. Positive definiteness of the full covariance is not required for this independence result.

Depends on

Used by

Dependency tree · two levels

32 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

Fan Li, STA610 Lecture 4: Maximum Likelihood Estimation and Inference for the Hierarchical Normal Model, PDF p. 3 (standard reference, not scraped)
Duchateau, Janssen, and Rowlands, Linear Mixed Models, Chapter 2 §2.4.3 and Appendix D (standard reference, not scraped)