PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Existence.GenericGardingKernel

The Gårding vector of a vector $\psi$ in a Hilbert space $H$ with respect to a real-valued kernel $k: \mathbb{R} \to \mathbb{R}$ is the vector in $H$ defined by the integral: $$\int_{-\infty}^{\infty} k(t) U(t) \psi \, dt$$ where $U(t)$ is a one-parameter family of operators on $H$. This definition generalizes the analytic Gårding vector by allowing for a generic kernel $k$ instead of a specific Gaussian kernel.

Let $H$ be a Hilbert space and $U(t)$ be a one-parameter family of operators on $H$. For a real-valued kernel $k: \mathbb{R} \to \mathbb{R}$, a vector $\psi \in H$, and a translation parameter $s \in \mathbb{R}$, if the map $t \mapsto k(t) U(t) \psi$ is integrable, then the action of the operator $U(s)$ on the Gårding vector of $\psi$ with respect to $k$ is given by: $$U(s) \left( \int_{-\infty}^{\infty} k(t) U(t) \psi \, dt \right) = \int_{-\infty}^{\infty} k(u - s) U(u) \psi \, du$$ where the term on the left represents $U(s)$ applied to the Gårding vector $\text{gardingVectorAt}(k, \psi)$.

Let $H$ be a complex Hilbert space and $U(t)$ be a family of unitary operators on $H$ such that for every $\xi \in H$, the map $t \mapsto U(t)\xi$ is continuous. Let $k, k' : \mathbb{R} \to \mathbb{R}$ be continuous functions such that $k'$ is the derivative of $k$ everywhere. Let $\psi \in H$ be a vector such that the function $t \mapsto k(t) U(t) \psi$ is integrable. Suppose there exists an integrable function $g : \mathbb{R} \to \mathbb{R}$ such that for all $u \in \mathbb{R}$ and all $x$ in the unit ball $B(0, 1) \subset \mathbb{R}$, the inequality $|k'(u - x)| \cdot \|\psi\| \leq g(u)$ holds. Then the orbit of the Gårding vector $s \mapsto U(s) \int_{-\infty}^{\infty} k(t) U(t) \psi \, dt$ is differentiable at $s = 0$, and its derivative is given by: $$\left. \frac{d}{ds} \right|_{s=0} U(s) \int_{-\infty}^{\infty} k(t) U(t) \psi \, dt = \int_{-\infty}^{\infty} -k'(u) U(u) \psi \, du$$