@[reducible, inline]

abbrev SchrodingerEquation.Rn (n : ℕ) : Type

Abbreviation for the $n$-dimensional Euclidean space $\mathbb{R}^n$.

def SchrodingerEquation.IsFreeSchrodingerSolution (ψ : ℝ → ℝ → ℂ) : Prop

The predicate that $\psi : \mathbb{R} \times \mathbb{R} \to \mathbb{C}$ solves the 1D free Schrödinger equation $i\partial_t \psi + \tfrac{1}{2}\partial_x^2 \psi = 0$ on $t > 0$.

noncomputable def SchrodingerEquation.complexLaplacian {n : ℕ} (f : Rn n → ℂ) (x : Rn n) : ℂ

The complex Laplacian $\Delta f(x) = \sum_{j=1}^n \partial_{x_j}^2 f(x)$ for a complex-valued function $f : \mathbb{R}^n \to \mathbb{C}$, defined via iterated Fréchet derivatives along the standard basis directions.

def SchrodingerEquation.IsFreeSchrodingerSolutionND {n : ℕ} (ψ : ℝ → Rn n → ℂ) : Prop

The predicate that $\psi : \mathbb{R} \times \mathbb{R}^n \to \mathbb{C}$ solves the $n$-dimensional free Schrödinger equation $i\partial_t \psi + \tfrac{1}{2}\Delta \psi = 0$ on $t > 0$.

noncomputable def SchrodingerEquation.fundamentalSolutionFT (t ξ : ℝ) : ℂ

The Fourier transform of the 1D Schrödinger fundamental solution: $\hat{K}(t, \xi) = e^{-2\pi^2 i t \xi^2}$.

noncomputable def SchrodingerEquation.solutionFT (φ : ℝ → ℂ) (t ξ : ℝ) : ℂ

The Fourier transform of the 1D free Schrödinger solution with initial data $\phi$: $\hat{\psi}(t,\xi) = \hat{K}(t,\xi)\hat{\phi}(\xi)$.

noncomputable def SchrodingerEquation.schrodingerKernel {n : ℕ} (t : ℝ) (x : Rn n) : ℂ

Definition 2.0.1. The fundamental solution to the free Schrödinger equation in $\mathbb{R}^n$: $$K(t, x) = \frac{1}{(2\pi i t)^{n/2}} e^{i |x|^2 / (2t)}.$$

noncomputable def SchrodingerEquation.schrodingerKernel1D (t x : ℝ) : ℂ

The 1D specialization of the Schrödinger fundamental solution: $K(t, x) = (2\pi i t)^{-1/2} e^{i x^2 / (2t)}$ for $x \in \mathbb{R}$.

theorem SchrodingerEquation.schrodingerKernel_norm {n : ℕ} (t : ℝ) (x : Rn n) (ht : t > 0) : ‖schrodingerKernel t x‖ = (2 * Real.pi * t) ^ (-↑n / 2)

The pointwise modulus of the Schrödinger kernel in dimension $n$ is $|K(t,x)| = (2\pi t)^{-n/2}$ for $t > 0$, independently of $x$.

theorem SchrodingerEquation.schrodingerKernel1D_norm (t x : ℝ) (ht : t > 0) : ‖schrodingerKernel1D t x‖ = 1 / √(2 * Real.pi * t)

In 1D, $|K(t,x)| = 1 / \sqrt{2\pi t}$ for $t > 0$.

noncomputable def SchrodingerEquation.schrodingerConvolution (φ : ℝ → ℂ) (t x : ℝ) : ℂ

The convolution $(K(t, \cdot) * \phi)(x) = \int_{\mathbb{R}} K(t, x - y) \phi(y) \, dy$ in 1D, giving the candidate solution to the free Schrödinger equation with initial data $\phi$.

theorem SchrodingerEquation.schrodingerKernel1D_time_deriv (t x : ℝ) (ht : t > 0) : Complex.I * deriv (fun (s : ℝ) => schrodingerKernel1D s x) t = schrodingerKernel1D t x * (-Complex.I / (2 * ↑t) + ↑(x ^ 2) / (2 * ↑t ^ 2))

Computation of the time derivative of the 1D Schrödinger kernel: $i\partial_t K(t,x) = K(t,x) \cdot \left(-\frac{i}{2t} + \frac{x^2}{2t^2}\right)$.

theorem SchrodingerEquation.schrodingerKernel1D_laplacian (t x : ℝ) (ht : t > 0) : 1 / 2 * deriv (deriv (schrodingerKernel1D t)) x = schrodingerKernel1D t x * (Complex.I / (2 * ↑t) - ↑(x ^ 2) / (2 * ↑t ^ 2))

