Character induction norm bound (source code)

= Character induction norm bound

Extend a class function $\psi$ on $H$ by zero outside $H$. For coset representatives $x_1,\ldots,x_m$ of $G/H$, $\operatorname{Ind}_H^G\psi(g)=\sum_j\psi_0(x_j^{-1}gx_j)$. Each summand has squared normalized $G$-norm $\|\psi\|_H^2/m$. Pointwise <Cauchy-Schwarz inequality> and summation give $\|\operatorname{Ind}\psi\|_G^2\le m\|\psi\|_H^2$. If $\psi$ is an irreducible character, its norm is one, and the sum of squared induction multiplicities is at most the subgroup index.