Gaussian unitary ensemble

The Gaussian unitary ensemble, or GUE, is a probability law on finite complex Hermitian matrices .

Each word names a different part of the definition:

• Gaussian: the freely chosen real scalar coordinates have Gaussian laws;
• unitary: changing basis by a deterministic unitary matrix does not change the matrix law; and
• ensemble: the object is a probability measure over matrices, not one particular matrix.

Those three facts do not follow from one another. This repository constructs the coordinate law, pushes it through Hermitian assembly, proves concentration on the Hermitian locus, proves unitary-conjugation invariance, and then proves the first two finite trace and empirical spectral moments in separate modules.

The entire \(n=2\) construction

For dimension \(n=2\), the repository’s Wigner variance scale is

Choose four centered real Gaussian variables:

with all four primitive real coordinates independent. Here the second parameter of \(N(m,v)\) is the variance, not the standard deviation.

The two diagonal variables use variance \(s_2=1/2\). The real and imaginary parts of the one strict-upper entry use half that variance:

Set

and assemble

This matrix is Hermitian for every coordinate outcome. Randomness chooses \(a,d,x,y\); conjugate reflection determines the lower-left entry.

The upper entry has total squared-magnitude expectation

The factor \(1/4\) on each Cartesian component is therefore essential. Giving both \(x\) and \(y\) variance \(1/2\) would double the intended off-diagonal energy.

Compute \(\mathbb E\,\operatorname{Tr}(H)\)

The trace reads only the diagonal:

Both coordinates are centered, so linearity of expectation gives

No eigenvalue calculation is needed for this first trace moment.

Compute \(\mathbb E\,\operatorname{Tr}(H^2)\)

Multiplying the matrix by itself gives diagonal entries

Therefore

For a centered real random variable, its second moment equals its variance. Substitute the four variance entries:

The doubled off-diagonal term is geometric, not an extra random coordinate. Both \(H_{01}H_{10}=|z|^2\) and \(H_{10}H_{01}=|z|^2\) enter the trace of the square.

Why the normalized spectral second moment is one

Let \(\lambda_1,\lambda_2\in\mathbb R\) be the eigenvalues of \(H\). Its empirical spectral measure is

The second moment of this one sample measure is

Taking the ensemble expectation gives

The normalization occurs at a precise place: the empirical measure divides the spectral counting measure by the number of eigenvalues. The ordinary matrix trace itself is not normalized.

The repository proves this finite identity in every positive dimension, not only at \(n=2\).

The same count for every positive dimension

For \(n\gt0\), there are \(n\) diagonal entries with variance \(1/n\), and \(\binom n2\) strict-upper entries with expected squared magnitude \(1/n\). Since each upper entry appears twice in \(\operatorname{Tr}(H^2)\),

Consequently,

This exact finite calculation explains one purpose of Wigner scaling: the average squared eigenvalue stays of order one as dimension changes.

Six layers that must not be collapsed

The Hermitian-set theorem is a measure-one statement. It should not be silently strengthened to a theorem that the topological support is exactly the entire Hermitian space.

Likewise, unitary invariance is an equality of full matrix probability laws. It is stronger than saying that individual entries have symmetric marginal distributions, and it is separate from Hermitian-locus concentration.

The project normalization ledger

The acronym GUE is not enough to recover scale conventions. This project uses:

For a strict-upper entry,

so

The component variance \(1/(2n)\), the complex squared-magnitude expectation \(1/n\), and the normalized spectral second moment \(1\) are three different quantities.

In Lean: name the coordinate law

NonlinearDynamics.Random.GUE.coordinateMeasure 2

In Lean: ask for the exact second trace moment

NonlinearDynamics.Random.GUE.integral_tracePower_two 2

The first trace theorem is the parallel declaration GUE.integral_tracePower_one 2, whose right side is zero.

In Lean: ask for the normalized spectral moment

NonlinearDynamics.Random.GUE.integral_empiricalSpectralMoment_two_succ 1

Exact project excerpts

Full project check. This uses the repository’s pinned Lean and Mathlib dependencies and may require substantial disk space and memory. The scale functions in GaussianUnitaryEnsemble.lean are:

noncomputable def varianceScale : ℕ → ℝ≥0
  | 0 => 0
  | n + 1 => (((n + 1 : ℕ) : ℝ≥0))⁻¹

noncomputable def diagonalVariance (n : ℕ) : ℝ≥0 := varianceScale n

noncomputable def upperCartesianVariance (n : ℕ) : ℝ≥0 := varianceScale n / 2

The coordinate and matrix measures are then defined exactly as follows:

