Let $(V,||\cdot||)$ be a complex Hilbert space and let $G$ be a real Lie group with Lie algebra $\mathfrak{g}$. Let $\pi : G \rightarrow GL(V)$ be a continuous unitary representation. As in Bump's book "Automorphic forms and Representations" define a vector $v \in V$ to be $C^{1}$, if for every $X \in \mathfrak{g}$ the limit $\pi(X)v := \lim_{t \rightarrow 0}{t^{-1}(\pi(e^{tX})v - v)}$ exits. Iteratively define what a $C^k$-vector is and then say that a vector $v \in V$ is smooth if it is $C^k$ for all $k \geq 1$.
My questions concerns the sequential completeness of the space of smooth vectors (denote it $V^{\infty}$) with respect to the locally convex vector space topology as described in my answer here.
First of all, is the space $V^{\infty}$ known to be sequentially complete?
As a first step towards proving this, I did the following: Let $\{v_n\}_{n \geq 1} \subset V^{\infty}$ be a Cauchy sequence of smooth vectors. Then it is in particular a Cauchy-sequence in $V$, hence convergent to some unique $v \in V$. The goal is to show that $v$ is smooth and that $v_n \rightarrow v$ in the $V^{\infty}$-topology. Let's start by trying to show that $v$ is $C^{1}$. So let $X \in \mathfrak{g}$ be fixed. As the sequence $\{\pi(X)v_n\}_{n \geq 1}$ is Cauchy in $V$, it converges to a unique limit $v' \in V$, say. We should try to show that $\pi(X)v = v'$. It is not quite clear how to do that. I guess the following is the naive apporach: For any nonzero $t \in \mathbb{R}$ and $n \geq 1$ one has $$ \frac{\pi(e^{tX})v - v}{t} -v' = \frac{\pi(e^{tX})(v-v_n) - (v-v_n)}{t} + \left(\frac{\pi(e^{tX})v_n -v_n}{t} \right) + (\pi(X)v_n -v') $$ Now given $\varepsilon > 0$ we can pick $n$ such that the last term is $\leq \varepsilon/3$, say in norm. By the differentiability of $v_n$ there is $\delta > 0$ such that the middle term is $\leq \varepsilon/3$ in norm for all $0 < |t| < \delta$. But I don't know how to control the first term then. Alright, this didn't quite work.
I then tried to imitate a "fundamental theorem of calculus proof" of the analogous statement for point-wise convergent sequences of differentiable functions on an interval with uniformly convergent derivatives. This is what I've got:
Define continuous, $V$-valued curves $\gamma_n, \gamma: \mathbb{R} \rightarrow V$ by $\gamma_n(t) = \pi(e^{tX})v_n$ and $\gamma(t) = \pi(e^{tX})v$. We have for all $t \in \mathbb{R}$, $$ \gamma_n(t) = \int_{0}^t{\gamma_n'(s)ds} + v_n = \int_{0}^{t}{\pi(e^{sX}) \pi(X)v_n\, ds} + v_n\,, $$ by taking inner products and then using the fundamental theorem of calculus. If we fix $t$ and let $n \rightarrow \infty$, we get, by unitarity of $\pi(e^{t}X)$, $$ \gamma(t) = \pi(e^{tX})v = \int_{0}^{t}{\pi(e^{sX})v'\, ds} + v $$ Rearrange this for $t \neq 0$ and obtain $$ \frac{\pi(e^{tX})v-v}{t} = \frac{1}{t} \int_{0}^{t}{\pi(e^{sX})v'\, ds} \quad (=:I_t) $$ By the intermediate value theorem for integration (continuity of exp and strong continuity of the representation), the integrals $I_t$ on the right converges weakly to $v'$, as $t \rightarrow 0$. On the other hand, by the triangle inequality, $||I_t|| \leq ||v'||$. Since we are working in a Hilbert space, this suffices to conclude $||I_t - v'|| \rightarrow 0$, as $t \rightarrow 0$.
Does this work?
Added some weeks later: The last part of the argument can be simplified a little bit, by proving directly norm-convergence instead of only weak convergence