The incompressible Navier–Stokes equations on $\mathbb{R}^n$ : admissible data and physically reasonable solutions (Fefferman (1)–(4), (6), (7))

Definition

NavierStokes

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

analysisfluid-dynamicsmillennium-prizenavier-stokespartial-differential-equations

This bundle fixes, in the namespace NavierStokes, the objects of Charles Fefferman's official description of the Clay Millennium Prize Problem on the Navier–Stokes equations: the equations (1)–(3) with zero external force, the class (4) of admissible initial data, and the notion (6)–(7) of a physically reasonable solution. The dimension $n$ is a parameter throughout; the goal of the mission uses $n = 3$ and one milestone uses $n = 2$ .

Ambient objects. Vec n is Euclidean space $\mathbb{R}^n$ with its Euclidean norm $|x|$ and Lebesgue measure, and e i is the $i$ -th standard unit vector $e_i$ . A velocity field is a function $u$ of a time $t \in \mathbb{R}$ and a point $x \in \mathbb{R}^n$ with values in $\mathbb{R}^n$ ; in Lean, $u\,t$ is the field at time $t$ and $u\,t\,x$ is Fefferman's $u(x,t)$ . A pressure $p(x,t)$ is real-valued.

Differential operators. For a vector field $v : \mathbb{R}^n \to \mathbb{R}^n$ , $\operatorname{div} v\,(x) = \sum_{i=1}^{n} \frac{\partial v_i}{\partial x_i}(x) \qquad\text{(`div`, Fefferman (2))},$ computed as $\sum_i \big(Dv(x)\,e_i\big)_i$ from the Fréchet derivative $Dv(x)$ , and $|\nabla v|^2(x) = \sum_{i,j=1}^{n} \Big(\frac{\partial v_i}{\partial x_j}(x)\Big)^2 = \sum_{j}\|Dv(x)\,e_j\|^2 \qquad\text{(`gradNormSq`)}.$ The Laplacian $\Delta$ and the gradient $\nabla$ used below are Mathlib's: $\Delta v(x) = \sum_i D^2 v(x)[e_i,e_i]$ acts componentwise, and $\nabla p(x)$ is the vector representing $Dp(x)$ through the inner product.

