The Duhamel formula yields the Navier–Stokes momentum equation

Open

NavierStokes.momentum_pressureOf_of_isMildSolutionOn

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

analysisfluid-dynamicsnavier-stokespartial-differential-equations

Let $\nu>0$ and let $u$ be a mild Navier–Stokes solution on a time set $S$ equal either to $[0,\infty)$ or to $[0,T)$ . With the pressure

p(t)=(-\Delta)^{-1}\operatorname{div}((u(t)\cdot\nabla)u(t)),

the velocity and pressure satisfy, for every $t\in S$ with $t>0$ and every $x\in\mathbb R^3$ ,

\partial_tu+(u\cdot\nabla)u=\nu\Delta u-\nabla p.

This is the differential momentum identity needed to upgrade the Kato–Fujita Duhamel formulation to a classical Navier–Stokes solution.

Preamble

import Definitions.Def_NavierStokes_Mild
import Mathlib
open scoped ContDiff Gradient
open Laplacian MeasureTheory

Formal statement

namespace NavierStokes
theorem momentum_pressureOf_of_isMildSolutionOn (ν : ℝ) (hν : 0 < ν)
    (u₀ : Vec 3 → Vec 3) (u : ℝ → Vec 3 → Vec 3) (S : Set ℝ)
    (hS : S = Set.Ici 0 ∨ ∃ T : ℝ, S = Set.Ico 0 T)
    (hu : IsMildSolutionOn ν u₀ u S) :
    ∀ t ∈ S, 0 < t → ∀ x,
      deriv (fun s => u s x) t + fderiv ℝ (u t) x (u t x) =
        ν • Δ (u t) x - ∇ (pressureOf u t) x := by sorry
end NavierStokes

Source

T. Kato, Strong L^p-solutions of the Navier–Stokes equation in R^m, Math. Z. 187 (1984), 471–480, https://doi.org/10.1007/BF01174182, §1, equations (1.3)–(1.5), and Theorem 1 prime; H. Fujita and T. Kato, Arch. Rational Mech. Anal. 16 (1964), 269–315, §4. Exact formal context: Prove2Me definition NavierStokes_Mild, theorem id 22ac75d3-ebba-403c-ad68-a493ac2dd884.

View graph