Heat-kernel convolution

This file records the scalar convolution interface used by the heat-kernel route to the Newtonian kernel. The heat kernel is the left factor and the compactly supported function is the right factor, so Mathlib's right-factor regularity and derivative-transport theorems apply directly.

noncomputable def CKN.Foundation.Heat.heatConv (t : ℝ) (u : Parabolic.Vec3 → ℝ) : Parabolic.Vec3 → ℝ

Spatial convolution of the heat kernel with a scalar function.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Foundation.Heat.heatConv_eq_integral (t : ℝ) (u : Parabolic.Vec3 → ℝ) (x : Parabolic.Vec3) : heatConv t u x = ∫ (y : Parabolic.Vec3), heatKernel y t * u (x - y)

Pointwise integral form of heatConv.

theorem CKN.Foundation.Heat.heatKernel_scaling {x : Parabolic.Vec3} {t : ℝ} (ht : 0 < t) : heatKernel x t = (√t)⁻¹ ^ 3 * heatKernel ((√t)⁻¹ • x) 1

Heat-kernel scaling in the spatial variable.

theorem CKN.Foundation.Heat.heatKernel_profile_tendsto_zero_cobounded : Filter.Tendsto (fun (z : Parabolic.Vec3) => ‖z‖ ^ 3 * heatKernel z 1) (Bornology.cobounded Parabolic.Vec3) (nhds 0)

The Gaussian profile has vanishing polynomially weighted tails.

theorem CKN.Foundation.Heat.heatKernel_profile_tendsto_zero_cobounded_nat : Filter.Tendsto (fun (z : Parabolic.Vec3) => ‖z‖ ^ 3 * heatKernel z 1) (Bornology.cobounded Parabolic.Vec3) (nhds 0)

The heat-kernel profile tail in the natural-number power form.

theorem CKN.Foundation.Heat.heatConv_tendsto_self_nhdsWithin_zero_smooth {u : Parabolic.Vec3 → ℝ} (hu : ContDiff ℝ (↑⊤) u) (huSupport : HasCompactSupport u) (x : Parabolic.Vec3) : Filter.Tendsto (fun (t : ℝ) => heatConv t u x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (u x))

Compactly supported heat convolution converges pointwise to its input at positive times tending to zero.

theorem CKN.Foundation.Heat.heatConv_hasDerivAt_integral_smooth {u : Parabolic.Vec3 → ℝ} (hu : ContDiff ℝ (↑⊤) u) (huSupport : HasCompactSupport u) {t : ℝ} (ht : 0 < t) (x : Parabolic.Vec3) : HasDerivAt (fun (s : ℝ) => heatConv s u x) (∫ (y : Parabolic.Vec3), heatKernelTimeDerivative y t * u (x - y)) t

Time differentiation of heat convolution under the spatial integral.

theorem CKN.Foundation.Heat.heatConv_hasDerivAt_laplacianIntegral_smooth {u : Parabolic.Vec3 → ℝ} (hu : ContDiff ℝ (↑⊤) u) (huSupport : HasCompactSupport u) {t : ℝ} (ht : 0 < t) (x : Parabolic.Vec3) : HasDerivAt (fun (s : ℝ) => heatConv s u x) (∫ (y : Parabolic.Vec3), heatKernelLaplacian y t * u (x - y)) t

The time derivative is the spatial-Laplacian integral of the heat kernel.

theorem CKN.Foundation.Heat.heatKernel_le_prefactor {y : Parabolic.Vec3} {t : ℝ} (ht : 0 < t) : heatKernel y t ≤ (4 * Real.pi * t) ^ (-3 / 2)

The heat kernel is bounded by its spatially constant prefactor.

theorem CKN.Foundation.Heat.heatConv_abs_le_prefactor_mul_integral_smooth {u : Parabolic.Vec3 → ℝ} (hu : ContDiff ℝ (↑⊤) u) (huSupport : HasCompactSupport u) {t : ℝ} (ht : 0 < t) (x : Parabolic.Vec3) : |heatConv t u x| ≤ (4 * Real.pi * t) ^ (-3 / 2) * ∫ (y : Parabolic.Vec3), ‖u y‖

A compactly supported convolution has the standard large-time bound.

theorem CKN.Foundation.Heat.heatKernel_tendsto_zero_atTop (y : Parabolic.Vec3) : Filter.Tendsto (fun (t : ℝ) => heatKernel y t) Filter.atTop (nhds 0)

The heat kernel tends pointwise to zero at large time.

theorem CKN.Foundation.Heat.heatConv_tendsto_zero_atTop_smooth {u : Parabolic.Vec3 → ℝ} (hu : ContDiff ℝ (↑⊤) u) (huSupport : HasCompactSupport u) (x : Parabolic.Vec3) : Filter.Tendsto (fun (t : ℝ) => heatConv t u x) Filter.atTop (nhds 0)

Heat convolution of a compactly supported continuous function vanishes at large time.