Empirical spectral measure

An empirical spectral measure turns the eigenvalues of one finite matrix into one measure on the number line. Every eigenvalue slot receives equal weight, and repeated eigenvalues contribute repeatedly.

For a positive-dimensional \(n\times n\) Hermitian matrix \(H\) with ordered real eigenvalues

first form the spectral counting measure

It has total mass \(n\). Then divide every atom by \(n\):

The result has total mass one when \(n\gt0\). It is therefore a probability measure describing the fraction of eigenvalue slots in any measurable region.

A \(3\times3\) example with a repeated eigenvalue

Take the real diagonal, hence Hermitian, matrix

Its decreasing eigenvalue vector is

The value \(2\) occurs in two different index slots. The spectral counting measure therefore is

Its mass on the whole real line is

Normalize by the number of slots:

Now

Replacing the eigenvalue vector by the set of distinct values \(\{2,-1\}\) would erase the multiplicity at \(2\). It would produce the wrong masses and the wrong moments.

First moment: normalized trace

Integrating the identity function against the counting measure adds all three eigenvalue slots:

For the normalized empirical measure,

The first empirical spectral moment is the average eigenvalue, not the unnormalized trace.

Second moment: normalized trace square

The second counting-measure moment is

Because

this is exactly

Normalize once more:

The example has empirical mean \(1\) and empirical second moment \(3\). Its empirical variance is consequently \(3-1^2=2\), although the current project theorem names only the first two raw moments.

The exact general moment bridge

For any intrinsic \(n\times n\) Hermitian matrix, the project proves

and

The cast into \(\mathbb C\) matches the complex-valued matrix trace. Since all Hermitian eigenvalues are real, this changes the codomain, not the numerical values in the worked example.

The normalized sample moments are

with the project’s zero-dimensional inverse convention included in the Lean theorems.

Ordering is useful even though measures discard order

The sum of Dirac measures is unchanged if the eigenvalue vector is permuted. The project nevertheless starts with a decreasing vector because canonical coordinates support statements about the largest and smallest eigenvalues.

Pinned Mathlib supplies Matrix.IsHermitian.eigenvalues₀ in decreasing order. The project transports that vector to the concrete index type Fin n using an order-preserving cast and proves orderedHermitianEigenvalues_antitone.

Multiplicity survives that ordering. In the example, the first two coordinates both equal \(2\); the measure then adds their two unit atoms at the same real location.

The \(n=0\) policy

At dimension zero, there are no eigenvalue slots. The finite sum defining the counting measure is empty, so

The project defines the empirical measure uniformly as

When \(n=0\), the counting measure is already zero, and scalar multiplication of the zero measure remains zero. Thus

This zero measure has total mass zero, so it is not a probability measure on \(\mathbb R\). The project exposes:

• empiricalSpectralMeasure_isZeroOrProbability in every dimension;
• empiricalSpectralMeasure_succ_isProbability for dimension n + 1; and
• empiricalSpectralProbability n H as a genuine bundled probability measure only in positive dimension.

No artificial eigenvalue at zero is inserted merely to make the empty case look probabilistic.

One realized measure is not its probability law

Suppose now that \(H(\omega)\) is random.

For finite GUE, the project names the distribution GUE.empiricalSpectralLaw n. It is a probability measure on Measure ℝ. In positive dimension it also offers a law valued in ProbabilityMeasure ℝ.

This distinction is especially sharp at \(n=0\):

The realized empirical measure is the zero measure on \(\mathbb R\). Its law is a Dirac probability measure on the space of measures. These live on different spaces and have different total masses.

In Lean: one matrix gives one measure

NonlinearDynamics.Random.RandomMatrix.empiricalSpectralMeasure H

In Lean: the second sample moment is a trace power

NonlinearDynamics.Random.RandomMatrix.empiricalSpectralMoment_two H

In Lean: a random matrix gives a law of measures

NonlinearDynamics.Random.GUE.empiricalSpectralLaw 3

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 authoritative deterministic definitions are in HermitianSpectrum.lean:

noncomputable def spectralCountingMeasure {n : ℕ}
    (H : HermitianEuclidean n) : Measure ℝ :=
  ∑ i, Measure.dirac (orderedHermitianEigenvalues H i)

noncomputable def empiricalSpectralMeasure {n : ℕ}
    (H : HermitianEuclidean n) : Measure ℝ :=
  (n : ℝ≥0∞)⁻¹ • spectralCountingMeasure H

The first line preserves multiplicity because the sum runs over all finite index slots, not over the set of distinct real values. The second line normalizes the complete counting measure.

