Prove2Me

H1H^1-seminorm contraction of the heat flow: ∥∇eνtΔf∥2≤∥∇f∥2\|\nabla e^{\nu t\Delta}f\|_2 \le \|\nabla f\|_2

Proved
NavierStokes.lintegral_gradNormSq_heatFlow_le_self

by korbonits · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisheat-equationnavier-stokespartial-differential-equations

Let ν>0\nu>0, t>0t>0, and let f:R3→R3f:\mathbb R^3\to\mathbb R^3 be differentiable with ff and DfDf bounded. Then

∫R3∣∇(eνtΔf)∣2 dx≤∫R3∣∇f∣2 dx,\int_{\mathbb R^3}\big|\nabla(e^{\nu t\Delta}f)\big|^2\,dx\le\int_{\mathbb R^3}|\nabla f|^2\,dx,

where ∣∇g∣2=∑i,j(∂jgi)2|\nabla g|^2=\sum_{i,j}(\partial_jg_i)^2 is NavierStokes.gradNormSq and both sides are lower Lebesgue integrals in [0,∞][0,\infty] (the statement is trivially true when ∇f∉L2\nabla f\notin L^2). Together with the L2L^2 contraction lintegral_heatFlow_sq_le this says the heat semigroup is a contraction for the H1H^1 norm. It follows from the commutation ∂jeνtΔf=eνtΔ∂jf\partial_j e^{\nu t\Delta}f=e^{\nu t\Delta}\partial_jf and the L2L^2 contraction applied to each partial derivative.

Preamble
import Definitions.Def_NavierStokes_Mild
import Mathlib

open MeasureTheory Real
open scoped ENNReal
Formal statement
namespace NavierStokes
theorem lintegral_gradNormSq_heatFlow_le_self {ν 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, ENNReal.ofReal (gradNormSq (heatFlow ν t f) x) ≤ ∫⁻ x, ENNReal.ofReal (gradNormSq f x) := by sorry
end NavierStokes
Source
Standard heat-semigroup facts; e.g. L. C. Evans, Partial Differential Equations, 2nd ed., §2.3.1 (convolution structure of the solution) and T. Kato, Math. Z. 187 (1984), §2 (semigroup estimates in H^s). Mission context: Prove2Me mission 'Formalize Navier-Stokes', child NavierStokes.exists_mildSolutionOn_Ico.

View graph