The resolvent of the Laplacian on tempered distributions

For c > 0 the shifted Laplacian -Δ + c is the Fourier multiplier with symbol (2π)² ‖ξ‖² + c, the factor (2π)² coming from Mathlib's normalization of the Fourier transform. This symbol is bounded below by c, so the Fourier multiplier with the reciprocal symbol is a two-sided inverse TemperedDistribution.laplacianResolvent c of -Δ + c on all tempered distributions. It extends the resolvent SchwartzMap.laplacianResolvent on Schwartz space.

On the L² Sobolev scale the resolvent gains two derivatives: it maps H^s to H^{s+2}. With Mathlib's mapping property of the Laplacian, this gives elliptic regularity for -Δ + c: a tempered distribution f lies in H^{s+2} exactly when -Δ f + c f lies in H^s. Inverting a constant-coefficient first-order operator L satisfying a Weitzenböck identity L* L = L L* = -Δ + c on the Sobolev scale reduces to this statement, through L⁻¹ = L* (-Δ + c)⁻¹.

Main declarations

• TemperedDistribution.neg_laplacian_add_smul_eq_fourierMultiplierCLM: -Δ + c is the Fourier multiplier with symbol (2π)² ‖ξ‖² + c.
• TemperedDistribution.laplacianResolvent c: the Fourier multiplier with symbol ((2π)² ‖ξ‖² + c)⁻¹ (TemperedDistribution.laplacianResolvent_eq_fourierMultiplierCLM), characterized for c > 0 as the two-sided inverse of -Δ + c by TemperedDistribution.laplacianResolvent_neg_laplacian_add_smul and TemperedDistribution.neg_laplacian_laplacianResolvent_add_smul.
• TemperedDistribution.eq_zero_of_neg_laplacian_add_smul_eq_zero: for c > 0, -Δ + c has trivial kernel on tempered distributions.
• TemperedDistribution.laplacianResolvent_toTemperedDistributionCLM_eq: on Schwartz functions it is SchwartzMap.laplacianResolvent.
• TemperedDistribution.MemSobolev.laplacianResolvent: the resolvent maps H^s to H^{s+2}.
• TemperedDistribution.memSobolev_add_two_iff_neg_laplacian_add_smul: f ∈ H^{s+2} if and only if -Δ f + c f ∈ H^s.

References

• M. Taylor, Partial Differential Equations I, Chapter 4, §1 (the Sobolev spaces H^s and the mapping properties of elliptic operators with constant coefficients).

theorem TemperedDistribution.neg_laplacian_add_smul_eq_fourierMultiplierCLM {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] (c : ℝ) (f : TemperedDistribution E F) : -Laplacian.laplacian f + c • f = (fourierMultiplierCLM F fun (ξ : E) => ↑((2 * Real.pi) ^ 2 * ‖ξ‖ ^ 2 + c)) f

The shifted Laplacian -Δ + c is the Fourier multiplier with symbol (2π)² ‖ξ‖² + c.

noncomputable def TemperedDistribution.laplacianResolvent {E : Type u_1} (F : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] (c : ℝ) : TemperedDistribution E F →L[ℂ] TemperedDistribution E F

The resolvent of the Laplacian (c - Δ)⁻¹ on tempered distributions: the Fourier multiplier with symbol ((2π)² ‖ξ‖² + c)⁻¹. For c > 0 it is the two-sided inverse of -Δ + c (laplacianResolvent_neg_laplacian_add_smul and neg_laplacian_laplacianResolvent_add_smul); for c ≤ 0 the value is not meaningful.

theorem TemperedDistribution.laplacianResolvent_eq_fourierMultiplierCLM {E : Type u_1} (F : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] (c : ℝ) : laplacianResolvent F c = fourierMultiplierCLM F fun (ξ : E) => ↑((2 * Real.pi) ^ 2 * ‖ξ‖ ^ 2 + c)⁻¹

The resolvent of the Laplacian is the Fourier multiplier with symbol ((2π)² ‖ξ‖² + c)⁻¹.

@[simp]

theorem TemperedDistribution.laplacianResolvent_neg_laplacian_add_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] {c : ℝ} (hc : 0 < c) (f : TemperedDistribution E F) : (laplacianResolvent F c) (-Laplacian.laplacian f + c • f) = f

The resolvent of the Laplacian is a left inverse of -Δ + c, for c > 0.

@[simp]

theorem TemperedDistribution.neg_laplacian_laplacianResolvent_add_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] {c : ℝ} (hc : 0 < c) (f : TemperedDistribution E F) : -Laplacian.laplacian ((laplacianResolvent F c) f) + c • (laplacianResolvent F c) f = f

The resolvent of the Laplacian is a right inverse of -Δ + c, for c > 0.

theorem TemperedDistribution.eq_zero_of_neg_laplacian_add_smul_eq_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] {c : ℝ} (hc : 0 < c) {f : TemperedDistribution E F} (hf : -Laplacian.laplacian f + c • f = 0) : f = 0

For c > 0, the shifted Laplacian -Δ + c has trivial kernel on tempered distributions.

@[simp]

theorem TemperedDistribution.laplacianResolvent_toTemperedDistributionCLM_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {c : ℝ} (hc : 0 < c) (f : SchwartzMap E F) : (laplacianResolvent F c) ((SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) f) = (SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) ((SchwartzMap.laplacianResolvent c) f)

The resolvent of the Laplacian on tempered distributions extends the resolvent SchwartzMap.laplacianResolvent on Schwartz space, for c > 0.

theorem TemperedDistribution.MemSobolev.laplacianResolvent {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] {c s : ℝ} (hc : 0 < c) {f : TemperedDistribution E F} (hf : MemSobolev s 2 f) : MemSobolev (s + 2) 2 ((TemperedDistribution.laplacianResolvent F c) f)

The resolvent of the Laplacian gains two derivatives: it maps the Sobolev space H^s to H^{s+2}, for c > 0.

theorem TemperedDistribution.memSobolev_add_two_iff_neg_laplacian_add_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] {c s : ℝ} (hc : 0 < c) {f : TemperedDistribution E F} : MemSobolev (s + 2) 2 f ↔ MemSobolev s 2 (-Laplacian.laplacian f + c • f)

Elliptic regularity for the shifted Laplacian: for c > 0, a tempered distribution f lies in the Sobolev space H^{s+2} if and only if -Δ f + c f lies in H^s.