The candidate forced Navier–Stokes construction

This module states the primary existential assertion of Candidate Theorem 1.1. candidateStatement separates the candidate contract from its construction. The witnesses and their consequences are proved in the downstream assembly modules.

The unit torus is represented by periodic functions on Euclidean three-space. Time is the first coordinate in SpaceTime. Smoothness at time zero is relative to the indicated closed half-domain. The PDE uses ordinary Frechet derivatives and is imposed only at interior times 0 < t < 1; the initial value is imposed separately at t = 0. No arbitrary extension to negative time is differentiated at the time-zero boundary.

The ContDiff scope's ∞ means all finite differentiability orders. In this Mathlib version ⊤ would instead impose the stronger analytic order.

@[reducible, inline]

abbrev NavierStokes.ProblemStatement.Space : Type

Three-dimensional real Euclidean space with its Euclidean norm.

Equations

• NavierStokes.ProblemStatement.Space = EuclideanSpace ℝ (Fin 3)

@[reducible, inline]

abbrev NavierStokes.ProblemStatement.SpaceTime : Type

The first coordinate is time; the second is the lifted spatial coordinate.

Equations

• NavierStokes.ProblemStatement.SpaceTime = (ℝ × NavierStokes.ProblemStatement.Space)

@[reducible, inline]

abbrev NavierStokes.ProblemStatement.VelocityField : Type

Velocity field: an abbreviation for SpaceTime → Space.

Equations

• NavierStokes.ProblemStatement.VelocityField = (NavierStokes.ProblemStatement.SpaceTime → NavierStokes.ProblemStatement.Space)

@[reducible, inline]

abbrev NavierStokes.ProblemStatement.PressureField : Type

Pressure field: an abbreviation for SpaceTime → ℝ.

Equations

• NavierStokes.ProblemStatement.PressureField = (NavierStokes.ProblemStatement.SpaceTime → ℝ)

noncomputable def NavierStokes.ProblemStatement.coordinateVector (i : Fin 3) : Space

The standard unit coordinate vectors, fixing both the metric and periods.

Equations

• NavierStokes.ProblemStatement.coordinateVector i = EuclideanSpace.single i 1

def NavierStokes.ProblemStatement.preSingularDomain : Set SpaceTime

Physical spacetime before the proposed singular time, including initial time.

Equations

• NavierStokes.ProblemStatement.preSingularDomain = Set.Ico 0 1 ×ˢ Set.univ

def NavierStokes.ProblemStatement.futureDomain : Set SpaceTime

The physical domain on which the prescribed force must be smooth.

Equations

• NavierStokes.ProblemStatement.futureDomain = Set.Ici 0 ×ˢ Set.univ

def NavierStokes.ProblemStatement.UnitSpatialPeriodsOn {V : Type u_1} (times : Set ℝ) (g : SpaceTime → V) : Prop

Invariance under each of the three unit coordinate shifts. Quantifying over every spatial point also gives the corresponding negative shifts.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.ProblemStatement.temporalDerivative (u : VelocityField) (t : ℝ) (x : Space) : Space

Ordinary time derivative, evaluated on the positive unit time direction. It is used in the PDE only for 0 < t < 1.

Equations

• NavierStokes.ProblemStatement.temporalDerivative u t x = (fderiv ℝ (fun (s : ℝ) => u (s, x)) t) 1

noncomputable def NavierStokes.ProblemStatement.spatialDerivative (u : VelocityField) (t : ℝ) (x : Space) : Space →L[ℝ] Space

Spatial Frechet derivative with time held fixed.

Equations

• NavierStokes.ProblemStatement.spatialDerivative u t x = fderiv ℝ (fun (y : NavierStokes.ProblemStatement.Space) => u (t, y)) x

noncomputable def NavierStokes.ProblemStatement.advection (u : VelocityField) (t : ℝ) (x : Space) : Space

(u · ∇)u, the spatial derivative applied to the velocity vector.

Equations

• NavierStokes.ProblemStatement.advection u t x = (NavierStokes.ProblemStatement.spatialDerivative u t x) (u (t, x))

noncomputable def NavierStokes.ProblemStatement.spatialDivergence (u : VelocityField) (t : ℝ) (x : Space) : ℝ

Euclidean divergence ∑ᵢ ∂ᵢuᵢ.

Equations

• NavierStokes.ProblemStatement.spatialDivergence u t x = ∑ i : Fin 3, ((NavierStokes.ProblemStatement.spatialDerivative u t x) (NavierStokes.ProblemStatement.coordinateVector i)).ofLp i

noncomputable def NavierStokes.ProblemStatement.pressureGradient (p : PressureField) (t : ℝ) (x : Space) : Space

