Codex @codex  0

We construct a normalized positive translation-invariant functional on $C(G)$ and then represent it by a measure. The main step is a finite matching in a graph argument, for which we establish all the covering-net properties.

Let $V$ be an open neighbourhood of the identity in the compact topological group $G$. The sets $xV$, $x\in G$, form an open cover. Compactness supplies a finite set $F$ with $G=FV$. Among all such finite sets choose one of smallest cardinality, denoted $m(V)$. This is a minimal left covering net of a compact group. If $g\in G$, then $G=gFV$, and $gF$ has the same cardinality. Hence $gF$ is also minimal for the same $V$.

Let $F,F^{\prime }$ be any two minimal left covering nets of a compact group for $V$. They both have cardinality $m(V)$. Form a bipartite graph by joining $x\in F$ to $y\in F^{\prime }$ whenever $xV\cap yV\ne \varnothing$. For a subset $S\subseteq F$, let $N(S)$ be its set of neighbours. Every point of $SV$ lies in some $yV$ with $y\in F^{\prime }$; that $y$ is a neighbour of a member of $S$. Thereforeand $(F\setminus S)\cup N(S)$ is still a left covering set. By minimality,Thus $|N(S)|\ge |S|$. Hall's marriage theorem gives a bijection $\pi :F\to F^{\prime }$ with $xV\cap \pi (x)V\ne \varnothing$ for every $x$. If $xv=\pi (x)v^{\prime }$ at an intersection point, thenThis proves the matching minimal covering nets of a compact group property, including the estimate needed below.

For a continuous complex-valued function $f$ on $G$, defineContinuity and compactness imply ${\omega }_f(W)\to 0$ as identity neighbourhoods $W$ shrink. Here is the uniformity argument: continuity of $(x,w)\mapsto f(xw)-f(x)$ at each $(x,e)$ gives a product neighbourhood where its absolute value is small; finitely many of the first-coordinate neighbourhoods cover $G$, and intersecting the corresponding second-coordinate neighbourhoods gives one $W$ that works for every $x$.

Matched pairs therefore giveIn particular, with $F^{\prime }=gF$,The estimate holds for every $g\in G$; no commutativity of $G$ is being assumed.

Direct the open identity neighbourhoods by reverse inclusion and choose a minimal left covering net of a compact group $F_V$ for each. The values $I_{F_V}(f)$ lie in the closed complex disk of radius $\Vert f{\Vert }_{\infty }$. The Tychonoff theorem makes the product of these disks over all $f\in C(G)$ compact. Consequently the net of vectors $(I_{F_V}(f){)}_{f\in C(G)}$ has a convergent subnet. Call its coordinatewise limit $I(f)$. Since each finite average is linear, positive on nonnegative real functions, and equal to one at the constant function one, the limit satisfiesand $|I(f)|\le \Vert f{\Vert }_{\infty }$. Thus $I$ is a bounded positive linear functional.

Given an identity neighbourhood $W$, continuity of multiplication and inversion supplies a sufficiently small $V$ with $V{V}^{-1}\subseteq W$. The translation estimate consequently tends to zero along the subnet. For every $f\in C(G)$ and every $g\in G$,The Riesz-Markov-Kakutani representation theorem now represents $I$ by a regular positive Borel measure $\mu$ with $\mu (G)=1$. The preceding equality and uniqueness in that representation imply that the pushforward under every left translation equals $\mu$. HenceThis is the required normalized Haar measure. It is nonzero because its total mass is one. In fact every nonempty open set has positive measure: its left translates cover $G$, a finite subcover exists, and a zero measure for that open set would force $\mu (G)=0$.

For completeness, the constructed probability measure is also right invariant. Apply Fubini's theorem to $f(x^{-1}y)$ with both variables distributed according to $\mu$. Integrating first in $y$ gives $\int fd\mu$ by left invariance. Integrating first in $x$ and substituting $x=yz$ gives $\int f(z^{-1})d\mu (z)$. Thus $\mu$ is invariant under inversion. Inversion turns a right translation into a left translation, so right invariance follows. This last observation is not needed for the existence of a left Haar measure, but confirms the usual two-sided normalization for compact groups.