Finite Hermitian Spectra and Empirical Measures

Begin with one matrix you can finish by hand

Take the real symmetric, hence complex Hermitian, matrix

Hermitian means \(H^*=H\), where \(^*\) is conjugate transpose. Here every entry is real and the two off-diagonal entries agree, so that check is visible without a theorem prover.

An eigenpair is a scalar \(\lambda\) and a nonzero vector \(v\) satisfying \(Hv=\lambda v\). Two direct multiplications give

The characteristic polynomial confirms that there are no other eigenvalue slots:

The project’s ordered convention is decreasing, so the exact ordered spectrum is

This vector keeps two slots, not merely a set of distinct values. If an eigenvalue repeats, it repeats in the vector. That is how algebraic multiplicity survives the next construction.

Place one atom at each slot

The Dirac measure \(\delta_x\) is the particular measure that puts unit mass at the single point \(x\). The spectral counting measure of our matrix is therefore

It has total mass two. Divide by the number of eigenvalue slots to obtain the empirical spectral measure

Here is the measure atom by atom. A singleton \(\{x\}\) asks how much mass is located exactly at \(x\).

Two power-sum checks tie the atoms back to the entries:

and, since

we have

A near-miss in reconstruction: the spectrum forgets the basis

Now compare \(H\) with the diagonal matrix

Both matrices are Hermitian. Both have the same decreasing ordered spectrum \((3,1)\), hence the same counting measure and empirical measure:

Yet the matrices are not equal. For example, \(H_{01}=1\) while \(D_{01}=0\). Their displayed eigenvectors are different too: the standard basis diagonalizes \(D\), whereas the diagonal directions \((1,1)\) and \((1,-1)\) diagonalize \(H\). In fact,

This is not a failure of spectral theory. The spectrum is deliberately basis-independent. It records energy levels and multiplicities while forgetting the coordinate basis and eigenvectors. Therefore no theorem should try to reconstruct arbitrary matrix entries from \(L_H\) alone.

Five objects that the phrase “spectral distribution” can hide

The running matrix has now produced a vector and a measure without any probability experiment. Randomness adds more layers, each with a different type.

The second and fifth rows share the Lean type Measure ℝ, but they are not the same construction. The second belongs to one realized matrix. The fifth averages over an outer law and forgets sample-to-sample variation. Likewise, the third row is a function; it is not itself the fourth row’s probability measure.

For finite Gaussian unitary ensemble (GUE) matrices, the repository now has all five layers, but not in one source file:

• RMT-10A, HermitianSpectrum.lean, defines the first three objects and proves law transport only under an explicit coordinatewise eigenvalue-measurability hypothesis.
• RMT-10B, HermitianSpectrumContinuity.lean, proves the ordered coordinates are 1-Lipschitz, continuous, and measurable, then removes that hypothesis from the measure-valued interfaces.
• RMT-10C, GaussianUnitaryEnsembleSpectrum.lean, defines GUE.empiricalSpectralLaw and GUE.meanEmpiricalSpectralMeasure and proves their finite zero/positive-dimensional facts.

The empty-size boundary

At \(n=0\), there are no eigenvalue slots. RMT-10A defines both the counting measure and empirical measure to be zero:

The inner zero measure is not a probability measure because its total mass is zero. Nevertheless, RMT-10C’s outer law at size zero is the probability measure \(\delta_0\) on the space Measure ℝ: it puts all outer mass on the single sample measure \(0\). Its mean measure is again zero. This is a useful type test: a probability law may be concentrated on an object that is not itself a probability measure.

Choose a route up

Learning objectives

By the summit, you should be able to compute the running example without a black box, explain multiplicity and unitary invariance, distinguish all five typed objects above, defend the \(n=0\) policy, read seven Lean interfaces token by token, and state exactly which claims belong to RMT-10A, RMT-10B, and RMT-10C. You should also be able to name what is absent: no joint eigenvalue density, semicircle law, large-dimension convergence, rigidity, local spacing limit, spectral form factor, or out-of-time-order correlator is proved here.

In Lean: seven bridges from one spectrum to a law

The numeric worksheet later in the chapter checks the size-two arithmetic using only Std. The interfaces in this section are different: they are full project checks of exact Mathlib-backed declarations. Install the repository’s pinned dependencies first; these checks may require substantial disk space and memory.

Bridge one: the ordered spectrum is a function on finite slots

RandomMatrix.orderedHermitianEigenvalues H : Fin n → ℝ

For the running matrix, a human writes \(\Lambda(H)=(3,1)\). The project definition generalizes the slot structure, while our direct eigenvector certificates establish the two concrete values.

Bridge two: trace is the first ordered power sum

RandomMatrix.trace_eq_sum_orderedHermitianEigenvalues H

At size two these statements read \(4=3+1\) and \(10=3^2+1^2\). They are pointwise algebraic identities, not expectations.

Bridge three: counting measure means one Dirac mass per slot

RandomMatrix.spectralCountingMeasure H : Measure ℝ

For the running spectrum, the definition unfolds to \(\delta_3+\delta_1\). If the spectrum were \((3,3)\), the result would be \(2\delta_3\), not \(\delta_3\).

Bridge four: empirical means normalize the slot count

