The whole-space assertion of Part II, Theorem 1.1

This module states the R³ theorem, including its comparison claim, independently of the existing periodic target. The coordinates, Euclidean norm, and differential operators are those of NavierStokes.ProblemStatement; no periodicity assumption is made here. Time is the first coordinate of spacetime.

The force is a globally smooth function whose topological support is compact and contained in strictly positive time. This represents the zero extension of an element of C_c^∞(R³ × (0, ∞); R³) and, in particular, requires support separated from initial time as well as from spatial and future-time infinity.

Smoothness of velocity and pressure at time zero is relative to the physical half-domain. The equation uses ordinary derivatives at positive times; zero initial velocity is imposed separately. This avoids differentiating an arbitrary extension to negative time at the boundary. ∞ in the ContDiff scope means every finite differentiability order.

breakdownStatement is the full proposition to prove. Introducing it does not assert that it has a proof or supply a witness.

@[reducible, inline]

abbrev NavierStokesR3.ProblemStatement.Space : Type

R³ with its ordinary Euclidean norm.

Equations

• NavierStokesR3.ProblemStatement.Space = NavierStokes.ProblemStatement.Space

@[reducible, inline]

abbrev NavierStokesR3.ProblemStatement.SpaceTime : Type

Spacetime, with time first.

Equations

• NavierStokesR3.ProblemStatement.SpaceTime = NavierStokes.ProblemStatement.SpaceTime

@[reducible, inline]

abbrev NavierStokesR3.ProblemStatement.VelocityField : Type

Velocity field: an abbreviation for NavierStokes.ProblemStatement.VelocityField.

Equations

• NavierStokesR3.ProblemStatement.VelocityField = NavierStokes.ProblemStatement.VelocityField

@[reducible, inline]

abbrev NavierStokesR3.ProblemStatement.PressureField : Type

Pressure field: an abbreviation for NavierStokes.ProblemStatement.PressureField.

Equations

• NavierStokesR3.ProblemStatement.PressureField = NavierStokes.ProblemStatement.PressureField

@[reducible, inline]

abbrev NavierStokesR3.ProblemStatement.preSingularDomain : Set NavierStokes.ProblemStatement.SpaceTime

The physical domain before the asserted singular time.

Equations

• NavierStokesR3.ProblemStatement.preSingularDomain = NavierStokes.ProblemStatement.preSingularDomain

@[reducible, inline]

abbrev NavierStokesR3.ProblemStatement.futureDomain : Set NavierStokes.ProblemStatement.SpaceTime

The physical domain for a global competing solution.

Equations

• NavierStokesR3.ProblemStatement.futureDomain = NavierStokes.ProblemStatement.futureDomain

def NavierStokesR3.ProblemStatement.positiveTimeDomain : Set SpaceTime

The open set in which the prescribed force must have compact support.

Equations

• NavierStokesR3.ProblemStatement.positiveTimeDomain = Set.Ioi 0 ×ˢ Set.univ

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

The exact incompressible Navier--Stokes residual at viscosity ν. The viscosity multiplies only the spatial Laplacian.

Equations

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

def NavierStokesR3.ProblemStatement.CompactPositiveTimeSupport (f : VelocityField) : Prop

Compact spacetime support contained in t > 0, using the closure of the nonzero set. Together with global smoothness this is the required force class.

Equations

• NavierStokesR3.ProblemStatement.CompactPositiveTimeSupport f = (HasCompactSupport f ∧ tsupport f ⊆ NavierStokesR3.ProblemStatement.positiveTimeDomain)

def NavierStokesR3.ProblemStatement.SquareIntegrableAtTime (u : VelocityField) (t : ℝ) : Prop

Square integrability with respect to ordinary Lebesgue volume on R³. This condition is explicit because the real Bochner integral is totalized.

Equations

• NavierStokesR3.ProblemStatement.SquareIntegrableAtTime u t = MeasureTheory.Integrable (fun (x : NavierStokesR3.ProblemStatement.Space) => ‖u (t, x)‖ ^ 2) MeasureTheory.volume

noncomputable def NavierStokesR3.ProblemStatement.kineticEnergy (u : VelocityField) (t : ℝ) : ℝ

Kinetic energy at a time. It is used below only together with the explicit integrability condition SquareIntegrableAtTime.

Equations

• NavierStokesR3.ProblemStatement.kineticEnergy u t = 1 / 2 * ∫ (x : NavierStokesR3.ProblemStatement.Space), ‖u (t, x)‖ ^ 2

def NavierStokesR3.ProblemStatement.UniformFiniteEnergy (times : Set ℝ) (u : VelocityField) : Prop

One finite bound for the kinetic energy at every time in times, with square integrability required at every such time.

Equations

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

@[reducible, inline]

abbrev NavierStokesR3.ProblemStatement.SpeedUnboundedAtOne (u : NavierStokes.ProblemStatement.VelocityField) : Prop

Pointwise unbounded speed in every left neighborhood of time one. For the continuous, compactly supported spatial slices in CandidateProperties, this expresses the L∞ blow-up assertion of Theorem 1.1.

Equations

• NavierStokesR3.ProblemStatement.SpeedUnboundedAtOne = NavierStokes.ProblemStatement.SpeedUnboundedAtOne

structure NavierStokesR3.ProblemStatement.CandidateProperties (ν : ℝ) (u : VelocityField) (p : PressureField) (f : VelocityField) (K : Set Space) : Prop

The properties of the constructed fields in Theorem 1.1. The same single compact set K contains both spatial supports for every 0 ≤ t < 1.

