Physlib

PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Existence.GardingVectorWitness

The full `IsAnalyticVector` witness for Gårding vectors (Milestone 2 of Track A, completed)

The capstone of `STONE_GENERATOR_EXISTENCE_PLAN.md`'s Milestone 1′: `analyticGardingVector U ε ψ` is a genuine `LinearPMap.IsAnalyticVector` of `stoneCandidateGenerator`, for *every* strongly continuous one-parameter unitary group `U` and every `ψ`. Combined with the ported Nelson's analytic-vector theorem (`AnalyticVector/Nelson.lean`), this is the existence direction of Stone's theorem via Gårding vectors, entirely avoiding the classical Bochner/spectral-measure route.

The assembly

Write `Gₙ := gardingVectorAt U (iteratedDeriv n (gaussianKernel ε)) ψ` (so `G₀ = analyticGardingVector U ε ψ`, `rfl`). `gardingVectorAt_iteratedKernel_hasDerivAt` (`IteratedKernelGrowth.lean`) gives, for every `n`: `Gₙ ∈ (stoneCandidateGenerator hUmul).domain` and `stoneCandidateGenerator hUmul Gₙ = I • Gₙ₊₁` (the same argument as `stoneCandidateGenerator_analyticGardingVector`, one order at a time). Since `T` is linear on its domain, `v n := Iⁿ • ⟨Gₙ, _⟩` then satisfies the `IteratesSeq` recursion exactly (the factor of `I` at each step is absorbed by the extra power of `I` on the left): `T (v n) = Iⁿ • (T Gₙ) = Iⁿ • (I • Gₙ₊₁) = Iⁿ⁺¹ • Gₙ₊₁ = v (n+1)`. Since `|I| = 1`, `‖(v n : H)‖ = ‖Gₙ‖`, bounded via `gaussianKernel_iteratedDeriv_L1_bound` and unitarity by `‖ψ‖ · C^(n+1) · √(n!)`. Choosing `t` small enough that `C·t < 1` turns the majorant series into a genuine geometric series (dominating the `1/√(n!) ≤ 1` factor crudely, which is all that is needed for the analytic-vector radius, even though the true series is far better than geometric) — summable, completing the witness.

3 declarations

theorem

Iterated Gaussian Gårding Vectors belong to the Generator Domain

Let HH be a complex Hilbert space and let U:R→L(H)U: \mathbb{R} \to \mathcal{L}(H) be a strongly continuous one-parameter unitary group. For any ε>0\varepsilon > 0, let ρε(t)=(πε)−1/2e−t2/ε\rho_\varepsilon(t) = (\pi \varepsilon)^{-1/2} e^{-t^2/\varepsilon} be the Gaussian kernel. For any vector ψ∈H\psi \in H and any natural number nn, the Gårding vector associated with the nn-th iterated derivative of the Gaussian kernel, defined by ∫−∞∞(dndtnρε(t))U(t)ψ dt, \int_{-\infty}^{\infty} \left( \frac{d^n}{dt^n} \rho_\varepsilon(t) \right) U(t)\psi \, dt, belongs to the domain of the infinitesimal generator of the unitary group UU.

theorem

Action of the Stone Generator on Iterated Gaussian Gårding Vectors: TGn=iGn+1T G_n = i G_{n+1}

Let HH be a complex Hilbert space and let U:R→L(H)U: \mathbb{R} \to \mathcal{L}(H) be a strongly continuous one-parameter unitary group. Let TT denote the infinitesimal generator of UU (the `stoneCandidateGenerator`). For any ε>0\varepsilon > 0, let ρε(t)=(πε)−1/2e−t2/ε\rho_\varepsilon(t) = (\pi \varepsilon)^{-1/2} e^{-t^2/\varepsilon} be the Gaussian kernel. For any vector ψ∈H\psi \in H and any natural number nn, let GnG_n be the Gårding vector associated with the nn-th derivative of the Gaussian kernel: Gn=∫−∞∞(dndtnρε(t))U(t)ψ dt. G_n = \int_{-\infty}^{\infty} \left( \frac{d^n}{dt^n} \rho_\varepsilon(t) \right) U(t)\psi \, dt. Then GnG_n lies in the domain of TT, and the action of the generator on GnG_n is given by T(Gn)=iGn+1, T(G_n) = i G_{n+1}, where ii is the imaginary unit.

theorem

The Gårding vector ψε\psi_\varepsilon is an analytic vector for the infinitesimal generator of UU

Let HH be a complex Hilbert space and U:R→L(H)U: \mathbb{R} \to \mathcal{L}(H) be a strongly continuous one-parameter unitary group. Let AA denote the infinitesimal generator of UU (represented by `stoneCandidateGenerator`). For any ε>0\varepsilon > 0 and any vector ψ∈H\psi \in H, the analytic Gårding vector ψε=∫−∞∞1πεe−t2/εU(t)ψ dt \psi_\varepsilon = \int_{-\infty}^{\infty} \frac{1}{\sqrt{\pi \varepsilon}} e^{-t^2/\varepsilon} U(t) \psi \, dt is an analytic vector for the operator AA. That is, ψε\psi_\varepsilon belongs to the domain of all iterations AnA^n and the power series expansion of eitAψεe^{itA}\psi_\varepsilon has a positive radius of convergence.