Approximate identity: $e^{\nu t\Delta}f(x)\to f(x)$ as $t\to0$

Proved

NavierStokes.tendsto_heatFlow

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

analysisheat-equationnavier-stokespartial-differential-equations

Let $\nu>0$ , let $f:\mathbb R^3\to\mathbb R^3$ be bounded and measurable ( $|f|\le M$ ), and let $f$ be continuous at the point $x$ . Then

\lim_{t\to0}\big(e^{\nu t\Delta}f\big)(x)=f(x).

(For $t\le0$ the heat flow NavierStokes.heatFlow is $f$ itself by convention, so the limit is over a full neighbourhood of $0$ .) This is the approximate-identity property of the Gaussian kernel: writing $e^{\nu t\Delta}f(x)-f(x)=\int K_\nu(t,y)\big(f(x-y)-f(x)\big)dy$ , the part of the integral over $|y|<r$ is at most $\varepsilon/2$ by continuity, while the tail $|y|\ge r$ contributes at most $2M\cdot2\sqrt2\,e^{-r^2/(8\nu t)}\le 2M\cdot2\sqrt2\cdot 8\nu t/r^2$ , which tends to $0$ . It gives the continuity at $t=0$ of the linear part of Kato's mild solution.

Preamble

import Definitions.Def_NavierStokes_Mild
import Mathlib

open MeasureTheory Real
open scoped ENNReal Topology

Formal statement

namespace NavierStokes
theorem tendsto_heatFlow {ν : ℝ} (hν : 0 < ν) {f : Vec 3 → Vec 3} (hf : AEStronglyMeasurable f volume)
    {M : ℝ} (hM : ∀ y, ‖f y‖ ≤ M) {x : Vec 3} (hfx : ContinuousAt f x) :
    Filter.Tendsto (fun t => heatFlow ν t f x) (𝓝 0) (𝓝 (f x)) := by sorry
end NavierStokes

Source

Approximate-identity property of the heat kernel; e.g. L. C. Evans, Partial Differential Equations, 2nd ed., AMS GSM 19 (2010), §2.3.1, Theorem 1(iii) (u(x,t) → g(x⁰) as (x,t) → (x⁰,0)). Mission context: Prove2Me mission 'Formalize Navier-Stokes', children NavierStokes.exists_mildSolutionOn_Ico and isSolutionOn_of_isMildSolutionOn (continuity of the linear part at t = 0).

View graph

Approximate identity: eνtΔf(x)→f(x)e^{\nu t\Delta}f(x)\to f(x)eνtΔf(x)→f(x) as t→0t\to0t→0

Approximate identity: $e^{\nu t\Delta}f(x)\to f(x)$ as $t\to0$