A mild solution of Navier–Stokes with the Leray pressure is a physically reasonable solution

Open

NavierStokes.isSolutionOn_of_isMildSolutionOn

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

analysisfluid-dynamicsnavier-stokespartial-differential-equations

Mild solutions are physically reasonable solutions. Let $\nu>0$ , let $u_0$ be admissible initial data in Fefferman's sense (IsInitialData: $C^\infty$ , divergence-free, all derivatives decaying faster than any power), let the time set $S$ be either the half-line $[0,\infty)$ or a half-open interval $[0,T)$ , and let $u$ be a mild solution on $S$ in the sense of IsMildSolutionOn ν u₀ u S. Then the pair $(u, p)$ with the Leray pressure

p(t) = (-\Delta)^{-1}\partial_i\partial_j\big(u_i(t)u_j(t)\big) = N\big(\operatorname{div}((u(t)\cdot\nabla)u(t))\big)

(pressureOf u) is a physically reasonable solution on $S$ in the sense of IsSolutionOn: $u$ and $p$ are jointly $C^\infty$ on $S\times\mathbb R^3$ , the momentum equation $\partial_t u + (u\cdot\nabla)u = \nu\Delta u - \nabla p$ holds for all $t\in S$ , $t>0$ , $u$ is divergence-free, $u(0)=u_0$ , and the energy $\int|u|^2\,dx$ is bounded on $S$ .

This is the "mild $\Rightarrow$ classical" half of the Kato–Fujita theory (Kato 1984, §1 and Theorem 1′; Fujita–Kato 1964, §4). The argument: differentiating the Duhamel formula in $t$ (justified by the locally uniform $H^k$ bounds, which give uniform bounds on $P((u\cdot\nabla)u)$ and its Laplacian) yields $\partial_t u = \nu\Delta u - P((u\cdot\nabla)u)$ ; since $P v = v + \nabla N(\operatorname{div} v)$ , this is the momentum equation with $\nabla p = -\nabla N(\operatorname{div}((u\cdot\nabla)u))$ , i.e. $p=$ pressureOf u t up to the sign convention $(-\Delta)N = \mathrm{id}$ . Joint smoothness of $p$ follows from that of $u$ and the $H^k$ bounds (all derivatives of $(u\cdot\nabla)u$ lie in $L^1\cap L^\infty$ ). The energy bound is the energy field of the mild solution.

The two admissible time sets are exactly the ones needed: the statement serves both the local milestone ( $S=[0,T)$ ) and the small-data global milestone ( $S=[0,\infty)$ ).

Preamble

import Definitions.Def_NavierStokes_Mild
import Mathlib

Formal statement

namespace NavierStokes
theorem isSolutionOn_of_isMildSolutionOn (ν : ℝ) (hν : 0 < ν) (u₀ : Vec 3 → Vec 3)
    (h₀ : IsInitialData u₀) (u : ℝ → Vec 3 → Vec 3) (S : Set ℝ)
    (hS : S = Set.Ici 0 ∨ ∃ T : ℝ, S = Set.Ico 0 T) (hu : IsMildSolutionOn ν u₀ u S) :
    IsSolutionOn ν u₀ u (pressureOf u) S := 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 and Theorem 1' (mild solutions are classical); J. Leray, Acta Math. 63 (1934), §§14–16 (pressure as the Newton potential of ∂ᵢ∂ⱼ(uᵢuⱼ), energy bound). Mission context: C. Fefferman, Clay problem description (2000), pp. 1–2, eqs. (1)–(3), (6), (7).

View graph