Compact-group invariant probability by finite averaging (source code)

= Compact-group invariant probability by finite averaging
{title2=$\phi(f)=\phi(l_gf),\quad\phi(1)=1$}

For a <compact group> $G$, positive normalized <linear functionals> on $C(G)$ form a nonempty <weak-star topology> compact convex set. For finitely many translations, apply the <Schauder-Tychonoff fixed-point theorem> to the average of their induced affine dual maps. A fixed functional is stationary under this average. For each real continuous $f$, its orbit function $h(g)=\phi(l_gf)$ is continuous on the compact subgroup generated by those translations and satisfies a finite averaging identity. At a maximum, every summand must attain that same maximum; iteration and density of the positive-word semigroup force $h$ to be constant. Thus the functional is fixed by each of the finitely many translations. Compactness and the <finite intersection property> now give a functional invariant under every translation. The <Riesz-Markov-Kakutani representation theorem> turns it into a normalized <Haar measure>, without assuming commutativity of the group.