Navier–Stokes on $\mathbb{R}^3$ : heat flow, Newton potential, Leray projection and mild solutions

Definition

NavierStokes_Mild

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

analysisfluid-dynamicsnavier-stokespartial-differential-equations

Mild solutions of the three-dimensional Navier–Stokes equations. This bundle introduces the objects of the classical Kato–Fujita route to Fefferman's statements: one first solves the integral (Duhamel) form of the equations by a fixed-point argument, then shows that the resulting mild solution is a genuine classical solution in the sense of NavierStokes.IsSolutionOn.

Throughout, Vec 3 = ℝ³, all integrals are Lebesgue/Bochner integrals for Lebesgue measure, and the definitions NavierStokes.div, NavierStokes.IsInitialData, NavierStokes.IsSolutionOn are those of the mission's base bundle NavierStokes.

Heat kernel and heat flow. heatKernel ν t x = (4πνt)^{-3/2} e^{-|x|^2/(4νt)} is the fundamental solution of $\partial_t - \nu\Delta$ on $\mathbb R^3$ , and heatFlow ν t f is the semigroup $e^{\nu t\Delta}$ applied componentwise,

(e^{\nu t\Delta} f)(x) = \int_{\mathbb R^3} K_\nu(t, x-y)\, f(y)\, dy \quad (t>0),

with the convention heatFlow ν t f = f for $t \le 0$ .

Newton potential. newton g x = (4π)^{-1} ∫ g(y)/|x−y| dy is $(-\Delta)^{-1} g$ on $\mathbb R^3$ .
Convective term. advect u x = Du(x)\,u(x) is $(u\cdot\nabla)u = \sum_j u_j \partial_j u$ .
Leray–Helmholtz projection. leray v = v + ∇ N(div v), i.e. $P v = v - \nabla\Delta^{-1}\operatorname{div} v$ , the $L^2$ -orthogonal projection onto divergence-free fields.
Pressure. pressureOf u t = N(div((u(t)·∇)u(t))), i.e. $p = (-\Delta)^{-1}\partial_i\partial_j(u_iu_j)$ , so that $(u\cdot\nabla)u - P\big((u\cdot\nabla)u\big) = \nabla p$ ; this is the pressure determined by the velocity in Leray's and Kato's constructions.
IsMildSolutionOn ν u₀ u S. A velocity field $u$ is a (smooth, $H^\infty$ -valued) mild solution on the time set $S$ ( $[0,T)$ or $[0,\infty)$ ) when: $u(0)=u_0$ ; $(t,x)\mapsto u(x,t)$ is $C^\infty$ on $S\times\mathbb R^3$ ; $\operatorname{div}u(t)=0$ for $t\in S$ ; the kinetic energy $\int|u(x,t)|^2dx$ is bounded uniformly on $S$ ; for every $k$ the $L^2$ norm of the $k$ -th spatial derivative $\|D^k u(t)\|_{L^2}$ is bounded uniformly on every bounded piece $S\cap(-\infty,T]$ ; the Duhamel integrand $s\mapsto e^{\nu(t-s)\Delta}P\big((u(s)\cdot\nabla)u(s)\big)(x)$ is integrable on $(0,t)$ ; and Kato's integral equation

u(t) = e^{\nu t\Delta}u_0 - \int_0^t e^{\nu(t-s)\Delta}\,P\big((u(s)\cdot\nabla)u(s)\big)\,ds

holds pointwise for every $t\in S$ , $t>0$ .

The integrability field is recorded explicitly because Mathlib's Bochner integral of a non-integrable function is $0$ ; without it the Duhamel equation could be satisfied vacuously.

Definition code

import Definitions.Def_NavierStokes
import Mathlib

/-!
Mild (Kato–Fujita) formulation of the Navier–Stokes equations on `ℝ³`, as the intermediate
object in the classical route to Fefferman's statements: first produce a *mild* solution by a
fixed-point argument for the Duhamel integral equation, then upgrade it to a physically
reasonable (classical) solution `NavierStokes.IsSolutionOn`.

References.  T. Kato, *Strong Lᵖ-solutions of the Navier–Stokes equation in ℝᵐ, with
applications to weak solutions*, Math. Z. 187 (1984), 471–480, eq. (1.3)–(1.5) (the integral
equation `u(t) = e^{tΔ}u₀ − ∫₀ᵗ e^{(t−s)Δ} P (u·∇)u (s) ds`); H. Fujita and T. Kato, *On the
Navier–Stokes initial value problem I*, Arch. Rational Mech. Anal. 16 (1964), 269–315.
J. Leray, *Sur le mouvement d'un liquide visqueux emplissant l'espace*, Acta Math. 63 (1934),
193–248, §§14–16 (pressure via the Newton potential, energy bound).

Conventions.  `Vec 3 = ℝ³`.  All integrals are Lebesgue/Bochner integrals with respect to the
Lebesgue measure; a Bochner integral of a non-integrable function is `0` by Mathlib's convention,
which is why `IsMildSolutionOn` records the integrability of the Duhamel integrand explicitly.
-/

namespace NavierStokes

open scoped ContDiff Gradient
open MeasureTheory Real

/-- The heat kernel of `∂ₜ − ν Δ` on `ℝ³` at time `t`:
`K_ν(t, x) = (4 π ν t)^{-3/2} exp(−|x|² / (4 ν t))`. -/
noncomputable def heatKernel (ν t : ℝ) (x : Vec 3) : ℝ :=
  (4 * π * ν * t) ^ (-(3 : ℝ) / 2) * Real.exp (-‖x‖ ^ 2 / (4 * ν * t))

