Laplacian of the heat flow: $\Delta(e^{\nu t\Delta}f) = (\Delta K_t) * f$

Proved

NavierStokes.laplacian_heatFlow

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

analysisheat-equationnavier-stokespartial-differential-equations

Let $\nu>0$ , $t>0$ and let $f:\mathbb R^3\to\mathbb R^3$ be bounded and measurable ( $|f|\le M$ ). Then $u=e^{\nu t\Delta}f$ is twice differentiable and its Laplacian (Mathlib's Δ, the trace of the second Fréchet derivative over an orthonormal basis) is obtained by differentiating the kernel under the integral:

\Delta u(x_0) = \int_{\mathbb R^3}\Delta_xK_\nu(t,x_0-y)\,f(y)\,dy,\qquad \Delta_xK_\nu(t,z)=K_\nu(t,z)\Big(\frac{|z|^2}{4\nu^2t^2}-\frac{3}{2\nu t}\Big).

Here $K_\nu(t,z)=(4\pi\nu t)^{-3/2}e^{-|z|^2/(4\nu t)}$ is NavierStokes.heatKernel. The proof differentiates $x\mapsto\int K(x-y)f(y)\,dy$ twice under the integral sign, with Gaussian domination $|z|^2K(z)\le 8\nu t\,(4\pi\nu t)^{-3/2}e^{-|z|^2/8\nu t}$ uniform on unit balls, and evaluates the trace of the second-derivative kernel $D^2K(z)(v,w)=K(z)\big(\tfrac{\langle z,v\rangle\langle z,w\rangle}{4\nu^2t^2}-\tfrac{\langle v,w\rangle}{2\nu t}\big)$ . It is the spatial half of the heat equation for the semigroup.

Preamble

import Definitions.Def_NavierStokes_Mild
import Mathlib

open MeasureTheory Real Laplacian
open scoped ENNReal

Formal statement

namespace NavierStokes
theorem laplacian_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) :
    Δ (heatFlow ν t f) x₀ =
      ∫ y, (heatKernel ν t (x₀ - y) *
        ((1 / (2 * ν * t)) ^ 2 * ‖x₀ - y‖ ^ 2 - 3 * (1 / (2 * ν * t)))) • f y := 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

Laplacian of the heat flow: Δ(eνtΔf)=(ΔKt)∗f\Delta(e^{\nu t\Delta}f) = (\Delta K_t) * fΔ(eνtΔf)=(ΔKt​)∗f

Laplacian of the heat flow: $\Delta(e^{\nu t\Delta}f) = (\Delta K_t) * f$