noncomputable def coordinateMeasure (n : ℕ) : Measure (HermitianCoordinateSpace n) :=
  (gaussianProductMeasure (fun _ : Fin n => 0) (fun _ => diagonalVariance n)).prod
    (cartesianComplexGaussianProductMeasure
      (fun _ : StrictUpperIndex n => 0)
      (fun _ => upperCartesianVariance n)
      (fun _ => upperCartesianVariance n))

noncomputable def matrixLaw (n : ℕ) :
    Measure (Matrix (Fin n) (Fin n) ℂ) :=
  RandomMatrix.law (RandomMatrix.hermitianCoordinateMap n)
    (RandomMatrix.measurable_hermitianCoordinateMap n) (coordinateMeasure n)

The first definition builds the exact joint law of the free coordinates. The second applies the measurable deterministic assembly map. Neither definition mentions eigenvalues or unitary invariance.

The positive-dimensional spectral normalization theorem in GaussianUnitaryEnsembleSpectrum.lean is short:

@[simp] theorem integral_empiricalSpectralMoment_two_succ (n : ℕ) :
    ∫ H, empiricalSpectralMoment 2 H ∂intrinsicLaw (n + 1) = 1 := by
  rw [integral_empiricalSpectralMoment_two]
  norm_cast
  exact inv_mul_cancel₀ (by positivity)

It rewrites with the all-dimensions formula \(n^{-1}n\), then uses positivity of \(n+1\) to cancel the reciprocal. This proof is the formal endpoint of the worked \(n=2\) calculation.

Standalone tutorial: moment ledger

Standalone tutorial. This worksheet imports only Std and evaluates the rational arithmetic in the size-two example. It is not a random-variable construction and supplies no Gaussian law, independence, matrix-support, invariance, or spectral theorem.

Save it as GUE2MomentLedgerScratch.lean:

import Std

structure GUE2Ledger where
  meanA : Rat
  meanD : Rat
  meanX : Rat
  meanY : Rat
  varA : Rat
  varD : Rat
  varX : Rat
  varY : Rat
deriving Repr

def scalarSecondMoment (mean variance : Rat) : Rat :=
  variance + mean ^ 2

def expectedTrace (L : GUE2Ledger) : Rat :=
  L.meanA + L.meanD

def expectedTraceSq (L : GUE2Ledger) : Rat :=
  scalarSecondMoment L.meanA L.varA
    + scalarSecondMoment L.meanD L.varD
    + 2 * (scalarSecondMoment L.meanX L.varX
      + scalarSecondMoment L.meanY L.varY)

def expectedNormalizedSecond (L : GUE2Ledger) : Rat :=
  expectedTraceSq L / 2

def wignerGUE2 : GUE2Ledger :=
  { meanA := 0, meanD := 0, meanX := 0, meanY := 0
    varA := (1 : Rat) / 2
    varD := (1 : Rat) / 2
    varX := (1 : Rat) / 4
    varY := (1 : Rat) / 4 }

#eval expectedTrace wignerGUE2
#eval expectedTraceSq wignerGUE2
#eval expectedNormalizedSecond wignerGUE2

Run it with:

elan run leanprover/lean4:v4.32.0 lean GUE2MomentLedgerScratch.lean

The exact rational outputs should be \(0\), \(2\), and \(1\). The worksheet checks only the displayed moment ledger. The project declarations below carry the measure-theoretic and spectral content.

Try the exact declarations in the project

import NonlinearDynamics.Random.RandomMatrices.GaussianUnitaryEnsembleSpectrum

#check NonlinearDynamics.Random.GUE.varianceScale
#check NonlinearDynamics.Random.GUE.varianceScale_zero
#check NonlinearDynamics.Random.GUE.varianceScale_succ
#check NonlinearDynamics.Random.GUE.diagonalVariance
#check NonlinearDynamics.Random.GUE.upperCartesianVariance
#check NonlinearDynamics.Random.GUE.coordinateMeasure
#check NonlinearDynamics.Random.GUE.coordinateMeasure_diagonal_hasLaw
#check NonlinearDynamics.Random.GUE.coordinateMeasure_upper_hasLaw
#check NonlinearDynamics.Random.GUE.coordinateMeasure_diagonal_iIndepFun
#check NonlinearDynamics.Random.GUE.coordinateMeasure_upper_iIndepFun
#check NonlinearDynamics.Random.GUE.matrixLaw
#check NonlinearDynamics.Random.GUE.matrixLaw_diagonal_hasLaw
#check NonlinearDynamics.Random.GUE.matrixLaw_upper_hasLaw
#check NonlinearDynamics.Random.GUE.coordinateMeasure_zero
#check NonlinearDynamics.Random.GUE.matrixLaw_zero
#check NonlinearDynamics.Random.GUE.matrixLaw_hermitianSet
#check NonlinearDynamics.Random.GUE.matrixLaw_isUnitaryConjugationInvariant
#check NonlinearDynamics.Random.GUE.integral_tracePower_one
#check NonlinearDynamics.Random.GUE.integral_tracePower_two
#check NonlinearDynamics.Random.RandomMatrix.empiricalSpectralMoment_two
#check NonlinearDynamics.Random.GUE.integral_empiricalSpectralMoment_two
#check NonlinearDynamics.Random.GUE.integral_empiricalSpectralMoment_two_succ