Computation of the spatial Laplacian of the 1D Schrödinger kernel: $\tfrac{1}{2}\partial_x^2 K(t,x) = K(t,x) \cdot \left(\frac{i}{2t} - \frac{x^2}{2t^2}\right)$.

theorem SchrodingerEquation.lemma_2_0_2_K_solves_schrodinger : IsFreeSchrodingerSolution fun (t x : ℝ) => schrodingerKernel1D t x

Lemma 2.0.2 (1D case). The fundamental solution $K(t,x)$ verifies the free Schrödinger equation $i\partial_t K + \tfrac{1}{2}\partial_x^2 K = 0$ for $t > 0$.

theorem SchrodingerEquation.schrodingerKernel_time_deriv {n : ℕ} (t : ℝ) (x : Rn n) (ht : t > 0) : Complex.I * deriv (fun (s : ℝ) => schrodingerKernel s x) t = schrodingerKernel t x * (-↑n * Complex.I / (2 * ↑t) + ↑(‖x‖ ^ 2) / (2 * ↑t ^ 2))

The time derivative of the $n$-dimensional Schrödinger kernel: $i\partial_t K(t,x) = K(t,x) \cdot \left(-\frac{n i}{2t} + \frac{|x|^2}{2t^2}\right)$.

theorem SchrodingerEquation.schrodingerKernel_second_partial {n : ℕ} (t : ℝ) (x : Rn n) (ht : t > 0) (j : Fin n) : (fderiv ℝ (fun (y : Rn n) => (fderiv ℝ (schrodingerKernel t) y) (EuclideanSpace.single j 1)) x) (EuclideanSpace.single j 1) = schrodingerKernel t x * (Complex.I / ↑t + (Complex.I * ↑(x.ofLp j) / ↑t) ^ 2)

The second partial derivative of the $n$-dimensional Schrödinger kernel in the $j$-th direction: $\partial_{x_j}^2 K(t,x) = K(t,x) \cdot \left(\frac{i}{t} + \left(\frac{i x_j}{t}\right)^2\right)$.

theorem SchrodingerEquation.schrodingerKernel_laplacian {n : ℕ} (t : ℝ) (x : Rn n) (ht : t > 0) : 1 / 2 * complexLaplacian (schrodingerKernel t) x = schrodingerKernel t x * (↑n * Complex.I / (2 * ↑t) - ↑(‖x‖ ^ 2) / (2 * ↑t ^ 2))

Computation of the spatial Laplacian of the $n$-dimensional Schrödinger kernel: $\tfrac{1}{2}\Delta K(t,x) = K(t,x) \cdot \left(\frac{n i}{2t} - \frac{|x|^2}{2t^2}\right)$.

theorem SchrodingerEquation.lemma_2_0_2_K_solves_schrodinger_nD {n : ℕ} : IsFreeSchrodingerSolutionND fun (t : ℝ) (x : Rn n) => schrodingerKernel t x

Lemma 2.0.2 ($n$-dimensional case). The fundamental solution $K(t,x)$ verifies the free Schrödinger equation $i\partial_t K + \tfrac{1}{2}\Delta K = 0$ for $t > 0$, $x \in \mathbb{R}^n$.

theorem SchrodingerEquation.proposition_2_0_3_initial_data_recovery (φ : ℝ → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) (x : ℝ) : Filter.Tendsto (fun (t : ℝ) => schrodingerConvolution φ t x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (φ x))

Proposition 2.0.3 (1D case). For $\phi \in C_c^\infty(\mathbb{R})$, the convolution $(K(t,\cdot) * \phi)(x)$ recovers the initial data as $t \to 0^+$: $\lim_{t \to 0^+} (K(t,\cdot) * \phi)(x) = \phi(x)$.

noncomputable def SchrodingerEquation.schrodingerSolution (φ : ℝ → ℂ) : ℝ → ℝ → ℂ

The candidate 1D solution $\psi(t, x) = (K(t, \cdot) * \phi)(x)$ to the free Schrödinger equation with initial data $\phi$.

noncomputable def SchrodingerEquation.schrodingerConvolutionND {n : ℕ} (φ : Rn n → ℂ) (t : ℝ) (x : Rn n) : ℂ

The convolution $(K(t,\cdot) * \phi)(x) = \int_{\mathbb{R}^n} K(t, x - y) \phi(y) \, d^n y$ in $n$ dimensions.

noncomputable def SchrodingerEquation.schrodingerSolutionND {n : ℕ} (φ : Rn n → ℂ) : ℝ → Rn n → ℂ

The candidate $n$-dimensional solution $\psi(t, x) = (K(t, \cdot) * \phi)(x)$ to the free Schrödinger equation with initial data $\phi : \mathbb{R}^n \to \mathbb{C}$.

