The resolvent of the Laplacian on Schwartz space #

For c > 0 the shifted Laplacian -Δ + c is a bijection of Schwartz space. With Mathlib's normalization of the Fourier transform, 𝓕 (Δ f) ξ = -(2π)² ‖ξ‖² 𝓕 f ξ, so -Δ + c is the Fourier multiplier with symbol (2π)² ‖ξ‖² + c. This symbol is bounded below by c, and its reciprocal ((2π)² ‖ξ‖² + c)⁻¹ has temperate growth, so the Fourier multiplier with the reciprocal symbol is a continuous inverse of -Δ + c on Schwartz functions with values in a complex Banach space.

For Schwartz functions with values in a real Banach space G, the Fourier transform is not available directly, since it takes values in a complex space. We embed the values in the complexification TauCeti.Complexification G, apply the complex inverse, and take real parts. Since the Laplacian commutes with these real-linear maps, the result is a continuous real-linear inverse SchwartzMap.laplacianResolvent c of -Δ + c on 𝓢(E, G), which is the resolvent (c - Δ)⁻¹ of the Laplacian at c.

Inverting -Δ + c is the basic step in inverting constant-coefficient first-order operators L satisfying a Weitzenböck identity L* L = L L* = -Δ + c: then L⁻¹ = L* (-Δ + c)⁻¹.

Main declarations #

TauCeti.hasTemperateGrowth_inv_mul_norm_sq_add: the symbol (a ‖ξ‖² + c)⁻¹, for a ≥ 0 and c > 0, has temperate growth.
SchwartzMap.neg_laplacian_fourierMultiplierCLM_add_smul and SchwartzMap.fourierMultiplierCLM_neg_laplacian_add_smul: the Fourier multiplier with symbol ((2π)² ‖ξ‖² + c)⁻¹ is a two-sided inverse of -Δ + c on complex Schwartz space.
SchwartzMap.laplacianResolvent c: the inverse of -Δ + c on Schwartz functions with values in a real Banach space, characterized by SchwartzMap.neg_laplacian_laplacianResolvent_add_smul and SchwartzMap.laplacianResolvent_neg_laplacian_add_smul.

References #

M. Taylor, Partial Differential Equations I, Chapter 3, §1 (the Fourier transform on Schwartz space and constant-coefficient operators).

source

theorem TauCeti.hasTemperateGrowth_inv_mul_norm_sq_add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {a c : ℝ} (ha : 0 ≤ a) (hc : 0 < c) :

Function.HasTemperateGrowth fun (ξ : E) => (a * ‖ξ‖ ^ 2 + c)⁻¹

The symbol ξ ↦ (a ‖ξ‖² + c)⁻¹, for a ≥ 0 and c > 0, has temperate growth. It is a rescaling of the Bessel potential (1 + ‖ξ‖²)⁻¹.

source

@[simp]

theorem SchwartzMap.neg_laplacian_fourierMultiplierCLM_add_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {c : ℝ} (hc : 0 < c) (f : SchwartzMap E F) :

-Laplacian.laplacian ((fourierMultiplierCLM F fun (ξ : E) => ((2 * Real.pi) ^ 2 * ‖ξ‖ ^ 2 + c)⁻¹) f) + c • (fourierMultiplierCLM F fun (ξ : E) => ((2 * Real.pi) ^ 2 * ‖ξ‖ ^ 2 + c)⁻¹) f = f

The Fourier multiplier with symbol ((2π)² ‖ξ‖² + c)⁻¹ is a right inverse of -Δ + c.

source

@[simp]

theorem SchwartzMap.fourierMultiplierCLM_neg_laplacian_add_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {c : ℝ} (hc : 0 < c) (f : SchwartzMap E F) :

(fourierMultiplierCLM F fun (ξ : E) => ((2 * Real.pi) ^ 2 * ‖ξ‖ ^ 2 + c)⁻¹) (-Laplacian.laplacian f + c • f) = f

The Fourier multiplier with symbol ((2π)² ‖ξ‖² + c)⁻¹ is a left inverse of -Δ + c.

source

noncomputable def SchwartzMap.laplacianResolvent {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {G : Type u_2} [NormedAddCommGroup G] [NormedSpace ℝ G] (c : ℝ) :

SchwartzMap E G →L[ℝ ] SchwartzMap E G

The resolvent of the Laplacian (c - Δ)⁻¹ on Schwartz functions with values in a real Banach space G. For c > 0 it is the two-sided inverse of -Δ + c (neg_laplacian_laplacianResolvent_add_smul and laplacianResolvent_neg_laplacian_add_smul). It is the real part of the Fourier multiplier with symbol ((2π)² ‖ξ‖² + c)⁻¹, applied to the complexification TauCeti.Complexification G of the values. For c ≤ 0 the value is not meaningful.