The exact second counting-moment theorem is:

theorem integral_sq_complex_ofReal_spectralCountingMeasure {n : ℕ}
    (H : HermitianEuclidean n) :
    ∫ x : ℝ, (x : ℂ) ^ 2 ∂spectralCountingMeasure H =
      Matrix.trace ((hermitianToMatrix H) ^ 2) := by
  rw [spectralCountingMeasure]
  rw [integral_finsetSum_measure]
  · simp only [integral_dirac]
    exact (trace_sq_eq_sum_sq_orderedHermitianEigenvalues H).symm
  · intro i _
    exact integrable_dirac (by simp)

The proof expands the finite sum of Dirac measures, evaluates the integral at each atom, and invokes the checked eigenvalue power-sum identity.

The normalized moment layer in GaussianUnitaryEnsembleSpectrum.lean defines:

noncomputable def empiricalSpectralMoment {n : ℕ} (k : ℕ)
    (H : HermitianEuclidean n) : ℂ :=
  ∫ x : ℝ, (x : ℂ) ^ k ∂empiricalSpectralMeasure H

theorem empiricalSpectralMoment_two {n : ℕ} (H : HermitianEuclidean n) :
    empiricalSpectralMoment 2 H =
      (((n : ℕ) : ℝ)⁻¹ : ℂ) * Matrix.trace ((hermitianToMatrix H) ^ 2) := by
  rw [empiricalSpectralMoment, empiricalSpectralMeasure,
    integral_smul_measure, ENNReal.toReal_inv]
  rw [integral_sq_complex_ofReal_spectralCountingMeasure]
  norm_cast

Finally, the law of the random measure is a separate definition:

noncomputable def empiricalSpectralLaw (n : ℕ) : Measure (Measure ℝ) :=
  (intrinsicLaw n).map empiricalSpectralMeasure

The nested type Measure (Measure ℝ) is deliberate: the outer measure describes how the inner realized measures vary.

Standalone tutorial: multiplicity worksheet

Standalone tutorial. This worksheet imports only Std. It calculates the finite eigenvalue ledger using exact rationals. It does not define Dirac measures, diagonalize matrices, or prove the project trace theorems.

Save it as EmpiricalSpectrum3Scratch.lean:

import Std

def eigenvalueSlots : List Rat :=
  [2, 2, -1]

def countingMomentOf (xs : List Rat) (k : Nat) : Rat :=
  xs.foldl (fun total x => total + x ^ k) 0

def empiricalMomentOf (xs : List Rat) (k : Nat) : Rat :=
  match xs with
  | [] => 0
  | _ :: _ => countingMomentOf xs k / (xs.length : Rat)

#eval eigenvalueSlots.length
#eval eigenvalueSlots.count 2
#eval eigenvalueSlots.count (-1)
#eval countingMomentOf eigenvalueSlots 1
#eval empiricalMomentOf eigenvalueSlots 1
#eval countingMomentOf eigenvalueSlots 2
#eval empiricalMomentOf eigenvalueSlots 2
#eval empiricalMomentOf [] 2

Run it with:

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

The outputs should be \(3,2,1,3,1,9,3,0\). The second output is the multiplicity of eigenvalue \(2\); the final output implements the explicit empty-list policy.

Try the exact declarations in the project

import NonlinearDynamics.Random.RandomMatrices.GaussianUnitaryEnsembleSpectrum

