From Random Matrices to Laws

This entry is the code companion to formalization/NonlinearDynamics/Random/RandomMatrices/Laws.lean. Every named declaration in that file appears below with its exact statement or complete definition. The Lean source is the build authority.

The wider ascent begins in Random Matrices: From Outcomes to Spectra. The three preceding code companions cover matrix measurability, Hermitian structure, and trace-power observables.

Choose your route

Learning objectives

By the summit, a reader should be able to:

1. define a pushforward measure using inverse images;
2. explain why RandomMatrix.law asks for a measurability proof explicitly;
3. derive the law of a measurable composite in either order;
4. explain why a probability measure remains a probability measure after pushforward;
5. use a Dirac law as a deterministic test case;
6. distinguish congruence from unitary similarity and from invariance in law;
7. read Matrix.unitaryGroup ι ℂ as certified unitary matrices;
8. state exactly what HasUnitaryConjugationInvariantLaw means; and
9. list the missing ingredients before the project can claim GUE.

The ascent in one picture

flowchart LR
  A[Sample measure mu on Omega] --> B[Measurable matrix map X]
  B --> C[Matrix law: map X mu]
  C --> D[Map congruence A]
  D --> E[Law of A X A*]
  F[Hermitian at every sample] --> G[Congruence remains Hermitian]
  H[Unitary U] --> D
  C --> I{Same measure after every U?}
  E --> I
  I --> J[Unitary-conjugation-invariant law]
  K[Gaussian coordinates and normalization] -. future .-> L[GUE law]
  J -. required property .-> L

Reading the map. The upper path transports probability: a measurable sample map pushes a source measure onto matrix space, and a measurable congruence pushes that law again. The lower path is algebraic: congruence preserves Hermiticity sample by sample. The equality test compares measures, not individual matrices. Gaussian coordinates, independence, and normalization are future work, so the GUE node is deliberately outside the checked path.

Four objects, four jobs

For this introductory probability picture, let \((\Omega,\mathcal F,\mu)\) be a probability space and let

The law forgets the names of source outcomes. It retains every probability question asked through the matrix value. Two maps can live on different sample spaces, disagree pointwise wherever a comparison makes sense, and still have the same law.

This is why ensemble symmetry cannot normally mean

That would require each realized matrix to be fixed. The distributional statement asks whether transforming all realizations redistributes probability mass.

Pushforwards move mass forward by pulling sets back

For measurable \(f:S\to T\) and a measure \(\mu\) on \(S\), the pushforward is

for every measurable \(B\subseteq T\). Points move forward through \(f\), but sets move backward through \(f^{-1}\). Measures consume sets, so the mass arriving in \(B\) is found by measuring all source points that land in \(B\).

For a measurable random matrix \(X\),

The Knowledge Base pages on pushforwards and probability laws develop this picture independently of Lean.

Lineage, contribution, and non-claims

Measure-theoretic probability defines the distribution of a random element as a pushforward. Kallenberg gives the general framework (Kallenberg, 2021). Mathlib supplies Measure.map, its evaluation and composition theorems, Dirac measures, the probability-measure typeclass, and a finite matrix unitary group (Mathlib pushforward API; Mathlib unitary-group API).

Random-matrix references formulate ensembles as measures on matrix spaces and treat conjugation invariance as a symmetry of those measures (Anderson, Guionnet, and Zeitouni, 2010).

This module contributes a measurable congruence action, a law constructor with visible measurability evidence, project-level pushforward identities, a measure-level unitary-invariance predicate, and a bridge from bundled Hermitian matrices to equality in law.

It does not define Gaussian variables, independence, covariance, density, dimension scaling, GUE, expected moments, eigenvalue laws, or asymptotics.

Open the module

import Mathlib.LinearAlgebra.UnitaryGroup
import Mathlib.MeasureTheory.Measure.Dirac
import Mathlib.MeasureTheory.Measure.Typeclasses.Probability
import NonlinearDynamics.Random.RandomMatrices.Hermitian

