1. The Fourier transform of a complex Gaussian
The derivation of the explicit form of the kernel of the Schrödinger propagator hinges on the fact that we can calculate the Fourier transform of the Gaussians
u(x) = e^{-⟨A x, x⟩ / 2}
for some non-degenerate symmetric matrix A with \operatorname{Re}(A) ≥ 0.
If A is real, symmetric and non-degenerate, then the Fourier transform of
u(x) = e^{-i⟨A x, x⟩ / 2}
is given by
\hat{u}(ξ) = ∣\operatorname{det}(A)|^{-1/2} e^{iπ \operatorname{sgn}(A)/4} e^{i ⟨A⁻¹ ξ, ξ⟩ / 2}
(This is not entirely correct, there will be funny factors of 2π).
This chapter follows Hörmander (2003)Lars Hörmander, 2003. “The analysis of linear partial differential operators. I”. In Classics in Mathematics, Springer..
1.1. Sketch of the proof
There are various proofs of this calculation and it is impossible to completely avoid using a basis
and a diagonalizing A.
1.1.1. Step 0: Complex Gaussians as tempered distributions
The very first step to even state the theorem in Lean is to define the complex Gaussian as a
tempered distribution. Along the way, one should also define the real Gaussian
u(x) = e^{-⟨A x, x⟩}
for A positive definite as a Schwartz function.
Writing A = A₀ + i B₀, we have that
\begin{aligned}
e^{-⟨A x, x⟩ / 2} &= e^{-⟨A₀ x, x⟩ / 2} e^{-i ⟨B₀ x, x⟩ / 2}
\end{aligned}
Since by assumption A₀ is non-negative, the first factor has temperate growth. The second
factor has temperate growth and therefore the product defines a tempered distribution.
1.1.2. Step 1: A simple regularity theorem
First we prove that a tempered distribution u that satisfies ∂_x u = 0 for all x is
constant. An equivalent statement is that if u satisfies x u = 0 for all x, then
u = c δ₀ for some constant c.
This is Theorem 3.1.16 in Hörmander (2003)Lars Hörmander, 2003. “The analysis of linear partial differential operators. I”. In Classics in Mathematics, Springer..
The proof of Theorem 3.1.16 is straightforward: let φ be a test function and using Taylor's
theorem, write
φ(x) = φ(0) + ∑ x_j φ_j(x)
for some φ_j. Then plug this expression into u and use the assumption.
1.1.3. Step 2: ODE of the Gaussian
Next we observe that (∂_x + A x) u = 0 if and only if u(x) = c · e^{-⟨A x, x⟩ / 2}. This
relies on Step 0 and Step 1.
One direction is trivial, for the other direction apply Step 1 to e^{⟨A x, x⟩ / 2} u.
1.1.4. Step 3: Calculate the Fourier transform up to a constant
From Step 2 we derive that the Fourier transform of a complex Gaussian is again a complex Gaussian.
1.1.5. Step 4: Calculate the constant: analytic square root of the determinant
Define the analytic square root (\operatorname{det} A)^{1/2} for A symmetric and positive real
part following Hörmander (2003)Lars Hörmander, 2003. “The analysis of linear partial differential operators. I”. In Classics in Mathematics, Springer. (p. 87).
The important result is that
(\operatorname{det}(iB))^{1/2} = |\operatorname{det}(B)|^{1/2} e^{iπ (\operatorname{sgn}(B))/4}
where \operatorname{sgn} is the signature and B is assumed to be purely imaginary and
non-singular.
1.1.6. Step 5: Calculate the constant: part 2
tba