The heat kernel has unit mass

Proved

NavierStokes.integral_heatKernel

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

analysisheat-equationnavier-stokespartial-differential-equations

For $\nu>0$ and $t>0$ ,

\int_{\mathbb R^3} (4\pi\nu t)^{-3/2}\,e^{-|x|^2/(4\nu t)}\,dx = 1 .

This is the normalisation of the fundamental solution of $\partial_t-\nu\Delta$ (Evans, §2.3.1). It follows from the Gaussian integral $\int_{\mathbb R^3}e^{-b|x|^2}dx = (\pi/b)^{3/2}$ with $b = 1/(4\nu t)$ .

Preamble

import Definitions.Def_NavierStokes_Mild
import Mathlib

open MeasureTheory Real

Formal statement

namespace NavierStokes
theorem integral_heatKernel {ν t : ℝ} (hν : 0 < ν) (ht : 0 < t) :
    ∫ x, heatKernel ν t x = 1 := by sorry
end NavierStokes

Source

Standard heat-kernel facts on ℝ³; see e.g. L. C. Evans, Partial Differential Equations, 2nd ed., AMS GSM 19 (2010), §2.3.1 (fundamental solution, Lemma p. 46: unit mass) and §2.3.3; for the Kato route: T. Kato, Math. Z. 187 (1984), §2 eq. (2.1)–(2.3) (semigroup estimates ‖∇e^{tΔ}f‖₂ ≤ C t^{-1/2}‖f‖₂). Mission context: Prove2Me mission 'Formalize Navier-Stokes', child NavierStokes.exists_mildSolutionOn_Ico (Kato local existence).

View graph