The imports supply certified unitary matrices, point-mass measures, IsProbabilityMeasure, and the project’s measurable Hermitian API. The local context is:

open Matrix MeasureTheory
open scoped Matrix

universe uΩ uι

namespace NonlinearDynamics.Random

namespace RandomMatrix

variable {Ω : Type uΩ} {ι : Type uι} [MeasurableSpace Ω]

The notation Aᴴ means conjugate transpose.

The deterministic action: congruence

For a fixed square matrix \(A\), define \(C_A(H)=AHA^*\).

RandomMatrix.congruence

/-- The deterministic congruence map `H ↦ A * H * Aᴴ` on square complex
matrices. No invertibility or unitarity assumption is needed for this map. -/
def congruence [Fintype ι] (A : Matrix ι ι ℂ) : Matrix ι ι ℂ → Matrix ι ι ℂ :=
  fun H ↦ A * H * Aᴴ

For arbitrary \(A\), this is congruence, not similarity. Similarity uses \(A^{-1}\). If \(A\) is unitary, \(A^*=A^{-1}\), and the same formula becomes unitary conjugation.

RandomMatrix.measurable_congruence

/-- Congruence by a fixed finite matrix is measurable for the entrywise
measurable space on matrices. -/
theorem measurable_congruence [Fintype ι] (A : Matrix ι ι ℂ) :
    Measurable (congruence A) := by
  exact measurable_mul
    (measurable_mul
      (measurable_const (A := A)) measurable_id)
    (measurable_const (A := Aᴴ))

The variable \(H\) is observed by measurable_id. Fixed \(A\) and \(A^*\) are measurable constants. Finite matrix multiplication builds \(H\mapsto AH\) and then \(H\mapsto AHA^*\). Finiteness enters through the finite sums in matrix multiplication.

The identity, zero, and composition laws

/-- Congruence by the identity matrix is the identity action. -/
@[simp]
theorem congruence_one [Fintype ι] [DecidableEq ι] (H : Matrix ι ι ℂ) :
    congruence (1 : Matrix ι ι ℂ) H = H := by
  simp [congruence]

/-- Congruence sends the zero matrix to the zero matrix. -/
@[simp]
theorem congruence_zero [Fintype ι] (A : Matrix ι ι ℂ) :
    congruence A (0 : Matrix ι ι ℂ) = 0 := by
  simp [congruence]

/-- Congruence by a product is the composite of the two congruence maps. -/
theorem congruence_mul [Fintype ι] (A B H : Matrix ι ι ℂ) :
    congruence (A * B) H = congruence A (congruence B H) := by
  simp only [congruence, Matrix.conjTranspose_mul]
  simp only [Matrix.mul_assoc]

The third theorem encodes

The order matters: \(C_B\) acts first. Matrix.conjTranspose_mul reverses the factors under conjugate transpose.

RandomMatrix.congruence_isHermitian

/-- Congruence preserves Hermiticity, without any invertibility assumption on
the fixed matrix. -/
theorem congruence_isHermitian [Fintype ι] (A : Matrix ι ι ℂ)
    {H : Matrix ι ι ℂ} (hH : H.IsHermitian) : (congruence A H).IsHermitian :=
  Matrix.isHermitian_mul_mul_conjTranspose A hH

If \(H^*=H\), then \((AHA^*)^*=AH^*A^*=AHA^*\). This is sample-level algebra. It says nothing about the probabilities of different Hermitian matrices.

RandomMatrix.map_congruence_one

/-- Pushing a measure forward by identity congruence leaves it unchanged. -/
@[simp]
theorem map_congruence_one [Fintype ι] [DecidableEq ι]
    (ν : Measure (Matrix ι ι ℂ)) :
    Measure.map (congruence (1 : Matrix ι ι ℂ)) ν = ν := by
  convert Measure.map_id using 2
  funext H
  exact congruence_one H

