 Mehler formula for Hermite functions

For $|t|<1$, this identity sums the Hermite function expansion into a Gaussian. One proof takes the Bargmann-Fock space inner product of the generating functions ${\pi }^{-1/4}\exp (-x^2/2+\sqrt{2}xz-z^2/2)$ at $\sqrt{t}z$. Writing $z=u+iv$, the two resulting real Gaussian integrals have quadratic coefficients $1+t$ and $1-t$ and linear coefficients $\sqrt{2t}(x+y)$ and $i\sqrt{2t}(x-y)$. Evaluation gives the formula. Setting $t=e^{-2s}$ and multiplying by $e^{-s}$ gives the harmonic oscillator transition kernel of $e^{-s(-d^2/d{x}^2+x^2)}$.