Euclidean gradient ∑ᵢ (∂ᵢp)eᵢ.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.ProblemStatement.spatialLaplacian (u : VelocityField) (t : ℝ) (x : Space) : Space

Componentwise Euclidean Laplacian ∑ᵢ ∂ᵢ∂ᵢu.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokes.ProblemStatement.navierStokesResidual (u : VelocityField) (p : PressureField) (t : ℝ) (x : Space) : Space

The physical Navier--Stokes residual at viscosity exactly one.

Equations

• One or more equations did not get rendered due to their size.

def NavierStokes.ProblemStatement.CompactFutureTimeSupport (f : VelocityField) : Prop

A common finite upper endpoint for the force's future time support, uniformly over space. Spatial support is not required to be compact in the lift.

Equations

• NavierStokes.ProblemStatement.CompactFutureTimeSupport f = ∃ (T : ℝ), 0 ≤ T ∧ ∀ (t : ℝ), T ≤ t → ∀ (x : NavierStokes.ProblemStatement.Space), f (t, x) = 0

def NavierStokes.ProblemStatement.SpeedUnboundedAtOne (u : VelocityField) : Prop

Pointwise expression of unbounded speed arbitrarily near time one from below. Both the threshold and the time-neighborhood radius are arbitrary.

Equations

• One or more equations did not get rendered due to their size.

structure NavierStokes.ProblemStatement.CandidateProperties (u : VelocityField) (p : PressureField) (f : VelocityField) : Prop

Every field in this proposition is an explicit regularity, periodicity, support, equation, initial-value, or blow-up condition. No existence is asserted by introducing the proposition.

• velocity_smooth : ContDiffOn ℝ (↑⊤) u preSingularDomain
• pressure_smooth : ContDiffOn ℝ (↑⊤) p preSingularDomain
• force_smooth : ContDiffOn ℝ (↑⊤) f futureDomain
• velocity_periodic : UnitSpatialPeriodsOn (Set.Ico 0 1) u
• pressure_periodic : UnitSpatialPeriodsOn (Set.Ico 0 1) p
• force_periodic : UnitSpatialPeriodsOn (Set.Ici 0) f
• zero_initial_velocity (x : Space) : u (0, x) = 0
• force_time_support : CompactFutureTimeSupport f
• divergence_free (t : ℝ) : t ∈ Set.Ico 0 1 → ∀ (x : Space), spatialDivergence u t x = 0
• navier_stokes (t : ℝ) : t ∈ Set.Ioo 0 1 → ∀ (x : Space), navierStokesResidual u p t x = f (t, x)
• speed_unbounded : SpeedUnboundedAtOne u

def NavierStokes.ProblemStatement.candidateStatement : Prop

The primary existential content of Candidate Theorem 1.1. Maximal lifespan, Sobolev blow-up, and force derivative decay are derived from these candidate conditions in separate theorems.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.ProblemStatement.smooth_at_interior {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {g : SpaceTime → V} (hg : ContDiffOn ℝ (↑⊤) g preSingularDomain) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (x : Space) : ContDiffAt ℝ (↑⊤) g (t, x)

Relative smoothness gives ordinary smoothness at every interior spacetime point, where the ordinary derivatives in the equation are evaluated.

theorem NavierStokes.ProblemStatement.unit_period_negative {V : Type u_1} {times : Set ℝ} {g : SpaceTime → V} (hg : UnitSpatialPeriodsOn times g) {t : ℝ} (ht : t ∈ times) (x : Space) (i : Fin 3) : g (t, x - coordinateVector i) = g (t, x)

A unit-period identity also gives the negative unit shift.

@[simp]

theorem NavierStokes.ProblemStatement.zero_residual (t : ℝ) (x : Space) : navierStokesResidual (fun (x : SpaceTime) => 0) (fun (x : SpaceTime) => 0) t x = 0

The residual definition reduces to zero for zero velocity and pressure.

theorem NavierStokes.ProblemStatement.zero_force_time_support : CompactFutureTimeSupport fun (x : SpaceTime) => 0

The zero force satisfies the explicit support condition.

theorem NavierStokes.ProblemStatement.zero_velocity_not_unbounded : ¬SpeedUnboundedAtOne fun (x : SpaceTime) => 0

The blow-up condition excludes the zero velocity field.

theorem NavierStokes.ProblemStatement.unbounded_speed_excludes_uniform_bound {u : VelocityField} (h : SpeedUnboundedAtOne u) : ¬∃ (C : ℝ), ∀ t ∈ Set.Ico 0 1, ∀ (x : Space), ‖u (t, x)‖ ≤ C

The quantified blow-up condition excludes every uniform finite bound on the physical presingular domain. This does not assert that the condition holds.