Measure.map_id handles the identity function. funext proves that identity congruence is that function.

The explicit law interface

RandomMatrix.law

/-- The pushforward law of a measurable matrix-valued map.

The measurability proof is deliberately an explicit argument even though the
value of `Measure.map` itself does not store that proof. It supports the
standard pushforward evaluation and composition theorems below.
-/
noncomputable def law (X : RandomMatrix Ω ι ι ℂ) (_hX : Measurable X)
    (μ : Measure Ω) : Measure (Matrix ι ι ℂ) :=
  Measure.map X μ

The proof argument _hX does not occur in the right-hand side. It guards the public interface. Mathlib makes Measure.map X μ total: if \(X\) is not almost-everywhere measurable with respect to \(\mu\), the result is defined to be the zero measure (Mathlib pushforward API). A bare map expression can therefore typecheck without denoting the intended law.

The project API requires the stronger measure-independent proof Measurable X. That proof supports every later measure, the standard measurable-set formula, and clean composition. A future API could instead be based on AEMeasurable X μ, but this module is not.

noncomputable says that Lean does not promise an executable algorithm for a general measure. It does not weaken the mathematical definition.

RandomMatrix.law_apply

/-- A matrix law evaluates a measurable set by taking its preimage under the
random matrix. -/
theorem law_apply (X : RandomMatrix Ω ι ι ℂ) (hX : Measurable X)
    (μ : Measure Ω) {s : Set (Matrix ι ι ℂ)} (hs : MeasurableSet s) :
    law X hX μ s = μ (X ⁻¹' s) := by
  exact Measure.map_apply hX hs

This is the defining equation

hX certifies the matrix map. hs certifies the target event. The theorem does not prove that any particular eigenvalue, norm, or spectral event is measurable. Those events need their own proofs.

RandomMatrix.law_comp

/-- The law of a measurable composite is the pushforward of the original law. -/
theorem law_comp {X : RandomMatrix Ω ι ι ℂ} (hX : Measurable X)
    {f : Matrix ι ι ℂ → Matrix ι ι ℂ} (hf : Measurable f) (μ : Measure Ω) :
    law (f ∘ X) (hf.comp hX) μ = Measure.map f (law X hX μ) := by
  exact (Measure.map_map hf hX).symm

There are two routes:

One transforms each sample and then takes its law. The other takes the matrix law first and pushes it through \(f\). Mathlib’s theorem is oriented in the opposite equality direction, so the proof uses .symm.

This project theorem is specialized to matrix endomorphisms. It supports congruence directly. It does not directly produce the scalar law of trace or tracePower, whose codomain is \(\mathbb C\). Mathlib’s general map_map is the template for a future codomain-general theorem.

Probability preservation and the Dirac check

/-- A probability measure on the sample space induces a probability law. -/
theorem law_isProbabilityMeasure (X : RandomMatrix Ω ι ι ℂ) (hX : Measurable X)
    (μ : Measure Ω) [IsProbabilityMeasure μ] : IsProbabilityMeasure (law X hX μ) :=
  Measure.isProbabilityMeasure_map hX.aemeasurable

/-- Under a Dirac measure on the sample space, the law is the Dirac measure at
the realized matrix. -/
theorem law_dirac (X : RandomMatrix Ω ι ι ℂ) (hX : Measurable X) (ω : Ω) :
    law X hX (Measure.dirac ω) = Measure.dirac (X ω) := by
  exact Measure.map_dirac' hX ω

A probability measure has total mass one. Pushforward preserves that total because the preimage of the whole matrix space is all of \(\Omega\). Mathlib needs only almost-everywhere measurability here, obtained from hX.aemeasurable. This does not imply integrability of a future observable.

A Dirac measure concentrates all mass at one point. The identity

reduces a law statement to ordinary evaluation. It is the deterministic sanity check for later transformations.

Unitary invariance lives at the level of measures

Mathlib’s unitary group

For finite \(\iota\), an element

variable [Fintype ι] [DecidableEq ι]
variable (U : Matrix.unitaryGroup ι ℂ)

is a matrix packaged with the equations \(UU^*=I\) and \(U^*U=I\). Mathlib gives these values a group structure and a coercion to Matrix ι ι ℂ (Mathlib unitary-group API). Thus

#check (U : Matrix ι ι ℂ)

uses the underlying matrix while U still carries its certificate.

For unitary \(U\), \(U^*=U^{-1}\), so \(H\mapsto UHU^*\) is both congruence and similarity. It preserves each realization’s spectrum. This Laws module does not invoke the spectral theorem.

RandomMatrix.IsUnitaryConjugationInvariant

/-- A finite complex matrix law is invariant under unitary conjugation when
every unitary congruence pushforward leaves it unchanged. -/
def IsUnitaryConjugationInvariant [Fintype ι] [DecidableEq ι]
    (ν : Measure (Matrix ι ι ℂ)) : Prop :=
  ∀ U : Matrix.unitaryGroup ι ℂ,
    Measure.map (congruence (U : Matrix ι ι ℂ)) ν = ν

In symbols,

This compares measures. Equivalently, every measurable matrix event gets the same mass before and after unitary conjugation. It does not say \(UHU^*=H\) for each matrix or sample.

The predicate accepts any measure, not only a probability measure. Normalization remains a separate property.

The two invariant sanity checks

/-- The zero measure is invariant under unitary conjugation. -/
theorem isUnitaryConjugationInvariant_zero [Fintype ι] [DecidableEq ι] :
    IsUnitaryConjugationInvariant (0 : Measure (Matrix ι ι ℂ)) := by
  intro U
  simp

/-- The Dirac measure at the zero matrix is invariant under unitary
conjugation. -/
theorem isUnitaryConjugationInvariant_dirac_zero [Fintype ι] [DecidableEq ι] :
    IsUnitaryConjugationInvariant
      (Measure.dirac (0 : Matrix ι ι ℂ)) := by
  intro U
  rw [Measure.map_dirac' (measurable_congruence (U : Matrix ι ι ℂ))]
  simp

The zero measure is fixed by every measurable map, but it is not a probability law. The Dirac mass at the zero matrix is a probability law, and

This example is intentionally degenerate. It tests the definition without a Gaussian claim. A Dirac law at a generic nonzero Hermitian matrix is not fixed by every unitary.

Lift laws to bundled Hermitian matrices

A HermitianRandomMatrix stores a matrix map, global measurability, and pointwise Hermiticity.

The source first leaves the unbundled namespace and opens the bundled one:

end RandomMatrix

namespace HermitianRandomMatrix

variable {Ω : Type uΩ} {ι : Type uι} [MeasurableSpace Ω]

The bundled law and probability theorem

/-- The law of a bundled Hermitian random matrix. Its measurability evidence is
the corresponding field of the bundle. -/
noncomputable def law (X : HermitianRandomMatrix Ω ι) (μ : Measure Ω) :
    Measure (Matrix ι ι ℂ) :=
  RandomMatrix.law X.toRandomMatrix X.measurable_toRandomMatrix μ

/-- A probability measure on the sample space gives a probability law for a
bundled Hermitian random matrix. -/
theorem law_isProbabilityMeasure (X : HermitianRandomMatrix Ω ι) (μ : Measure Ω)
    [IsProbabilityMeasure μ] : IsProbabilityMeasure (law X μ) :=
  RandomMatrix.law_isProbabilityMeasure X.toRandomMatrix
    X.measurable_toRandomMatrix μ

The bundle supplies X.measurable_toRandomMatrix, so callers do not repeat the proof. The law still lives on the full complex matrix space. Although every realization is Hermitian, this file proves no full-measure support theorem for the Hermitian subset.

HermitianRandomMatrix.law_conjugateBy

/-- The law of `A X Aᴴ` is the congruence pushforward of the law of `X`. -/
theorem law_conjugateBy [Fintype ι] (A : Matrix ι ι ℂ)
    (X : HermitianRandomMatrix Ω ι) (μ : Measure Ω) :
    law (X.conjugateBy A) μ =
      Measure.map (RandomMatrix.congruence A) (law X μ) := by
  exact RandomMatrix.law_comp X.measurable_toRandomMatrix
    (RandomMatrix.measurable_congruence A) μ

Sample by sample, X.conjugateBy A is \(\omega\mapsto AX(\omega)A^*\). The theorem says

This identifies the transformed law. It does not claim invariance. The matrix \(A\) need not be unitary, while the result remains pointwise Hermitian because congruence preserves Hermiticity.

The bundled invariance predicate and its equality-in-law form

/-- A bundled Hermitian random matrix has a unitary-conjugation-invariant law
under `μ` when its pushforward law has that measure-level property. -/
def HasUnitaryConjugationInvariantLaw [Fintype ι] [DecidableEq ι]
    (X : HermitianRandomMatrix Ω ι) (μ : Measure Ω) : Prop :=
  RandomMatrix.IsUnitaryConjugationInvariant (law X μ)

/-- Invariance of the law is equivalent to equality in law after conjugation
by every element of `Matrix.unitaryGroup`. -/
theorem hasUnitaryConjugationInvariantLaw_iff [Fintype ι] [DecidableEq ι]
    (X : HermitianRandomMatrix Ω ι) (μ : Measure Ω) :
    HasUnitaryConjugationInvariantLaw X μ ↔
      ∀ U : Matrix.unitaryGroup ι ℂ,
        law (X.conjugateBy (U : Matrix ι ι ℂ)) μ = law X μ := by
  simp only [HasUnitaryConjugationInvariantLaw,
    RandomMatrix.IsUnitaryConjugationInvariant, law_conjugateBy]

When \(\mu\) is a probability measure, the right side is equality in distribution:

Equality in distribution means equality of pushforward probability measures. For an arbitrary measure \(\mu\), the checked theorem still states equality of pushforward measures, but probability terminology is not implied. The original and transformed maps share a sample space here, yet the theorem does not assert pointwise equality. The proof unfolds the definitions and rewrites the transformed law with law_conjugateBy.

The four symmetry levels

Unitary invariance in law does not require \(UX(\omega)U^*=X(\omega)\). A symmetric distribution can move individual samples around an orbit while leaving the distribution unchanged.

Declaration inventory

The file exposes twenty named declarations.

How to run the exact module

From the repository root:

source "$HOME/.elan/env"
cd formalization
lake env lean -DwarningAsError=true \
  NonlinearDynamics/Random/RandomMatrices/Laws.lean

Build the complete formalization from formalization/:

lake build

From the repository root, check the public teaching content:

make content-hygiene
make site-check

Preview drafts with make blog-serve at http://127.0.0.1:1333/.

Design decisions and limitations

The explicit hX argument prevents Mathlib’s total, zero-on-non-a.e.-measurable fallback from masquerading as a valid law. The bundled Hermitian type pays that proof once. The congruence map exists for all finite \(A\), while invariance restricts the actor to Mathlib’s unitary group. Arbitrary measures come first; IsProbabilityMeasure adds normalization as a separate property.

Important missing layers remain:

• no theorem that the bundled law gives full measure to the Hermitian subset;
• no codomain-general project theorem for scalar observable laws;
• no law constructor based only on almost-everywhere measurability;
• no general equality-in-law relation across different sample spaces;
• no Haar probability or integration on the unitary group;
• no Gaussian primitives, independence, covariance, or normalization;
• no eigenvalue measurability, spectral law, integrability, or expectation; and
• no GUE construction or GUE invariance theorem.

The frontier: what remains before GUE

Everything in this section is a roadmap. The checked declarations above stand on their own.

A finite GUE construction still needs an explicit dimension, a probability space or direct matrix measure, Gaussian diagonal and off-diagonal primitives, independence, conjugate reflection, an exact variance and dimension-scaling convention, measurability of the assembled matrix, identification of its law, and a proof that every unitary congruence pushforward fixes that law.

The current module supplies the language for the last steps, not their Gaussian premises or proof. Dyson’s symmetry analysis motivates the unitary class (Dyson, 1962); modern random-matrix texts develop concrete Gaussian laws and their normalization (Anderson, Guionnet, and Zeitouni, 2010).

Exercises: from preimages to ensemble design

1. Read a law on an event. Rewrite law X hX μ s as a source-space expression. Why does the answer use a preimage rather than an image?
2. Run the Dirac check. Put all source mass at \(\omega\). Where is the resulting matrix law concentrated?
3. Compose congruences. Apply \(C_B\), then \(C_A\). Use congruence_mul to identify the combined matrix and verify the order.
4. Separate symmetry from normalization. Explain why the invariant zero measure is not a probability law while \(\delta_0\) is.
5. Separate pointwise and law equality. Use a symmetric two-point scalar law under sign reversal as an analogy for unitary orbits.
6. Break a Hermitian Dirac law. Choose Hermitian \(H\) and unitary \(U\) with \(UHU^*\ne H\), then map \(\delta_H\).
7. Generalize law_comp. Give it an arbitrary target measurable space \(T\) and measurable \(f:\mathrm{Matrix}\to T\).
8. Design Hermitian support. State that the bundled law gives full mass to Hermitian matrices and identify the target-set measurability obligation.
9. Design the GUE endpoint. Write a normalization ledger and the exact HasUnitaryConjugationInvariantLaw goal the ensemble should satisfy.

Summit register

A measurable matrix map pushes a source measure onto matrix space. Measurable matrix transformations compose with that pushforward, probability mass remains one, and Dirac inputs behave like deterministic evaluation. Congruence supplies the algebraic action and preserves Hermiticity.

Restricting the actor to Mathlib’s unitary group lets the module define unitary-conjugation invariance as equality of measures. The bundled iff theorem translates it into equality in law between \(X\) and \(UXU^*\). This is the correct launchpad for GUE, not a GUE result.

References

The software references were checked against the project’s Mathlib 4.32.0 pin and official generated documentation on 2026-07-20. Book and journal links point to publisher or DOI records.

Mathlib contributors. Mathlib 4.32.0 release, commit 81a5d257c8e410db227a6665ed08f64fea08e997.

Mathlib contributors. Pushforward of a measure, with pinned source. This is the official source for Measure.map, its non-a.e.-measurable fallback, map_apply, map_id, and map_map.

Mathlib contributors. Dirac measures, with pinned source. This documents Measure.dirac and Measure.map_dirac'.

Mathlib contributors. Probability-measure typeclasses, with pinned source. This documents IsProbabilityMeasure and Measure.isProbabilityMeasure_map.

Mathlib contributors. The finite matrix unitary group, with pinned source. This is the official source for Matrix.unitaryGroup, its equations, group structure, and coercion to matrices.

Olav Kallenberg. Foundations of Modern Probability, third edition, Springer, 2021. This is a standard source for measurable random elements, image measures, and equality in distribution.

Greg W. Anderson, Alice Guionnet, and Ofer Zeitouni. An Introduction to Random Matrices, Cambridge University Press, 2010. This develops Gaussian ensembles, invariant matrix laws, and their normalization choices.

Freeman J. Dyson. Statistical Theory of the Energy Levels of Complex Systems. I, Journal of Mathematical Physics 3, 140–156, 1962. This primary historical source organizes spectral statistics by orthogonal, unitary, and symplectic symmetry classes. It does not warrant a claim that this module constructed GUE.