Admissible initial data (IsInitialData u₀, Fefferman's condition (4)). A vector field $u^0 : \mathbb{R}^n \to \mathbb{R}^n$ is admissible when

$u^0$ is $C^\infty$ ;
$\operatorname{div} u^0 = 0$ everywhere;
$u^0$ and all its derivatives decay faster than any power: for all $k, K \in \mathbb{N}$ there is a constant $C_{kK}$ with

(1+|x|)^{K}\,\|D^k u^0(x)\| \le C_{kK} \quad \text{for all } x \in \mathbb{R}^n .

Fefferman writes the third condition as $|\partial_x^\alpha u^0(x)| \le C_{\alpha K}(1+|x|)^{-K}$ for every multi-index $\alpha$ and every $K$ ; bounding all partial derivatives of order $k$ is equivalent to bounding the operator norm of the $k$ -th Fréchet derivative, so the two families of conditions coincide. Admissible data are exactly the divergence-free Schwartz functions.

Physically reasonable solutions (IsSolutionOn ν u₀ u p S, and IsSolution ν u₀ u p for $S = [0,\infty)$ ). Given a viscosity $\nu$ , an initial datum $u^0$ and a set of times $S \subseteq \mathbb{R}$ (in this mission $S = [0,\infty)$ or $S = [0,T)$ ), the pair $(u,p)$ is a physically reasonable solution on $S$ when

(Fefferman (6)) $(t,x) \mapsto u(x,t)$ and $(t,x) \mapsto p(x,t)$ are $C^\infty$ on $S \times \mathbb{R}^n$ , including one-sided smoothness at the boundary of $S$ ;
(Fefferman (1), $f \equiv 0$ ) for every $t \in S$ with $t > 0$ and every $x \in \mathbb{R}^n$ ,

\frac{\partial u}{\partial t}(x,t) + \sum_{j=1}^{n} u_j(x,t)\,\frac{\partial u}{\partial x_j}(x,t) = \nu\,\Delta u(x,t) - \nabla p(x,t),

where the convective term is the derivative of $u(\cdot,t)$ at $x$ in the direction $u(x,t)$ ; 3. (Fefferman (2)) $\operatorname{div} u(\cdot,t) = 0$ for every $t \in S$ ; 4. (Fefferman (3)) $u(\cdot,0) = u^0$ ; 5. (Fefferman (7), bounded energy) there is a constant $C$ with $\int_{\mathbb{R}^n} |u(x,t)|^2\,dx < C$ for all $t \in S$ .

These are the data in terms of which Fefferman's statement (A) and the classical partial results (local existence, small-data global existence, the two-dimensional case) are stated.

Formalization Note Fefferman imposes equation (1) for $t \ge 0$ ; here it is imposed at the interior times $t > 0$ with two-sided derivatives, while smoothness up to $t = 0$ is Mathlib's ContDiffOn on the closed half-space, so the equation at $t = 0$ follows by continuity. The energy integral is a Lebesgue integral with values in $[0,\infty]$ (∫⁻), which equals $\infty$ when $u(\cdot,t) \notin L^2$ , so condition 5 cannot hold vacuously. No sign condition on $\nu$ and no admissibility of $u^0$ are built into IsSolutionOn; they are hypotheses of the theorems. Values of $u$ and $p$ at times outside $S$ are unconstrained.

Definition code

import Mathlib

/-!
C. L. Fefferman, *Existence and smoothness of the Navier–Stokes equation*, Clay Mathematics
Institute Millennium Prize Problem description (2000), pp. 1–2.

The objects of equations (1)–(4), (6), (7): the unknown velocity `u(x,t) ∈ ℝⁿ` and pressure
`p(x,t) ∈ ℝ` for `x ∈ ℝⁿ`, `t ≥ 0`; the divergence; the admissible initial data `u⁰`; and the
notion of a "physically reasonable" solution (smooth, with bounded energy).  The external force
`f` is identically zero throughout, as in statement (A).

Conventions.  `Vec n` is `ℝⁿ` with its Euclidean norm.  A time-dependent vector field is a
function `u : ℝ → Vec n → Vec n`, so `u t` is the velocity field at time `t` and `u t x` is
Fefferman's `u(x,t)`.  The Laplacian `Δ` is Mathlib's Laplacian on real inner product spaces
(the sum of the second derivatives along an orthonormal basis, applied componentwise), and
`∇` is Mathlib's gradient.
-/

namespace NavierStokes

open scoped ContDiff InnerProductSpace Gradient
open Laplacian MeasureTheory

/-- Euclidean space `ℝⁿ`. -/
abbrev Vec (n : ℕ) := EuclideanSpace ℝ (Fin n)

/-- The `i`-th standard unit vector `e_i` of `ℝⁿ`. -/
noncomputable def e {n : ℕ} (i : Fin n) : Vec n := EuclideanSpace.single i 1

/-- Fefferman (2): the divergence `div v = ∑ᵢ ∂vᵢ/∂xᵢ` of a vector field `v : ℝⁿ → ℝⁿ`,
computed from the Fréchet derivative: `∂vᵢ/∂xᵢ (x) = (Dv(x) e_i)_i`. -/
noncomputable def div {n : ℕ} (v : Vec n → Vec n) (x : Vec n) : ℝ :=
  ∑ i, fderiv ℝ v x (e i) i

/-- `|∇v|² = ∑ᵢ ∑ⱼ (∂vᵢ/∂xⱼ)²`, the squared Frobenius norm of the Jacobian of `v` at `x`,
written as `∑ⱼ ‖Dv(x) e_j‖²`. -/
noncomputable def gradNormSq {n : ℕ} (v : Vec n → Vec n) (x : Vec n) : ℝ :=
  ∑ j, ‖fderiv ℝ v x (e j)‖ ^ 2

/-- Fefferman's admissible initial data: `u⁰` is a `C^∞` divergence-free vector field on `ℝⁿ`
satisfying the decay condition (4):
`|∂ₓ^α u⁰(x)| ≤ C_{αK} (1 + |x|)^{-K}` on `ℝⁿ`, for any `α` and `K`.
The multi-index bound is recorded through the norm of the `k`-th Fréchet derivative,
in the equivalent form `(1 + |x|)^K ‖D^k u⁰(x)‖ ≤ C_{kK}`. -/
structure IsInitialData {n : ℕ} (u₀ : Vec n → Vec n) : Prop where
  smooth : ContDiff ℝ ∞ u₀
  divFree : ∀ x, div u₀ x = 0
  decay : ∀ k K : ℕ, ∃ C : ℝ, ∀ x, (1 + ‖x‖) ^ K * ‖iteratedFDeriv ℝ k u₀ x‖ ≤ C

/-- `(u, p)` is a physically reasonable solution of the Navier–Stokes equations with viscosity
`ν`, zero external force and initial datum `u₀`, on the set `S ⊆ ℝ` of times (`S = [0, ∞)` or
`S = [0, T)`).  The fields are:

* `smooth_u`, `smooth_p`: Fefferman (6), `p, u ∈ C^∞(ℝⁿ × S)`, i.e. the maps
  `(t, x) ↦ u(x,t)` and `(t, x) ↦ p(x,t)` are `C^∞` on `S × ℝⁿ` (up to the boundary of `S`);
* `momentum`: Fefferman (1) with `f ≡ 0`, at every time `t ∈ S` with `t > 0` and every `x`:
  `∂u/∂t + ∑ⱼ uⱼ ∂u/∂xⱼ = ν Δu − ∇p`, where `∑ⱼ uⱼ ∂u/∂xⱼ` is the derivative of `u(·,t)` at
  `x` in the direction `u(x,t)`;
* `divFree`: Fefferman (2), `div u(·,t) = 0` for every `t ∈ S`;
* `initial`: Fefferman (3), `u(x,0) = u⁰(x)`;
* `boundedEnergy`: Fefferman (7), `∫_{ℝⁿ} |u(x,t)|² dx < C` for all `t ∈ S`, with the
  integral taken as a Lebesgue integral in `[0, ∞]` (so it is `∞` when `u(·,t) ∉ L²`). -/
structure IsSolutionOn {n : ℕ} (ν : ℝ) (u₀ : Vec n → Vec n)
    (u : ℝ → Vec n → Vec n) (p : ℝ → Vec n → ℝ) (S : Set ℝ) : Prop where
  smooth_u : ContDiffOn ℝ ∞ (Function.uncurry u) (S ×ˢ Set.univ)
  smooth_p : ContDiffOn ℝ ∞ (Function.uncurry p) (S ×ˢ Set.univ)
  momentum : ∀ t ∈ S, 0 < t → ∀ x,
    deriv (fun s => u s x) t + fderiv ℝ (u t) x (u t x) = ν • Δ (u t) x - ∇ (p t) x
  divFree : ∀ t ∈ S, ∀ x, div (u t) x = 0
  initial : u 0 = u₀
  boundedEnergy : ∃ C : ℝ, ∀ t ∈ S, ∫⁻ x, ‖u t x‖ₑ ^ 2 < ENNReal.ofReal C

/-- `(u, p)` is a physically reasonable solution on `ℝⁿ × [0, ∞)`: Fefferman's (1), (2), (3),
(6), (7) with `f ≡ 0`. -/
def IsSolution {n : ℕ} (ν : ℝ) (u₀ : Vec n → Vec n)
    (u : ℝ → Vec n → Vec n) (p : ℝ → Vec n → ℝ) : Prop :=
  IsSolutionOn ν u₀ u p (Set.Ici 0)

end NavierStokes

Source

C. L. Fefferman, Existence and smoothness of the Navier–Stokes equation, Clay Mathematics Institute Millennium Prize Problem description (2000), https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf, p. 1, equations (1)–(4), (6), (7) and the surrounding text (definition of the unknowns u, p, of ν, of Δ, of div, and of 'physically reasonable' solutions); p. 2, statement (A) fixes f ≡ 0

Read-back

What the Lean code literally says, in plain math · claude-fable-5-1

Read-back

Throughout, $n$ is a natural number (any $n \ge 0$ , including $n = 0$ ) that is an implicit argument to every declaration below; nothing anywhere in the bundle requires $n \ge 1$ or $n = 3$ .

`Vec n`

$\mathrm{Vec}_n$ is literally Mathlib's EuclideanSpace ℝ (Fin n): the real vector space $\mathbb{R}^n$ of functions $\{0,\dots,n-1\} \to \mathbb{R}$ , carrying the Euclidean ( $\ell^2$ ) inner product $\langle x, y\rangle = \sum_i x_i y_i$ , the Euclidean norm $\|x\| = \big(\sum_i x_i^2\big)^{1/2}$ , and the standard Lebesgue measure as its default measure (the product of $n$ copies of Lebesgue measure on $\mathbb{R}$ ; the unit cube has measure $1$ ). Because this is an abbreviation rather than a new type, every Mathlib fact and instance about EuclideanSpace applies verbatim. Edge case: for $n = 0$ , $\mathrm{Vec}_0$ is a one-point space $\{0\}$ , and its default measure gives that single point mass $1$ (the empty product).

`e i`

For $i \in \{0,\dots,n-1\}$ (a Fin n index), $e_i \in \mathrm{Vec}_n$ is the vector with $1$ in coordinate $i$ and $0$ elsewhere, i.e. the $i$ -th standard basis vector, $\|e_i\| = 1$ . Edge case: when $n = 0$ there is no admissible $i$ , so no such vector exists (sums over $i$ below are then empty).

`div v x`

For any function $v : \mathrm{Vec}_n \to \mathrm{Vec}_n$ (no regularity assumed) and any point $x \in \mathrm{Vec}_n$ , the real number

\operatorname{div} v\,(x) \;=\; \sum_{i=0}^{n-1} \big[\,Dv(x)\,e_i\,\big]_i ,

where $Dv(x)$ is Mathlib's Fréchet derivative of $v$ at $x$ (a continuous linear map $\mathrm{Vec}_n \to \mathrm{Vec}_n$ ), $Dv(x)\,e_i$ is that linear map applied to the basis vector $e_i$ (the $i$ -th partial derivative vector $\partial_i v(x)$ ), and $[\cdot]_i$ takes its $i$ -th coordinate. When $v$ is differentiable at $x$ this is $\sum_i \partial_i v_i(x)$ , the ordinary divergence. Edge cases: Mathlib's fderiv is a total function — if $v$ is not differentiable at $x$ , $Dv(x)$ is the zero map and $\operatorname{div} v\,(x) = 0$ ; for $n = 0$ the sum is empty and $\operatorname{div} v\,(x) = 0$ always.

`gradNormSq v x`

For any $v : \mathrm{Vec}_n \to \mathrm{Vec}_n$ and $x \in \mathrm{Vec}_n$ , the real number

\operatorname{gradNormSq} v\,(x) \;=\; \sum_{j=0}^{n-1} \big\|\,Dv(x)\,e_j\,\big\|^2 ,

the sum over basis directions $e_j$ of the squared Euclidean norm of the directional derivative $\partial_j v(x) \in \mathrm{Vec}_n$ ; when $v$ is differentiable at $x$ this equals $\sum_{i,j} (\partial_j v_i(x))^2$ , the squared Frobenius norm of the Jacobian matrix. Edge cases: if $v$ is not differentiable at $x$ , fderiv returns the zero map and the value is $0$ ; for $n = 0$ the value is $0$ . This definition is not referenced by any other declaration in the bundle.

`IsInitialData u₀`

For a function $u_0 : \mathrm{Vec}_n \to \mathrm{Vec}_n$ , the proposition " $u_0$ is initial data" is the conjunction of exactly three conditions:

smooth: $u_0$ is $C^\infty$ on all of $\mathrm{Vec}_n$ in Mathlib's sense of ContDiff ℝ ∞. Here ∞ (under the ContDiff scoped notation) is the element $\top$ of $\mathbb{N}_\infty$ viewed inside WithTop ℕ∞; it means "continuously differentiable of every finite order $k \in \mathbb{N}$ ", and is strictly weaker than the symbol ω, which would mean real-analytic. No analyticity is asserted.
divFree: for every $x \in \mathrm{Vec}_n$ , $\operatorname{div} u_0\,(x) = 0$ , with $\operatorname{div}$ as defined above (given condition 1, this is the genuine divergence $\sum_i \partial_i (u_0)_i (x) = 0$ ). For $n = 0$ this holds automatically.
decay: for every pair of natural numbers $k, K \in \mathbb{N}$ there exists a real constant $C$ (allowed to depend on $k$ and $K$ , but not on $x$ ) such that for every $x \in \mathrm{Vec}_n$ ,

(1 + \|x\|)^K \,\big\|\, D^k u_0 (x) \,\big\| \;\le\; C ,

where $D^k u_0(x)$ is Mathlib's $k$ -th iterated Fréchet derivative at $x$ — a continuous $k$ -linear map $(\mathrm{Vec}_n)^k \to \mathrm{Vec}_n$ — and $\|\cdot\|$ is its operator norm. For $k = 0$ , $\|D^0 u_0(x)\| = \|u_0(x)\|$ , so the case $k=0$ says $u_0$ itself is bounded by $C (1+\|x\|)^{-K}$ for every $K$ ; $K = 0$ says every derivative is bounded. The inequality is $\le$ , not $<$ ; $C$ is only required to be real (since the left side is $\ge 0$ and $\mathrm{Vec}_n$ is non-empty, any witnessing $C$ is automatically $\ge 0$ ). Because iteratedFDeriv is total, the condition is stated for all $x$ regardless of differentiability, but condition 1 makes these the true derivatives.

No integrability, measurability, or $L^2$ condition on $u_0$ is part of this structure beyond what follows from the three items.

`IsSolutionOn ν u₀ u p S`

Data: a real number $\nu \in \mathbb{R}$ (any real — no sign or nonzero requirement), a function $u_0 : \mathrm{Vec}_n \to \mathrm{Vec}_n$ , a time-dependent velocity $u : \mathbb{R} \to (\mathrm{Vec}_n \to \mathrm{Vec}_n)$ (write $u_t := u(t,\cdot)$ ), a time-dependent scalar $p : \mathbb{R} \to (\mathrm{Vec}_n \to \mathbb{R})$ (write $p_t$ ), and an arbitrary set of times $S \subseteq \mathbb{R}$ . The proposition is the conjunction of exactly six conditions. Nothing requires $u_0$ to satisfy IsInitialData; nothing constrains $u$ or $p$ at times outside $S$ except condition 5.

smooth_u: the uncurried map $(t,x) \mapsto u_t(x)$ from $\mathbb{R} \times \mathrm{Vec}_n$ to $\mathrm{Vec}_n$ is $C^\infty$ on the set $S \times \mathrm{Vec}_n = \{(t,x) : t \in S\}$ in Mathlib's ContDiffOn sense, with ∞ as above (all finite orders, not analytic). ContDiffOn is smoothness relative to the set: at each point $(t,x)$ with $t \in S$ , the function has Taylor expansions of every finite order on some neighbourhood of $(t,x)$ within $S \times \mathrm{Vec}_n$ . Consequences of this being relative: at times $t$ interior to $S$ this is ordinary joint smoothness in $(t,x)$ ; at boundary points of $S$ (e.g. $t = 0$ when $S = [0,\infty)$ ) it is one-sided smoothness in $t$ ; at a time $t$ that is isolated in $S$ the condition constrains only smoothness in $x$ and says nothing about dependence on $t$ . If $S = \varnothing$ the condition is vacuous.
smooth_p: the same statement for $(t,x) \mapsto p_t(x)$ , valued in $\mathbb{R}$ .
momentum: for every $t \in S$ with $0 < t$ (strictly), and for every $x \in \mathrm{Vec}_n$ (the whole space, no boundary),

\frac{d}{ds}\Big|_{s=t} u_s(x) \;+\; Du_t(x)\big[u_t(x)\big] \;=\; \nu\, \Delta u_t(x) \;-\; \nabla p_t(x),

an equation between vectors in $\mathrm{Vec}_n$ , where:

$\frac{d}{ds}|_{s=t} u_s(x)$ is Mathlib's deriv of the one-variable map $s \mapsto u_s(x)$ at $t$ , taken in the full real line (two-sided, not relative to $S$ ); it is the junk value $0$ if that map is not differentiable at $t$ . When $t$ is interior to $S$ , condition 1 makes it the genuine time derivative $\partial_t u(t,x)$ ; when $t>0$ lies in $S$ but is not interior to $S$ , condition 1 does not guarantee differentiability in the full line and the term may be the default $0$ .
$Du_t(x)[u_t(x)]$ is the Fréchet derivative of $u_t$ at $x$ applied to the vector $u_t(x)$ , i.e. $\sum_j u_{t,j}(x)\,\partial_j u_t(x) = (u_t\cdot\nabla)u_t(x)$ ; condition 1 restricted to the slice $\{t\}\times\mathrm{Vec}_n$ makes this genuine.
$\Delta u_t(x)$ is Mathlib's Laplacian of the vector-valued map $u_t : \mathrm{Vec}_n \to \mathrm{Vec}_n$ : the trace of the second Fréchet derivative, $\sum_i D^2 u_t(x)[b_i, b_i]$ over an orthonormal basis $(b_i)$ , applied componentwise; for $C^2$ maps this is $\sum_i \partial_i^2 u_t(x)$ , and where the map is not twice differentiable it is whatever the total iteratedFDeriv returns (default/zero values).
$\nabla p_t(x) \in \mathrm{Vec}_n$ is Mathlib's gradient: the vector representing the Fréchet derivative $Dp_t(x)$ through the inner product, $\langle \nabla p_t(x), v\rangle = Dp_t(x)\,v$ ; i.e. $(\partial_1 p_t(x),\dots,\partial_n p_t(x))$ ; it is $0$ where $p_t$ is not differentiable at $x$ .
$\nu\,\Delta u_t(x)$ is scalar multiplication by $\nu$ .

The equation is not required at $t = 0$ , nor at any $t \le 0$ in $S$ , nor at any $t \notin S$ . There is no forcing term.

divFree: for every $t \in S$ (including $t = 0$ or negative $t$ if they lie in $S$ ) and every $x \in \mathrm{Vec}_n$ , $\operatorname{div} u_t\,(x) = 0$ with $\operatorname{div}$ as defined above (genuine divergence by condition 1).
initial: $u_0$ (the function $u$ at time $0$ ) equals the given $u_0$ as functions on $\mathrm{Vec}_n$ : $u(0,x) = u_0(x)$ for all $x$ . This is required whether or not $0 \in S$ ; membership of $0$ in $S$ is not assumed anywhere in this structure. If $0 \notin S$ , conditions 1–4 say nothing about $u$ at time $0$ , yet condition 5 still pins it to $u_0$ .
boundedEnergy: there exists a real number $C$ such that for every $t \in S$ ,

\int^{-}_{\mathrm{Vec}_n} \|u_t(x)\|^2 \, dx \;<\; \operatorname{ofReal}(C),

where the integral is Mathlib's lower Lebesgue integral (∫⁻) with respect to the Lebesgue measure on $\mathrm{Vec}_n$ of the extended-nonnegative-valued function $x \mapsto \|u_t(x)\|_e^{\,2} \in [0,\infty]$ — it is defined for every function without any measurability hypothesis and always takes a value in $[0,\infty]$ — and $\operatorname{ofReal}(C) = \max(C,0)$ regarded in $[0,\infty]$ . The inequality is strict. Consequently the energy $\int \|u_t\|^2$ is finite for every $t\in S$ and bounded uniformly over $t \in S$ ; if $C \le 0$ the right side is $0$ and the condition can only hold when $S = \varnothing$ . For $n = 0$ the integral is $\|u_t(0)\|^2$ .

Note that $p$ enters the structure only through condition 2 and through $\nabla p_t$ in condition 3.

`IsSolution ν u₀ u p`

For $\nu \in \mathbb{R}$ , $u_0 : \mathrm{Vec}_n \to \mathrm{Vec}_n$ , $u : \mathbb{R} \to (\mathrm{Vec}_n \to \mathrm{Vec}_n)$ , $p : \mathbb{R} \to (\mathrm{Vec}_n \to \mathbb{R})$ , this is by definition IsSolutionOn ν u₀ u p S with $S = [0,\infty)$ (Mathlib's Set.Ici 0, closed at $0$ , unbounded above). Spelled out, it asserts exactly:

$(t,x)\mapsto u_t(x)$ and $(t,x)\mapsto p_t(x)$ are $C^\infty$ on $[0,\infty)\times\mathrm{Vec}_n$ in the relative sense (ordinary joint smoothness for $t>0$ ; one-sided in $t$ at $t = 0$ );
the momentum equation of item 3 above holds for every $t > 0$ and every $x\in\mathrm{Vec}_n$ (here every such $t$ is interior to $S$ , so the time derivative is the genuine two-sided $\partial_t u$ ); it is not asserted at $t = 0$ ;
$\operatorname{div} u_t(x) = 0$ for every $t \ge 0$ and every $x$ ;
$u(0,\cdot) = u_0$ ;
there is a real $C$ with $\int^{-}\|u_t(x)\|^2\,dx < \operatorname{ofReal}(C)$ for every $t \ge 0$ .

The values of $u$ and $p$ at negative times are completely unconstrained, $\nu$ may be zero or negative, $u_0$ is not required to satisfy IsInitialData, and no uniqueness is asserted.

Human review

Endorsed by Shuze Chen · Sep 8, 2026
Endorsed by korbonits · Sep 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

The incompressible Navier–Stokes equations on Rn\mathbb{R}^nRn: admissible data and physically reasonable solutions (Fefferman (1)–(4), (6), (7))

Read-back

Vec n

e i

div v x

gradNormSq v x

IsInitialData u₀

IsSolutionOn ν u₀ u p S

IsSolution ν u₀ u p

The incompressible Navier–Stokes equations on $\mathbb{R}^n$ : admissible data and physically reasonable solutions (Fefferman (1)–(4), (6), (7))

`Vec n`

`e i`

`div v x`

`gradNormSq v x`

`IsInitialData u₀`

`IsSolutionOn ν u₀ u p S`

`IsSolution ν u₀ u p`