Semigroup property of the heat flow: $e^{\nu s\Delta}e^{\nu t\Delta}f = e^{\nu(s+t)\Delta}f$

Proved

NavierStokes.heatFlow_heatFlow

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

analysisheat-equationnavier-stokespartial-differential-equations

Let $\nu>0$ , $s,t>0$ , and let $f:\mathbb R^3\to\mathbb R^3$ be a bounded measurable vector field ( $|f|\le M$ ). Then at every point $x$ ,

\big(e^{\nu s\Delta}e^{\nu t\Delta}f\big)(x) = \big(e^{\nu(s+t)\Delta}f\big)(x),

i.e. the heat flow NavierStokes.heatFlow is a semigroup in time. The proof combines Fubini's theorem (the double integral $\iint K_s(x-y)K_t(y-z)|f(z)|\,dy\,dz$ converges because both kernels have unit mass and $f$ is bounded) with the convolution identity $K_s*K_t=K_{s+t}$ (integral_heatKernel_mul_heatKernel). It is the identity behind all manipulations of Duhamel's formula in the Kato route to local existence.

Preamble

import Definitions.Def_NavierStokes_Mild
import Mathlib

open MeasureTheory Real
open scoped ENNReal RealInnerProductSpace

Formal statement

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

Source

Semigroup property of the Gaussian heat kernel; e.g. L. C. Evans, Partial Differential Equations, 2nd ed., §2.3.1, and E. M. Stein–R. Shakarchi, Fourier Analysis, Ch. 5 (Gaussians are closed under convolution). Mission context: Prove2Me mission 'Formalize Navier-Stokes', child NavierStokes.exists_mildSolutionOn_Ico (Duhamel manipulations).

View graph

Semigroup property of the heat flow: eνsΔeνtΔf=eν(s+t)Δfe^{\nu s\Delta}e^{\nu t\Delta}f = e^{\nu(s+t)\Delta}feνsΔeνtΔf=eν(s+t)Δf

Semigroup property of the heat flow: $e^{\nu s\Delta}e^{\nu t\Delta}f = e^{\nu(s+t)\Delta}f$