RandomMatrix.empiricalSpectralMeasure H : Measure ℝ

For our matrix, the dimension is two, so each unit counting atom becomes an empirical atom of mass one half.

Bridge five: measurability belongs to the whole observable

RandomMatrix.measurable_empiricalSpectralMeasure : Measurable (@RandomMatrix.empiricalSpectralMeasure n)

This is a current project theorem, but it belongs to HermitianSpectrumContinuity.lean, not to the base RMT-10A module.

Bridge six: a random spectral law is an outer measure

GUE.empiricalSpectralLaw n : Measure (Measure ℝ)

This named unconditional law first appears in RMT-10C. RMT-10A’s strongest law statement is only the conditional equality between ambient and intrinsic pushforward routes.

Bridge seven: joining the outer law gives one mean measure

GUE.meanEmpiricalSpectralMeasure n = (GUE.empiricalSpectralLaw n).join

The displayed equality is the body of the RMT-10C definition. It does not by itself prove a density, an interchange of arbitrary integrals, or an asymptotic limit.

Try the exact RMT-10A declarations in the repository

import NonlinearDynamics.Random.RandomMatrices.HermitianSpectrum

open Matrix MeasureTheory
open scoped ENNReal Matrix
open NonlinearDynamics.Random

#print RandomMatrix.orderedHermitianEigenvalues
#check RandomMatrix.orderedHermitianEigenvalues_antitone
#check RandomMatrix.trace_eq_sum_orderedHermitianEigenvalues
#check RandomMatrix.trace_sq_eq_sum_sq_orderedHermitianEigenvalues
#check RandomMatrix.orderedHermitianEigenvalues_hermitianCongruence
#print RandomMatrix.spectralCountingMeasure
#check RandomMatrix.spectralCountingMeasure_univ
#print RandomMatrix.empiricalSpectralMeasure
#check RandomMatrix.empiricalSpectralMeasure_zero
#check RandomMatrix.empiricalSpectralMeasure_succ_isProbability
#check RandomMatrix.empiricalSpectralProbability
#check RandomMatrix.measurable_empiricalSpectralMeasure_of_measurable_eigenvalues
#check RandomMatrix.map_matrixLaw_ambientEmpiricalSpectralMeasure_eq_map_intrinsicLaw_of_measurable_eigenvalues

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

Try the exact RMT-10B measurability bridge

import NonlinearDynamics.Random.RandomMatrices.HermitianSpectrumContinuity

open NonlinearDynamics.Random

#check RandomMatrix.abs_orderedHermitianEigenvalues_sub_le_frobenius
#check RandomMatrix.lipschitzWith_orderedHermitianEigenvalues_apply
#check RandomMatrix.continuous_orderedHermitianEigenvalues_apply
#check RandomMatrix.measurable_orderedHermitianEigenvalues_apply
#check RandomMatrix.measurable_spectralCountingMeasure
#check RandomMatrix.measurable_empiricalSpectralMeasure
#check RandomMatrix.measurable_empiricalSpectralProbability
#check RandomMatrix.measurable_ambientEmpiricalSpectralMeasure
#check RandomMatrix.map_matrixLaw_ambientEmpiricalSpectralMeasure_eq_map_intrinsicLaw

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

Try the exact RMT-10C law and mean interfaces

import NonlinearDynamics.Random.RandomMatrices.GaussianUnitaryEnsembleSpectrum

open NonlinearDynamics.Random

#check RandomMatrix.empiricalSpectralMeasure
#check GUE.empiricalSpectralLaw
#check GUE.empiricalSpectralLawProbability
#check GUE.empiricalSpectralProbabilityLaw
#check GUE.empiricalSpectralLaw_zero
#print GUE.meanEmpiricalSpectralMeasure
#check GUE.meanEmpiricalSpectralMeasure_zero
#check GUE.meanEmpiricalSpectralMeasure_succ_isProbability
#check GUE.integral_empiricalSpectralMoment_one
#check GUE.integral_empiricalSpectralMoment_two
#check GUE.integral_empiricalSpectralMoment_two_succ

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

Base camp zero: intrinsic Hermitian matrices

The project’s intrinsic carrier RandomMatrix.HermitianEuclidean n is a real normed space whose elements are complex \(n\)-by-\(n\) matrices together with a proof of Hermiticity. If \(H\) is represented by the matrix \(A\), the property is

where \(A^*\) is the conjugate transpose.

Bundling the property matters. A theorem about an intrinsic value may use Hermiticity without carrying a new premise at every line. The earlier Frobenius-geometry module also gives this carrier the topology and measurable space inherited from its finite real Euclidean structure. At the RMT-10A boundary, the remaining problem was not a missing measurable structure on the matrix space. It was the lack, inside that module, of a theorem connecting the specific ordered-eigenvalue functions to that structure. RMT-10B now supplies that theorem.

The module uses hermitianToMatrix when it needs the ambient matrix and hermitianCongruence U H for the intrinsic action

For unitary \(U\), this action stays inside the Hermitian carrier.

Base camp one: the finite Hermitian spectral theorem

For a complex Hermitian matrix \(H\), the finite spectral theorem supplies a unitary matrix \(U\) and a real diagonal vector \(\lambda\) such that