theorem SchrodingerEquation.proposition_2_0_3_initial_data_recovery_nD {n : ℕ} (φ : Rn n → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) (x : Rn n) : Filter.Tendsto (fun (t : ℝ) => schrodingerConvolutionND φ t x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (φ x))

Proposition 2.0.3 ($n$-dimensional case). For $\phi \in C_c^\infty(\mathbb{R}^n)$, $\lim_{t \to 0^+} \frac{1}{(2\pi i t)^{n/2}} \int_{\mathbb{R}^n} e^{i |x-y|^2 / (2t)} \phi(y)\, d^n y = \phi(x)$.

theorem SchrodingerEquation.differentiation_under_integral_schrodinger (φ : ℝ → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) (t : ℝ) (ht : 0 < t) (x : ℝ) : Complex.I * deriv (fun (s : ℝ) => schrodingerConvolution φ s x) t + 1 / 2 * deriv (deriv (schrodingerConvolution φ t)) x = 0

The differentiation-under-the-integral identity: the 1D convolution $K(t,\cdot) * \phi$ solves the free Schrödinger equation, obtained by passing the time and spatial derivatives inside the integral.

theorem SchrodingerEquation.smoothness_schrodinger_convolution (φ : ℝ → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) : ContDiff ℝ ⊤ fun (p : ℝ × ℝ) => schrodingerConvolution φ p.1 p.2

For $\phi \in C_c^\infty(\mathbb{R})$, the 1D Schrödinger convolution $(t, x) \mapsto (K(t, \cdot) * \phi)(x)$ is $C^\infty$ jointly in $(t, x)$.

theorem SchrodingerEquation.theorem_2_1_solves_equation (φ : ℝ → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) : IsFreeSchrodingerSolution (schrodingerSolution φ)

Theorem 2.1 (existence, 1D). The candidate solution $\psi = K(t, \cdot) * \phi$ indeed solves the free Schrödinger equation for $t > 0$.

theorem SchrodingerEquation.theorem_2_1_initial_data (φ : ℝ → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) (x : ℝ) : Filter.Tendsto (fun (t : ℝ) => schrodingerSolution φ t x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (φ x))

Theorem 2.1 (initial data, 1D). The candidate solution $\psi$ attains the initial data $\phi$ as $t \to 0^+$.

theorem SchrodingerEquation.theorem_2_1_smoothness (φ : ℝ → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) : ContDiff ℝ ⊤ fun (p : ℝ × ℝ) => schrodingerSolution φ p.1 p.2

Theorem 2.1 (smoothness, 1D). The solution $\psi(t, x)$ is smooth in $(t, x)$.

theorem SchrodingerEquation.theorem_2_1_dispersive_estimate (φ : ℝ → ℂ) (t : ℝ) (ht : 0 < t) (x : ℝ) : ‖schrodingerSolution φ t x‖ ≤ 1 / √(2 * Real.pi * t) * ∫ (y : ℝ), ‖φ y‖

Theorem 2.1 (dispersive estimate, 1D). For $t > 0$, the solution satisfies $\|\psi(t, \cdot)\|_{L^\infty} \le \frac{1}{\sqrt{2\pi t}} \|\phi\|_{L^1}$.

theorem SchrodingerEquation.theorem_2_1_dispersive_estimate_nD {n : ℕ} (φ : Rn n → ℂ) (t : ℝ) (ht : 0 < t) (x : Rn n) : ‖schrodingerSolutionND φ t x‖ ≤ (2 * Real.pi * t) ^ (-↑n / 2) * ∫ (y : Rn n), ‖φ y‖

Theorem 2.1 (dispersive estimate, $n$D). For $t > 0$, $\|\psi(t, \cdot)\|_{L^\infty(\mathbb{R}^n)} \le (2\pi t)^{-n/2} \|\phi\|_{L^1(\mathbb{R}^n)}$.

theorem SchrodingerEquation.theorem_2_1_uniqueness (φ : ℝ → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) (ψ₁ ψ₂ : ℝ → ℝ → ℂ) (hψ₁ : IsFreeSchrodingerSolution ψ₁) (hψ₂ : IsFreeSchrodingerSolution ψ₂) (hψ₁_smooth : ContDiff ℝ ⊤ fun (p : ℝ × ℝ) => ψ₁ p.1 p.2) (hψ₂_smooth : ContDiff ℝ ⊤ fun (p : ℝ × ℝ) => ψ₂ p.1 p.2) (hψ₁_init : ∀ (x : ℝ), Filter.Tendsto (fun (t : ℝ) => ψ₁ t x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (φ x))) (hψ₂_init : ∀ (x : ℝ), Filter.Tendsto (fun (t : ℝ) => ψ₂ t x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (φ x))) (t : ℝ) (ht : 0 < t) (x : ℝ) : ψ₁ t x = ψ₂ t x

