Existence And Smoothness Of The Navier–Stokes Equation

This file formalizes the Clay Mathematics Institute millennium problem concerning the existence and smoothness of solutions to the Navier-Stokes equations in three spatial dimensions. While the definitions are generalized to arbitrary dimension n, the millennium problem specifically concerns the case n = 3.

References

• Wikipedia
• Clay Mathematics Institute

Main Theorems (Clay Millennium Problem for n = 3)

The Clay Millennium Problem asks for a proof of one of the following four statements:

• navier_stokes_existence_and_smoothness_R3: (A) Global existence on ℝ³
• navier_stokes_existence_and_smoothness_periodic: (B) Global existence on ℝ³/ℤ³
• navier_stokes_breakdown_R3: (C) Existence of breakdown scenario on ℝ³
• navier_stokes_breakdown_periodic: (D) Existence of breakdown scenario on ℝ³/ℤ³

Variable conventions

Fefferman writes the velocity as $u(x,t)$, the initial velocity as $u^\circ(x)$, the pressure as $p(x,t)$, the force as $f(x,t)$, and the viscosity as $\nu$. In Lean, u₀ : ℝ^n → ℝ^n denotes the initial velocity, while v : ℝ^n → ℝ → ℝ^n denotes the solution velocity. The curried order v x t, p x t, and f x t keeps the source convention that position comes before time.

Since the Clay statement gives equation (1) on the closed time half-line $t \ge 0$, the time derivative is encoded with derivWithin relative to Set.Ici 0. The Clay PDF also includes errata; in particular, we include spatial 1-periodicity of the pressure in the periodic case. The sign correction to the weak-solution identity in the errata is not represented here, since this file formalizes the four prize alternatives rather than the later weak-solution discussion.

noncomputable def NavierStokes.divergence {n : ℕ} (v : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) (x : EuclideanSpace ℝ (Fin n)) : ℝ

The divergence $\nabla \cdot v$ of a vector field $v : \mathbb{R}^n \to \mathbb{R}^n$ at a point $x$, computed as the trace of the Jacobian matrix.

In coordinates, $\nabla \cdot v = \sum_i \partial v_i / \partial x_i$.

This is available as the notation ∇⬝ v. If v is not differentiable at x, then fderiv is the zero map, so this definition has the corresponding junk value $0$.

Equations

• ∇⬝ v x = (LinearMap.trace ℝ (EuclideanSpace ℝ (Fin n))) ↑(fderiv ℝ v x)

def NavierStokes.«term∇⬝» : Lean.ParserDescr

The divergence $\nabla \cdot v$ of a vector field $v : \mathbb{R}^n \to \mathbb{R}^n$ at a point $x$, computed as the trace of the Jacobian matrix.

In coordinates, $\nabla \cdot v = \sum_i \partial v_i / \partial x_i$.

This is available as the notation ∇⬝ v. If v is not differentiable at x, then fderiv is the zero map, so this definition has the corresponding junk value $0$.

Equations

