Classical Navier–Stokes solutions with prescribed initial data

The periodic and finite-energy comparison arguments share the same local equation. SolutionOn records this common contract independently of periodicity and energy bounds. Viscosity, initial time, initial velocity, and the time set are parameters. Smoothness is relative to the time set; the equation is imposed only after the initial time, so no derivative of an arbitrary extension across that boundary is used.

This interface adapts the shared solution vocabulary of https://github.com/Code4me2/NavierStokesAndEuler/tree/26e896edbdbe1215c0d50ddba24b2b6453646f5f.

noncomputable def NavierStokes.viscousResidual (viscosity : ℝ) (velocity : ProblemStatement.VelocityField) (pressure : ProblemStatement.PressureField) (time : ℝ) (position : ProblemStatement.Space) : ProblemStatement.Space

The Navier–Stokes equation's left-hand side at an arbitrary viscosity.

Equations

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

@[simp]

theorem NavierStokes.viscousResidual_one (velocity : ProblemStatement.VelocityField) (pressure : ProblemStatement.PressureField) (time : ℝ) (position : ProblemStatement.Space) : viscousResidual 1 velocity pressure time position = ProblemStatement.navierStokesResidual velocity pressure time position

@[simp]

theorem NavierStokes.viscousResidual_zero_fields (viscosity time : ℝ) (position : ProblemStatement.Space) : viscousResidual viscosity (fun (x : ProblemStatement.SpaceTime) => 0) (fun (x : ProblemStatement.SpaceTime) => 0) time position = 0

structure NavierStokes.SolutionOn (viscosity initialTime : ℝ) (initialVelocity : ProblemStatement.Space → ProblemStatement.Space) (times : Set ℝ) (force velocity : ProblemStatement.VelocityField) (pressure : ProblemStatement.PressureField) : Prop

A smooth incompressible solution with specified initial value. The initial value is required at initialTime even if the chosen time set omits that point. No positivity assumption on viscosity is needed for the definition or restriction API.

• velocity_smooth : ContDiffOn ℝ (↑⊤) velocity (times ×ˢ Set.univ)
• pressure_smooth : ContDiffOn ℝ (↑⊤) pressure (times ×ˢ Set.univ)
• initial_velocity (position : ProblemStatement.Space) : velocity (initialTime, position) = initialVelocity position
• divergence_free (time : ℝ) : time ∈ times → ∀ (position : ProblemStatement.Space), ProblemStatement.spatialDivergence velocity time position = 0
• navier_stokes (time : ℝ) : time ∈ times → initialTime < time → ∀ (position : ProblemStatement.Space), viscousResidual viscosity velocity pressure time position = force (time, position)

theorem NavierStokes.SolutionOn.mono {viscosity initialTime : ℝ} {initialVelocity : ProblemStatement.Space → ProblemStatement.Space} {times smallerTimes : Set ℝ} {force velocity : ProblemStatement.VelocityField} {pressure : ProblemStatement.PressureField} (solution : SolutionOn viscosity initialTime initialVelocity times force velocity pressure) (subset : smallerTimes ⊆ times) : SolutionOn viscosity initialTime initialVelocity smallerTimes force velocity pressure

Restrict a solution's regularity and equation to a smaller time set.

theorem NavierStokes.SolutionOn.zero (viscosity initialTime : ℝ) (times : Set ℝ) : SolutionOn viscosity initialTime (fun (x : ProblemStatement.Space) => 0) times (fun (x : ProblemStatement.SpaceTime) => 0) (fun (x : ProblemStatement.SpaceTime) => 0) fun (x : ProblemStatement.SpaceTime) => 0

The identically zero fields solve the equation with zero force and initial velocity.

theorem NavierStokes.ProblemStatement.CandidateProperties.toSolutionOn {velocity force : VelocityField} {pressure : PressureField} (candidate : CandidateProperties velocity pressure force) : SolutionOn 1 0 (fun (x : Space) => 0) (Set.Ico 0 1) force velocity pressure

The periodic blow-up candidate satisfies the shared local solution contract.