Theorem 2.1 (uniqueness, 1D). Any two smooth solutions of the 1D free Schrödinger equation that attain the same initial data $\phi$ as $t \to 0^+$ must agree at all $(t, x)$ with $t > 0$.

theorem SchrodingerEquation.leibniz_time_derivative_nD {n : ℕ} (φ : Rn n → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) (t : ℝ) (ht : 0 < t) (x : Rn n) : deriv (fun (s : ℝ) => schrodingerConvolutionND φ s x) t = ∫ (y : Rn n), deriv (fun (s : ℝ) => schrodingerKernel s (x - y)) t * φ y

Leibniz rule for the time derivative of the $n$D Schrödinger convolution: the time derivative of $(K(t, \cdot) * \phi)(x)$ equals the convolution of $\partial_t K$ with $\phi$.

theorem SchrodingerEquation.leibniz_laplacian_nD {n : ℕ} (φ : Rn n → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) (t : ℝ) (ht : 0 < t) (x : Rn n) : complexLaplacian (schrodingerConvolutionND φ t) x = ∫ (y : Rn n), complexLaplacian (schrodingerKernel t) (x - y) * φ y

Leibniz rule for the spatial Laplacian of the $n$D Schrödinger convolution: $\Delta_x$ of $(K(t, \cdot) * \phi)(x)$ equals the convolution of $\Delta K$ with $\phi$.

theorem SchrodingerEquation.integrable_time_deriv_kernel_mul_phi {n : ℕ} (φ : Rn n → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) (t : ℝ) (ht : 0 < t) (x : Rn n) : MeasureTheory.Integrable (fun (y : Rn n) => deriv (fun (s : ℝ) => schrodingerKernel s (x - y)) t * φ y) MeasureTheory.volume

Integrability of $\partial_t K(t, x - y) \cdot \phi(y)$ in $y$, needed to interchange the time derivative and the integral.

theorem SchrodingerEquation.integrable_laplacian_kernel_mul_phi {n : ℕ} (φ : Rn n → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) (t : ℝ) (ht : 0 < t) (x : Rn n) : MeasureTheory.Integrable (fun (y : Rn n) => complexLaplacian (schrodingerKernel t) (x - y) * φ y) MeasureTheory.volume

Integrability of $\Delta K(t, x - y) \cdot \phi(y)$ in $y$, needed to interchange the spatial Laplacian and the integral.

theorem SchrodingerEquation.leibniz_schrodinger_operator_nD {n : ℕ} (φ : Rn n → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) (t : ℝ) (ht : 0 < t) (x : Rn n) : Complex.I * deriv (fun (s : ℝ) => schrodingerConvolutionND φ s x) t + 1 / 2 * complexLaplacian (schrodingerConvolutionND φ t) x = ∫ (y : Rn n), (Complex.I * deriv (fun (s : ℝ) => schrodingerKernel s (x - y)) t + 1 / 2 * complexLaplacian (schrodingerKernel t) (x - y)) * φ y

The Schrödinger differential operator commutes with the convolution integral: $(i\partial_t + \tfrac{1}{2}\Delta)(K * \phi) = \int (i\partial_t K + \tfrac{1}{2}\Delta K)(x-y) \phi(y)\,d^n y$.

theorem SchrodingerEquation.differentiation_under_integral_schrodinger_nD {n : ℕ} (φ : Rn n → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) (t : ℝ) (ht : 0 < t) (x : Rn n) : Complex.I * deriv (fun (s : ℝ) => schrodingerConvolutionND φ s x) t + 1 / 2 * complexLaplacian (schrodingerConvolutionND φ t) x = 0

Combining the Leibniz rule with Lemma 2.0.2: in $n$ dimensions, the convolution $(K(t, \cdot) * \phi)(x)$ solves the free Schrödinger equation for $t > 0$.

theorem SchrodingerEquation.smoothness_schrodinger_convolution_nD {n : ℕ} (φ : Rn n → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) : ContDiff ℝ ⊤ fun (p : ℝ × Rn n) => schrodingerConvolutionND φ p.1 p.2

For $\phi \in C_c^\infty(\mathbb{R}^n)$, the $n$D Schrödinger convolution $(t, x) \mapsto (K(t, \cdot) * \phi)(x)$ is $C^\infty$ jointly in $(t, x)$.

theorem SchrodingerEquation.theorem_2_1_solves_equation_nD {n : ℕ} (φ : Rn n → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) : IsFreeSchrodingerSolutionND (schrodingerSolutionND φ)

Theorem 2.1 (existence, $n$D). The candidate solution $\psi = K(t, \cdot) * \phi$ solves the $n$-dimensional free Schrödinger equation for $t > 0$.