The columns of \(U\) form an orthonormal eigenbasis. Every diagonal entry of \(\operatorname{diag}(\lambda)\) is real, and each root of the characteristic polynomial appears according to its algebraic multiplicity. Mathlib’s official matrix-spectrum module proves this diagonalization and exposes both ordered and reindexed eigenvalue interfaces (Mathlib contributors).

The theorem changes what can be regarded as intrinsic. Matrix entries depend on a basis. The multiset of eigenvalues does not. If two Hermitian matrices are related by a unitary basis change, they describe the same diagonal operator in different coordinates.

Multiplicity is not an optional annotation

For

the set of distinct eigenvalues is \(\{5,2\}\), but the characteristic polynomial is

The ordered vector is \((5,2,2)\). The repeated coordinate is needed for

and for every spectral power sum. The counting measure will later turn those two copies of \(2\) into an atom of mass two. A set of distinct spectral locations cannot recover this information.

Camp one: why the sorted enumeration matters

Mathlib offers two closely related definitions for a Hermitian matrix whose entry index type is \(\iota\):

Matrix.IsHermitian.eigenvalues₀ :
  Fin (Fintype.card ι) → ℝ

Matrix.IsHermitian.eigenvalues :
  ι → ℝ

The first is canonical as an ordered finite ordinal. Mathlib proves eigenvalues₀_antitone, so lower indices contain no smaller values:

The second reuses the original index type by choosing a general equivalence with the finite ordinal. That equivalence preserves the number of indices. It need not preserve any order living on \(\iota\). This is entirely appropriate for results that only need a product or sum over all eigenvalues, but it is not a sorted coordinate interface.

The project specializes to \(\iota=\operatorname{Fin}(n)\). Mathlib’s theorem Fintype.card_fin n identifies the cardinality of that type with \(n\). The definition orderedHermitianEigenvalues transports eigenvalues₀ along the corresponding finite cast:

noncomputable def orderedHermitianEigenvalues {n : ℕ}
    (H : HermitianEuclidean n) : Fin n → ℝ :=
  fun i => H.2.eigenvalues₀
    (Fin.cast (Fintype.card_fin n).symm i)

This cast is order preserving. The theorem orderedHermitianEigenvalues_antitone transports Mathlib’s antitonicity through Fin.cast_le_cast. When sums later need an explicit equivalence, the proof uses Fin.castOrderIso (Fintype.card_fin n).symm.

Why spend proof effort on order if the empirical measure forgets permutations? Because this vector is intended as a reusable spectral interface. The largest eigenvalue is coordinate zero. Monotone comparisons between coordinates have a meaning. Future perturbation and extreme-eigenvalue results can state their coordinates without first quotienting by permutations. The measure layer then uses the same vector without losing multiplicity.

Camp two: trace as a spectral power sum

Trace is basis invariant. In an eigenbasis it becomes the sum of diagonal eigenvalues:

The project theorem trace_eq_sum_orderedHermitianEigenvalues states this in the ambient complex codomain:

theorem trace_eq_sum_orderedHermitianEigenvalues
    (H : HermitianEuclidean n) :
    Matrix.trace (hermitianToMatrix H) =
      ∑ i, (orderedHermitianEigenvalues H i : ℂ)

The coercion from real eigenvalues to complex numbers is explicit. The matrix trace is complex because the ambient entries are complex, even though Hermiticity forces its value to be real.

The proof route through characteristic roots

The proof is not a rewrite with Mathlib’s arbitrarily reindexed trace_eq_sum_eigenvalues. It follows a route that preserves the chosen ordered interface:

1. Hermiticity proves the characteristic polynomial splits.
2. The matrix trace is rewritten as the sum of characteristic-polynomial roots.
3. Mathlib identifies that root multiset with the values of eigenvalues₀.
4. A sum along the order isomorphism moves from the cardinality-indexed vector to Fin n.

The value of a finite sum is permutation invariant, but the proof explicitly connects it to the same ordered vector used everywhere else.

The square sees spectral energy

The second identity is

RMT-09 reached the left side without eigenvalues by proving that a Hermitian trace square is the Frobenius norm square. RMT-10A now reaches the right side through diagonalization. The theorem trace_sq_eq_sum_sq_orderedHermitianEigenvalues makes the bridge exact.

Let \(D=\operatorname{diag}(\lambda)\) and \(H=UDU^*\). Then

Cyclicity of trace and \(U^*U=I\) give

The Lean proof follows this calculation with matrix associativity, Matrix.trace_mul_cycle, the unitary identity, and the explicit diagonal formula. It then reindexes Mathlib’s diagonal eigenvalues to eigenvalues₀ and finally to the project vector.

These identities are deterministic. They do not assert integrability under a random-matrix law. RMT-09 separately proved integrability and expected values for the first two ambient Gaussian unitary ensemble (GUE) trace powers. RMT-10C now combines those layers into normalized sample moments and their exact finite GUE expectations in Finite Gaussian Unitary Ensemble Empirical Spectral Laws and Normalized Moments.

Camp three: unitary congruence changes coordinates, not spectrum

For a unitary matrix \(U\), intrinsic congruence sends \(H\) to \(UHU^*\). The characteristic polynomial is unchanged:

