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

Proved

NavierStokes.div_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 differentiable with $f$ and $Df$ bounded. Then the divergence of the heat flow is the heat flow of the divergence:

\operatorname{div}\big(e^{\nu t\Delta}f\big)(x)=\int_{\mathbb R^3}K_\nu(t,x-y)\,\operatorname{div}f(y)\,dy .

Here NavierStokes.div is Fefferman's divergence $\sum_i\partial_iv_i$ computed from the Fréchet derivative, and $K_\nu$ is the heat kernel. The statement follows from the commutation $\partial_i(e^{\nu t\Delta}f)=e^{\nu t\Delta}(\partial_if)$ (fderiv_heatFlow_eq_heatFlow_fderiv) by taking the $i$ -th component and summing.

Preamble

import Definitions.Def_NavierStokes_Mild
import Mathlib

open MeasureTheory Real
open scoped ENNReal

Formal statement

namespace NavierStokes
theorem div_heatFlow {ν t : ℝ} (hν : 0 < ν) (ht : 0 < t) {f : Vec 3 → Vec 3}
    (hf : Differentiable ℝ f) {M₀ M₁ : ℝ} (h0 : ∀ y, ‖f y‖ ≤ M₀) (h1 : ∀ y, ‖fderiv ℝ f y‖ ≤ M₁)
    (x : Vec 3) :
    div (heatFlow ν t f) x = ∫ y, heatKernel ν t (x - y) * div f y := by sorry
end NavierStokes

Source

The heat semigroup commutes with the divergence and hence preserves divergence-free fields; standard (e.g. Kato, Math. Z. 187 (1984), §1: e^{tΔ} commutes with P and with derivatives). Mission context: Prove2Me mission 'Formalize Navier-Stokes', child NavierStokes.exists_mildSolutionOn_Ico (divergence-free field of the mild solution).

View graph

Divergence of the heat flow: div⁡(eνtΔf)=Kt∗div⁡f\operatorname{div}(e^{\nu t\Delta}f) = K_t * \operatorname{div} fdiv(eνtΔf)=Kt​∗divf

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