The Haar probability measure on the matrix unitary group

Category: 1-Mathlib (CSD-free).

Matrix.unitaryGroup ι ℂ is a compact Hausdorff topological group with a Borel structure (UnitaryCompact.lean), so Mathlib's Haar measure is available on it, and haarMeasure ⊤ — the Haar measure normalised to give the whole group mass 1 — is its Haar probability measure.

• unitaryHaarProb — that measure, under the name every consumer uses (the Fubini–Study measure on ℂℙ^{N-1} is its pushforward along an orbit map, Projectivization/FubiniStudy.lean);
• instIsProbabilityMeasureUnitaryHaarProb, unitaryHaarProb_isHaarMeasure — the two instances, both inherited from Mathlib (haarMeasure_self, isHaarMeasure_haarMeasure). Right-invariance, from uniqueness on a compact group, is instIsMulRightInvariantUnitaryHaarProb (FubiniStudyUnique.lean).

Until 2026-09-16 this file re-built the measure by hand ((haar univ)⁻¹ • haar) and re-proved both instances; the external review of the Physlib closure flagged the duplication.

noncomputable def Matrix.UnitaryGroup.unitaryHaarProb {ι : Type u_1} [Fintype ι] [DecidableEq ι] : MeasureTheory.Measure ↥(unitaryGroup ι ℂ)

The Haar probability measure on U(N): Mathlib's haarMeasure ⊤, the Haar measure normalised so that the whole (compact) group has mass 1.

Equations

• Matrix.UnitaryGroup.unitaryHaarProb = MeasureTheory.Measure.haarMeasure ⊤

instance Matrix.UnitaryGroup.instIsProbabilityMeasureUnitaryHaarProb {ι : Type u_1} [Fintype ι] [DecidableEq ι] : MeasureTheory.IsProbabilityMeasure unitaryHaarProb

unitaryHaarProb is a probability measure: haarMeasure K₀ K₀ = 1 at K₀ = ⊤.

instance Matrix.UnitaryGroup.unitaryHaarProb_isHaarMeasure {ι : Type u_1} [Fintype ι] [DecidableEq ι] : unitaryHaarProb.IsHaarMeasure

unitaryHaarProb is a Haar measure (Mathlib's isHaarMeasure_haarMeasure).