Global existence and smoothness on $\mathbb{R}^3$ for small initial data: $\|u^0\|_{L^2}^2\|\nabla u^0\|_{L^2}^2 \le c\,\nu^4$

Throughout, $\mathbb{R}^3$ denotes Euclidean 3-space (the type Vec 3, i.e. $\mathbb{R}^{\{0,1,2\}}$ with the Euclidean norm $\|\cdot\|$ and Lebesgue measure $dx$), $e_0,e_1,e_2$ its standard basis vectors, $Dv(x)$ the Fréchet derivative of a map $v:\mathbb{R}^3\to\mathbb{R}^3$ at $x$ (a linear map $\mathbb{R}^3\to\mathbb{R}^3$; if $v$ is not differentiable at $x$ this is the junk value $0$), and $D^k v(x)$ the $k$-th iterated derivative (a $k$-linear map, with $\|D^0v(x)\| = \|v(x)\|$, and $\|\cdot\|$ the operator norm; again junk if $v$ is not $k$ times differentiable there). The declaration asserts:

Order of quantifiers. A single real constant $c>0$ is chosen first, and it must work uniformly for every viscosity $\nu>0$ and every admissible initial datum $u_0$; nothing else is asserted about $c$ (no formula, no bound). $\nu$ is strictly positive. The solution $(u,p)$ is chosen last and may depend on $\nu$ and $u_0$; existence only, not uniqueness.

The custom notions.

• $\operatorname{div} v(x) := \sum_{i=0}^{2}\big(Dv(x)\,e_i\big)_i = \sum_i \partial_i v_i(x)$, the usual divergence (with junk $0$ contributions wherever $v$ is not differentiable).
• $\mathrm{gradNormSq}\, v(x) := \sum_{j=0}^{2}\big\|Dv(x)\,e_j\big\|^2 = \sum_{i,j}(\partial_j v_i(x))^2$, the squared Frobenius norm of the Jacobian, $\|\nabla v(x)\|_F^2$.
• $\mathrm{IsInitialData}(u_0)$ is the conjunction of three conditions: (i) $u_0$ is $C^\infty$ on all of $\mathbb{R}^3$ (here "$\infty$" is the smooth order $\top$ of $\mathbb{N}\cup\{\infty\}$ cast into WithTop ℕ∞, i.e. all finite-order derivatives exist and are continuous; it is not the analytic order $\omega$); (ii) $\operatorname{div}u_0(x)=0$ for every $x\in\mathbb{R}^3$; (iii) for every pair of naturals $k,K$ there is a real $C$ (depending on $k,K$; necessarily $C\ge0$ since the left side is $\ge 0$) with $(1+\|x\|)^K\,\|D^k u_0(x)\|\le C$ for all $x$ — i.e. $u_0$ and all its derivatives decay faster than every polynomial (a Schwartz-type condition). In particular $u_0\in L^2$ and $\nabla u_0\in L^2$, so both integrals in the smallness hypothesis are integrals of genuinely integrable continuous functions. (In general the Bochner integral $\int f$ of a non-integrable $f$ is $0$ by convention, which would make the smallness hypothesis read $0\le c\nu^4$ and hold automatically; the decay condition rules this out here.)
• $\mathrm{IsSolution}(\nu,u_0,u,p)$ means $\mathrm{IsSolutionOn}$ with time set $S=[0,\infty)$, i.e. the conjunction of six conditions on the maps $u=(t,x)\mapsto u(t,x)$ and $p=(t,x)\mapsto p(t,x)$, which are defined on all of $\mathbb{R}\times\mathbb{R}^3$ but constrained only on $[0,\infty)\times\mathbb{R}^3$:
  1. $u$ is $C^\infty$ on the set $[0,\infty)\times\mathbb{R}^3$ in the relative sense: at every point of that set (including boundary points $t=0$) it has, for every finite order $m$, a continuous Taylor expansion of order $m$ computed along the set; on the interior $(0,\infty)\times\mathbb{R}^3$ this is ordinary $C^\infty$ smoothness, at $t=0$ it is one-sided smoothness from the right, and it says nothing about $u(t,\cdot)$ for $t<0$.
  2. $p$ satisfies the same relative $C^\infty$ condition on $[0,\infty)\times\mathbb{R}^3$.
  3. (Momentum) for every $t\ge 0$ with additionally $t>0$ (so: for every $t>0$, not at $t=0$) and every $x\in\mathbb{R}^3$,

where $\partial_t u(t,x)$ is the ordinary one-variable derivative of $s\mapsto u(s,x)$ at $s=t$ (junk $0$ if not differentiable, though condition 1 makes it genuine for $t>0$), the second term is $(u\cdot\nabla)u=\sum_j u_j\,\partial_j u$, $\Delta$ is Mathlib's Laplacian on a finite-dimensional inner-product space, $\Delta f(x)=\sum_i D^2 f(x)[e_i,e_i]$ applied componentwise to the $\mathbb{R}^3$-valued $u(t,\cdot)$ (junk if $u(t,\cdot)$ is not $C^2$, but genuine here for $t>0$), $\nabla$ is Mathlib's gradient (the vector Riesz-dual to $D_x p(t,\cdot)(x)$; junk $0$ if $p(t,\cdot)$ is not differentiable at $x$), and $\nu\,\cdot$ is scalar multiplication. 4. $\operatorname{div}\big(u(t,\cdot)\big)(x)=0$ for every $t\ge0$ (including $t=0$) and every $x$. 5. $u(0,\cdot)=u_0$ as functions, i.e. $u(0,x)=u_0(x)$ for every $x$ (exact pointwise equality, not almost-everywhere, not a limit as $t\to0^+$). 6. (Bounded energy) there is a real $C$ with

where $\int^-$ is the lower Lebesgue integral of a $[0,\infty]$-valued function (always defined, possibly $+\infty$, no integrability required; $\|\cdot\|_e$ is the norm viewed in $[0,\infty]$), and $\mathrm{ofReal}(C)=\max(C,0)$ in $[0,\infty]$. Since nothing is $<0$, this forces $C>0$, and it says exactly that $\sup_{t\ge0}\|u(t,\cdot)\|_{L^2}^2<C$ for some finite $C$ — a uniform-in-time finite $L^2$ bound with no stated relation to $u_0$, $\nu$, or $c$.

What is and is not asserted. The conclusion asks only for $(u,p)$ satisfying 1–6; it imposes no decay in $x$ on $u(t,\cdot)$ or $p(t,\cdot)$ beyond the $L^2$ bound in 6, no integrability or normalization of $p$ (any function of $t$ alone may be added to $p$ without affecting 1–6), no energy inequality, no continuity of $t\mapsto u(t,\cdot)$ in any norm beyond what 1 gives, and no uniqueness. The momentum equation is required for $t>0$ only; conditions 1, 2, 4 hold on all of $t\ge0$; condition 5 pins down $t=0$; nothing at all is required for $t<0$.

Degenerate cases. The hypotheses are satisfiable: $u_0\equiv0$ meets all three initial-data conditions and gives $0\le c\nu^4$, and for it $u\equiv0$, $p\equiv0$ satisfy 1–6, so the statement is not vacuous; moreover for any nonzero Schwartz-type divergence-free $u_0$ and any $\nu>0$, the product of integrals scales like $\lambda^4$ under $u_0\mapsto\lambda u_0$, so suitably rescaled data always satisfy the smallness hypothesis (whatever $c$ is), and conversely for fixed $u_0$ the hypothesis holds for all sufficiently large $\nu$. The smallness condition is a weak inequality $\le$ on the product $\|u_0\|_{L^2}^2\,\|\nabla u_0\|_{L^2}^2$ against $c\,\nu^4$; both factors are $\ge0$. The dimension is fixed at $3$ (the implicit dimension parameter of all the custom definitions is instantiated at $n=3$).