The heat kernel is integrable

Proved

NavierStokes.integrable_heatKernel

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

analysisheat-equationnavier-stokespartial-differential-equations

For $\nu>0$ and $t>0$ the heat kernel $K_\nu(t,\cdot) = (4\pi\nu t)^{-3/2}e^{-|\cdot|^2/(4\nu t)}$ is Lebesgue integrable on $\mathbb R^3$ (MeasureTheory.Integrable with respect to Lebesgue measure). It is a Gaussian, so this is the integrability of $e^{-b|x|^2}$ for $b>0$ .

Preamble

import Definitions.Def_NavierStokes_Mild
import Mathlib

open MeasureTheory Real

Formal statement

namespace NavierStokes
theorem integrable_heatKernel {ν t : ℝ} (hν : 0 < ν) (ht : 0 < t) :
    Integrable (heatKernel ν t) := 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