Convolution semigroup of heat kernels: $K_s * K_t = K_{s+t}$

Proved

NavierStokes.integral_heatKernel_mul_heatKernel

by korbonits · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisheat-equationnavier-stokespartial-differential-equations

For $\nu>0$ and times $s,t>0$ the heat kernels $K_\nu(t,x)=(4\pi\nu t)^{-3/2}e^{-|x|^2/(4\nu t)}$ on $\mathbb R^3$ satisfy the convolution identity

\int_{\mathbb R^3}K_\nu(s,w-y)\,K_\nu(t,y)\,dy = K_\nu(s+t,w)\qquad(w\in\mathbb R^3).

This is the Chapman–Kolmogorov / semigroup property of the Gaussian kernel. It follows by completing the square: the product of the two Gaussians is $A\,e^{-b|y|^2+c\langle w,y\rangle}$ with $b=\frac1{4\nu s}+\frac1{4\nu t}$ , $c=\frac1{2\nu s}$ , whose integral is $(\pi/b)^{3/2}e^{c^2|w|^2/(4b)}$ (Mathlib's Gaussian integral with a linear term), and the constants recombine to $(4\pi\nu(s+t))^{-3/2}e^{-|w|^2/(4\nu(s+t))}$ .

Preamble

import Definitions.Def_NavierStokes_Mild
import Mathlib

open MeasureTheory Real
open scoped ENNReal RealInnerProductSpace

Formal statement

namespace NavierStokes
theorem integral_heatKernel_mul_heatKernel {ν : ℝ} (hν : 0 < ν) {s t : ℝ} (hs : 0 < s) (ht : 0 < t)
    (w : Vec 3) :
    ∫ y, heatKernel ν s (w - y) * heatKernel ν t y = heatKernel ν (s + t) w := by sorry
end NavierStokes

Source

Semigroup property of the Gaussian heat kernel; e.g. L. C. Evans, Partial Differential Equations, 2nd ed., §2.3.1, and E. M. Stein–R. Shakarchi, Fourier Analysis, Ch. 5 (Gaussians are closed under convolution). Mission context: Prove2Me mission 'Formalize Navier-Stokes', child NavierStokes.exists_mildSolutionOn_Ico (Duhamel manipulations).

View graph

Convolution semigroup of heat kernels: Ks∗Kt=Ks+tK_s * K_t = K_{s+t}Ks​∗Kt​=Ks+t​

Convolution semigroup of heat kernels: $K_s * K_t = K_{s+t}$