• NavierStokes.«term∇⬝» = Lean.ParserDescr.node `NavierStokes.«term∇⬝» 1024 (Lean.ParserDescr.symbol "∇⬝")

@[simp]

theorem NavierStokes.divergence_of_not_differentiableAt {n : ℕ} {v : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)} {x : EuclideanSpace ℝ (Fin n)} (hv : ¬DifferentiableAt ℝ v x) : ∇⬝ v x = 0

The divergence of a vector field is $0$ at points where fderiv has its junk value.

@[simp]

theorem NavierStokes.divergence_zero {n : ℕ} (x : EuclideanSpace ℝ (Fin n)) : ∇⬝ 0 x = 0

The divergence of the zero vector field is zero.

@[simp]

theorem NavierStokes.divergence_const {n : ℕ} (c x : EuclideanSpace ℝ (Fin n)) : ∇⬝ (fun (x : EuclideanSpace ℝ (Fin n)) => c) x = 0

The divergence of a constant vector field is zero.

theorem NavierStokes.divergence_add {n : ℕ} {v w : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)} {x : EuclideanSpace ℝ (Fin n)} (hv : DifferentiableAt ℝ v x) (hw : DifferentiableAt ℝ w x) : ∇⬝ (fun (y : EuclideanSpace ℝ (Fin n)) => v y + w y) x = ∇⬝ v x + ∇⬝ w x

Divergence is additive at points where both vector fields are differentiable.

theorem NavierStokes.divergence_smul {n : ℕ} (c : ℝ) {v : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)} {x : EuclideanSpace ℝ (Fin n)} (hv : DifferentiableAt ℝ v x) : ∇⬝ (fun (y : EuclideanSpace ℝ (Fin n)) => c • v y) x = c * ∇⬝ v x

Divergence commutes with scalar multiplication at differentiability points.

def NavierStokes.IsOnePeriodic {n : ℕ} {α : Sort u_1} (f : EuclideanSpace ℝ (Fin n) → α) : Prop

A function $f : \mathbb{R}^n \to \alpha$ is 1-periodic if it is periodic in each coordinate with period $1$, i.e. $f(x + e_i) = f(x)$ for each unit vector $e_i$. This captures functions on the $n$-torus $\mathbb{R}^n/\mathbb{Z}^n$.

Equations

• NavierStokes.IsOnePeriodic f = ∀ (x : EuclideanSpace ℝ (Fin n)) (i : Fin n), f (x + EuclideanSpace.single i 1) = f x

structure NavierStokes.InitialVelocityCondition {n : ℕ} (u₀ : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) : Prop

Basic conditions on initial velocity field for the Navier-Stokes equations in $n$-dimensional space.

The initial velocity must be:

• Divergence-free (incompressibility condition: $\nabla \cdot u_0 = 0$)
• Smooth ($C^\infty$)

These conditions apply regardless of spatial dimension.

• div_free (x : EuclideanSpace ℝ (Fin n)) : ∇⬝ u₀ x = 0

  The initial velocity field is divergence-free (equation 2). This is the incompressibility constraint for the fluid.

• smooth : ContDiff ℝ (↑⊤) u₀

  The initial velocity field is smooth ($C^\infty$ in all variables).

structure NavierStokes.InitialVelocityConditionDecay {n : ℕ} (u₀ : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) extends NavierStokes.InitialVelocityCondition u₀ : Prop

Initial velocity conditions for the Navier-Stokes problem on all of $\mathbb{R}^n$.

In addition to being smooth and divergence-free, the velocity must decay faster than any polynomial at spatial infinity (condition 4 in Fefferman's paper).

This condition ensures the velocity field has finite energy and reasonable behavior as $\lVert x \rVert \to \infty$.

• div_free (x : EuclideanSpace ℝ (Fin n)) : ∇⬝ u₀ x = 0
• smooth : ContDiff ℝ (↑⊤) u₀
• decay (m : ℕ) (K : ℝ) : ∃ (C : ℝ), ∀ (x : EuclideanSpace ℝ (Fin n)), ‖iteratedFDeriv ℝ m u₀ x‖ ≤ C / (1 + ‖x‖) ^ K

  All derivatives of u₀ decay faster than any polynomial (condition 4). For any derivative order $m$ and any decay rate $K$, there exists a constant $C$ such that $\lVert \partial^m u_0(x) \rVert \le C/(1+\lVert x \rVert)^K$.

structure NavierStokes.InitialVelocityConditionPeriodic {n : ℕ} (u₀ : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) extends NavierStokes.InitialVelocityCondition u₀ : Prop

Initial velocity conditions for the periodic Navier-Stokes problem on $\mathbb{R}^n/\mathbb{Z}^n$.

The velocity must be smooth, divergence-free, and 1-periodic in each coordinate (condition 8, part 1 in Fefferman's paper).

• div_free (x : EuclideanSpace ℝ (Fin n)) : ∇⬝ u₀ x = 0
• smooth : ContDiff ℝ (↑⊤) u₀
• isOnePeriodic : IsOnePeriodic u₀

  The initial velocity is 1-periodic in each direction (condition 8, part 1).

structure NavierStokes.ForceCondition {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ → EuclideanSpace ℝ (Fin n)) : Prop

The basic smoothness condition on the external forcing term.

The force $f(x,t)$ must be smooth ($C^\infty$) in both space and time variables for $t \ge 0$.

• smooth : ContDiffOn ℝ (↑⊤) (↿f) (Set.univ ×ˢ Set.Ici 0)

  The force is smooth on $\mathbb{R}^n \times [0,\infty)$.

structure NavierStokes.ForceConditionDecay {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ → EuclideanSpace ℝ (Fin n)) extends NavierStokes.ForceCondition f : Prop

Force conditions for the Navier-Stokes problem on all of $\mathbb{R}^n$.

The force must be smooth and decay faster than any polynomial in both space and time (condition 5 in Fefferman's paper).

• smooth : ContDiffOn ℝ (↑⊤) (↿f) (Set.univ ×ˢ Set.Ici 0)
• decay (m : ℕ) (K : ℝ) : ∃ (C : ℝ), ∀ (x : EuclideanSpace ℝ (Fin n)), ∀ t ≥ 0, ‖iteratedFDerivWithin ℝ m (↿f) (Set.univ ×ˢ Set.Ici 0) (x, t)‖ ≤ C / (1 + ‖x‖ + t) ^ K

  All derivatives of f decay faster than any polynomial in space and time (condition 5). For any derivative order $m$ and any decay rate $K$, there exists $C$ such that $\lVert \partial^m_{x,t} f(x,t) \rVert \le C/(1+\lVert x \rVert+t)^K$ for $t \ge 0$.

structure NavierStokes.ForceConditionPeriodic {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ → EuclideanSpace ℝ (Fin n)) extends NavierStokes.ForceCondition f : Prop

Force conditions for the periodic Navier-Stokes problem on $\mathbb{R}^n/\mathbb{Z}^n$.

The force must be smooth, 1-periodic in space, and decay in time (conditions 8, part 1 and 9 in Fefferman's paper).

• smooth : ContDiffOn ℝ (↑⊤) (↿f) (Set.univ ×ˢ Set.Ici 0)
• isOnePeriodic (t : ℝ) : t ≥ 0 → IsOnePeriodic fun (x : EuclideanSpace ℝ (Fin n)) => f x t

  The force is 1-periodic in space for all times $t \ge 0$ (condition 8, part 1).

• decay (m : ℕ) (K : ℝ) : ∃ (C : ℝ), ∀ (x : EuclideanSpace ℝ (Fin n)), ∀ t ≥ 0, ‖iteratedFDerivWithin ℝ m (↿f) (Set.univ ×ˢ Set.Ici 0) (x, t)‖ ≤ C / (1 + t) ^ K

  All derivatives of f decay faster than any polynomial in time (condition 9).

structure NavierStokes.NavierStokesExistenceAndSmoothness {n : ℕ} (nu : ℝ) (u₀ : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) (f v : EuclideanSpace ℝ (Fin n) → ℝ → EuclideanSpace ℝ (Fin n)) (p : EuclideanSpace ℝ (Fin n) → ℝ → ℝ) : Prop

A solution (v, p) to the Navier-Stokes equations in n-dimensional space with viscosity $\nu$, initial velocity $u_0$, and external force $f$.

This structure captures the core requirements for a solution:

1. The velocity and pressure satisfy the Navier-Stokes PDE (equation 1)
2. The velocity remains divergence-free for all time (equation 2)
3. The initial condition is satisfied (equation 3)
4. The solution is smooth ($C^\infty$) for all time $t \ge 0$ (equations 6, 11)

• navier_stokes (x : EuclideanSpace ℝ (Fin n)) (t : ℝ) : t ≥ 0 → derivWithin (fun (x_1 : ℝ) => v x x_1) (Set.Ici 0) t + (fderiv ℝ (fun (x : EuclideanSpace ℝ (Fin n)) => v x t) x) (v x t) = nu • Laplacian.laplacian (fun (x : EuclideanSpace ℝ (Fin n)) => v x t) x - gradient (fun (x : EuclideanSpace ℝ (Fin n)) => p x t) x + f x t

  The Navier-Stokes equation (equation 1): $\partial v/\partial t + (v \cdot \nabla)v = \nu\Delta v - \nabla p + f$.

• div_free (x : EuclideanSpace ℝ (Fin n)) (t : ℝ) : t ≥ 0 → ∇⬝ (fun (x : EuclideanSpace ℝ (Fin n)) => v x t) x = 0

  Incompressibility constraint (equation 2): $\nabla \cdot v = 0$ for all $x$ and $t \ge 0$.

• initial_condition (x : EuclideanSpace ℝ (Fin n)) : v x 0 = u₀ x

  Initial condition (equation 3): $v(x,0) = u_0(x)$ for all $x$.

• velocity_smooth : ContDiffOn ℝ (↑⊤) (↿v) (Set.univ ×ˢ Set.Ici 0)

  The velocity field is smooth ($C^\infty$) on $\mathbb{R}^n \times [0,\infty)$ (conditions 6, 11).

• pressure_smooth : ContDiffOn ℝ (↑⊤) (↿p) (Set.univ ×ˢ Set.Ici 0)

  The pressure field is smooth ($C^\infty$) on $\mathbb{R}^n \times [0,\infty)$ (conditions 6, 11).

structure NavierStokes.NavierStokesExistenceAndSmoothnessRn {n : ℕ} (nu : ℝ) (u₀ : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) (f v : EuclideanSpace ℝ (Fin n) → ℝ → EuclideanSpace ℝ (Fin n)) (p : EuclideanSpace ℝ (Fin n) → ℝ → ℝ) extends NavierStokes.NavierStokesExistenceAndSmoothness nu u₀ f v p : Prop

A solution to the Navier-Stokes equations on all of $\mathbb{R}^n$ with appropriate decay and energy bounds.

In addition to the basic solution properties, we require:

• The velocity is in $L^2$ at each time $t \ge 0$ (finite kinetic energy)
• The total energy remains bounded for all time (condition 7)

• navier_stokes (x : EuclideanSpace ℝ (Fin n)) (t : ℝ) : t ≥ 0 → derivWithin (fun (x_1 : ℝ) => v x x_1) (Set.Ici 0) t + (fderiv ℝ (fun (x : EuclideanSpace ℝ (Fin n)) => v x t) x) (v x t) = nu • Laplacian.laplacian (fun (x : EuclideanSpace ℝ (Fin n)) => v x t) x - gradient (fun (x : EuclideanSpace ℝ (Fin n)) => p x t) x + f x t
• div_free (x : EuclideanSpace ℝ (Fin n)) (t : ℝ) : t ≥ 0 → ∇⬝ (fun (x : EuclideanSpace ℝ (Fin n)) => v x t) x = 0
• initial_condition (x : EuclideanSpace ℝ (Fin n)) : v x 0 = u₀ x
• velocity_smooth : ContDiffOn ℝ (↑⊤) (↿v) (Set.univ ×ˢ Set.Ici 0)
• pressure_smooth : ContDiffOn ℝ (↑⊤) (↿p) (Set.univ ×ˢ Set.Ici 0)
• integrable (t : ℝ) : t ≥ 0 → MeasureTheory.MemLp (fun (x : EuclideanSpace ℝ (Fin n)) => ‖v x t‖) 2 MeasureTheory.volume

  The velocity is square-integrable at each time $t \ge 0$ (condition 7).

• globally_bounded_energy : ∃ (E : ℝ), ∀ t ≥ 0, ∫ (x : EuclideanSpace ℝ (Fin n)), ‖v x t‖ ^ 2 < E

  The kinetic energy $\int \lVert v(x,t) \rVert^2\,dx$ remains uniformly bounded for all time (condition 7), where the integral is the Lebesgue integral.

structure NavierStokes.NavierStokesExistenceAndSmoothnessPeriodic {n : ℕ} (nu : ℝ) (u₀ : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) (f v : EuclideanSpace ℝ (Fin n) → ℝ → EuclideanSpace ℝ (Fin n)) (p : EuclideanSpace ℝ (Fin n) → ℝ → ℝ) extends NavierStokes.NavierStokesExistenceAndSmoothness nu u₀ f v p : Prop

A solution to the Navier-Stokes equations on the $n$-torus $\mathbb{R}^n/\mathbb{Z}^n$.

The velocity must be 1-periodic in each spatial direction for all times (condition 10). The pressure is also required to be 1-periodic, following the errata appended to the Clay problem statement.

• navier_stokes (x : EuclideanSpace ℝ (Fin n)) (t : ℝ) : t ≥ 0 → derivWithin (fun (x_1 : ℝ) => v x x_1) (Set.Ici 0) t + (fderiv ℝ (fun (x : EuclideanSpace ℝ (Fin n)) => v x t) x) (v x t) = nu • Laplacian.laplacian (fun (x : EuclideanSpace ℝ (Fin n)) => v x t) x - gradient (fun (x : EuclideanSpace ℝ (Fin n)) => p x t) x + f x t
• div_free (x : EuclideanSpace ℝ (Fin n)) (t : ℝ) : t ≥ 0 → ∇⬝ (fun (x : EuclideanSpace ℝ (Fin n)) => v x t) x = 0
• initial_condition (x : EuclideanSpace ℝ (Fin n)) : v x 0 = u₀ x
• velocity_smooth : ContDiffOn ℝ (↑⊤) (↿v) (Set.univ ×ˢ Set.Ici 0)
• pressure_smooth : ContDiffOn ℝ (↑⊤) (↿p) (Set.univ ×ˢ Set.Ici 0)
• isOnePeriodic_velocity (t : ℝ) : t ≥ 0 → IsOnePeriodic fun (x : EuclideanSpace ℝ (Fin n)) => v x t

  The velocity is 1-periodic in space for all times $t \ge 0$ (condition 10).

• isOnePeriodic_pressure (t : ℝ) : t ≥ 0 → IsOnePeriodic fun (x : EuclideanSpace ℝ (Fin n)) => p x t

  The pressure is 1-periodic in space for all times $t \ge 0$ (Clay errata).

theorem NavierStokes.navier_stokes_existence_and_smoothness_R3 (nu : ℝ) (hnu : nu > 0) (u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) (hu₀ : InitialVelocityConditionDecay u₀) : ∃ (v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)) (p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ), NavierStokesExistenceAndSmoothnessRn nu u₀ 0 v p

(A) Existence and smoothness of Navier–Stokes solutions on ℝ³.

theorem NavierStokes.navier_stokes_existence_and_smoothness_periodic (nu : ℝ) (hnu : nu > 0) (u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) (hu₀ : InitialVelocityConditionPeriodic u₀) : ∃ (v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)) (p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ), NavierStokesExistenceAndSmoothnessPeriodic nu u₀ 0 v p

(B) Existence and smoothness of Navier–Stokes solutions in ℝ³/ℤ³.

theorem NavierStokes.navier_stokes_breakdown_R3 (nu : ℝ) (hnu : nu > 0) : ∃ (u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) (f : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)), InitialVelocityConditionDecay u₀ ∧ ForceConditionDecay f ∧ ¬∃ (v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)) (p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ), NavierStokesExistenceAndSmoothnessRn nu u₀ f v p

(C) Breakdown of Navier–Stokes solutions on ℝ³.

theorem NavierStokes.navier_stokes_breakdown_periodic (nu : ℝ) (hnu : nu > 0) : ∃ (u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) (f : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)), InitialVelocityConditionPeriodic u₀ ∧ ForceConditionPeriodic f ∧ ¬∃ (v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)) (p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ), NavierStokesExistenceAndSmoothnessPeriodic nu u₀ f v p

(D) Breakdown of Navier–Stokes Solutions on ℝ³/ℤ³.