theorem SchrodingerEquation.theorem_2_1_initial_data_nD {n : ℕ} (φ : Rn n → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) (x : Rn n) : Filter.Tendsto (fun (t : ℝ) => schrodingerSolutionND φ t x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (φ x))

Theorem 2.1 (initial data, $n$D). The candidate solution $\psi$ attains the initial data $\phi$ as $t \to 0^+$, for $\phi \in C_c^\infty(\mathbb{R}^n)$.

theorem SchrodingerEquation.theorem_2_1_smoothness_nD {n : ℕ} (φ : Rn n → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) : ContDiff ℝ ⊤ fun (p : ℝ × Rn n) => schrodingerSolutionND φ p.1 p.2

Theorem 2.1 (smoothness, $n$D). The solution $\psi(t, x)$ is smooth in $(t, x)$.

theorem SchrodingerEquation.theorem_2_1_uniqueness_nD {n : ℕ} (φ : Rn n → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) (ψ₁ ψ₂ : ℝ → Rn n → ℂ) (hψ₁ : IsFreeSchrodingerSolutionND ψ₁) (hψ₂ : IsFreeSchrodingerSolutionND ψ₂) (hψ₁_smooth : ContDiff ℝ ⊤ fun (p : ℝ × Rn n) => ψ₁ p.1 p.2) (hψ₂_smooth : ContDiff ℝ ⊤ fun (p : ℝ × Rn n) => ψ₂ p.1 p.2) (hψ₁_init : ∀ (x : Rn n), Filter.Tendsto (fun (t : ℝ) => ψ₁ t x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (φ x))) (hψ₂_init : ∀ (x : Rn n), Filter.Tendsto (fun (t : ℝ) => ψ₂ t x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (φ x))) (t : ℝ) (ht : 0 < t) (x : Rn n) : ψ₁ t x = ψ₂ t x

Theorem 2.1 (uniqueness, $n$D). Any two smooth solutions of the $n$-dimensional free Schrödinger equation that attain the same initial data $\phi$ as $t \to 0^+$ must agree at all $(t, x)$ with $t > 0$.

theorem SchrodingerEquation.theorem_2_1_nD {n : ℕ} (φ : Rn n → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) : IsFreeSchrodingerSolutionND (schrodingerSolutionND φ) ∧ (∀ (x : Rn n), Filter.Tendsto (fun (t : ℝ) => schrodingerSolutionND φ t x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (φ x))) ∧ (ContDiff ℝ ⊤ fun (p : ℝ × Rn n) => schrodingerSolutionND φ p.1 p.2) ∧ (∀ t > 0, ∀ (x : Rn n), ‖schrodingerSolutionND φ t x‖ ≤ (2 * Real.pi * t) ^ (-↑n / 2) * ∫ (y : Rn n), ‖φ y‖) ∧ ∀ (ψ₁ ψ₂ : ℝ → Rn n → ℂ), IsFreeSchrodingerSolutionND ψ₁ → IsFreeSchrodingerSolutionND ψ₂ → (ContDiff ℝ ⊤ fun (p : ℝ × Rn n) => ψ₁ p.1 p.2) → (ContDiff ℝ ⊤ fun (p : ℝ × Rn n) => ψ₂ p.1 p.2) → (∀ (x : Rn n), Filter.Tendsto (fun (t : ℝ) => ψ₁ t x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (φ x))) → (∀ (x : Rn n), Filter.Tendsto (fun (t : ℝ) => ψ₂ t x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (φ x))) → ∀ t > 0, ∀ (x : Rn n), ψ₁ t x = ψ₂ t x

Theorem 2.1 (full statement, $n$D). For $\phi \in C_c^\infty(\mathbb{R}^n)$ there exists a unique smooth solution $\psi \in C^\infty((0, \infty) \times \mathbb{R}^n)$ to the free Schrödinger equation with $\psi(0, x) = \phi(x)$, given by $\psi(t, x) = (K(t, \cdot) * \phi)(x)$, and $\psi$ satisfies the dispersive estimate $\|\psi(t, \cdot)\|_{L^\infty} \le C t^{-n/2} \|\phi\|_{L^1}$.

theorem SchrodingerEquation.fourier_solution_norm_sq_eq (φ : ℝ → ℂ) (t ξ : ℝ) : ‖solutionFT φ t ξ‖ = ‖FourierAnalysis.fourierTransform φ ξ‖

The Fourier multiplier $\hat{K}(t, \xi) = e^{-2\pi^2 i t \xi^2}$ has modulus $1$, so the Fourier transform of the solution has the same pointwise modulus as $\hat{\phi}$: $|\hat{\psi}(t, \xi)| = |\hat{\phi}(\xi)|$.

