The heat flow preserves divergence-free fields

Proved

NavierStokes.div_heatFlow_eq_zero

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 a differentiable vector field with $f$ and $Df$ bounded. If $\operatorname{div}f\equiv0$ , then $\operatorname{div}\big(e^{\nu t\Delta}f\big)\equiv0$ : the heat semigroup maps divergence-free fields to divergence-free fields. This is used to show that the Duhamel term of Kato's mild solution stays divergence-free. It is an immediate consequence of $\operatorname{div}(e^{\nu t\Delta}f)=e^{\nu t\Delta}(\operatorname{div}f)$ (div_heatFlow).

Preamble

import Definitions.Def_NavierStokes_Mild
import Mathlib

open MeasureTheory Real
open scoped ENNReal

Formal statement

namespace NavierStokes
theorem div_heatFlow_eq_zero {ν 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₁)
    (hdiv : ∀ y, div f y = 0) (x : Vec 3) : div (heatFlow ν t f) x = 0 := 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