Theorem. Normalized Haar measure [fdip-007B]

✍️sourceAGENTDRAFTED

Every compact Hausdorff topological group \(G\) has a unique regular Borel probability measure \(\mu _G\) invariant under left translation. This is the normalized Haar theorem, used here as a cited statement; existence and uniqueness are not proved in these notes. The existence and uniqueness-up-to-scale statements are Theorems 4.3 and 4.6 in [gleason2010haar, pp. 6, 11]. Compactness permits normalization to total mass one.

The normalized measure is also invariant under right translation and inversion. Indeed, a right translate of \(\mu _G\) is another left-invariant regular probability measure, hence equals \(\mu _G\) by uniqueness. The pushforward under inversion is then left invariant, because inversion changes left translations into right translations; it too has total mass one and equals \(\mu _G\). These deductions explain why the same measure works with either orientation of an edge.

Every nonempty open set has positive Haar measure. If an open set had measure zero, choose a point in it; its left translates cover \(G\), and compactness gives a finite subcover, contradicting total mass one. Consequently a continuous function that vanishes \(\mu _G\)-almost everywhere vanishes everywhere.

For a finite group this measure is uniform counting. For \(U(1)=\{e^{i\theta }:\theta \in \mathbb R\}\), it is \(d\theta /(2\pi )\) on one period: translation invariance and total mass one identify this measure by uniqueness. Product Haar measure on the edge space \(G^E\) supplies the compact measure assumed in the joint matter law. For \(U(1)\) and \(SU(2)\), all spaces here are compact metrizable, so their Borel products have the usual product measurable structure.

Mathlib constructs Haar measure as MeasureTheory.Measure.haarMeasure, normalized on a chosen compact set with nonempty interior; for compact \(G\), choose that set to be all of \(G\). The separate declaration MeasureTheory.Measure.isHaarMeasure_eq_of_isProbabilityMeasure asserts equality of two Haar probability measures on a locally compact topological group with its Borel measurable structure. It has no second-countability assumption. These are correspondences for the construction and normalized uniqueness, respectively; the right and inversion invariance arguments above are stated separately.