Documentation

Atlas.IntroductionToPartialDifferentialEquations.code.CM19.SchrodingerFundamental

def euclidNormSq {n : } (x : Fin n) :

Squared Euclidean norm $|x|^2 = \sum_{i=1}^n (x^i)^2$ for $x \in \mathbb{R}^n$.

Instances For
    noncomputable def schrodingerKernel (n : ) (t : ) (x : Fin n) :

    The Schrödinger fundamental solution (Definition 2.0.1) in $n$ spatial dimensions: $$K(t, x) = \frac{1}{(2\pi i t)^{n/2}}\, \exp\!\left(\frac{i|x|^2}{2t}\right).$$

    Instances For
      noncomputable def spatialPartialDeriv {n : } (j : Fin n) (f : (Fin n)) (x : Fin n) :

      The partial derivative $\partial_j f(x)$ of a function $f : \mathbb{R}^n \to \mathbb{C}$ in the $j$-th coordinate direction, defined as the one-variable derivative obtained by varying the $j$-th coordinate while keeping the others fixed.

      Instances For
        noncomputable def spatialLaplacian {n : } (f : (Fin n)) (x : Fin n) :

        The spatial Laplacian $\Delta f = \sum_{j=1}^n \partial_j^2 f$.

        Instances For
          noncomputable def schrodingerOp (n : ) (u : (Fin n)) (t : ) (x : Fin n) :

          The free Schrödinger operator $i\,\partial_t u + \tfrac{1}{2}\Delta u$ applied to a time-dependent field $u(t, x)$.

          Instances For
            theorem hasDerivAt_ofReal (s : ) :
            HasDerivAt (fun (s : ) => s) 1 s

            The inclusion $\mathbb{R} \hookrightarrow \mathbb{C}$ has derivative $1$ at every point.

            theorem hasDerivAt_ofReal_sq (s : ) :
            HasDerivAt (fun (s : ) => s ^ 2) (2 * s) s

            The map $s \mapsto s^2 : \mathbb{R} \to \mathbb{C}$ has derivative $2s$.

            theorem hasDerivAt_cexp_affine_sq (a b : ) (s : ) :
            HasDerivAt (fun (s : ) => Complex.exp (a * s ^ 2 + b)) (Complex.exp (a * s ^ 2 + b) * (2 * a * s)) s

            Chain rule: $\frac{d}{ds} \exp(a s^2 + b) = \exp(a s^2 + b) \cdot 2as$ for complex constants $a, b$ and a real variable $s$.

            theorem hasDerivAt_cexp_affine_sq_times_linear (a b : ) (s : ) :
            HasDerivAt (fun (s : ) => Complex.exp (a * s ^ 2 + b) * (2 * a * s)) (Complex.exp (a * s ^ 2 + b) * (4 * a ^ 2 * s ^ 2 + 2 * a)) s

            Second derivative of $\exp(a s^2 + b)$: differentiating $\exp(a s^2 + b) \cdot 2as$ once more yields $\exp(a s^2 + b) (4 a^2 s^2 + 2 a)$.

            theorem euclidNormSq_update {n : } (x : Fin n) (j : Fin n) (s : ) :

            Updating the $j$-th coordinate of $x$ to $s$ shifts the squared norm by $-x_j^2 + s^2$, i.e. $|x[j \mapsto s]|^2 = |x|^2 - x_j^2 + s^2$.

            theorem second_spatialPartialDeriv_eq {n : } (j : Fin n) (f : (Fin n)) (x : Fin n) :
            spatialPartialDeriv j (spatialPartialDeriv j f) x = deriv (fun (r : ) => deriv (fun (s : ) => f (Function.update x j s)) r) (x j)

            Reformulates the second pure partial derivative $\partial_j^2 f$ as an iterated one-variable derivative obtained by varying the $j$-th coordinate.

            theorem second_partial_deriv_exp_phase {n : } (x : Fin n) (j : Fin n) (t : ) :
            spatialPartialDeriv j (spatialPartialDeriv j fun (y : Fin n) => Complex.exp (Complex.I * (euclidNormSq y) / (2 * t))) x = Complex.exp (Complex.I * (euclidNormSq x) / (2 * t)) * (4 * (Complex.I / (2 * t)) ^ 2 * (x j) ^ 2 + 2 * (Complex.I / (2 * t)))

            Closed-form for the second partial derivative $\partial_j^2$ of the Schrödinger phase $\exp(i|y|^2/(2t))$ at $x$, expressed in the $a = i/(2t)$ parametrization.

            theorem laplacian_exp_phase {n : } (x : Fin n) (t : ) (ht : t 0) :
            spatialLaplacian (fun (y : Fin n) => Complex.exp (Complex.I * (euclidNormSq y) / (2 * t))) x = Complex.exp (Complex.I * (euclidNormSq x) / (2 * t)) * (Complex.I * n / t - (euclidNormSq x) / t ^ 2)

            Closed-form for the spatial Laplacian of the Schrödinger phase $\exp(i|y|^2/(2t))$: $$\Delta_x \exp(i|x|^2/(2t)) = \exp(i|x|^2/(2t))\left(\frac{i n}{t} - \frac{|x|^2}{t^2}\right).$$

            theorem half_laplacian_schrodinger (n : ) (t : ) (x : Fin n) (ht : 0 < t) :
            1 / 2 * spatialLaplacian (schrodingerKernel n t) x = schrodingerKernel n t x * (Complex.I * n / (2 * t) - (euclidNormSq x) / (2 * t ^ 2))

            The spatial half-Laplacian of the Schrödinger kernel: $$\tfrac{1}{2}\Delta_x K(t, x) = K(t, x)\left(\frac{i n}{2t} - \frac{|x|^2}{2t^2}\right).$$ The constant prefactor $(2\pi i t)^{-n/2}$ pulls out and the half-Laplacian of the phase is computed via laplacian_exp_phase.

            theorem time_deriv_schrodinger (n : ) (t : ) (x : Fin n) (ht : t > 0) :
            Complex.I * deriv (fun (s : ) => schrodingerKernel n s x) t = schrodingerKernel n t x * (-n * Complex.I / (2 * t) + (euclidNormSq x) / (2 * t ^ 2))

            Time derivative of the Schrödinger kernel multiplied by $i$: $$i\,\partial_t K(t, x) = K(t, x)\left(-\frac{n i}{2 t} + \frac{|x|^2}{2 t^2}\right).$$ Combined with half_laplacian_schrodinger, this gives that $K$ solves $i\partial_t K + \tfrac{1}{2}\Delta K = 0$.

            theorem lemma_2_0_2_schrodinger_pde (n : ) (t : ) (x : Fin n) (ht : 0 < t) :

            Lemma 2.0.2: for $t > 0$, the Schrödinger fundamental solution $K(t, x)$ solves the free Schrödinger equation $i\,\partial_t K + \tfrac{1}{2}\Delta K = 0$ pointwise.

            def finDotProduct {n : } (ξ x : Fin n) :

            Dot product $\xi \cdot x = \sum_{i=1}^n \xi_i x_i$ on $\mathbb{R}^n$ indexed by $\text{Fin } n$.

            Instances For
              noncomputable def fourierTransformFin {n : } (f : (Fin n)) (ξ : Fin n) :

              Fourier transform on $\mathbb{R}^n$ with the analyst convention used in the book: $\hat f(\xi) = \int_{\mathbb{R}^n} f(x)\, e^{-2\pi i \xi \cdot x}\, d^n x.$

              Instances For
                noncomputable def inverseFourierTransformFin {n : } (f : (Fin n)) (x : Fin n) :

                Inverse Fourier transform on $\mathbb{R}^n$: $f^\vee(x) = \int_{\mathbb{R}^n} f(\xi)\, e^{2\pi i \xi \cdot x}\, d^n \xi.$

                Instances For
                  noncomputable def schrodingerKernelFT (n : ) (t : ) (ξ : Fin n) :

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

                  Instances For
                    noncomputable def schrodingerSolutionFT (n : ) (φ : (Fin n)) (t : ) (ξ : Fin n) :

                    The spatial Fourier transform of the (candidate) solution $\psi(t, \cdot)$: $\hat\psi(t, \xi) = \hat K(t, \xi)\,\hat\phi(\xi).$

                    Instances For
                      noncomputable def schrodingerConvolution (n : ) (φ : (Fin n)) (t : ) (x : Fin n) :

                      The convolution representation of the Schrödinger solution: $\psi(t, x) = (K(t, \cdot) * \phi)(x) = \int K(t, x - y)\,\phi(y)\, d^n y.$

                      Instances For
                        noncomputable def regularizedGaussian (n : ) (δ t : ) (ξ : Fin n) :

                        The regularized Gaussian replacing the oscillatory kernel: for $\delta > 0$, $g_\delta(t, \xi) = \exp\!\left(-2\pi^2 (\delta + i) t |\xi|^2\right).$ As $\delta \downarrow 0$, $g_\delta \to \hat K(t, \cdot)$ and the Gaussian is integrable, which permits a rigorous Fourier-inversion argument.

                        Instances For

                          The local fourierTransformFin (defined via Fin n-indexed dot products) coincides with the $n$-dimensional Fourier transform CM16.fourierTransformND developed in Class Meeting 16.

                          theorem regularization_limit {n : } (φ : (Fin n)) (hφ_smooth : ContDiff φ) (hφ_supp : HasCompactSupport φ) (t : ) (ht : 0 < t) (x : Fin n) :

                          Regularization step: writing the oscillatory kernel as the $\delta \downarrow 0$ limit of $g_\delta$ and applying dominated convergence (with bound $|\hat\phi|$), $$\psi(t, x) = (\hat K(t, \cdot)\,\hat\phi)^\vee(x) = \lim_{\delta \downarrow 0} (g_\delta(t, \cdot)\,\hat\phi)^\vee(x).$$

                          theorem ofReal_euclidNormSq {n : } (ξ : Fin n) :
                          (euclidNormSq ξ) = i : Fin n, (ξ i) ^ 2

                          Coercion identity: $(\sum_i (\xi_i)^2) \in \mathbb{C}$ equals $\sum_i (\xi_i : \mathbb{C})^2$.

                          For $\delta > 0$ and $t > 0$, the regularized Gaussian $g_\delta(t, \cdot)$ is integrable on $\mathbb{R}^n$: the real part of the exponent is $-2\pi^2 \delta t |\xi|^2 < 0$ for $\xi \neq 0$, which gives Gaussian decay.

                          theorem fubini_integ_regularizedGaussian_phi {n : } (φ : (Fin n)) (hφ_smooth : ContDiff φ) (hφ_supp : HasCompactSupport φ) (δ : ) ( : 0 < δ) (t : ) (ht : 0 < t) (x : Fin n) :

                          Joint integrability on $\mathbb{R}^n \times \mathbb{R}^n$ of the integrand $g_\delta(t, \xi)\, e^{2\pi i \xi \cdot (x-y)}\, \phi(y)$ needed to apply Fubini's theorem in convolution_via_FT_inversion.

                          theorem convolution_via_FT_inversion {n : } (φ : (Fin n)) (hφ_smooth : ContDiff φ) (hφ_supp : HasCompactSupport φ) (δ : ) ( : 0 < δ) (t : ) (ht : 0 < t) (x : Fin n) :

                          Convolution-via-Fourier-inversion at the regularized level: for any $\delta > 0$, $$(g_\delta(t, \cdot)\,\hat\phi)^\vee(x) = \int g_\delta^\vee(t, x - y)\,\phi(y)\, d^n y.$$ The proof combines the product formula for the inverse Fourier transform with Fubini's theorem to swap the $\xi$ and $y$ integrals.

                          noncomputable def regularizedGaussianInverseFT (n : ) (δ t : ) (z : Fin n) :

                          The closed-form inverse Fourier transform of the regularized Gaussian: $$g_\delta^\vee(t, z) = (2\pi(\delta + i)t)^{-n/2}\, \exp\!\left(\frac{-|z|^2}{2t(\delta + i)} \right).$$ At $\delta = 0$ this formally recovers the Schrödinger kernel $K(t, z)$.

                          Instances For
                            theorem inverseFT_regularizedGaussian_eq_closedForm {n : } (δ : ) ( : 0 < δ) (t : ) (ht : 0 < t) (z : Fin n) :

                            The inverse Fourier transform of the regularized Gaussian agrees with the closed-form expression regularizedGaussianInverseFT. Proved by reducing to the complex Gaussian Fourier transform formula CM16.fourier_gaussian_complex.

                            theorem pointwise_limit_regularized_kernel {n : } (t : ) (ht : 0 < t) (z : Fin n) :

                            Pointwise convergence of the regularized inverse Fourier transform to the Schrödinger kernel: for each $z$, $g_\delta^\vee(t, z) \to K(t, z)$ as $\delta \downarrow 0$. This is the pointwise input to the dominated convergence argument in dominated_convergence_convolution.

                            theorem ae_strongly_measurable_regularized_integrand {n : } (φ : (Fin n)) (hφ_smooth : ContDiff φ) (hφ_supp : HasCompactSupport φ) (t : ) (ht : 0 < t) (x : Fin n) (δ : ) ( : 0 < δ) :

                            For $\delta > 0$, the integrand $y \mapsto g_\delta^\vee(t, x - y)\,\phi(y)$ is $\mathrm{AEStronglyMeasurable}$ with respect to Lebesgue measure on $\mathbb{R}^n$.

                            Inverse Fourier transform expressed via the forward transform at $-z$: $f^\vee(z) = \hat f(-z)$. This is the standard symmetry used to reduce inverse-transform estimates to forward-transform results.

                            noncomputable def scaledGaussian (n : ) (z : ) (x : Fin n) :

                            The complex-scaled Gaussian $x \mapsto \exp(-\pi z |x|^2)$ for $z \in \mathbb{C}$ with $\operatorname{Re} z > 0$.

                            Instances For
                              theorem fourier_scaledGaussian_complex {n : } (z : ) (hz : 0 < z.re) (him : z.im 0) (ξ : Fin n) :

                              Fourier transform of the complex-scaled Gaussian (Proposition 3.0.3 of CM16, in scaledGaussian form): for $\operatorname{Re} z > 0$ and $\operatorname{Im} z \neq 0$, $$\widehat{\exp(-\pi z |\cdot|^2)}(\xi) = z^{-n/2}\, \exp(-\pi |\xi|^2 / z).$$

                              theorem norm_inverseFT_regularizedGaussian_uniform_bound {n : } (t : ) (ht : 0 < t) :
                              ∃ (C : ), ∀ (δ : ), 0 < δ∀ (z : Fin n), inverseFourierTransformFin (regularizedGaussian n δ t) z C

                              Uniform $L^\infty$ bound on $g_\delta^\vee(t, \cdot)$ in $\delta > 0$ and $z \in \mathbb{R}^n$: there exists $C > 0$ (depending on $n, t$) with $\|g_\delta^\vee(t, z)\| \le C$ for all $\delta > 0$. One may take $C = (2\pi t)^{-n/2}$.

                              theorem uniform_bound_regularized_kernel_on_compact {n : } (t : ) (ht : 0 < t) (K : Set (Fin n)) (hK : IsCompact K) :
                              ∃ (C : ) (δ₀ : ), 0 < δ₀ δSet.Ioo 0 δ₀, zK, inverseFourierTransformFin (regularizedGaussian n δ t) z C

                              Localized form of the uniform bound: for any compact set $K \subset \mathbb{R}^n$ there exists a uniform constant $C$ and a threshold $\delta_0 > 0$ such that $g_\delta^\vee(t, z)$ is bounded by $C$ for all $\delta \in (0, \delta_0)$ and $z \in K$.

                              theorem uniform_bound_regularized_integrand {n : } (φ : (Fin n)) (hφ_smooth : ContDiff φ) (hφ_supp : HasCompactSupport φ) (t : ) (ht : 0 < t) (x : Fin n) :
                              ∃ (bound : (Fin n)), MeasureTheory.Integrable bound MeasureTheory.volume ∀ᶠ (δ : ) in nhdsWithin 0 (Set.Ioi 0), ∀ᵐ (y : Fin n), inverseFourierTransformFin (regularizedGaussian n δ t) (x - y) * φ y bound y

                              Integrable dominating function for the convolution integrand: for $\phi \in C_c^\infty(\mathbb{R}^n)$ there is an integrable function $\text{bound}(y) = |C| \cdot \|\phi(y)\|$ such that eventually in $\delta \downarrow 0$, $\|g_\delta^\vee(t, x - y)\,\phi(y)\| \le \text{bound}(y)$ almost everywhere in $y$. This is the hypothesis required for dominated convergence under the integral.

                              theorem dominated_convergence_convolution {n : } (φ : (Fin n)) (hφ_smooth : ContDiff φ) (hφ_supp : HasCompactSupport φ) (t : ) (ht : 0 < t) (x : Fin n) :
                              ((nhdsWithin 0 (Set.Ioi 0)).limUnder fun (δ : ) => (y : Fin n), inverseFourierTransformFin (regularizedGaussian n δ t) (x - y) * φ y) = schrodingerConvolution n φ t x

                              Dominated convergence for the convolution: as $\delta \downarrow 0$, $$\int g_\delta^\vee(t, x - y)\,\phi(y)\, d^n y \longrightarrow \int K(t, x - y)\,\phi(y)\, d^n y = (K(t, \cdot) * \phi)(x).$$

                              theorem proposition_2_0_1_convolution_representation (n : ) (φ : (Fin n)) (hφ_smooth : ContDiff φ) (hφ_supp : HasCompactSupport φ) (t : ) (ht : 0 < t) (x : Fin n) :

                              Proposition 2.0.1 (Calculation of the fundamental solution $K(t, x)$ for Schrödinger's equation): for $\phi \in C_c^\infty(\mathbb{R}^n)$ and $t > 0$, the function $\psi$ defined by $\hat\psi(t, \xi) = \hat K(t, \xi)\,\hat\phi(\xi)$ admits the convolution representation $$\psi(t, x) = (K(t, \cdot) * \phi)(x) = \int K(t, x - y)\,\phi(y)\, d^n y,$$ where $K(t, x) = (2\pi i t)^{-n/2}\, e^{i|x|^2/(2t)}$. The proof passes through the regularized Gaussian $g_\delta$ and takes the limit $\delta \downarrow 0$.