The theorem orderedHermitianEigenvalues_hermitianCongruence proves the strong coordinatewise statement

Its Lean proof has two conceptual stages.

First, it uses the characteristic-polynomial identity Matrix.charpoly_mul_comm. Moving a factor cyclically and reducing \(U^*U\) to the identity proves that the two characteristic polynomials are equal.

Second, it avoids selecting or matching individual eigenvectors. Mathlib describes eigenvalues₀ as the decreasing sort of the real parts of the characteristic roots. Equal characteristic polynomials have equal root multisets, and sorting the same multiset by the same order yields the same list. Function extensionality then gives equality of every project coordinate.

This proof handles repeated eigenvalues naturally. When an eigenspace has dimension greater than one, an eigenbasis inside it is far from unique. The sorted root list is still canonical.

Once the vector equality is available, rewriting both definitions gives unitary invariance of both spectral measures:

These are pointwise deterministic invariances. They should be distinguished from the earlier theorem that the GUE matrix law is unitary invariant. The former says the observable is constant along every unitary orbit. The latter says the random input law is itself unchanged by the action.

Camp four: from repeated coordinates to finite atoms

The Dirac measure \(\delta_x\) places unit mass at the point \(x\). For a measurable set \(B\subseteq\mathbb R\),

Mathlib’s official Dirac module provides that atomic measure together with its map and probability properties. Its counting-measure module defines global counting measure as a sum of Dirac measures (Mathlib contributors). RMT-10A uses the same idea over a finite eigenvalue index:

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

If two indices carry the same eigenvalue, two equal Dirac measures occur in the sum. Their masses add. This is exactly how algebraic multiplicity becomes measure multiplicity.

Total mass

Every Dirac measure assigns mass one to the whole real line. There are \(n\) index slots, so

The theorem spectralCountingMeasure_univ states this uniformly, including the empty case. The specialized theorem spectralCountingMeasure_zero makes the zero-dimensional identity visible:

Unitary invariance is transferred by spectralCountingMeasure_hermitianCongruence, which rewrites every Dirac location with the already proved ordered-vector equality.

The first two counting-measure moments

Integrating against a finite sum of Dirac atoms evaluates the integrand at each atom. Therefore

and

The project states these as integral_complex_ofReal_spectralCountingMeasure and integral_sq_complex_ofReal_spectralCountingMeasure. The integrands are coerced into \(\mathbb C\), matching the codomain of the trace. Finite sums of Dirac integrals are automatically integrable for these pointwise finite values, and the proof supplies those obligations to integral_finsetSum_measure.

For positive dimension, the corresponding empirical moments follow on paper by multiplying by \(1/n\):

Those two normalized formulas are explanatory consequences. RMT-10A does not publish them as separate public declarations, and at \(n=0\) the right sides would require a separate convention.

Camp five: dimension zero is not a probability space of eigenvalues

For \(n\gt0\), normalization gives

The dimension-zero case has no eigenvalue slots. There is no uniform probability distribution over an empty set. One could force a total probability-valued definition by choosing an arbitrary fallback point and returning a Dirac measure there, but that point would not be an eigenvalue and would inject fake spectral mass.

The project instead defines

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

In the extended nonnegative reals, the inverse of zero is infinity. The empty counting measure is zero, and infinity scaled by the zero measure is zero. Thus

Three declarations expose the boundary at the right strengths:

• empiricalSpectralMeasure_zero proves the exact empty-case equality.
• empiricalSpectralMeasure_isZeroOrProbability says the measure has total mass zero or one in every natural dimension.
• empiricalSpectralMeasure_succ_isProbability proves mass one for dimensions written as \(n+1\).

Mathlib’s IsZeroOrProbabilityMeasure typeclass is precisely the uniform proposition needed here. Its ProbabilityMeasure ℝ type is a subtype containing a measure together with a proof that its total mass is one (Mathlib contributors).

The definition empiricalSpectralProbability n H bundles \(L_H\) into that subtype only when \(H\) has dimension \(n+1\). This makes a valuable impossible state unrepresentable: code receiving that wrapper never has to wonder whether it was handed the zero-dimensional zero measure.

Unitary invariance survives scaling and appears as empiricalSpectralMeasure_hermitianCongruence.

Camp six: the Giry measurability gate

A measure can itself be a point in a measurable space. Mathlib equips Measure α with the Giry measurable structure: the smallest measurable structure making every evaluation map

measurable when \(B\) is measurable. The official Giry module includes all measures, not only probability measures, and proves that Dirac embedding, measure addition, mapping, joining, and related constructions are measurable (Mathlib contributors).

For the spectral counting map

the outer operations are therefore available. If every coordinate map \(H\mapsto\lambda_i(H)\) is measurable, composition with measurable Dirac and finite measurable addition proves that the whole counting-measure map is measurable. Scaling by the constant inverse dimension then proves measurability of the empirical-measure map.

RMT-10A packages these deductions as:

theorem measurable_spectralCountingMeasure_of_measurable_eigenvalues
    (h : ∀ i, Measurable
      (fun H => orderedHermitianEigenvalues H i)) :
    Measurable spectralCountingMeasure