• velocity_smooth : ContDiffOn ℝ (↑⊤) u preSingularDomain
• pressure_smooth : ContDiffOn ℝ (↑⊤) p preSingularDomain
• support_compact : IsCompact K
• velocity_support (t : ℝ) : t ∈ Set.Ico 0 1 → (tsupport fun (x : Space) => u (t, x)) ⊆ K
• pressure_support (t : ℝ) : t ∈ Set.Ico 0 1 → (tsupport fun (x : Space) => p (t, x)) ⊆ K
• force_smooth : ContDiff ℝ (↑⊤) f
• force_support : CompactPositiveTimeSupport f
• zero_initial_velocity (x : Space) : u (0, x) = 0
• divergence_free (t : ℝ) : t ∈ Set.Ico 0 1 → ∀ (x : Space), NavierStokes.ProblemStatement.spatialDivergence u t x = 0
• navier_stokes (t : ℝ) : t ∈ Set.Ioo 0 1 → ∀ (x : Space), navierStokesResidual ν u p t x = f (t, x)
• energy_bounded : UniformFiniteEnergy (Set.Ico 0 1) u
• speed_unbounded : SpeedUnboundedAtOne u

structure NavierStokesR3.ProblemStatement.Candidate (ν : ℝ) : Type

Data realizing the primary existence assertion at one viscosity.

• velocity : VelocityField

  Velocity field of Candidate, of type VelocityField.

• pressure : PressureField

  Pressure field of Candidate, of type PressureField.

• force : VelocityField

  Force of Candidate, of type VelocityField.

• support : Set Space

  Support set of Candidate, of type Set Space.

• properties : CandidateProperties ν self.velocity self.pressure self.force self.support

structure NavierStokesR3.ProblemStatement.GlobalFiniteEnergySolution (ν : ℝ) (f : VelocityField) : Type

A global smooth solution with uniformly bounded kinetic energy for the given viscosity and the given force, starting from the same zero datum.

There are no support, periodicity, pressure-growth, derivative-growth, or energy inequality assumptions on a competitor. The square-integrability requirement and its uniform energy bound use all of R³ and all nonnegative times.

• velocity : VelocityField

  Velocity field of GlobalFiniteEnergySolution, of type VelocityField.

• pressure : PressureField

  Pressure field of GlobalFiniteEnergySolution, of type PressureField.

• velocity_smooth : ContDiffOn ℝ (↑⊤) self.velocity futureDomain
• pressure_smooth : ContDiffOn ℝ (↑⊤) self.pressure futureDomain
• zero_initial_velocity (x : Space) : self.velocity (0, x) = 0
• divergence_free (t : ℝ) : t ∈ Set.Ici 0 → ∀ (x : Space), NavierStokes.ProblemStatement.spatialDivergence self.velocity t x = 0
• navier_stokes (t : ℝ) : t ∈ Set.Ioi 0 → ∀ (x : Space), navierStokesResidual ν self.velocity self.pressure t x = f (t, x)
• energy_bounded : UniformFiniteEnergy (Set.Ici 0) self.velocity

def NavierStokesR3.ProblemStatement.candidateStatement (ν : ℝ) : Prop

The primary existence assertion at one fixed viscosity.

Equations

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

def NavierStokesR3.ProblemStatement.coreBreakdownStatement : Prop

The primary existence assertion for every positive viscosity.

Equations

• NavierStokesR3.ProblemStatement.coreBreakdownStatement = ∀ (ν : ℝ), 0 < ν → NavierStokesR3.ProblemStatement.candidateStatement ν

def NavierStokesR3.ProblemStatement.breakdownStatement : Prop

The full assertion of Theorem 1.1: at every positive viscosity there is a candidate whose same prescribed force and zero datum have no global smooth solution with uniformly bounded kinetic energy. This is a target proposition, not an asserted theorem.

Equations

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

theorem NavierStokesR3.ProblemStatement.candidateStatement_iff_nonempty (ν : ℝ) : candidateStatement ν ↔ Nonempty (Candidate ν)

Bundling the witnesses in Candidate does not change any hypothesis of the explicit primary existence assertion.

@[simp]

theorem NavierStokesR3.ProblemStatement.residual_at_viscosity_one (u : VelocityField) (p : PressureField) (t : ℝ) (x : Space) : navierStokesResidual 1 u p t x = NavierStokes.ProblemStatement.navierStokesResidual u p t x

The unit-viscosity residual is exactly the existing differential expression.

theorem NavierStokesR3.ProblemStatement.CompactPositiveTimeSupport.eq_zero_of_nonpos {f : VelocityField} (hf : CompactPositiveTimeSupport f) {t : ℝ} (ht : t ≤ 0) (x : Space) : f (t, x) = 0

The support convention really excludes forcing at every nonpositive time.

theorem NavierStokesR3.ProblemStatement.UniformFiniteEnergy.mono {times shorter : Set ℝ} {u : VelocityField} (hu : UniformFiniteEnergy times u) (hsub : shorter ⊆ times) : UniformFiniteEnergy shorter u

Restricting the set of times preserves the same energy bound.

theorem NavierStokesR3.ProblemStatement.zero_force_has_global_solution (ν : ℝ) : Nonempty (GlobalFiniteEnergySolution ν fun (x : NavierStokes.ProblemStatement.SpaceTime) => 0)

Zero velocity and pressure solve the equation for zero force at any viscosity. This checks that the competing-solution class is inhabited.

theorem NavierStokesR3.ProblemStatement.breakdown_implies_core (h : breakdownStatement) : coreBreakdownStatement

The full target contains the primary candidate-existence target.