On a compact group there is exactly one symmetric notion of volume. Every forced measure downstream of this programme inherits its uniqueness from that one fact.
Here is the problem. Suppose you want to average over all rotations, or pick a random symmetry, or say two families of transformations are the same size. You need a notion of volume on the set of transformations itself -- and it had better not depend on your parametrisation, or your average is an artefact of your coordinates.
The demand sounds mild: sizes should not change when everything is shifted by a group element. For compact groups it is devastatingly restrictive. Exactly one such volume exists, once you fix the total to one. Not one natural choice among several -- one, full stop.
So questions like what does a random unitary do have definite, coordinate-independent answers. That is Haar's gift, and half of modern mathematics quietly leans on it.
Trace the programme's central claim back far enough and you land here. The chain: the unitary group is compact, so it has a unique invariant probability measure. The state space is a quotient of that group -- a homogeneous space. Push the measure down along the orbit map and the uniqueness comes with it. That is the whole proof that the Fubini-Study measure is forced.
Remove this link and everything downstream changes character: the measure becomes a preference, the Born derivation becomes circular, the reply to the smuggled-measure objection evaporates. It is also, pleasingly, what makes the base point of the construction immaterial -- any two orbit maps differ by a group element, and Haar measure cannot see group elements.
A compact topological group carries a unique translation-invariant Borel probability measure. On a homogeneous space of such a group, invariant measures are unique up to scale, and normalisation fixes the scale.
The corpus uses the unitary group's Haar measure directly and pushes it forward along the orbit map; uniqueness downstairs is inherited from uniqueness upstairs. No geometric argument is involved in the uniqueness proof -- it is group theory and measure theory all the way down.
Alfred Haar (1885-1933) was born in Budapest and took his doctorate at Gottingen under Hilbert in 1909; the Haar wavelet, now the first example in every wavelet course, is from that thesis. With Frigyes Riesz he built the mathematics institute at Szeged into a serious research centre -- and its journal, Acta Scientiarum Mathematicarum, into a serious journal.
The measure theorem is from 1933, the last year of his life; he died of cancer at forty-seven. Von Neumann, who had been sceptical that such a measure existed in general, used it almost immediately to solve Hilbert's fifth problem for compact groups, and Weil built the general theory soon after. The result outlived its author before the year was out.
Source links are pinned to a commit, so they do not drift. The anchors above are checked mechanically against the Lean tree on every build. The mathematics is not, and cannot be: that is a human responsibility and it rests with the author.
Part of Constraint-Surface Dynamics · Formalised in csd-lean4.
Google Analytics counts visits to this page, which stores cookies in your browser. They record how the page was reached, not who you are, and nothing is passed on. Blocking cookies for this site breaks nothing here. Details.