theorem measurable_empiricalSpectralMeasure_of_measurable_eigenvalues
    (h : ∀ i, Measurable
      (fun H => orderedHermitianEigenvalues H i)) :
    Measurable empiricalSpectralMeasure

For positive dimension, subtype construction then yields measurable_empiricalSpectralProbability_of_measurable_eigenvalues.

What RMT-10A assumes, and RMT-10B proves

Inside RMT-10A, the implication is checked while its premise remains an argument to the theorem.

Pinned Mathlib’s matrix-spectrum module provides eigenvalues₀, antitonicity in the index, and algebraic spectral identities. It does not provide continuity of the map from Hermitian matrices to each ordered eigenvalue coordinate, nor the weaker measurability theorem needed here. Antitonicity in \(i\) says nothing about dependence on \(H\).

The repository’s next module, RMT-10B, discharges the premise. It proves the Frobenius perturbation inequality

then derives 1-Lipschitz continuity, continuity, and coordinatewise measurability. Therefore the current project may write the unconditional measurable_empiricalSpectralMeasure. When discussing RMT-10A alone, however, writing

without displaying its hypothesis would overstate that module’s interface.

Camp seven: a total observable on all complex matrices

The intrinsic map \(H\mapsto L_H\) accepts only bundled Hermitian inputs. The project’s ambient GUE matrix law lives on the full type of complex matrices, even though it is constructed as the pushforward of an intrinsic Hermitian law. To compose an intrinsic observable with that ambient law, RMT-10A defines a total extension.

The map matrixToHermitianOrZero n behaves as follows:

This is a policy choice for totalization, not a spectral claim about non-Hermitian matrices. Sending an off-locus matrix to zero does not assert that its spectrum is zero. It gives the ambient function a value where the intended Hermitian observable is outside its domain.

The theorem measurable_matrixToHermitianOrZero is unconditional. The Hermitian locus is a measurable set from the earlier geometry module. The matrix-to-Frobenius inclusion is measurable coordinatewise. Mathlib’s measurable piecewise construction then combines the Hermitian branch with the constant-zero branch.

The theorem matrixToHermitianOrZero_hermitianToMatrix proves that the extension is a left inverse on genuine intrinsic inputs:

The ambient observable is now a simple composition:

noncomputable def ambientEmpiricalSpectralMeasure (n : ℕ)
    (A : Matrix (Fin n) (Fin n) ℂ) : Measure ℝ :=
  empiricalSpectralMeasure (matrixToHermitianOrZero n A)

Its RMT-10A measurability theorem remains conditional because the totalization is measurable but that module still requests ordered-eigenvalue measurability. RMT-10B supplies the request and exports measurable_ambientEmpiricalSpectralMeasure unconditionally.

Why zero totalization is harmless for the checked GUE comparison

The ambient GUE law is not an unrelated law that merely happens to give the Hermitian set probability one. It is definitionally connected to the intrinsic law by the checked pushforward identity

Push the ambient law through the totalized observable and use associativity of measure map. Every source sample first enters the ambient space through hermitianToMatrix, then immediately returns through the left inverse. Pointwise, the composition reduces to the intrinsic empirical measure.

Under the coordinatewise measurability hypothesis, RMT-10A proves:

theorem
  map_matrixLaw_ambientEmpiricalSpectralMeasure_eq_map_intrinsicLaw_of_measurable_eigenvalues
    (h : ∀ i, Measurable
      (fun H => orderedHermitianEigenvalues H i)) :
    (GUE.matrixLaw n).map (ambientEmpiricalSpectralMeasure n) =
      (GUE.intrinsicLaw n).map empiricalSpectralMeasure

This is an exact equality of two measures on Measure ℝ. It says the ambient and intrinsic routes agree whenever both maps are licensed. It does not remove the premise, introduce a named unconditional GUE empirical spectral law, or claim a density for that law.

What the two routes mean

The left route matches downstream code that starts from the existing ambient matrix law. Non-Hermitian inputs have a total fallback, though this particular source law reaches the observable through the intrinsic inclusion.

The right route is mathematically direct. It samples from the real Euclidean Hermitian carrier and applies the intrinsic spectral observable.

The equality proves representational independence between those routes, not an asymptotic or universality statement.

Type the size-two ledger yourself with Lean and Std

The exact project spectrum uses Mathlib’s complex matrices, Hermitian spectral theorem, finite measures, and Giry measurable space. A first-time reader can check the running arithmetic before loading that machinery. The worksheet below imports only Lean’s Std library and models real two-by-two matrices with four integer fields.

Create a scratch directory outside formalization/. Save this exact block as HermitianSpectraTutorial.lean:

import Std

namespace HermitianSpectraTutorial

structure Vec2 where
  x : Int
  y : Int
  deriving Repr, DecidableEq

def Vec2.scale (a : Int) (v : Vec2) : Vec2 :=
  { x := a * v.x, y := a * v.y }

structure Matrix2 where
  a00 : Int
  a01 : Int
  a10 : Int
  a11 : Int
  deriving Repr, DecidableEq

def Matrix2.mulVec (A : Matrix2) (v : Vec2) : Vec2 :=
  { x := A.a00 * v.x + A.a01 * v.y
    y := A.a10 * v.x + A.a11 * v.y }

def Matrix2.IsHermitian (A : Matrix2) : Prop :=
  A.a01 = A.a10

