Averaging a Hermitian form unitarizes a finite-dimensional compact-group representation

Given: AC, a compact Hausdorff group $K$ with normalized Haar probability $\mu$, a continuous finite-dimensional complex representation $\rho :K\to \mathrm{GL}(V)$, a Hermitian inner product $h_0$ on $V$ linear in the first variable, and the averaged form $h$.

The averaged form is well defined: $h$ is a sesquilinear form on $V$, linear in the first variable and conjugate-linear in the second, it is Hermitian in the sense $h(v,w)=\overline{h(w,v)}$, the integrand $k\mapsto h_0(\rho (k)v,\rho (k)w)$ is continuous on $K$ for all $v,w\in V$, and a continuous complex function on the compact space $K$ is bounded and integrable against the Borel probability measure $\mu$, so the defining integral is a finite complex number (Averaged Hermitian form for a compact group).

Normalized Haar: $\mu$ is a Borel probability measure with $\mu (K)=1$ that is left and right invariant, $\mu (aE)=\mu (E)$ and $\mu (Ea)=\mu (E)$ for every Borel set $E\subseteq K$ and every $a\in K$, and $\mu (U)>0$ for every nonempty open $U\subseteq K$ (Normalized Haar probability on a compact group, Haar measure is positive on nonempty open sets and finite on compact sets, Measure spaces).

The form $h_0$ is an inner product: it is linear in the first variable, conjugate-linear in the second, Hermitian, and positive definite, $h_0(v,v)\ge 0$ with $h_0(v,v)=0$ exactly for $v=0$; its induced length is $\mathrm{\parallel }v{\mathrm{\parallel }}_h:=\sqrt{h(v,v)}$ for any inner product $h$ (Real and complex inner-product spaces and their induced length, Real and complex inner product spaces, with the inner product linear in the first argument).

$\rho$ is a group homomorphism with $\rho (e)=I_V$ and $\rho (kg)=\rho (k)\rho (g)$ for all $k,g\in K$, and each $\rho (g)$ is an invertible linear map of $V$; the map $\rho :K\to \mathrm{GL}(V)$ is continuous (A finite-dimensional representation $\rho :G\to \mathrm{GL}(V)$ over a field, and its degree).

A continuous self-map $T$ of the measure space $(K,\mathcal{B}(K),\mu )$ is Borel measurable, and it is measure preserving when $\mu (T^{-1}E)=\mu (E)$ for every Borel $E$; in that case ${\int }_{K}f\circ Td\mu ={\int }_{K}fd\mu$ for every integrable $f$ (Measure-preserving transformations and systems, Integral invariance under measure-preserving maps). Right translation $T_g(k):=kg$ is a homeomorphism because multiplication in a topological group is continuous (Topological group: multiplication and inversion are continuous), and by [F2] it is measure preserving: $T_g^{-1}E=E{g}^{-1}$ has $\mu (E{g}^{-1})=\mu (E)$.

Nonnegative measurable real functions have an extended integral that is monotone and positively homogeneous, and for nonnegative simple functions it agrees with the simple integral $\int {\sum }_j{c}_j{\chi }_{E_j}d\mu ={\sum }_j{c}_j\mu (E_j)$; in particular $\int c{\mathbf{1}}_{U}d\mu =c\mu (U)$ for $c\ge 0$. For a real measurable $f\ge 0$ the Lebesgue integral of $f$ equals this nonnegative integral, since the negative part vanishes (Monotonicity and nonnegative homogeneity of the nonnegative integral, The nonnegative integral agrees with the simple integral on simple functions, The integral of a nonnegative simple function, Integrable real and complex functions, and their integrals).

A linear map $T:V\to W$ between inner product spaces is a linear isometry if $\mathrm{\parallel }Tv\mathrm{\parallel }=\mathrm{\parallel }v\mathrm{\parallel }$ for every $v$, and an invertible linear isometry from a finite-dimensional complex inner product space to itself is a unitary operator (Linear isometries, and orthogonal or unitary operators on finite-dimensional inner product spaces).

A map is continuous exactly when preimages of open sets are open, and the interval $(\epsilon ,\mathrm{\infty })$ is open in $\mathbb{R}$ for every real $\epsilon$ (For a map of spaces the following agree: continuity at every point, preimages of open sets open, preimages of closed sets closed, preimages of subbasic open sets open, and $f(\bar{A})\subseteq \overline{f(A)}$, Continuity of a map of topological spaces at a point and globally, The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies).