Maximum principle for the heat flow: $\|e^{\nu t\Delta}f\|_\infty \le \|f\|_\infty$

Proved

NavierStokes.norm_heatFlow_le

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 any vector field bounded pointwise by $M$ , i.e. $|f(y)|\le M$ for all $y$ . Then for every time $t$ and point $x$ the heat flow (NavierStokes.heatFlow) satisfies

\big|(e^{\nu t\Delta}f)(x)\big| \le M .

For $t>0$ this is because $e^{\nu t\Delta}f$ is the convolution of $f$ with the positive, unit-mass kernel $K_\nu(t,\cdot)$ (so $|K*f|\le K*|f|\le M$ ); for $t\le0$ the heat flow is $f$ itself by convention. No measurability of $f$ is assumed: if the defining integral does not converge, Mathlib's convention makes it $0$ , and the bound holds trivially. This is the $L^\infty$ contraction (maximum principle) for the heat semigroup.

Preamble

import Definitions.Def_NavierStokes_Mild
import Mathlib

open MeasureTheory Real

Formal statement

namespace NavierStokes
theorem norm_heatFlow_le {ν : ℝ} (hν : 0 < ν) (t : ℝ) {f : Vec 3 → Vec 3} {M : ℝ}
    (hM : ∀ y, ‖f y‖ ≤ M) (x : Vec 3) : ‖heatFlow ν t f x‖ ≤ M := by sorry
end NavierStokes

Source

Standard heat-kernel facts on ℝ³; see e.g. L. C. Evans, Partial Differential Equations, 2nd ed., AMS GSM 19 (2010), §2.3.1 (fundamental solution, Lemma p. 46: unit mass) and §2.3.3; for the Kato route: T. Kato, Math. Z. 187 (1984), §2 eq. (2.1)–(2.3) (semigroup estimates ‖∇e^{tΔ}f‖₂ ≤ C t^{-1/2}‖f‖₂). Mission context: Prove2Me mission 'Formalize Navier-Stokes', child NavierStokes.exists_mildSolutionOn_Ico (Kato local existence).

View graph

Maximum principle for the heat flow: ∥eνtΔf∥∞≤∥f∥∞\|e^{\nu t\Delta}f\|_\infty \le \|f\|_\infty∥eνtΔf∥∞​≤∥f∥∞​

Maximum principle for the heat flow: $\|e^{\nu t\Delta}f\|_\infty \le \|f\|_\infty$