Let $K$ be a compact real Lie group. Is it true that for every neighborhood $U$ of the identity in $K$ there exists a nonzero smooth function $f : K \to \mathbb C$ supported in $U$ such that $f$ is $K$-finite for the (left) regular representation? That is, such that the subspace $$span\{ f(k \;\cdot) : k \in K \} \subset C^\infty(K)$$ is finite-dimensional?
I was reading a proof that for a linear connected reductive real Lie group $G$ with maximal compact $K$ and a (continuous) representation $\pi : G \to V$ on a Hilbert space, the $K$-finite vectors of $V$ are smooth: http://www.math.utah.edu/~mcafee/SmoothVectorsDenseInV.pdf (See the proof of Lemma 4.1). In Knapp's book on representation theory, this is Proposition 8.5.
The existence of $K$-finite approximations of the identity seems to be a missing argument. I have trouble constructing something that is simultaneously supported in $U$ and $K$-finite.
It turns out we cannot hope for a compactly supported one, but an $L^2$ approximation of the identity will do:
Write the Cartan decomposition of $G$ as $G = KP$. On $P$, we can take any smooth nonnegative approximation $g$ of the identity, supported on a small neighborhood $U'$ of $1$. On $K$, we construct a $K$-finite smooth $L^2$-approximation $f$ of the identity as follows: By Peter-Weyl, there exists a finite linear combination of matrix coefficients of representations of $K$, which is at $L^2$ distance less than $\epsilon$ from something supported on $U$, say the scaled characteristic function $Vol(U)^{-1}1_U$ of $U$. Set $F(kp) = |f(k)|g(p)$. We may assume $\int_K |f| = \int_P g = 1$.
Then for $v \in V$, $$\begin{align} \left\Vert \int_G F(g) \pi(g) v dg - v \right\Vert & = \left\Vert \int_G F(g) (\pi(g) v - v) dg\right\Vert \\ & \leq \int_{KU' - UU'} |F(g)| \Vert \pi(g)v - v \Vert dg \\ & \quad + \int_{UU'} |F(g)| \Vert \pi(g)v - v \Vert dg \\ &\leq \Vert F \Vert_{L^1(KU'-UU')} \sup_{g \in KU'}\Vert \pi(g)v - v \Vert \\ & \quad + \Vert F \Vert_{L^1(UU')} \sup_{g \in UU'}\Vert \pi(g)v - v \Vert \\ & \ll_{v} \Vert f \Vert_{L^1(K-U)} + \sup_{g \in UU'}\Vert \pi(g)v - v \Vert \end{align}$$ which tends to $0$ as $\epsilon \to 0$ and $UU'$ gets smaller: The norm $\Vert f \Vert_{L^1(K-U)}$ is bounded by the distance $\Vert f - vol(U)^{-1}1_U\Vert_{L^2(K)}$ using Cauchy-Schwarz.) Thus $v$ can be approximated by smooth $K$-finite vectors.