Originally written by Claude Opus 5.5 (Anthropic), September 2026, with a separate historical AI spot-check of that text. Repaired and self-checked by GPT-6.1 Sol (OpenAI), Ultra reasoning effort, October 2026. The current edition has no separately recorded independent AI or human review. Original programme content is dedicated under CC0.
Bounded prerequisite selection (October 2026). This companion selects the original header and credits (lines 1–19) and the full conventions and positive Riesz argument (lines 21–96), including all six construction steps, regularity on sigma-finite sets, compactly supported density and the positive-functional norm argument. Original introductory references to later parts of the full Haar lesson are retained as source context. The required topology and measure proofs are available locally in topology-cutoffs and measure-tools. References to later Haar sections, Hilbert spaces and arbitrary-product results concern unselected material. The later Fremlin-following uniqueness supplement is not included. The selected source prose and mathematics are unchanged apart from link destinations and line-ending normalization. Selection and link repair: GPT-6.1 Sol (OpenAI), Ultra reasoning effort, for the AN-01 course project.
This lesson constructs Haar measure on an arbitrary locally compact group and develops the measure theory that goes with it. Sections 2–6 work on locally compact spaces. They prove the Riesz representation theorem for Radon measures, treat image measures and densities, build the product of two Radon measures with its Tonelli and Fubini theorems, and identify of a product with a Hilbert tensor product. Sections 7–11 turn to groups: topological groups, existence and uniqueness of Haar measure, the modular function, and the inversion formula. Sections 12–15 treat products of groups, groups that are not -compact, convolution, and approximate identities. Section 16 has exercises with solutions.
No countability assumption is made anywhere. The group need not be -compact, second countable or unimodular, and its Haar measure need not be -finite. This generality needs care: a Borel set of infinite measure can have only null compact subsets, and Fubini's theorem can fail. Section 13 shows what goes wrong, and the rest of the lesson is arranged so that it does no harm.
Haar measure makes a locally compact group into a measure space on which acts by translations. Then is a Banach -algebra under convolution, and carries the left and right regular representations. These objects are the starting point of abstract harmonic analysis, and of the group von Neumann algebras studied in the course on modular theory and weights.
The lesson builds on four sources, cited where they are used:
The exact statements are collected at the end, under "Results used from other lessons". Core preparation is Point-Set Topology; Measure and Integration provides Fremlin’s broader measure-theory setting. The arbitrary-product and Hilbert-space proofs used here are the advanced programme results named above.
Freely accessible complementary treatments are Fremlin’s Measure Theory and F. van Doorn’s Formalized Haar Measure. Fischer and Ruzhansky’s freely accessible Quantization on Nilpotent Lie Groups supplies further convolution and Heisenberg-group examples. The historical development from Haar and von Neumann to Weil and Cartan is discussed in F. van Doorn’s paper; the original accessible von Neumann and Cartan papers are linked below.
1. Conventions
Spaces. An LCH space is a Hausdorff space that is locally compact. Its compact subsets are closed. is the space of continuous complex functions with compact support, is the set of with and , and . For an open set we write when , and . For a compact set we write when , and on . A function is lower semicontinuous (lsc) if every set is open; lsc functions are Borel.
Four tools from topology. The first two tools are proved in the lesson on the Stone–Weierstrass theorem; we derive the other two from them.
(T2) (Urysohn's lemma) If as in (T1), there is with . Proof. Take from (T1). Corollary 5.2 of the Stone–Weierstrass lesson, applied to the compact set and the closed set , gives with , on and off . Then .
(T3) (Partitions of unity) If is compact and with each open, there are with on and everywhere. Proof. For each pick an index with , and by (T1) an open whose compact closure lies in . Finitely many cover . Let be the union of the closures of the chosen that were assigned to . Then is compact, , and . Choose by (T2) and set and . By induction, . This lies in , and it equals on each .
(T4) (Tube lemma) If and are compact and with open in , there are open and with . Proof. Fix . Each , , lies in an open box inside ; finitely many boxes of this kind have covering . Put and ; then . Cover by finitely many , and let and .
Measures and functions. A measure is positive and countably additive. denotes the Borel sets of , the -algebra generated by the open sets; functions on are Borel unless said otherwise. A Borel set is -finite for a measure when countably many Borel sets of finite measure cover it. For , consists of the Borel functions with , modulo functions that vanish almost everywhere. Hilbert spaces are complex, and the inner product is linear in . For a Borel we use the layer functions
They are simple Borel functions, and they vanish where does. They increase, , because the -th term of is at most the sum of the terms of with indices and . And at every point: if , then , and if , then . The monotone and dominated convergence theorems, Hölder's inequality, and the completeness of are proved in Measure and Hilbert space tools for Haar integration, Theorems 2.1, 2.2, 3.1 and 3.2. The exact uses are listed under "Results used from other lessons".
Groups. A group is a locally compact group when it carries a locally compact Hausdorff topology for which and are continuous; is its identity. For a function on and put
Then and . The left and right regular representations of on are and , where is the modular function of Section 10; Exercise 16.3 shows that they are unitary representations.
2. Radon measures and the Riesz representation theorem
Definition 2.1 (Radon measure). A Radon measure on an LCH space is a measure on with the following three properties.
(R1) for every compact .
(R2) (outer regularity) for every Borel set .
(R3) (inner regularity on open sets) for every open .
This is the notion of regularity used throughout the lesson. Inner regularity is not required on all Borel sets, because it can fail (Example 13.4). Proposition 2.3 shows that it holds on every -finite set.
Theorem 2.2 (Riesz representation theorem). Take a positive linear functional on . There is exactly one Radon measure on with for every . Moreover, every Radon measure satisfies, with ,
Regularity warning: The stronger requirement that a measure be inner and outer regular on every Borel set is inappropriate here. In that form it fails for the Haar integral of (Example 13.4).
Proof.Step 1: formula (2.1) and uniqueness. Let be Radon. If , then . If is compact, Urysohn's lemma (T2) gives , and then . With (R3) this proves the first formula. If , then ; if is open, (T2) gives with . With (R2) this proves the second formula. By the first formula, two Radon measures that give every the same integral agree on open sets, and then on all Borel sets by (R2).
Step 2: an outer measure. For open define , and for any put . Then on open sets, and is monotone. Let with open, and let . The compact set lies in for some . The partition of unity (T3) gives with on . So with , and . Hence . For arbitrary sets , choose open with ; this gives . So is an outer measure.
Step 3: open sets are measurable. Let be open. By Carathéodory's theorem the preceding tools lesson, Theorem 1.1 it is enough to show whenever . First let be open. Given , choose with . The set is open; choose with . The supports of and are disjoint, so and
since . For general , take an open with , apply the open case, and use monotonicity. By Carathéodory's theorem the -measurable sets form a -algebra on which is countably additive. It contains the open sets, hence . Let be the restriction of to . It satisfies (R2) by construction.
Step 4: compact sets. Let be compact and ; in particular . For the open set contains , and every satisfies . So , and letting gives . Some with exists by (T2) with , so , which is (R1). Given , choose an open with and then with : . This proves the second formula of (2.1).
Step 5: (R3). If , then for every open , so , and by (R2). Taking the supremum over gives . The reverse inequality is monotonicity.
Step 6: represents . By linearity it suffices to treat real with . Fix . Put , for (compact sets), and . Then , each is in with , and . Integrating, . On the other side, by Step 4. Also for every open , so , and by (R2). Summing over , both and lie between and . These bounds differ by at most . Let .
Proposition 2.3 (Regularity on -finite sets). Every Radon measure on has the following properties.
If is Borel and , then .
The same holds for every Borel set that is -finite for .
Every -finite Borel set is the union of a -compact set and a Borel null set.
Proof. (1) Let . By (R2) choose an open with , so . Again by (R2) choose an open with . By (R3) choose a compact with . The compact set lies in : a point of outside is in . And .
(2) Write as an increasing union of Borel sets of finite measure; then , and (1) applies to each .
(3) With as in (2), choose compact with . The -compact set lies in , and for every , so .
Where the hypotheses enter. Local compactness and the Hausdorff property are used only through (T1)–(T3): they supply enough functions . No countability is used, and the measure need not be -finite. A measure that is inner and outer regular on every Borel set would be more convenient, but Example 13.4 shows that on the group no measure of that kind represents Haar integration. So the lesson never uses inner regularity on arbitrary Borel sets.
Bounded functionals on
The operator-algebra lessons also use the bounded, not necessarily positive, linear functionals on , the space of continuous functions vanishing at infinity with the norm . Call a functional hermitian if is real for every real . Two facts are used below.
is dense in . For and , the set is compact. Choose by (T2). Then and .
Norms of positive functionals. A positive linear functional on is hermitian, since every real is . If is bounded, then , and by (2.1) this is for the Radon measure that represents on . Indeed, for choose with , and write with real. Then forces , and with . The functions suffice, by the density just proved.
Original source bibliography, retained
References
[Fremlin] D. H. Fremlin, Measure Theory, Volumes 1, 2 and 4, author’s freely accessible text and editable TeX. Volume 4 uses complete, locally determined Radon measures; Proposition 13.7 relates that convention to ours.
[van Doorn] F. van Doorn, Formalized Haar Measure, 2021, arXiv version 1. The paper constructs Haar measure on arbitrary LCH groups; its uniqueness proof assumes second countability. The current mathlib uniqueness development also distinguishes regularity hypotheses.
[Cartan 1940] H. Cartan, Sur la mesure de Haar, Comptes Rendus de l'Académie des Sciences de Paris 211 (1940), 759–762. https://gallica.bnf.fr/ark:/12148/bpt6k3163d/f759.item
[von Neumann 1936] J. von Neumann, The uniqueness of Haar's measure, Matematicheskii Sbornik (N.S.) 1(43) (1936), 721–734. https://www.mathnet.ru/eng/sm5481
[Fischer–Ruzhansky] V. Fischer and M. Ruzhansky, Quantization on Nilpotent Lie Groups, Birkhäuser, 2016, freely accessible. Its Heisenberg and homogeneous-group treatment complements Example 12.3; its convolution discussion includes the full Young bound of Theorem 14.4. The calculations and proof here are independently written.
Source and rights
The selected original programme exposition is dedicated under CC0 1.0. Historical authorship and checking statements remain exactly as supplied in the source header. External references retain their own rights; their text is not reproduced here. The CC0 legal text and component provenance accompany this selection. The full transparent source remains available at its original source location.