Prove2Me

The heat flow commutes with differentiation: ∂veνtΔf=eνtΔ∂vf\partial_v e^{\nu t\Delta} f = e^{\nu t\Delta}\partial_v f

Proved
NavierStokes.fderiv_heatFlow_eq_heatFlow_fderiv

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 its Jacobian DfDf bounded (∣f∣≤M0|f|\le M_0, ∥Df∥≤M1\|Df\|\le M_1). Then for every point x0x_0 and direction vv,

∂v(eνtΔf)(x0)=(eνtΔ ∂vf)(x0),\partial_v\big(e^{\nu t\Delta}f\big)(x_0) = \big(e^{\nu t\Delta}\,\partial_v f\big)(x_0),

i.e. the heat semigroup commutes with directional derivatives (equivalently, ∇(K∗f)=K∗∇f\nabla(K*f)=K*\nabla f). The proof writes eνtΔf(x)=∫K(y)f(x−y) dye^{\nu t\Delta}f(x)=\int K(y)f(x-y)\,dy and differentiates under the integral sign, the bound K(y)M1K(y)M_1 providing the domination. This is the lemma that transfers L2L^2 estimates for the heat flow to H1H^1 estimates in Kato's fixed-point argument.

Preamble
import Definitions.Def_NavierStokes_Mild
import Mathlib

open MeasureTheory Real
open scoped ENNReal
Formal statement
namespace NavierStokes
theorem fderiv_heatFlow_eq_heatFlow_fderiv {ν 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₀ v : Vec 3) :
    fderiv ℝ (heatFlow ν t f) x₀ v = heatFlow ν t (fun y => fderiv ℝ f y v) 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