The heat flow solves the heat equation: $\partial_t e^{\nu t\Delta}f = \nu\,\Delta e^{\nu t\Delta}f$

Proved

NavierStokes.hasDerivAt_heatFlow

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

analysisheat-equationnavier-stokespartial-differential-equations

Let $\nu>0$ and let $f:\mathbb R^3\to\mathbb R^3$ be bounded and measurable ( $|f|\le M$ ). Then for every $t>0$ and $x\in\mathbb R^3$ the function $s\mapsto(e^{\nu s\Delta}f)(x)$ (NavierStokes.heatFlow) is differentiable at $s=t$ with

\frac{\partial}{\partial t}\big(e^{\nu t\Delta}f\big)(x) = \nu\,\Delta\big(e^{\nu t\Delta}f\big)(x),

i.e. $u(t,x)=e^{\nu t\Delta}f(x)$ is a classical solution of the heat equation $\partial_tu=\nu\Delta u$ on $(0,\infty)\times\mathbb R^3$ (Evans, §2.3.1, Theorem 1). The proof differentiates $t\mapsto\int K_\nu(t,x-y)f(y)\,dy$ under the integral sign on the interval $(t/2,2t)$ , using the kernel identity $\partial_tK_\nu=\nu\Delta K_\nu$ and the Gaussian domination $|\partial_tK_\nu(s,z)|\le C_t(1+|z|^2)e^{-|z|^2/8\nu t}$ for $s\in(t/2,2t)$ , and then identifies the resulting convolution with $\nu\Delta(e^{\nu t\Delta}f)$ via laplacian_heatFlow. This is the input needed to show that Kato's mild solutions of Navier–Stokes are classical solutions.

Preamble

import Definitions.Def_NavierStokes_Mild
import Mathlib

open MeasureTheory Real Laplacian
open scoped ENNReal

Formal statement

namespace NavierStokes
theorem hasDerivAt_heatFlow {ν t : ℝ} (hν : 0 < ν) (ht : 0 < t) {f : Vec 3 → Vec 3}
    (hf : AEStronglyMeasurable f volume) {M : ℝ} (hM : ∀ y, ‖f y‖ ≤ M) (x : Vec 3) :
    HasDerivAt (fun s => heatFlow ν s f x) (ν • Δ (heatFlow ν t f) x) t := by sorry
end NavierStokes

Source

The heat kernel solves the heat equation; e.g. L. C. Evans, Partial Differential Equations, 2nd ed., AMS GSM 19 (2010), §2.3.1, Theorem 1 (solution of the initial-value problem; the semigroup is C^∞ and satisfies u_t − Δu = 0 for t > 0). Mission context: Prove2Me mission 'Formalize Navier-Stokes', child NavierStokes.isSolutionOn_of_isMildSolutionOn (mild ⇒ classical needs ∂_t e^{νtΔ} = νΔ e^{νtΔ}).

View graph

The heat flow solves the heat equation: ∂teνtΔf=ν ΔeνtΔf\partial_t e^{\nu t\Delta}f = \nu\,\Delta e^{\nu t\Delta}f∂t​eνtΔf=νΔeνtΔf

The heat flow solves the heat equation: $\partial_t e^{\nu t\Delta}f = \nu\,\Delta e^{\nu t\Delta}f$