The Laplacian of a convolution

On a finite-dimensional real inner product space, convolution with a locally integrable function commutes with the Laplacian on C² functions with compact support:

Δ (f ⋆ g) = f ⋆ Δ g.

Each second directional derivative passes onto g by the rule ∂ᵥ (f ⋆ g) = f ⋆ ∂ᵥ g (HasCompactSupport.fderiv_convolution_right_apply), and the Laplacian is their sum along an orthonormal basis (TauCeti.laplacian_eq_sum_fderiv_fderiv_apply).

This is how a convolution against a fundamental solution, such as the Newtonian potential, is shown to solve Poisson's equation: the Laplacian moves onto the smooth compactly supported factor, where the distributional identity for the kernel applies (TauCeti.laplacian_convolution_eq_neg_of_integral_laplacian_mul).

Main declarations

• HasCompactSupport.laplacian_convolution_right: Δ (f ⋆[L, μ] g) = f ⋆[L, μ] Δ g.
• TauCeti.laplacian_convolution_eq_neg_of_integral_laplacian_mul: if -ΔK = δ in the sense of distributions, then -Δ (K ⋆ f) = f for every C² function f with compact support.

theorem HasCompactSupport.laplacian_convolution_right {E : Type u_1} {E₀ : Type u_2} {E' : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.SFinite μ] [μ.IsAddLeftInvariant] [NormedAddCommGroup E₀] [NormedSpace ℝ E₀] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → E₀} {g : E → E'} (L : E₀ →L[ℝ] E' →L[ℝ] F) (hcg : HasCompactSupport g) (hf : MeasureTheory.LocallyIntegrable f μ) (hg : ContDiff ℝ 2 g) : Laplacian.laplacian (MeasureTheory.convolution f g L μ) = MeasureTheory.convolution f (Laplacian.laplacian g) L μ

The Laplacian of a convolution. If f is locally integrable and g is C² with compact support, then Δ (f ⋆ g) = f ⋆ Δ g.

theorem TauCeti.laplacian_convolution_eq_neg_of_integral_laplacian_mul {E : Type u_1} {F : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.SFinite μ] [μ.IsAddLeftInvariant] [NormedAddCommGroup F] [NormedSpace ℝ F] [μ.IsNegInvariant] [CompleteSpace F] {K : E → ℝ} {f : E → F} (hK : MeasureTheory.LocallyIntegrable K μ) (hKΔ : ∀ (φ : E → ℝ), ContDiff ℝ 2 φ → HasCompactSupport φ → ∀ (x : E), ∫ (y : E), Laplacian.laplacian φ y * K (x - y) ∂μ = -φ x) (hf : ContDiff ℝ 2 f) (hc : HasCompactSupport f) : Laplacian.laplacian (MeasureTheory.convolution K f (ContinuousLinearMap.lsmul ℝ ℝ) μ) = -f

Convolution with a fundamental solution solves Poisson's equation. Let K be locally integrable with -ΔK = δ in the sense of distributions, tested against real C² functions with compact support: ∫ Δφ(y) K(x - y) dy = -φ x for every such φ and every x. Then for every f of class C² with compact support, Δ (K ⋆ f) = -f.