In physics, a typical situation one is confronted with is to compute the product of an exponential of operators. Let $A$ and $B$ be some (possibly unbounded) self adjoint operators on a Hilbert space $\mathcal{H}$, if the operators $A$ and $B$ satisfy $$ [A,B] = c I$$ for some $c \in \mathbb{C}$, then it follows that $$ e^A e^B = e^{A + B - \frac{1}{2} [A,B]} \ .$$ The usual "proof" in physics, is to consider a function defined by $$ F(t) = e^{- (A + B)t}e^{A t} e^{B t}$$ then take (strong) derivatives, and the conlusion follows from some additional calculations.
The problem with this approach, and all other similar approaches, is that we are either assuming $A$ and $B$ to be bounded operators or, in the context of the actual BCH formula, to be elements of some Lie algebra. The problem is that almost all practical operators for which we need this formula, the operators $A$ and $B$ are unbounded. Because of the unboundedness, there are countless issues which cannot fully be resolved without additional regularity properties added to the operators.
One such regularity "trick" is the usage of so-called analytic vectors. If $A$ is an unbounded self adjoint operator, we say that $\psi \in \mathcal{H}$ is an analytic vector of $A$ if $\psi \in \cap_{n \in \mathbb{N}} D(A^n)$, and $$ \sum_{n \geq 0} \frac{t^n || A^n \psi ||}{n!} < \infty \ .$$ In this case, one has $$ e^{i A t} \psi = \sum_{n \geq 0} \frac{(itA)^n}{n!} \psi \ .$$ The exponential here is defined via the spectral theorem for normal operators. To make a long story short, one eventually comes to the conclusion, that if $A$ and $B$ are self-adjoint operators satisfying $[A,B] = c I$, equipped with some additional conditions akin to the analytic vector condition, then we are able to conclude that $$ e^{i A t} e^{ i Bt} \psi = \lim_{N \to \infty} \lim_{M \to \infty} \sum_{n=0}^N \sum_{m=0}^M \frac{(i A t)^n (i B t)^m}{n! m!} \psi \ .$$ Despite searching for this computation, I have not yet found anywhere where this might have been computed term by term.
So, my question is how does one approach such a computation? Trying to write out the terms term by term, the individual terms quickly become too intractable, at least for me, to deal with. Any hints, comments, or references on this computation?