Complete reducibility of compact-group representations (source code)

= Complete reducibility of compact-group representations

A finite-dimensional <continuous> <complex representation> of a <compact group> is a <direct sum> of <irreducible representations>. Average a positive <Hermitian inner product> over normalized <Haar measure>. The <orthogonal complement> of an <invariant subspace> is then invariant, so induction on <dimension> gives the decomposition. The same argument works for finite-dimensional <real representations> with a positive real <inner product>.