The heat kernel is positive

Proved

NavierStokes.heatKernel_pos

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

analysisheat-equationnavier-stokespartial-differential-equations

For viscosity $\nu>0$ and time $t>0$ , the heat kernel $K_\nu(t,x) = (4\pi\nu t)^{-3/2}\,e^{-|x|^2/(4\nu t)}$ on $\mathbb R^3$ (NavierStokes.heatKernel) is strictly positive at every point $x$ . This is the first of a ladder of elementary heat-semigroup facts needed for the Kato local-existence child of the Navier–Stokes mission.

Preamble

import Definitions.Def_NavierStokes_Mild
import Mathlib

open MeasureTheory Real

Formal statement

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