/-- The heat semigroup `e^{ν t Δ}` applied componentwise to a vector field `f : ℝ³ → ℝ³`:
`(e^{ν t Δ} f)(x) = ∫ K_ν(t, x − y) f(y) dy` for `t > 0`, and `f` itself for `t ≤ 0`. -/
noncomputable def heatFlow (ν t : ℝ) (f : Vec 3 → Vec 3) (x : Vec 3) : Vec 3 :=
  if 0 < t then ∫ y, heatKernel ν t (x - y) • f y else f x

/-- The Newton potential `N g = (−Δ)⁻¹ g` on `ℝ³`: `(N g)(x) = (4π)⁻¹ ∫ g(y) / |x − y| dy`. -/
noncomputable def newton (g : Vec 3 → ℝ) (x : Vec 3) : ℝ :=
  (4 * π)⁻¹ * ∫ y, g y / ‖x - y‖

/-- The convective term `(u · ∇) u = ∑ⱼ uⱼ ∂u/∂xⱼ`, i.e. the derivative of `u` at `x` in the
direction `u x`. -/
noncomputable def advect (u : Vec 3 → Vec 3) (x : Vec 3) : Vec 3 :=
  fderiv ℝ u x (u x)

/-- The Leray–Helmholtz projection onto divergence-free fields,
`P v = v − ∇ Δ⁻¹ (div v) = v + ∇ N (div v)`, with `N` the Newton potential. -/
noncomputable def leray (v : Vec 3 → Vec 3) (x : Vec 3) : Vec 3 :=
  v x + ∇ (newton (div v)) x

/-- The pressure determined by a velocity field through the Leray projection:
`p(t) = N (div ((u(t) · ∇) u(t))) = (−Δ)⁻¹ ∂ᵢ∂ⱼ (uᵢ uⱼ)`, so that
`(u · ∇) u − P ((u · ∇) u) = ∇ p`. -/
noncomputable def pressureOf (u : ℝ → Vec 3 → Vec 3) (t : ℝ) : Vec 3 → ℝ :=
  newton (div (advect (u t)))

/-- `u` is a (smooth, `H^∞`-valued) **mild solution** of the Navier–Stokes equations with
viscosity `ν` and initial datum `u₀` on the set `S ⊆ ℝ` of times (`S = [0, T)` or `S = [0, ∞)`):

* `initial`: `u(0) = u₀`;
* `smooth`: `(t, x) ↦ u(x, t)` is `C^∞` on `S × ℝ³`;
* `divFree`: `div u(·, t) = 0` for `t ∈ S`;
* `energy`: the kinetic energy `∫ |u(x,t)|² dx` is bounded uniformly on `S`;
* `sobolev`: for every `k`, the `L²` norm of the `k`-th spatial derivative of `u(·, t)` is bounded
  uniformly for `t` in every bounded subinterval `S ∩ (−∞, T]` (so `u(t) ∈ H^k` for all `k`,
  locally uniformly in time);
* `integrable`: the Duhamel integrand `s ↦ e^{ν (t − s) Δ} P ((u · ∇) u)(s) (x)` is integrable on
  `(0, t)`;
* `duhamel`: Kato's integral equation
  `u(t) = e^{ν t Δ} u₀ − ∫₀ᵗ e^{ν (t − s) Δ} P ((u(s) · ∇) u(s)) ds` holds pointwise for
  `t ∈ S`, `t > 0`. -/
structure IsMildSolutionOn (ν : ℝ) (u₀ : Vec 3 → Vec 3) (u : ℝ → Vec 3 → Vec 3) (S : Set ℝ) :
    Prop where
  initial : u 0 = u₀
  smooth : ContDiffOn ℝ ∞ (Function.uncurry u) (S ×ˢ Set.univ)
  divFree : ∀ t ∈ S, ∀ x, div (u t) x = 0
  energy : ∃ C : ℝ, ∀ t ∈ S, ∫⁻ x, ‖u t x‖ₑ ^ 2 ≤ ENNReal.ofReal C
  sobolev : ∀ (k : ℕ) (T : ℝ), ∃ C : ℝ, ∀ t ∈ S ∩ Set.Iic T,
    ∫⁻ x, ‖iteratedFDeriv ℝ k (u t) x‖ₑ ^ 2 ≤ ENNReal.ofReal C
  integrable : ∀ t ∈ S, 0 < t → ∀ x,
    IntegrableOn (fun s => heatFlow ν (t - s) (leray (advect (u s))) x) (Set.Ioo 0 t)
  duhamel : ∀ t ∈ S, 0 < t → ∀ x,
    u t x = heatFlow ν t u₀ x - ∫ s in Set.Ioo 0 t, heatFlow ν (t - s) (leray (advect (u s))) x

end NavierStokes

Source

T. Kato, Strong L^p-solutions of the Navier–Stokes equation in R^m, with applications to weak solutions, Math. Z. 187 (1984) 471–480, https://doi.org/10.1007/BF01174182, §1 eq. (1.3)–(1.5) and Theorem 1 (m = 3); H. Fujita, T. Kato, On the Navier–Stokes initial value problem I, Arch. Rational Mech. Anal. 16 (1964) 269–315, https://doi.org/10.1007/BF00276188, Theorem 4.1. Mission context: C. Fefferman, Existence and smoothness of the Navier–Stokes equation, Clay Mathematics Institute (2000), p. 2, https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf

View graph

Navier–Stokes on R3\mathbb{R}^3R3: heat flow, Newton potential, Leray projection and mild solutions

Navier–Stokes on $\mathbb{R}^3$ : heat flow, Newton potential, Leray projection and mild solutions