Second derivatives of compactly supported convolutions

Smooth compactly supported kernels regularize continuous functions.

The Hessian of a convolution is the convolution of the kernel Hessian.

theorem LiebThirring.contDiff_convolution_of_continuous {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsLocallyFiniteMeasure μ] {w b : E → ℝ} {n : ℕ∞} (hw : Continuous w) (hb : ContDiff ℝ (↑n) b) (hbc : HasCompactSupport b) : ContDiff ℝ (↑n) (MeasureTheory.convolution w b (ContinuousLinearMap.lsmul ℝ ℝ) μ)

Smooth compactly supported kernels regularize continuous functions.

theorem LiebThirring.fderiv_fderiv_convolution {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsLocallyFiniteMeasure μ] [MeasureTheory.SFinite μ] [μ.IsAddLeftInvariant] {w b : E → ℝ} (hw : Continuous w) (hb : ContDiff ℝ 2 b) (hbc : HasCompactSupport b) (x u v : E) : ((fderiv ℝ (fderiv ℝ (MeasureTheory.convolution w b (ContinuousLinearMap.lsmul ℝ ℝ) μ)) x) u) v = ∫ (z : E), w z * ((fderiv ℝ (fderiv ℝ b) (x - z)) u) v ∂μ

The Hessian of a convolution is the convolution of the kernel Hessian.

theorem LiebThirring.hasCompactSupport_kernel_hessian {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {b : E → ℝ} (hbc : HasCompactSupport b) (u v : E) : HasCompactSupport fun (z : E) => ((fderiv ℝ (fderiv ℝ b) z) u) v

Scalar evaluations of the kernel Hessian have compact support.

theorem LiebThirring.continuous_kernel_hessian {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {b : E → ℝ} (hb : ContDiff ℝ 2 b) (u v : E) : Continuous fun (z : E) => ((fderiv ℝ (fderiv ℝ b) z) u) v

Scalar evaluations of a C² kernel Hessian are continuous.

theorem LiebThirring.integrable_mul_kernel_hessian {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsLocallyFiniteMeasure μ] {w b : E → ℝ} (hw : Continuous w) (hb : ContDiff ℝ 2 b) (hbc : HasCompactSupport b) (x u v : E) : MeasureTheory.Integrable (fun (z : E) => w z * ((fderiv ℝ (fderiv ℝ b) (x - z)) u) v) μ

Scalar Hessian evaluations against a continuous function are integrable.

theorem LiebThirring.laplacian_convolution {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsLocallyFiniteMeasure μ] [MeasureTheory.SFinite μ] [μ.IsAddLeftInvariant] {w b : E → ℝ} (hw : Continuous w) (hb : ContDiff ℝ 2 b) (hbc : HasCompactSupport b) (x : E) : Laplacian.laplacian (MeasureTheory.convolution w b (ContinuousLinearMap.lsmul ℝ ℝ) μ) x = ∫ (z : E), w z * Laplacian.laplacian b (x - z) ∂μ

The Laplacian commutes with convolution by a compactly supported C² kernel.