The two-dimensional case: existence and smoothness of Navier–Stokes solutions on $\mathbb{R}^2$ (Ladyzhenskaya)

Read-back of NavierStokes.existence_and_smoothness_R2.

Fix a real number $\nu$ with $\nu > 0$ (strict), and a map $u_0 : \mathbb{R}^2 \to \mathbb{R}^2$, where $\mathbb{R}^2$ carries the Euclidean inner product and norm (the dimension is hard-coded to $2$ in this theorem; the definitions below are stated for general $n$ but only $n=2$ is used). Assume $u_0$ is "initial data" in the following custom sense, which is the conjunction of three conditions: (i) $u_0$ is $C^\infty$ on all of $\mathbb{R}^2$ (here $\infty$ denotes smoothness of every finite order, not real-analyticity, which would be the separate symbol $\omega$); (ii) for every $x \in \mathbb{R}^2$ the custom divergence vanishes, $\operatorname{div} u_0(x) := \sum_{i=1}^{2} \big(Du_0(x)\,e_i\big)_i = 0$, where $Du_0(x)$ is the Fréchet derivative (a total function that returns the zero map wherever the function is not differentiable, though smoothness rules that out here) and $e_i$ the standard basis vectors, so this is $\partial_1 (u_0)_1 + \partial_2 (u_0)_2 = 0$; (iii) Schwartz-type decay: for every pair of natural numbers $k, K$ there is a real $C$ (depending on $k,K$) such that for all $x$, $(1+\|x\|)^K\,\|D^k u_0(x)\| \le C$, where $D^k u_0(x)$ is the $k$-th iterated Fréchet derivative as a $k$-multilinear map with its operator norm (so $k=K=0$ just says $u_0$ is bounded; since the left side is $\ge 0$, only $C \ge 0$ can work). The theorem then asserts the existence (not uniqueness — plain $\exists$, not $\exists!$) of a velocity field $u : \mathbb{R} \times \mathbb{R}^2 \to \mathbb{R}^2$, written $u(t,x)$ or $u_t(x)$, and a scalar pressure $p : \mathbb{R} \times \mathbb{R}^2 \to \mathbb{R}$, both defined for all real times including $t<0$, such that the following six conditions hold, all of which are relative to the time set $S = [0,\infty)$ (nothing whatsoever is required of $u$ or $p$ for $t<0$):

• Smoothness of $u$: the joint map $(t,x) \mapsto u(t,x)$ is $C^\infty$ on the set $[0,\infty) \times \mathbb{R}^2$. This is smoothness within a set with boundary: at interior points $(t>0)$ it is ordinary $C^\infty$ near the point; at boundary points $(t=0)$ it only asks for a smooth Taylor expansion valid on a neighbourhood intersected with $[0,\infty)\times\mathbb{R}^2$, i.e. one-sided smoothness in $t$ at $t=0$, with no constraint on how $u$ behaves for $t<0$.
• Smoothness of $p$: the same statement for $(t,x) \mapsto p(t,x)$.
• Momentum equation: for every $t \ge 0$ with additionally $t > 0$ (so effectively for every $t>0$; $t=0$ is excluded) and every $x \in \mathbb{R}^2$,

Here $\frac{d}{ds}u(s,x)$ is the ordinary one-variable derivative in time of the two-sided function $s\mapsto u(s,x)$ (a total function equal to $0$ where the derivative does not exist; for $t>0$ the interior smoothness above guarantees it is the genuine derivative); $(Du_t(x))[u_t(x)]$ is the spatial Fréchet derivative of the time-slice $u_t = u(t,\cdot)$ at $x$, applied to the vector $u_t(x)$, i.e. the convective term $(u\cdot\nabla)u$; $\Delta u_t(x)$ is Mathlib's Laplacian of the vector-valued map $u_t$ at $x$, namely $\sum_i D^2 u_t(x)[e_i,e_i]$ over an orthonormal basis (componentwise Laplacian; a total function, $0$ where the second derivative fails to exist — again excluded by smoothness); $\nu\,\cdot$ is scalar multiplication; and $\nabla p_t(x)$ is Mathlib's gradient of the scalar slice $p_t$ at $x$, the vector dual to the Fréchet derivative $Dp_t(x)$ under the inner product (also total, $0$ where non-differentiable).

• Divergence-free: for every $t \ge 0$ (including $t = 0$) and every $x$, $\operatorname{div} u_t(x) = \sum_{i=1}^2 (Du_t(x)\,e_i)_i = 0$.
• Initial condition: $u_0 = u(0,\cdot)$ as an equality of functions $\mathbb{R}^2 \to \mathbb{R}^2$ (pointwise for every $x$).
• Bounded energy: there is a single real $C$ such that for every $t \ge 0$,

where the integral is the lower Lebesgue integral against Lebesgue measure on $\mathbb{R}^2$ of the $[0,\infty]$-valued function $x\mapsto\|u(t,x)\|^2$ (this is always defined, with no integrability hypothesis needed; it takes the value $+\infty$ when the function is not integrable, and is the supremum over dominated measurable simple functions even if the integrand were non-measurable), and $\operatorname{ofReal}(C)\in[0,\infty]$ is $C$ if $C\ge 0$ and $0$ if $C<0$. Because the inequality is strict and the right side is finite, this forces each $u_t$ to have finite $L^2$ norm with a bound uniform in $t$; if $C \le 0$ the condition is unsatisfiable (nothing is $<0$ in $[0,\infty]$), so effectively $C>0$. No monotonicity or relation to the initial energy is asserted, and no integrability, decay, or normalization of $p$ is asserted anywhere.

On degenerate cases: the hypotheses are not vacuous — e.g. $u_0 \equiv 0$ satisfies all three initial-data conditions — and for that particular $u_0$ the conclusion is trivially witnessed by $u \equiv 0$, $p \equiv 0$; for general admissible $u_0$ the conclusion is a genuine existence claim. The decay condition (iii) is imposed only on $u_0$ and is not required of $u_t$ for $t>0$; the only spatial control on $u_t$ for $t>0$ is smoothness, the divergence constraint, and the uniform finite-energy bound above.