Haar measure on the matrix unitary group #

Category: 1-Mathlib (CSD-free Mathlib smoke test).

This file verifies that Mathlib's Haar measure infrastructure (MeasureTheory.Measure.haar) is callable on Matrix.unitaryGroup (Fin N) ℂ once the topology/compactness/measurability instances from UnitaryCompact.lean are in place.

The chain #

For haar : Measure G to typecheck, Lean needs:

Group G — Mathlib's Matrix.unitaryGroup is a Group (subgroup of units).
TopologicalSpace G — inherited from Matrix _ _ ℂ via the subtype topology.
IsTopologicalGroup G — Mathlib generic from Topology/Algebra/Star/Unitary.lean.
MeasurableSpace G — installed by UnitaryCompact.instMeasurableSpace.
BorelSpace G — installed by UnitaryCompact.instBorelSpace.
LocallyCompactSpace G — chains automatically: CompactSpace (UnitaryCompact.instCompactSpace) gives WeaklyLocallyCompactSpace (Mathlib priority-100 instance), which gives LocallyCompactSpace in the presence of R1Space (implied by T2Space, which the subtype inherits from Matrix _ _ ℂ).

Verified #

unitaryHaar : Measure (Matrix.unitaryGroup (Fin N) ℂ) — the chosen Haar measure.
IsHaarMeasure unitaryHaar — left-invariant + finite on compacts + positive on nonempty opens.
IsFiniteMeasure unitaryHaar — the whole space is compact, so the Haar measure is finite.

What this unlocks #

With Mathlib's Haar measure callable, the next steps for LF4 are normalisation to a probability measure (deferred to a follow-up tranche) and the Fubini-Study pushforward to ℂℙ^{N-1}.

Tags #

unitary group, Haar measure, compact group

source

noncomputable def Matrix.UnitaryGroup.unitaryHaar {N : ℕ} :

MeasureTheory.Measure ↥(unitaryGroup (Fin N) ℂ)

A chosen Haar measure on the matrix unitary group Matrix.unitaryGroup (Fin N) ℂ. This is MeasureTheory.Measure.haar specialised.

Equations

Matrix.UnitaryGroup.unitaryHaar = MeasureTheory.Measure.haar

Instances For

source

instance Matrix.UnitaryGroup.unitaryHaar_isHaarMeasure {N : ℕ} :

unitaryHaar.IsHaarMeasure

unitaryHaar is a Haar measure (left-invariant + regular + positive on opens + finite on compacts).

source

instance Matrix.UnitaryGroup.instIsFiniteMeasureUnitaryHaar {N : ℕ} :

MeasureTheory.IsFiniteMeasure unitaryHaar

unitaryHaar is finite (because the whole group is compact).

Smoke-test usage #

Confirms that the typeclass chain (CompactSpace → WeaklyLocallyCompactSpace → LocallyCompactSpace given T2; plus IsTopologicalGroup, MeasurableSpace, BorelSpace) fires correctly. The four examples below all elaborate via inferInstance; each is a witness that Lean can synthesise the corresponding fact about the Haar measure.

Normalisation to a probability measure #

unitaryHaar is finite (compact group) and gives positive mass to the whole space (Haar measure on a nonempty open set is positive). We can therefore rescale by (unitaryHaar Set.univ)⁻¹ to obtain a probability measure that is still Haar (Haar property is preserved under positive finite scaling).

The resulting unitaryHaarProb is the canonical translation-invariant (Haar) probability measure on the unitary group U(N), and the ingredient that the Fubini-Study measure on ℂℙ^{N-1} will be constructed from via pushforward (next tranche).

source

theorem Matrix.UnitaryGroup.unitaryHaar_univ_ne_zero {N : ℕ} :

unitaryHaar Set.univ ≠ 0

The total mass unitaryHaar Set.univ is nonzero, because Set.univ is a nonempty open set and Haar measure is IsOpenPosMeasure.

source

theorem Matrix.UnitaryGroup.unitaryHaar_univ_ne_top {N : ℕ} :

unitaryHaar Set.univ ≠ ⊤

The total mass unitaryHaar Set.univ is finite, because the group is compact and Haar measure is IsFiniteMeasureOnCompacts.

source

noncomputable def Matrix.UnitaryGroup.unitaryHaarProb {N : ℕ} :

MeasureTheory.Measure ↥(unitaryGroup (Fin N) ℂ)

The probability-normalised Haar measure on the matrix unitary group.

Defined as (unitaryHaar Set.univ)⁻¹ • unitaryHaar. Both IsProbabilityMeasure and IsHaarMeasure are instances; see instIsProbabilityMeasureUnitaryHaarProb and unitaryHaarProb_isHaarMeasure below.

Equations