theorem SchrodingerEquation.fourierTransform_eq_fourier (f : ℝ → ℂ) (ξ : ℝ) : FourierAnalysis.fourierTransform f ξ = FourierTransform.fourier f ξ

The custom Fourier transform defined in CM16 agrees with Mathlib's Fourier transform $\mathcal{F}$.

theorem SchrodingerEquation.plancherel_theorem (f : ℝ → ℂ) (hf_smooth : ContDiff ℝ ⊤ f) (hf_supp : HasCompactSupport f) : ∫ (x : ℝ), ‖f x‖ ^ 2 = ∫ (ξ : ℝ), ‖FourierAnalysis.fourierTransform f ξ‖ ^ 2

Plancherel's theorem for compactly supported smooth functions in 1D: $\int_{\mathbb{R}} |f(x)|^2\,dx = \int_{\mathbb{R}} |\hat{f}(\xi)|^2\,d\xi$.

theorem SchrodingerEquation.FT_of_convolution_solution (φ : ℝ → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) (t : ℝ) (ht : 0 < t) (ξ : ℝ) : FourierAnalysis.fourierTransform (schrodingerConvolution φ t) ξ = solutionFT φ t ξ

The Fourier transform of the 1D Schrödinger convolution equals the multiplier representation: $\widehat{K(t, \cdot) * \phi}(\xi) = \hat{K}(t, \xi) \hat{\phi}(\xi)$.

theorem SchrodingerEquation.proposition_2_0_4_L2_preservation (φ : ℝ → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) (t : ℝ) (ht : 0 < t) (hψ_plancherel : ∫ (x : ℝ), ‖schrodingerConvolution φ t x‖ ^ 2 = ∫ (ξ : ℝ), ‖FourierAnalysis.fourierTransform (schrodingerConvolution φ t) ξ‖ ^ 2) : ∫ (x : ℝ), ‖schrodingerSolution φ t x‖ ^ 2 = ∫ (x : ℝ), ‖φ x‖ ^ 2

Proposition 2.0.4 (Preservation of $L^2$ norm, 1D). Under the assumptions of Theorem 2.1, $\|\psi(t, \cdot)\|_{L^2} = \|\phi\|_{L^2}$ for all $t > 0$. The proof goes through Plancherel and the fact that the Fourier multiplier has unit modulus.

noncomputable def SchrodingerEquation.fourierTransformRn {n : ℕ} (f : Rn n → ℂ) (ξ : Rn n) : ℂ

The $n$-dimensional Fourier transform $\hat{f}(\xi) = \int_{\mathbb{R}^n} f(x) e^{-2\pi i \langle \xi, x \rangle}\,d^n x$.

noncomputable def SchrodingerEquation.fundamentalSolutionFT_nD {n : ℕ} (t : ℝ) (ξ : Rn n) : ℂ

The Fourier transform of the $n$D Schrödinger fundamental solution: $\hat{K}(t, \xi) = e^{-2\pi^2 i t |\xi|^2}$.

noncomputable def SchrodingerEquation.solutionFT_nD {n : ℕ} (φ : Rn n → ℂ) (t : ℝ) (ξ : Rn n) : ℂ

The Fourier transform of the $n$D free Schrödinger solution with initial data $\phi$: $\hat{\psi}(t, \xi) = \hat{K}(t, \xi) \hat{\phi}(\xi)$.

theorem SchrodingerEquation.fourier_solution_norm_sq_eq_nD {n : ℕ} (φ : Rn n → ℂ) (t : ℝ) (ξ : Rn n) : ‖solutionFT_nD φ t ξ‖ = ‖fourierTransformRn φ ξ‖

The $n$D analogue: the modulus of the Fourier transform of the solution equals that of $\hat{\phi}$, since the Fourier multiplier $\hat{K}(t, \xi)$ has unit modulus.

theorem SchrodingerEquation.fourierTransformRn_eq_fourier {n : ℕ} (f : Rn n → ℂ) (ξ : Rn n) : fourierTransformRn f ξ = FourierTransform.fourier f ξ

The custom $n$D Fourier transform agrees with Mathlib's Fourier transform $\mathcal{F}$ on $\mathbb{R}^n$.

theorem SchrodingerEquation.plancherel_compact_support_nD {n : ℕ} (f : Rn n → ℂ) (hf_smooth : ContDiff ℝ ⊤ f) (hf_supp : HasCompactSupport f) : ∫ (x : Rn n), ‖f x‖ ^ 2 = ∫ (ξ : Rn n), ‖fourierTransformRn f ξ‖ ^ 2

Plancherel's theorem for compactly supported smooth functions in $\mathbb{R}^n$: $\int |f(x)|^2\,d^n x = \int |\hat{f}(\xi)|^2\,d^n \xi$.