#check NonlinearDynamics.Random.RandomMatrix.orderedHermitianEigenvalues
#check NonlinearDynamics.Random.RandomMatrix.orderedHermitianEigenvalues_antitone
#check NonlinearDynamics.Random.RandomMatrix.trace_eq_sum_orderedHermitianEigenvalues
#check NonlinearDynamics.Random.RandomMatrix.trace_sq_eq_sum_sq_orderedHermitianEigenvalues
#check NonlinearDynamics.Random.RandomMatrix.spectralCountingMeasure
#check NonlinearDynamics.Random.RandomMatrix.spectralCountingMeasure_zero
#check NonlinearDynamics.Random.RandomMatrix.spectralCountingMeasure_univ
#check NonlinearDynamics.Random.RandomMatrix.integral_complex_ofReal_spectralCountingMeasure
#check NonlinearDynamics.Random.RandomMatrix.integral_sq_complex_ofReal_spectralCountingMeasure
#check NonlinearDynamics.Random.RandomMatrix.empiricalSpectralMeasure
#check NonlinearDynamics.Random.RandomMatrix.empiricalSpectralMeasure_zero
#check NonlinearDynamics.Random.RandomMatrix.empiricalSpectralMeasure_isZeroOrProbability
#check NonlinearDynamics.Random.RandomMatrix.empiricalSpectralMeasure_succ_isProbability
#check NonlinearDynamics.Random.RandomMatrix.empiricalSpectralProbability
#check NonlinearDynamics.Random.RandomMatrix.measurable_empiricalSpectralMeasure
#check NonlinearDynamics.Random.RandomMatrix.empiricalSpectralMoment
#check NonlinearDynamics.Random.RandomMatrix.empiricalSpectralMoment_zero
#check NonlinearDynamics.Random.RandomMatrix.empiricalSpectralMoment_one
#check NonlinearDynamics.Random.RandomMatrix.empiricalSpectralMoment_two
#check NonlinearDynamics.Random.GUE.empiricalSpectralLaw
#check NonlinearDynamics.Random.GUE.empiricalSpectralLaw_zero
#check NonlinearDynamics.Random.GUE.meanEmpiricalSpectralMeasure
#check NonlinearDynamics.Random.GUE.meanEmpiricalSpectralMeasure_zero
#check NonlinearDynamics.Random.GUE.empiricalSpectralLaw_eq_map_matrixLaw_ambient

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

Measurability is the bridge to a distribution

The formula for \(\mu_H\) makes sense pointwise before any probability space is introduced. To push a matrix law through

the map must also be measurable into the space of measures carrying Mathlib’s Giry measurable structure.

The project proves a Frobenius-norm Weyl perturbation bound for ordered Hermitian eigenvalues, deduces continuity and coordinatewise measurability, and then proves measurable_empiricalSpectralMeasure. Only after that bridge is available does the pushforward law become an unconditional checked object.

This separates two questions:

1. Algebraic: what measure does a fixed matrix produce?
2. Probabilistic: can a random matrix law be pushed through that map?

A correct pointwise formula does not automatically answer the second question.

Unitary basis changes preserve the realized measure

For a unitary matrix \(U\), intrinsic congruence sends

The project proves the complete ordered eigenvalue vector unchanged, and therefore proves

This is a deterministic statement for each \(H\) and \(U\). It is different from unitary invariance of a random matrix law, although the two facts work together in GUE.

Distinctions and failure modes

Exercises

1. Replace the example by \(H=\operatorname{diag}(3,3,-2,-2)\). Compute \(\kappa_H(\{3\})\), \(\mu_H(\{3\})\), and both first two empirical moments.
2. Verify directly that permuting \((2,2,-1)\) leaves the sum of Dirac measures unchanged.
3. Explain why \(\delta_0\) is the law of the zero empirical measure at \(n=0\), while it is not the zero empirical measure itself.
4. Draw the carrier types for \(H\), \(\mu_H\), \(\mathcal L(\mu_H)\), and \(\mathbb E[\mu_H]\).

Where to continue

Finite Hermitian Spectra and Empirical Measures develops the ordered spectrum, multiplicity, counting measure, normalization, ambient totalization, and zero boundary in textbook detail. Hermitian Spectral Perturbation, Continuity, and Measurability proves the Weyl bound that turns this pointwise observable into a measurable map.

Finite Gaussian Unitary Ensemble Empirical Spectral Laws and Normalized Moments continues from one realized measure to its GUE distribution, Giry mean, and first two expected normalized moments. Read empirical spectral law for the outer probability law and finite matrix trace moment for the earlier ordinary-trace expectation layer.

References

Mathlib contributors. Spectral theory of Hermitian matrices, Mathlib 4 documentation. This official page defines the decreasingly sorted Hermitian eigenvalue vector and supplies the finite spectral theorem used by the project.

Mathlib contributors. Dirac measure and probability measures, Mathlib 4 documentation. These APIs underlie the finite atomic sum and the positive-dimensional probability wrapper.

Mathlib contributors. The Giry measurable structure on measures, Mathlib 4 documentation. This is the measure-space structure used when an empirical measure itself becomes a random output.

Terence Tao, Van Vu, with an appendix by Manjunath Krishnapur. Random matrices: Universality of ESDs and the circular law, The Annals of Probability 38 (2010), 2023-2065. This primary paper uses the normalized empirical spectral distribution convention for general complex matrices. Its non-Hermitian asymptotic results are context, not project theorems.

Nonlinear Dynamics in Lean contributors. HermitianSpectrum.lean, HermitianSpectrumContinuity.lean, and GaussianUnitaryEnsembleSpectrum.lean, the checked project sources for finite spectra, measure-valued measurability, random spectral laws, and normalized moments.

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