cd formalization
lake env lean -DwarningAsError=true NonlinearDynamics/Random/RandomMatrices/GaussianUnitaryEnsembleSpectrum.lean

Dimension zero and positive dimension are different

At \(n=0\), the project does not evaluate an informal \(1/0\). Instead:

• varianceScale 0 = 0 by its own definition branch;
• the coordinate law is Dirac at the unique empty coordinate point;
• the ambient matrix law is Dirac at the unique empty matrix;
• the intrinsic Hermitian law is also Dirac at its zero element;
• the zero-aware empirical spectral measure is the zero measure; and
• every empirical spectral moment is zero.

The raw law of empirical spectral measures is still a probability law: it is Dirac at the zero measure. But the zero empirical measure itself has total mass zero, so it is not a probability measure on \(\mathbb R\).

For \(n\gt0\), the empirical spectral measure has mass one and its expected second moment is one. The formal statement records that boundary explicitly:

Physics meaning without overclaiming

In quantum mechanics, a finite Hamiltonian is Hermitian so its measured energies are real. Replacing a basis by a unitary matrix sends

A unitary-invariant ensemble assigns the same law before and after that basis change. This is why the word unitary describes a symmetry class rather than the claim that the random matrix \(H\) is itself unitary.

Dyson’s unitary class models systems where the relevant antiunitary time-reversal symmetry is absent. GUE is an idealized reference model for spectral statistics, not a claim that every physical Hamiltonian has independent Gaussian entries in every basis.

The finite identity \(\mathbb E[n^{-1}\operatorname{Tr}(H^2)]=1\) says that the average squared eigenvalue is normalized. It does not prove a semicircle law, concentration, level repulsion, universality, or any large-\(n\) limit.

Distinctions and failure modes

Where to continue

Finite GUE from Independent Gaussian Coordinates builds the product law and explains every independence scope. From Normalized Hermitian Coordinates to Gaussian Unitary Ensemble Invariance proves the bridge from entry coordinates to isotropic Hermitian Gaussian geometry and then to unitary invariance.

First Exact Finite Gaussian Unitary Ensemble Trace Moments develops the integrability and first two trace calculations. Finite Gaussian Unitary Ensemble Empirical Spectral Laws and Normalized Moments continues from traces to zero-aware empirical spectral measures and their normalized expected moments.

Read Hermitian coordinate space for the deterministic assembly, unitary invariance for the law symmetry, and empirical spectral law for the measure-valued spectral layer.

References

Alice Guionnet. Rare Events in Random Matrix Theory, in Proceedings of the International Congress of Mathematicians 2022, volume 2, European Mathematical Society Press, 2022, pp. 1008-1052. Section 1.1.1 states the GUE entry variances \(1/n\) and \(1/(2n)\), the conventional density, and unitary invariance.

Freeman J. Dyson. Statistical Theory of the Energy Levels of Complex Systems. I, Journal of Mathematical Physics 3 (1962), 140-156. This primary source develops the orthogonal, unitary, and symplectic symmetry classes and their physical motivation.

Terence Tao. Topics in Random Matrix Theory, Graduate Studies in Mathematics 132, American Mathematical Society, 2012. This monograph develops finite Wigner-scaled ensembles and their spectral context. Its asymptotic results are context, not formalized claims here.

Mathlib contributors. Gaussian distributions over the reals and Hermitian matrices, Mathlib 4 documentation. These official APIs underlie the coordinate laws and Hermitian matrix statements.

Nonlinear Dynamics in Lean contributors. GaussianUnitaryEnsemble.lean, GaussianUnitaryEnsembleInvariance.lean, GaussianUnitaryEnsembleMoments.lean, and GaussianUnitaryEnsembleSpectrum.lean, the checked project sources for construction, symmetry, trace moments, and normalized spectral moments.

The upstream Mathlib revision audited for this entry is commit 81a5d257, pinned by formalization/lake-manifest.json.