instance (A : Matrix2) : Decidable A.IsHermitian := by
  unfold Matrix2.IsHermitian
  infer_instance

def isEigenpair (A : Matrix2) (lambda : Int) (v : Vec2) : Bool :=
  v != { x := 0, y := 0 } &&
    A.mulVec v == v.scale lambda

def trace (A : Matrix2) : Int :=
  A.a00 + A.a11

def traceSquare (A : Matrix2) : Int :=
  A.a00 * A.a00 + 2 * A.a01 * A.a10 + A.a11 * A.a11

def spectralSum (spectrum : List Int) : Int :=
  spectrum.foldl (fun total x => total + x) 0

def spectralSquareSum (spectrum : List Int) : Int :=
  spectrum.foldl (fun total x => total + x * x) 0

def atomCount (spectrum : List Int) (x : Int) : Nat :=
  spectrum.count x

def H : Matrix2 :=
  { a00 := 2, a01 := 1, a10 := 1, a11 := 2 }

def D : Matrix2 :=
  { a00 := 3, a01 := 0, a10 := 0, a11 := 1 }

def plus : Vec2 := { x := 1, y := 1 }
def minus : Vec2 := { x := 1, y := -1 }
def e0 : Vec2 := { x := 1, y := 0 }
def e1 : Vec2 := { x := 0, y := 1 }

def orderedSpectrumH : List Int := [3, 1]
def orderedSpectrumD : List Int := [3, 1]
def emptySpectrum : List Int := []

#eval [isEigenpair H 3 plus, isEigenpair H 1 minus,
  isEigenpair D 3 e0, isEigenpair D 1 e1]

#eval (orderedSpectrumH,
  [atomCount orderedSpectrumH 3,
   atomCount orderedSpectrumH 1,
   atomCount orderedSpectrumH 2],
  orderedSpectrumH.length)

#eval [trace H, traceSquare H,
  spectralSum orderedSpectrumH,
  spectralSquareSum orderedSpectrumH]

#eval [decide (H = D), decide (orderedSpectrumH = orderedSpectrumD),
  decide H.IsHermitian, decide D.IsHermitian]

#eval (emptySpectrum.length, atomCount emptySpectrum 0)

example : isEigenpair H 3 plus = true := by decide
example : isEigenpair H 1 minus = true := by decide
example : orderedSpectrumH = [3, 1] := by decide
example : atomCount orderedSpectrumH 3 = 1 := by decide
example : atomCount orderedSpectrumH 1 = 1 := by decide
example : atomCount orderedSpectrumH 2 = 0 := by decide
example : trace H = spectralSum orderedSpectrumH := by decide
example : traceSquare H = spectralSquareSum orderedSpectrumH := by decide
example : H ≠ D := by decide
example : orderedSpectrumH = orderedSpectrumD := by decide
example : emptySpectrum.length = 0 := by decide

end HermitianSpectraTutorial

Open a terminal in that scratch directory and type:

source "$HOME/.elan/env"
elan run leanprover/lean4:v4.32.0 lean HermitianSpectraTutorial.lean

This exact worksheet was executed successfully with Lean 4.32.0 while the chapter was rebuilt. Lean printed:

[true, true, true, true]
([3, 1], [1, 1, 0], 2)
[4, 10, 4, 10]
[false, true, true, true]
(0, 0)

Read the output in order:

1. the four candidate eigenpairs for \(H\) and \(D\) all satisfy \(Av=\lambda v\);
2. the ordered spectrum is \([3,1]\), its masses at \(3,1,2\) are \([1,1,0]\) in counting units, and it has two slots;
3. matrix trace, matrix trace square, spectral sum, and spectral square sum are \([4,10,4,10]\);
4. \(H=D\) is false, their spectrum lists are equal, and both symmetry checks are true; and
5. the empty spectrum has zero slots and zero atoms at zero.

Each example is a kernel-checked proof of one finite equality. The code deliberately stores empirical masses as integer atom counts with a separate denominator two, so there is no hidden floating-point calculation. It checks the tutorial ledger only. It does not prove the general Hermitian spectral theorem, compute Mathlib’s eigenvalues₀, construct a Measure ℝ, or check any project declaration. Its command is safe on an ordinary Mac or Linux host because it loads only the pinned compiler and Std.

A worked three-by-three audit

Let

The decreasing eigenvalue vector is

Its counting measure and empirical measure are

The total masses are

The first counting moment is

The second is

The empirical moments are \(1/3\) and \(11/3\), respectively. If \(U\) is any three-dimensional unitary matrix and \(K=UHU^*\), then \(K\) will usually have nondiagonal entries, but the checked invariance theorems give

No probability enters this example. If a random unitary were sampled and used to rotate \(H\), every realization would still have the same deterministic empirical measure. A probability law on those measures would therefore be a Dirac law at \(L_H\), provided the random construction and the relevant map were shown measurable. That final sentence illustrates the next level; it is not a declaration added by RMT-10A.

Physics: spectra are the basis-independent energy record

In finite-dimensional quantum mechanics, an observable such as a Hamiltonian is represented by a Hermitian operator. Hermiticity makes measurement outcomes real and supplies an orthonormal eigenbasis. The eigenvalues of the Hamiltonian are its possible energy levels. A unitary basis change alters the matrix coordinates but not those energies.

