Regularity and locality of the concrete Navier--Stokes residual

All operators below are the ordinary derivatives in ProblemStatement. The main regularity theorem is on an open spacetime domain; it does not differentiate an unspecified extension through a time boundary.

theorem NavierStokes.ResidualRegularity.contDiffOn_space_fderiv {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {s : Set ProblemStatement.SpaceTime} {g : ProblemStatement.SpaceTime → V} {m n : WithTop ℕ∞} (hs : IsOpen s) (hg : ContDiffOn ℝ n g s) (hmn : m + 1 ≤ n) : ContDiffOn ℝ m (fun (z : ProblemStatement.SpaceTime) => fderiv ℝ (fun (y : ProblemStatement.Space) => g (z.1, y)) z.2) s

Parameter-dependent spatial differentiation lowers regularity by one. The output is the actual Fréchet derivative of each spatial slice.

theorem NavierStokes.ResidualRegularity.contDiffOn_time_fderiv {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {s : Set ProblemStatement.SpaceTime} {g : ProblemStatement.SpaceTime → V} {m n : WithTop ℕ∞} (hs : IsOpen s) (hg : ContDiffOn ℝ n g s) (hmn : m + 1 ≤ n) : ContDiffOn ℝ m (fun (z : ProblemStatement.SpaceTime) => fderiv ℝ (fun (t : ℝ) => g (t, z.2)) z.1) s

Parameter-dependent time differentiation lowers regularity by one.

theorem NavierStokes.ResidualRegularity.contDiffOn_temporalDerivative {s : Set ProblemStatement.SpaceTime} {u : ProblemStatement.VelocityField} (hs : IsOpen s) (hu : ContDiffOn ℝ (↑⊤) u s) : ContDiffOn ℝ (↑⊤) (fun (z : ProblemStatement.SpaceTime) => ProblemStatement.temporalDerivative u z.1 z.2) s

theorem NavierStokes.ResidualRegularity.contDiffOn_spatialDerivative {s : Set ProblemStatement.SpaceTime} {u : ProblemStatement.VelocityField} (hs : IsOpen s) (hu : ContDiffOn ℝ (↑⊤) u s) : ContDiffOn ℝ (↑⊤) (fun (z : ProblemStatement.SpaceTime) => ProblemStatement.spatialDerivative u z.1 z.2) s

theorem NavierStokes.ResidualRegularity.contDiffOn_advection {s : Set ProblemStatement.SpaceTime} {u : ProblemStatement.VelocityField} (hs : IsOpen s) (hu : ContDiffOn ℝ (↑⊤) u s) : ContDiffOn ℝ (↑⊤) (fun (z : ProblemStatement.SpaceTime) => ProblemStatement.advection u z.1 z.2) s

theorem NavierStokes.ResidualRegularity.contDiffOn_pressureGradient {s : Set ProblemStatement.SpaceTime} {p : ProblemStatement.PressureField} (hs : IsOpen s) (hp : ContDiffOn ℝ (↑⊤) p s) : ContDiffOn ℝ (↑⊤) (fun (z : ProblemStatement.SpaceTime) => ProblemStatement.pressureGradient p z.1 z.2) s

theorem NavierStokes.ResidualRegularity.contDiffOn_spatialLaplacian {s : Set ProblemStatement.SpaceTime} {u : ProblemStatement.VelocityField} (hs : IsOpen s) (hu : ContDiffOn ℝ (↑⊤) u s) : ContDiffOn ℝ (↑⊤) (fun (z : ProblemStatement.SpaceTime) => ProblemStatement.spatialLaplacian u z.1 z.2) s

theorem NavierStokes.ResidualRegularity.contDiffOn_residual {s : Set ProblemStatement.SpaceTime} {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hs : IsOpen s) (hu : ContDiffOn ℝ (↑⊤) u s) (hp : ContDiffOn ℝ (↑⊤) p s) : ContDiffOn ℝ (↑⊤) (fun (z : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual u p z.1 z.2) s

Jointly smooth velocity and pressure have a jointly smooth actual residual.

theorem NavierStokes.ResidualRegularity.contDiffOn_residual_product {times : Set ℝ} {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (ht : IsOpen times) (hu : ContDiffOn ℝ (↑⊤) u (times ×ˢ Set.univ)) (hp : ContDiffOn ℝ (↑⊤) p (times ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual u p z.1 z.2) (times ×ˢ Set.univ)

theorem NavierStokes.ResidualRegularity.contDiffOn_residual_interior {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hu : ContDiffOn ℝ (↑⊤) u ProblemStatement.preSingularDomain) (hp : ContDiffOn ℝ (↑⊤) p ProblemStatement.preSingularDomain) : ContDiffOn ℝ (↑⊤) (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual u p z.1 z.2) (Set.Ioo 0 1 ×ˢ Set.univ)

The candidate's relative smoothness hypotheses suffice at all interior times.

Exact spatial periods

theorem NavierStokes.ResidualRegularity.space_fderiv_periods {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {g : ProblemStatement.SpaceTime → V} {times : Set ℝ} (hg : ProblemStatement.UnitSpatialPeriodsOn times g) : ProblemStatement.UnitSpatialPeriodsOn times fun (z : ProblemStatement.SpaceTime) => fderiv ℝ (fun (y : ProblemStatement.Space) => g (z.1, y)) z.2

A spatial unit period passes to the actual derivative of the spatial slice. No differentiability hypothesis is needed for this translation rule.

theorem NavierStokes.ResidualRegularity.temporalDerivative_periods {u : ProblemStatement.VelocityField} {times : Set ℝ} (htimes : IsOpen times) (hu : ProblemStatement.UnitSpatialPeriodsOn times u) : ProblemStatement.UnitSpatialPeriodsOn times fun (z : ProblemStatement.SpaceTime) => ProblemStatement.temporalDerivative u z.1 z.2

Time differentiation preserves spatial periods when the period identity holds on an open neighborhood of the time being differentiated.

theorem NavierStokes.ResidualRegularity.spatialDerivative_periods {u : ProblemStatement.VelocityField} {times : Set ℝ} (hu : ProblemStatement.UnitSpatialPeriodsOn times u) : ProblemStatement.UnitSpatialPeriodsOn times fun (z : ProblemStatement.SpaceTime) => ProblemStatement.spatialDerivative u z.1 z.2

theorem NavierStokes.ResidualRegularity.advection_periods {u : ProblemStatement.VelocityField} {times : Set ℝ} (hu : ProblemStatement.UnitSpatialPeriodsOn times u) : ProblemStatement.UnitSpatialPeriodsOn times fun (z : ProblemStatement.SpaceTime) => ProblemStatement.advection u z.1 z.2

theorem NavierStokes.ResidualRegularity.pressureGradient_periods {p : ProblemStatement.PressureField} {times : Set ℝ} (hp : ProblemStatement.UnitSpatialPeriodsOn times p) : ProblemStatement.UnitSpatialPeriodsOn times fun (z : ProblemStatement.SpaceTime) => ProblemStatement.pressureGradient p z.1 z.2

theorem NavierStokes.ResidualRegularity.spatialLaplacian_periods {u : ProblemStatement.VelocityField} {times : Set ℝ} (hu : ProblemStatement.UnitSpatialPeriodsOn times u) : ProblemStatement.UnitSpatialPeriodsOn times fun (z : ProblemStatement.SpaceTime) => ProblemStatement.spatialLaplacian u z.1 z.2

theorem NavierStokes.ResidualRegularity.residual_periods {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {times : Set ℝ} (htimes : IsOpen times) (hu : ProblemStatement.UnitSpatialPeriodsOn times u) (hp : ProblemStatement.UnitSpatialPeriodsOn times p) : ProblemStatement.UnitSpatialPeriodsOn times fun (z : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual u p z.1 z.2

The concrete residual has the same unit spatial periods as its inputs. Openness is needed only to pass the period identity through time differentiation.

theorem NavierStokes.ResidualRegularity.residual_periods_interior {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} (hu : ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 1) u) (hp : ProblemStatement.UnitSpatialPeriodsOn (Set.Ico 0 1) p) : ProblemStatement.UnitSpatialPeriodsOn (Set.Ioo 0 1) fun (z : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual u p z.1 z.2

Locality, without differentiability assumptions

theorem NavierStokes.ResidualRegularity.space_fderiv_congr {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f g : ProblemStatement.SpaceTime → V} {z : ProblemStatement.SpaceTime} (h : f =ᶠ[nhds z] g) : fderiv ℝ (fun (y : ProblemStatement.Space) => f (z.1, y)) z.2 = fderiv ℝ (fun (y : ProblemStatement.Space) => g (z.1, y)) z.2

theorem NavierStokes.ResidualRegularity.time_fderiv_congr {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f g : ProblemStatement.SpaceTime → V} {z : ProblemStatement.SpaceTime} (h : f =ᶠ[nhds z] g) : fderiv ℝ (fun (t : ℝ) => f (t, z.2)) z.1 = fderiv ℝ (fun (t : ℝ) => g (t, z.2)) z.1

theorem NavierStokes.ResidualRegularity.temporalDerivative_congr {u v : ProblemStatement.VelocityField} {z : ProblemStatement.SpaceTime} (h : u =ᶠ[nhds z] v) : ProblemStatement.temporalDerivative u z.1 z.2 = ProblemStatement.temporalDerivative v z.1 z.2

theorem NavierStokes.ResidualRegularity.spatialDerivative_congr {u v : ProblemStatement.VelocityField} {z : ProblemStatement.SpaceTime} (h : u =ᶠ[nhds z] v) : ProblemStatement.spatialDerivative u z.1 z.2 = ProblemStatement.spatialDerivative v z.1 z.2

theorem NavierStokes.ResidualRegularity.advection_congr {u v : ProblemStatement.VelocityField} {z : ProblemStatement.SpaceTime} (h : u =ᶠ[nhds z] v) : ProblemStatement.advection u z.1 z.2 = ProblemStatement.advection v z.1 z.2

theorem NavierStokes.ResidualRegularity.pressureGradient_congr {p q : ProblemStatement.PressureField} {z : ProblemStatement.SpaceTime} (h : p =ᶠ[nhds z] q) : ProblemStatement.pressureGradient p z.1 z.2 = ProblemStatement.pressureGradient q z.1 z.2

theorem NavierStokes.ResidualRegularity.spatialLaplacian_congr {u v : ProblemStatement.VelocityField} {z : ProblemStatement.SpaceTime} (h : u =ᶠ[nhds z] v) : ProblemStatement.spatialLaplacian u z.1 z.2 = ProblemStatement.spatialLaplacian v z.1 z.2

theorem NavierStokes.ResidualRegularity.residual_congr {u v : ProblemStatement.VelocityField} {p q : ProblemStatement.PressureField} {z : ProblemStatement.SpaceTime} (hu : u =ᶠ[nhds z] v) (hp : p =ᶠ[nhds z] q) : ProblemStatement.navierStokesResidual u p z.1 z.2 = ProblemStatement.navierStokesResidual v q z.1 z.2

Local agreement of the two inputs implies agreement of their concrete residual at the point, including the iterated spatial derivative.

theorem NavierStokes.ResidualRegularity.residual_eventuallyEq {u v : ProblemStatement.VelocityField} {p q : ProblemStatement.PressureField} {z : ProblemStatement.SpaceTime} (hu : u =ᶠ[nhds z] v) (hp : p =ᶠ[nhds z] q) : (fun (w : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual u p w.1 w.2) =ᶠ[nhds z] fun (w : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual v q w.1 w.2

theorem NavierStokes.ResidualRegularity.residual_eqOn {u v : ProblemStatement.VelocityField} {p q : ProblemStatement.PressureField} {s : Set ProblemStatement.SpaceTime} (hs : IsOpen s) (hu : Set.EqOn u v s) (hp : Set.EqOn p q s) : Set.EqOn (fun (z : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual u p z.1 z.2) (fun (z : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual v q z.1 z.2) s

theorem NavierStokes.ResidualRegularity.residual_eq_zero_of_eventually_zero {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {z : ProblemStatement.SpaceTime} (hu : u =ᶠ[nhds z] fun (x : ProblemStatement.SpaceTime) => 0) (hp : p =ᶠ[nhds z] fun (x : ProblemStatement.SpaceTime) => 0) : ProblemStatement.navierStokesResidual u p z.1 z.2 = 0

A local zero extension of velocity and pressure has zero residual.

theorem NavierStokes.ResidualRegularity.residual_eventually_zero {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {z : ProblemStatement.SpaceTime} (hu : u =ᶠ[nhds z] fun (x : ProblemStatement.SpaceTime) => 0) (hp : p =ᶠ[nhds z] fun (x : ProblemStatement.SpaceTime) => 0) : (fun (w : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual u p w.1 w.2) =ᶠ[nhds z] fun (x : ProblemStatement.SpaceTime) => 0