$L^2$ contraction of the heat flow: $\|e^{\nu t\Delta}f\|_2 \le \|f\|_2$

Proved

NavierStokes.lintegral_heatFlow_sq_le

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 (almost everywhere strongly) measurable. Then

\int_{\mathbb R^3}\big|(e^{\nu t\Delta}f)(x)\big|^2\,dx \;\le\; \int_{\mathbb R^3}|f(x)|^2\,dx ,

where both sides are lower Lebesgue integrals in $[0,\infty]$ (so the statement is meaningful, and trivially true, when $f\notin L^2$ ). This is the $L^2$ contraction property of the heat semigroup, i.e. Young's inequality $\|K*f\|_2\le\|K\|_1\|f\|_2$ for the unit-mass kernel $K_\nu(t,\cdot)$ . The natural proof is Jensen's (Cauchy–Schwarz) inequality $|K*f|^2\le K*|f|^2$ pointwise, followed by Tonelli and translation invariance of Lebesgue measure. It is the first of the Kato semigroup estimates and is used for the fixed-point step of the mild local-existence theorem.

Preamble

import Definitions.Def_NavierStokes_Mild
import Mathlib

open MeasureTheory Real

Formal statement

namespace NavierStokes
theorem lintegral_heatFlow_sq_le {ν t : ℝ} (hν : 0 < ν) (ht : 0 < t) (f : Vec 3 → Vec 3)
    (hf : AEStronglyMeasurable f volume) :
    ∫⁻ x, ‖heatFlow ν t f x‖ₑ ^ 2 ≤ ∫⁻ x, ‖f x‖ₑ ^ 2 := 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

L2L^2L2 contraction of the heat flow: ∥eνtΔf∥2≤∥f∥2\|e^{\nu t\Delta}f\|_2 \le \|f\|_2∥eνtΔf∥2​≤∥f∥2​

$L^2$ contraction of the heat flow: $\|e^{\nu t\Delta}f\|_2 \le \|f\|_2$