Independent definitions for the Navier–Stokes Comparator submission

This is a copy of the definitions and helper lemmas in NavierStokes.Comparator, without either challenge theorem or an import of the reference. The proof adapters use this module so their import closure contains no reference placeholders. Comparator checks these definitions against the independent reference at runtime.

Source: https://github.com/google-deepmind/formal-conjectures/blob/8bf45ed70d48b2b2a501de9c00b26bfa38c573ee/FormalConjectures/Millenium/NavierStokes.lean

noncomputable def NavierStokes.Comparator.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

• NavierStokes.Comparator.divergence v x = (LinearMap.trace ℝ (EuclideanSpace ℝ (Fin n))) ↑(fderiv ℝ v x)

@[simp]

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

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

@[simp]

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

The divergence of the zero vector field is zero.

@[simp]

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

The divergence of a constant vector field is zero.

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

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

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

Divergence commutes with scalar multiplication at differentiability points.

def NavierStokes.Comparator.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.Comparator.IsOnePeriodic f = ∀ (x : EuclideanSpace ℝ (Fin n)) (i : Fin n), f (x + EuclideanSpace.single i 1) = f x

structure NavierStokes.Comparator.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)) : divergence 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.Comparator.InitialVelocityConditionDecay {n : ℕ} (u₀ : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) extends NavierStokes.Comparator.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)) : divergence 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.Comparator.InitialVelocityConditionPeriodic {n : ℕ} (u₀ : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) extends NavierStokes.Comparator.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)) : divergence u₀ x = 0
• smooth : ContDiff ℝ (↑⊤) u₀
• isOnePeriodic : IsOnePeriodic u₀

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

structure NavierStokes.Comparator.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.Comparator.ForceConditionDecay {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ → EuclideanSpace ℝ (Fin n)) extends NavierStokes.Comparator.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.Comparator.ForceConditionPeriodic {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ → EuclideanSpace ℝ (Fin n)) extends NavierStokes.Comparator.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.Comparator.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 → divergence (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.Comparator.NavierStokesExistenceAndSmoothnessRn {n : ℕ} (nu : ℝ) (u₀ : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) (f v : EuclideanSpace ℝ (Fin n) → ℝ → EuclideanSpace ℝ (Fin n)) (p : EuclideanSpace ℝ (Fin n) → ℝ → ℝ) extends NavierStokes.Comparator.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 → divergence (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.Comparator.NavierStokesExistenceAndSmoothnessPeriodic {n : ℕ} (nu : ℝ) (u₀ : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) (f v : EuclideanSpace ℝ (Fin n) → ℝ → EuclideanSpace ℝ (Fin n)) (p : EuclideanSpace ℝ (Fin n) → ℝ → ℝ) extends NavierStokes.Comparator.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 → divergence (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).