Context
$\DeclareMathOperator\cp{cp}\DeclareMathOperator\AM{AM}\DeclareMathOperator\A{A}$For a finite group $G$ and $k\in\mathbb R$, define $$ m_k(G) = \frac{1}{|G|} \sum_{\pi\in\widehat{G}} (d_\pi)^{k+2}. $$
We can view $m_k(G)$ as the $k$th moment of a natural probability distribution on $\widehat{G}$. Particular cases have appeared in the literature under different names:
$m_{-2}(G)$ coincides with the commuting probability $\cp(G)$ which has been extensively studied.
$m_{-1}(G)$ coincides with the function $f(G)$ that is studied in connection with sums of character degrees, see e.g. Chapter 11 of Berkovich–Zhmud - Characters of finite groups.
$m_1(G)$ coincides with $\AM(\A(G))$, the amenability constant of the Fourier algebra of $G$.
(Strictly speaking, the last of these is a theorem not a definition: $\A(G)$ is a particular Banach algebra associated to any locally compact group $G$; the amenability constant is a $[0,\infty]$-valued invariant associated to any Banach algebra; the fact that $\AM(\A(G))=m_1(G)$ is a 1994 theorem of Johnson (Non-amenability of the Fourier algebra of a compact group).)
If $H$ is a subgroup of $G$, then the following inequalities are known:
$\cp(H)\geq \cp(G)$ — attributed to Ernest, with another proof by Gallagher;
$f(H)\geq f(G)$ — I don't know where this first appeared, but it can be found as part of Lemma 6 in Chapter 11 of Berkovich–Zhmud;
$\AM(\A(H)) \leq \AM(\A(G))$ — this holds for all locally compact groups, not just finite ones, and does not rely on Johnson's 1994 theorem.
An observation
During discussions last year with a visitor, I realised that the proof in the BZ book of $f(H)\geq f(G)$ can be generalised quite easily to show the following:
Theorem 1. If $F:{\mathbb N} \to {\mathbb R}$ is an increasing function (not necessarily strictly increasing) and $H\leq G$, then $$ \sum_{\pi\in\widehat{H}} \frac{(d_\pi)^2}{|H|} F(d_\pi) \leq \sum_{\pi\in\widehat{G}} \frac{(d_\pi)^2}{|G|} F(d_\pi). $$
As an immediate corollary, we obtain a result for moments that unifies the three inequalities mentioned above.
Corollary 2. Let $H\leq G$. If $k\leq 0$ then $m_k(H)\geq m_k(G)$. If $k\geq 0$ then $m_k(H)\leq m_k(G)$.
Questions regarding the literature
Q1. Does anyone know if Corollary 2 (or indeed Theorem 1) has appeared in the literature? If I am reinventing the wheel, it would be good to know sooner rather than later.
Q2. Do specialists think there is merit in writing up a proof of Theorem 1? It does feel like once one knows the three inequalities above and looks at the proof of the 2nd one in Berkovich–Zhmud's book, it is not hard to come up with the proof of Theorem 1. On the other hand, to my knowledge the only recorded proof of the 3rd inequality goes via Johnson's 1994 theorem and Banach-algebra facts.