Gradient estimate for the heat flow: $\|\nabla e^{\nu t\Delta}f\|_2^2 \le \frac{24}{\nu t}\|f\|_2^2$

Proved

NavierStokes.lintegral_gradNormSq_heatFlow_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 measurable. Then the Jacobian of the heat flow $u=e^{\nu t\Delta}f$ satisfies the smoothing estimate

\int_{\mathbb R^3}|\nabla u(x)|^2\,dx \;\le\; \frac{24}{\nu t}\int_{\mathbb R^3}|f(x)|^2\,dx ,

where $|\nabla u|^2=\sum_{i,j}(\partial_ju_i)^2$ is NavierStokes.gradNormSq and both sides are lower Lebesgue integrals in $[0,\infty]$ (trivially true if $f\notin L^2$ ). In semigroup language this is $\|\nabla e^{\nu t\Delta}\|_{L^2\to L^2}\le C(\nu t)^{-1/2}$ , the basic parabolic smoothing estimate used in Kato's contraction argument (Kato 1984, §2). The proof: $\partial_j u = (\partial_jK)*f$ (differentiation under the integral, justified by Gaussian domination), the pointwise Jensen inequality $|g*f|^2\le\|g\|_1\,(|g|*|f|^2)$ , Tonelli, and the bound $\|\partial_jK_\nu(t)\|_{L^1}\le 2\sqrt2\,(\nu t)^{-1/2}$ obtained from $r e^{-r^2/(4a)}\le 2\sqrt a\,e^{-r^2/(8a)}$ and the Gaussian integral. The constant $24 = 3\cdot(2\sqrt2)^2$ is not optimal. Formalization note. gradNormSq is built from Mathlib's fderiv, which is $0$ where a function is not differentiable; the theorem is nevertheless a genuine estimate because $e^{\nu t\Delta}f$ is differentiable for $f\in L^2$ .

Preamble

import Definitions.Def_NavierStokes_Mild
import Mathlib

open MeasureTheory Real

Formal statement

namespace NavierStokes
theorem lintegral_gradNormSq_heatFlow_le {ν t : ℝ} (hν : 0 < ν) (ht : 0 < t) (f : Vec 3 → Vec 3)
    (hf : AEStronglyMeasurable f volume) :
    ∫⁻ x, ENNReal.ofReal (gradNormSq (heatFlow ν t f) x) ≤
      ENNReal.ofReal (24 / (ν * t)) * ∫⁻ 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

Gradient estimate for the heat flow: ∥∇eνtΔf∥22≤24νt∥f∥22\|\nabla e^{\nu t\Delta}f\|_2^2 \le \frac{24}{\nu t}\|f\|_2^2∥∇eνtΔf∥22​≤νt24​∥f∥22​

Gradient estimate for the heat flow: $\|\nabla e^{\nu t\Delta}f\|_2^2 \le \frac{24}{\nu t}\|f\|_2^2$