For one finite Hamiltonian, the empirical spectral measure is therefore a compact ledger of energy levels with degeneracies. If an energy has a multidimensional eigenspace, the repeated atom records that degeneracy. The measure does not record eigenvectors, transition amplitudes, or which basis vectors span the degenerate subspace.

For a random Hamiltonian ensemble, a law over empirical spectral measures can describe sample-to-sample variation of the global energy-level distribution. That is only a starting point for quantum-chaos questions. Local spacing statistics typically require ordering, rescaling, and unfolding. Spectral form factors use pairwise phase information across levels. Eigenvector statistics need information discarded by \(L_H\). None is present merely because an empirical measure has been defined.

Dyson’s symmetry classification connects unitary symmetry classes with quantum-mechanical antiunitary symmetries (Dyson). That physics motivates why GUE and unitary congruence matter here. It does not imply that every physical Hamiltonian is GUE-distributed, nor does RMT-10A formalize a Hamiltonian dynamics model.

Empirical spectral distribution in the wider literature

The phrase empirical spectral distribution (ESD) is used for normalized eigenvalue counting in both Hermitian and non-Hermitian random-matrix theory. The codomain changes with the spectrum. Hermitian eigenvalues lie on \(\mathbb R\); a general complex matrix may have eigenvalues in \(\mathbb C\).

Tao, Vu, and Krishnapur define the ESD of a general complex matrix by counting its complex eigenvalues with equal weight, then study limiting distributions for normalized random matrices and prove circular-law results (Tao, Vu, and Krishnapur). That paper is useful here as a primary example of the finite normalized-counting convention and of the distinction between a sample ESD and an asymptotic law.

Its theorem is not a source for the present Hermitian claims. The paper’s matrices are not restricted to be Hermitian, its eigenvalues live in the complex plane, and its target asymptotic distribution is the circular law. RMT-10A proves no result from that asymptotic argument. The citation is deliberately scoped to shared vocabulary and measure architecture.

The complete public API

The module exposes twenty-six public declarations. The following atlas keeps unconditional algebra separate from conditional measure-valued probability.

Ordered finite spectrum

All five are unconditional finite-dimensional algebra.

Spectral counting measure

Only the last row is conditional inside RMT-10A. RMT-10B later discharges its premise and exports measurable_spectralCountingMeasure.

Empirical spectral measure

The first six are unconditional in RMT-10A. The last two display the premise that RMT-10B discharges before exporting unconditional counterparts.

Ambient totalization and GUE bridge

The final equality is the strongest law-level theorem in the file, and its hypothesis is part of its mathematical content.

Common wrong turns

Calling eigenvalues sorted

Mathlib’s eigenvalues is reindexed by a general finite equivalence. Use eigenvalues₀ when order matters, then transport that index with an order-preserving cast.

Replacing multiplicity by distinct locations

The empirical measure counts index slots. Collapsing repeated values to a set changes total mass before normalization and changes every moment afterward.

Calling the zero-dimensional object a probability measure

The project returns the zero measure at \(n=0\). It has mass zero. Only the n + 1 wrapper is a genuine ProbabilityMeasure.

Confusing an empirical measure with its law

\(L_H\) is one measure on \(\mathbb R\). A random \(H\) may induce a probability law on a space of such measures, but that is a pushforward and needs measurability.

Treating antitonicity as measurability

orderedHermitianEigenvalues_antitone compares coordinates within one fixed matrix. It does not compare nearby matrices and does not imply that \(H\mapsto\lambda_i(H)\) is measurable.

Forgetting which GUE bridge is being quoted

The RMT-10A name ending in of_measurable_eigenvalues assumes coordinatewise eigenvalue measurability. The theorem does not make that premise disappear. RMT-10B’s shorter theorem map_matrixLaw_ambientEmpiricalSpectralMeasure_eq_map_intrinsicLaw has no such argument because that successor imports the proof.

Reading zero totalization as non-Hermitian spectral theory

matrixToHermitianOrZero is an extension policy. On a non-Hermitian input it does not calculate that input’s complex spectrum.

Inferring asymptotics from finite moments

The trace and trace-square identities hold exactly at each finite dimension. They do not prove tightness, convergence, a semicircle law, or universality.

What has and has not been proved

Exercises from trailhead to summit

Trailhead

1. Compute the ordered eigenvalue vector, counting measure, and empirical measure of a two-dimensional scalar matrix \(aI\). How is multiplicity represented?
2. For the worked three-dimensional example, evaluate \(L_H(B)\) when \(B=[-2,0]\), \(B=\{-1\}\), and \(B=(0,\infty)\).
3. Show directly that the total mass of \(\sum_i\delta_{\lambda_i}\) is the number of index slots, even when all eigenvalues coincide.
4. Explain in plain language why the empirical measure forgets eigenvectors.

Mid-mountain