theorem SchrodingerEquation.integral_swap_convolution_FT_nD {n : ℕ} (φ : Rn n → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) (t : ℝ) (ht : 0 < t) (ξ : Rn n) : ∫ (x : Rn n) (y : Rn n), schrodingerKernel t (x - y) * φ y * Complex.exp (↑(-2 * Real.pi * inner ℝ ξ x) * Complex.I) = ∫ (y : Rn n) (x : Rn n), schrodingerKernel t (x - y) * φ y * Complex.exp (↑(-2 * Real.pi * inner ℝ ξ x) * Complex.I)

Fubini-style swap of the order of integration in the double integral arising in computing $\widehat{K(t, \cdot) * \phi}(\xi)$.

theorem SchrodingerEquation.fubini_integrability_convolution_FT_nD {n : ℕ} (φ : Rn n → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) (t : ℝ) (ht : 0 < t) (ξ : Rn n) : ∫ (x : Rn n), (∫ (y : Rn n), schrodingerKernel t (x - y) * φ y) * Complex.exp (↑(-2 * Real.pi * inner ℝ ξ x) * Complex.I) = ∫ (y : Rn n), φ y * ∫ (x : Rn n), schrodingerKernel t (x - y) * Complex.exp (↑(-2 * Real.pi * inner ℝ ξ x) * Complex.I)

Rearrangement (via Fubini) of the Fourier transform of the convolution as an iterated integral with $\phi$ outside and the kernel integrated against the Fourier exponential.

theorem SchrodingerEquation.FT_kernel_translation_nD {n : ℕ} (t : ℝ) (ht : 0 < t) (ξ y : Rn n) : ∫ (x : Rn n), schrodingerKernel t (x - y) * Complex.exp (↑(-2 * Real.pi * inner ℝ ξ x) * Complex.I) = Complex.exp (↑(-2 * Real.pi * inner ℝ ξ y) * Complex.I) * fourierTransformRn (schrodingerKernel t) ξ

Translation property of the Fourier transform applied to the Schrödinger kernel: $\int K(t, x - y) e^{-2\pi i \langle \xi, x\rangle}\,d^n x = e^{-2\pi i \langle \xi, y\rangle} \hat{K}(t, \xi)$.

theorem SchrodingerEquation.norm_sq_eq_sum_sq_real {n : ℕ} (ξ : Rn n) : ∑ i : Fin n, ξ.ofLp i ^ 2 = ‖ξ‖ ^ 2

The squared Euclidean norm equals the sum of coordinate squares: $\|\xi\|^2 = \sum_i \xi_i^2$.

theorem SchrodingerEquation.FT_complex_gaussian_1D (t : ℝ) (ht : 0 < t) (ξ_i : ℝ) : ∫ (u : ℝ), (↑(2 * Real.pi) * Complex.I * ↑t) ^ (-1 / 2) * Complex.exp (Complex.I * ↑(u ^ 2 / (2 * t))) * Complex.exp (↑(-2 * Real.pi * ξ_i * u) * Complex.I) = Complex.exp (↑(-2 * Real.pi ^ 2 * t * ξ_i ^ 2) * Complex.I)

The Fourier transform of the 1D complex Gaussian $\frac{1}{(2\pi i t)^{1/2}} e^{i u^2 / (2t)}$ at frequency $\xi$ equals $e^{-2\pi^2 i t \xi^2}$.

theorem SchrodingerEquation.FT_gaussian_nD_fubini {n : ℕ} (t : ℝ) (ht : 0 < t) (ξ : Rn n) : fourierTransformRn (schrodingerKernel t) ξ = ∏ i : Fin n, ∫ (u : ℝ), (↑(2 * Real.pi) * Complex.I * ↑t) ^ (-1 / 2) * Complex.exp (Complex.I * ↑(u ^ 2 / (2 * t))) * Complex.exp (↑(-2 * Real.pi * ξ.ofLp i * u) * Complex.I)

Factorization of the $n$D Fourier transform of $K(t, \cdot)$ as a product of 1D Fourier transforms of complex Gaussians, via Fubini and the product structure of $K$.

theorem SchrodingerEquation.FT_of_schrodinger_kernel_nD {n : ℕ} (t : ℝ) (ht : 0 < t) (ξ : Rn n) : fourierTransformRn (schrodingerKernel t) ξ = fundamentalSolutionFT_nD t ξ

The $n$D Fourier transform of the Schrödinger kernel agrees with the closed-form multiplier: $\hat{K}(t, \xi) = e^{-2\pi^2 i t |\xi|^2}$.

