Averaged Hermitian form for a compact group

Assume the Axiom of Choice (The Axiom of Choice). Let $K$ be a compact Hausdorff group and let $\mu$ be its normalized Haar probability measure (Normalized Haar probability on a compact group); this is the only place the Axiom of Choice is consumed by the definition.

Let $V$ be a finite-dimensional complex vector space and let $\rho :K\to \mathrm{GL}(V)$ be a continuous finite-dimensional complex representation: a homomorphism of groups such that $\rho$ is continuous when $\mathrm{GL}(V)\subseteq \mathrm{End}(V)$ carries the topology induced by a norm on $\mathrm{End}(V)$. In finite dimension any two norms on $\mathrm{End}(V)$ induce the same topology (A chosen algebraic basis identifies a finite-dimensional normed space with a coordinate space), so the continuity requirement does not depend on the norm chosen.

Let $h_0$ be a Hermitian inner product on $V$ that is linear in the first variable and conjugate-linear in the second (Real and complex inner-product spaces and their induced length). The averaged Hermitian form of the pair $(\rho ,h_0)$ is the map $h:V\times V\to \mathbb{C}$ defined by

$h(v,w):={\int }_K{h}_0(\rho (k)v,\rho (k)w)d\mu (k)\mathrm{.}$

Well-definedness and conventions. The form $h_0$ is linear in the first and conjugate-linear in the second variable, and so is $h$: for each fixed $k$ the integrand is linear in $v$ and conjugate-linear in $w$, and these properties pass through the integral. Hermitian symmetry likewise passes to the limit because the integrand of $h(w,v)$ is the complex conjugate of the integrand of $h(v,w)$ for every $k$. For fixed $v,w$ the integrand $k\mapsto h_0(\rho (k)v,\rho (k)w)$ is continuous: $\rho$ is continuous, evaluation $g\mapsto \rho (g)v$ is therefore continuous, and $h_0$ is continuous on the finite-dimensional space $V\times V$ (The inner product is jointly continuous). A continuous complex function on the compact space $K$ is bounded and integrable against the Borel probability measure $\mu$, so the displayed integral is a finite complex number and $h$ is a sesquilinear form, linear in its first variable and conjugate-linear in its second. Whether $h$ is positive definite and $\rho (K)$-invariant is a theorem, not a convention: those two properties are proved in Averaging a Hermitian form unitarizes a finite-dimensional compact-group representation.