The heat kernel on a Euclidean space

On a finite-dimensional real inner product space E of dimension n, the heat kernel (Gauss–Weierstrass kernel) at time t > 0 is the Gaussian

K_t(x) = (4πt)^(-n/2) exp(-‖x‖² / (4t)).

It is the fundamental solution of the heat equation ∂ₜu = Δu on ℝⁿ: the solution of the Cauchy problem with initial datum g is u(t, ·) = K_t ⋆ g, and the heat semigroup is convolution with K_t. This file records the basic properties of the kernel itself on which that theory rests:

• K_t is smooth in x, positive, and has total mass one;
• K solves the heat equation: ∂ₜ K_t(x) = Δ K_t(x) for t > 0;
• the semigroup (Chapman–Kolmogorov) identity K_t ⋆ K_s = K_{t+s};
• its Fourier transform, in Mathlib's convention 𝓕 f(ξ) = ∫ e^{-2πi⟪x, ξ⟫} f(x) dx, is 𝓕 K_t(ξ) = exp(-4π² t ‖ξ‖²).

The value of heatKernel t x for t ≤ 0 carries no meaning; every statement about the kernel as a heat kernel assumes 0 < t.

Main declarations

• TauCeti.heatKernel: the heat kernel K_t(x).
• TauCeti.heatKernel_pos: K_t > 0 for t > 0.
• TauCeti.heatKernel_eq_mul_heatKernel_one_smul: the parabolic scaling K_t(x) = (√t)⁻¹ ^ n K_1((√t)⁻¹ • x).
• TauCeti.contDiff_heatKernel: K_t is smooth.
• TauCeti.integral_heatKernel: ∫ K_t = 1 for t > 0.
• TauCeti.laplacian_heatKernel: Δ K_t(x) = (‖x‖² / (4t²) - n / (2t)) K_t(x).
• TauCeti.hasDerivAt_heatKernel: the heat equation ∂ₜ K_t(x) = Δ K_t(x) for t > 0.
• TauCeti.heatKernel_convolution_heatKernel: the semigroup identity K_t ⋆ K_s = K_{t+s}.
• TauCeti.fourier_heatKernel: 𝓕 K_t(ξ) = exp(-4π² t ‖ξ‖²).

References

• L. C. Evans, Partial Differential Equations, Section 2.3.1.
• E. M. Stein, G. Weiss, Introduction to Fourier Analysis on Euclidean Spaces, Chapter I, Theorem 1.13.

noncomputable def TauCeti.heatKernel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (t : ℝ) (x : E) : ℝ

The heat kernel (Gauss–Weierstrass kernel) on a finite-dimensional real inner product space E of dimension n: K_t(x) = (4πt)^(-n/2) exp(-‖x‖² / (4t)). It is meaningful only for t > 0.

Equations

• TauCeti.heatKernel t x = (4 * Real.pi * t) ^ (-↑(Module.finrank ℝ E) / 2) * Real.exp (-‖x‖ ^ 2 / (4 * t))

theorem TauCeti.heatKernel_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (t : ℝ) (x : E) : heatKernel t x = (4 * Real.pi * t) ^ (-↑(Module.finrank ℝ E) / 2) * Real.exp (-‖x‖ ^ 2 / (4 * t))

The defining formula of the heat kernel.

theorem TauCeti.heatKernel_pos {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {t : ℝ} (ht : 0 < t) (x : E) : 0 < heatKernel t x

The heat kernel is positive at every positive time.

@[simp]

theorem TauCeti.heatKernel_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (t : ℝ) (x : E) : heatKernel t (-x) = heatKernel t x

The heat kernel is radial; in particular it is even.

theorem TauCeti.heatKernel_eq_mul_heatKernel_one_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {t : ℝ} (ht : 0 < t) (x : E) : heatKernel t x = (√t)⁻¹ ^ Module.finrank ℝ E * heatKernel 1 ((√t)⁻¹ • x)

Parabolic scaling of the heat kernel. For t > 0, K_t is the L¹-normalized dilation of K_1 by the factor (√t)⁻¹: K_t(x) = (√t)⁻¹ ^ n K_1((√t)⁻¹ • x) with n = dim E.

theorem TauCeti.contDiff_heatKernel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (t : ℝ) {k : WithTop ℕ∞} : ContDiff ℝ k (heatKernel t)

The heat kernel K_t is smooth in the space variable (for every t).

theorem TauCeti.laplacian_heatKernel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (t : ℝ) (x : E) : Laplacian.laplacian (heatKernel t) x = (‖x‖ ^ 2 / (4 * t ^ 2) - ↑(Module.finrank ℝ E) / (2 * t)) * heatKernel t x

The Laplacian of the heat kernel: Δ K_t(x) = (‖x‖² / (4t²) - n / (2t)) K_t(x).

theorem TauCeti.hasDerivAt_heatKernel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {t : ℝ} (ht : 0 < t) (x : E) : HasDerivAt (fun (s : ℝ) => heatKernel s x) (Laplacian.laplacian (heatKernel t) x) t

The heat equation. For t > 0, the heat kernel solves ∂ₜ K_t(x) = Δ K_t(x).

@[simp]

theorem TauCeti.integral_heatKernel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {t : ℝ} (ht : 0 < t) : ∫ (x : E), heatKernel t x = 1

The heat kernel has mass one.

theorem TauCeti.integrable_heatKernel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {t : ℝ} (ht : 0 < t) : MeasureTheory.Integrable (heatKernel t) MeasureTheory.volume

The heat kernel is integrable at every positive time.

theorem TauCeti.heatKernel_convolution_heatKernel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {t s : ℝ} (ht : 0 < t) (hs : 0 < s) : MeasureTheory.convolution (heatKernel t) (heatKernel s) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume = heatKernel (t + s)

The semigroup property of the heat kernel (Chapman–Kolmogorov): K_t ⋆ K_s = K_{t+s} for t, s > 0.

theorem TauCeti.fourier_heatKernel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {t : ℝ} (ht : 0 < t) (ξ : E) : FourierTransform.fourier (fun (x : E) => ↑(heatKernel t x)) ξ = ↑(Real.exp (-(4 * Real.pi ^ 2 * t * ‖ξ‖ ^ 2)))

The Fourier transform of the heat kernel. In Mathlib's normalization 𝓕 f(ξ) = ∫ e^{-2πi⟪x, ξ⟫} f(x) dx, 𝓕 K_t(ξ) = exp(-4π² t ‖ξ‖²) for t > 0.