theorem SchrodingerEquation.FT_of_convolution_solution_nD {n : ℕ} (φ : Rn n → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) (t : ℝ) (ht : 0 < t) (ξ : Rn n) : fourierTransformRn (schrodingerConvolutionND φ t) ξ = solutionFT_nD φ t ξ

The Fourier transform of the $n$D Schrödinger convolution equals the multiplier representation: $\widehat{K(t, \cdot) * \phi}(\xi) = \hat{K}(t, \xi) \hat{\phi}(\xi)$.

theorem SchrodingerEquation.schrodingerConvolutionND_smooth {n : ℕ} (φ : Rn n → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) (t : ℝ) (ht : 0 < t) : ContDiff ℝ ⊤ (schrodingerConvolutionND φ t)

For fixed $t > 0$, the function $x \mapsto (K(t, \cdot) * \phi)(x)$ is $C^\infty$ in $x$, deduced from the joint smoothness in $(t, x)$.

theorem SchrodingerEquation.convolution_eq_fourierMultiplier {n : ℕ} (φ : Rn n → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) (t : ℝ) (ht : 0 < t) : (fun (x : Rn n) => ((SchwartzMap.fourierMultiplierCLM ℂ (fundamentalSolutionFT_nD t)) (hφ_supp.toSchwartzMap ⋯)) x) = schrodingerConvolutionND φ t

Identification of the Schrödinger convolution with the action of the Fourier multiplier $\hat{K}(t, \cdot)$ on the Schwartz function $\phi$: as functions, the convolution equals the Fourier-multiplier composition.

theorem SchrodingerEquation.schrodingerConvolutionND_decay {n : ℕ} (φ : Rn n → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) (t : ℝ) (ht : 0 < t) (k m : ℕ) : ∃ (C : ℝ), ∀ (x : Rn n), ‖x‖ ^ k * ‖iteratedFDeriv ℝ m (schrodingerConvolutionND φ t) x‖ ≤ C

Schwartz-type decay for the $n$D Schrödinger convolution: for every $k, m \in \mathbb{N}$ there is a constant $C$ with $\|x\|^k \|D^m (K * \phi)(x)\| \le C$.

noncomputable def SchrodingerEquation.convolution_solution_schwartz_nD {n : ℕ} (φ : Rn n → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) (t : ℝ) (ht : 0 < t) : { sf : SchwartzMap (Rn n) ℂ // ∀ (x : Rn n), sf x = schrodingerConvolutionND φ t x }

Promotion of $x \mapsto (K(t, \cdot) * \phi)(x)$ to a Schwartz function, packaging the smoothness and Schwartz-decay results.

theorem SchrodingerEquation.plancherel_convolution_solution_nD {n : ℕ} (φ : Rn n → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) (t : ℝ) (ht : 0 < t) : ∫ (x : Rn n), ‖schrodingerConvolutionND φ t x‖ ^ 2 = ∫ (ξ : Rn n), ‖fourierTransformRn (schrodingerConvolutionND φ t) ξ‖ ^ 2

Plancherel's theorem applied to the $n$D Schrödinger convolution, viewed as a Schwartz function: $\int |(K(t,\cdot) * \phi)(x)|^2,d^n x = \int |\widehat{K(t, \cdot) * \phi}(\xi)|^2,d^n \xi$.

theorem SchrodingerEquation.L2_norm_preservation_nD_fourier_proof {n : ℕ} (φ : Rn n → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) (t : ℝ) (ht : 0 < t) : ∫ (x : Rn n), ‖schrodingerConvolutionND φ t x‖ ^ 2 = ∫ (x : Rn n), ‖φ x‖ ^ 2

The Fourier-side proof of $L^2$-norm preservation in $n$ dimensions: using Plancherel and the fact that $\hat{K}$ has unit modulus, $\int \|(K(t, \cdot) * \phi)(x)\|^2\,d^n x = \int \|\phi(x)\|^2\,d^n x$.

theorem SchrodingerEquation.proposition_2_0_4_L2_preservation_nD {n : ℕ} (φ : Rn n → ℂ) (hφ_smooth : ContDiff ℝ ⊤ φ) (hφ_supp : HasCompactSupport φ) (t : ℝ) (ht : 0 < t) : ∫ (x : Rn n), ‖schrodingerSolutionND φ t x‖ ^ 2 = ∫ (x : Rn n), ‖φ x‖ ^ 2

Proposition 2.0.4 (Preservation of $L^2$ norm, $n$D). Under the assumptions of Theorem 2.1, $\|\psi(t, \cdot)\|_{L^2(\mathbb{R}^n)} = \|\phi\|_{L^2(\mathbb{R}^n)}$. In particular, if $\phi$ is a unit-mass wave function, then $\psi(t, \cdot)$ remains so for all $t > 0$.