5. Starting from \(H=UDU^*\), derive \(\operatorname{Tr}(H^2)=\operatorname{Tr}(D^2)\) one matrix-associativity step at a time.
6. Prove that equal characteristic polynomials of Hermitian matrices imply equal decreasing eigenvalue vectors. Identify where real roots and sorting enter.
7. Give a finite permutation of an eigenvalue vector. Prove that its Dirac sum is unchanged while its coordinate-zero value may change.
8. Compare the types Measure ℝ and ProbabilityMeasure ℝ. Which field or proof is added by the latter?
9. Propose two possible conventions at dimension zero. Explain why the arbitrary-Dirac convention is total and probabilistic but is not determined by the empty spectrum.

Summit

10. Assume each \(H\mapsto\lambda_i(H)\) is measurable. Build the measurability proof for \(H\mapsto\sum_i\delta_{\lambda_i(H)}\) from measurable Dirac and finite addition.
11. Explain why scaling a measurable measure-valued map by a fixed extended nonnegative real preserves measurability in the Giry structure.
12. Expand the intrinsic-versus-ambient GUE pushforward proof as a commuting diagram. Label the use of Measure.map_map and the left-inverse theorem.
13. State a continuity or perturbation theorem that would imply coordinatewise eigenvalue measurability. Be precise about the matrix norm and eigenvalue ordering.
14. Reconstruct the successor RMT-10C definition of the unconditional named GUE empirical spectral law and derive its dimension-zero behavior without inventing a probability measure on an empty spectrum.
15. Assuming positive dimension, combine the counting-measure moments with RMT-09 to derive the expected first two empirical moments under the project’s Wigner-scaled GUE. Compare your route with RMT-10C and mark which steps belong to deterministic algebra, integrability, and law transport.

Reproduce the chapter

On an ordinary Mac or Linux machine, a reader may run the bounded Std worksheet exactly as shown above. The exact RMT-10A, RMT-10B, and RMT-10C modules import Mathlib and are full project checks. From the repository root, run:

cd formalization
lake env lean NonlinearDynamics/Random/RandomMatrices/HermitianSpectrum.lean
lake env lean NonlinearDynamics/Random/RandomMatrices/HermitianSpectrumContinuity.lean
lake env lean NonlinearDynamics/Random/RandomMatrices/GaussianUnitaryEnsembleSpectrum.lean

These commands use the pinned project dependencies and may require substantial disk space and memory. A green technical build would still not complete the pending human mathematical, editorial, scientific-integrity, and accessibility reviews.

Where to continue

The empirical spectral measure entry is the compact operational reference. Read finite matrix trace moment for the preceding integrability and expectation layer, and unitary invariance for the symmetry distinction used here.

First Exact Finite Gaussian Unitary Ensemble Trace Moments supplies the finite expected trace identities that a later empirical-moment bridge can consume. From Normalized Hermitian Coordinates to Gaussian Unitary Ensemble Invariance constructs the intrinsic law and ambient pushforward identity used by the conditional comparison.

The successor formal milestone now proves coordinatewise continuity and measurability of the ordered Hermitian eigenvalues: Hermitian Spectral Perturbation, Continuity, and Measurability. It removes the hypotheses from the Giry interfaces and proves the ambient-versus-intrinsic GUE pushforward equality unconditionally. The next layer is now available: Finite Gaussian Unitary Ensemble Empirical Spectral Laws and Normalized Moments names the law, packages it as a probability measure, forms its Giry mean, and checks the first two normalized expected sample moments.

References

Mathlib contributors. Spectral theory of Hermitian matrices, Mathlib 4 documentation. This official page proves the finite Hermitian spectral theorem and defines eigenvalues₀, its antitonicity, the generally reindexed eigenvalues, characteristic-polynomial root identities, and trace as an eigenvalue sum.

Mathlib contributors. Dirac measure and counting measure, Mathlib 4 documentation. These official APIs define point masses, their integrals and pushforwards, and counting measure as a sum of Dirac measures. RMT-10A uses the finite indexed version of that atomic pattern.

Mathlib contributors. The Giry measurable structure on measures, Mathlib 4 documentation. This official module equips all measures with the evaluation-generated measurable structure and proves the measurability of the measure constructors used by the conditional spectral interfaces.

Mathlib contributors. Probability measures and probability-measure typeclasses, Mathlib 4 documentation. These official pages define ProbabilityMeasure as a subtype with total mass one and IsZeroOrProbabilityMeasure as the zero-or-unit-mass interface.

Terence Tao, Van Vu, with an appendix by Manjunath Krishnapur. Random matrices: Universality of ESDs and the circular law, arXiv:0807.4898v5, revised 23 April 2009 and accessed 21 July 2026; published in The Annals of Probability 38 (2010), 2023-2065, doi:10.1214/10-AOP534. This primary source defines normalized eigenvalue counting for general complex matrices and studies non-Hermitian circular-law asymptotics. It is cited only for the finite empirical-spectral-distribution convention and the distinction between a sample distribution and its limiting behavior.

Freeman J. Dyson. The Threefold Way: Algebraic Structure of Symmetry Groups and Ensembles in Quantum Mechanics, Journal of Mathematical Physics 3 (1962), 1199-1215. This primary source supplies historical physics context for the unitary symmetry class. It does not supply the project-specific finite measure definitions or any theorem formalized in RMT-10A.

The exact upstream Lean source audited for this chapter is Mathlib commit 81a5d257, the revision pinned by formalization/lake-manifest.json.