PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.Existence.GardingVectorWitness

Let $H$ be a Hilbert space and $U: \mathbb{R} \to \mathcal{L}(H)$ be a strongly continuous one-parameter family of unitary operators. Let $A$ be the candidate infinitesimal generator (the `stoneCandidateGenerator`) associated with $U$. For any natural number $n$, any positive real width $\epsilon > 0$, and any vector $\psi \in H$, the Gårding vector associated with the $n$-th derivative of the Gaussian kernel $g_\epsilon$, defined as $$\psi_{n, \epsilon} = \int_{-\infty}^{\infty} g_\epsilon^{(n)}(t) U(t)\psi \, dt,$$ belongs to the domain of the operator $A$.

Let $H$ be a Hilbert space and $U: \mathbb{R} \to \mathcal{L}(H)$ be a strongly continuous one-parameter family of unitary operators. Let $A$ be the candidate infinitesimal generator (the `stoneCandidateGenerator`) associated with $U$. Let $g_\epsilon$ denote the Gaussian kernel with width $\epsilon > 0$, and let $g_\epsilon^{(n)}$ be its $n$-th derivative. For any natural number $n \in \mathbb{N}$ and any vector $\psi \in H$, define the Gårding vector $\psi_{n, \epsilon}$ as $$\psi_{n, \epsilon} = \int_{-\infty}^{\infty} g_\epsilon^{(n)}(t) U(t)\psi \, dt.$$ Then the application of the generator $A$ to this vector satisfies the relation: $$A \psi_{n, \epsilon} = i \psi_{n+1, \epsilon},$$ where $i$ is the imaginary unit.

Let $H$ be a complex Hilbert space and $U: \mathbb{R} \to \mathcal{L}(H)$ be a strongly continuous one-parameter family of unitary operators. Let $A$ be the candidate infinitesimal generator (the `stoneCandidateGenerator`) associated with $U$. For any $\epsilon > 0$ and any vector $\psi \in H$, the Gårding vector $\psi_\epsilon$ defined by the Gaussian kernel $g_\epsilon$ as $$\psi_\epsilon = \int_{-\infty}^{\infty} g_\epsilon(t) U(t)\psi \, dt$$ is an analytic vector for $A$. That is, $\psi_\epsilon$ is in the domain of $A^n$ for all $n \in \mathbb{N}$, and there exists a $t > 0$ such that the power series $\sum_{n=0}^\infty \frac{\|A^n \psi_\epsilon\|}{n!} t^n$ converges.