Calculus of the physical Navier--Stokes residual

These identities concern the ordinary Frechet derivatives used by the actual PDE target in ProblemStatement. The velocity hypotheses give two continuous spatial derivatives on the time slice and a differentiable time slice at the point in question. No abstract differential operators are assumed linear.

theorem NavierStokes.ResidualCalculus.temporalDerivative_add (u e : ProblemStatement.VelocityField) (t : ℝ) (x : ProblemStatement.Space) (hu : DifferentiableAt ℝ (fun (s : ℝ) => u (s, x)) t) (he : DifferentiableAt ℝ (fun (s : ℝ) => e (s, x)) t) : ProblemStatement.temporalDerivative (fun (z : ProblemStatement.SpaceTime) => u z + e z) t x = ProblemStatement.temporalDerivative u t x + ProblemStatement.temporalDerivative e t x

Time differentiation is additive for differentiable velocity time slices.

theorem NavierStokes.ResidualCalculus.spatialDerivative_add (u e : ProblemStatement.VelocityField) (t : ℝ) (x : ProblemStatement.Space) (hu : DifferentiableAt ℝ (fun (y : ProblemStatement.Space) => u (t, y)) x) (he : DifferentiableAt ℝ (fun (y : ProblemStatement.Space) => e (t, y)) x) : ProblemStatement.spatialDerivative (fun (z : ProblemStatement.SpaceTime) => u z + e z) t x = ProblemStatement.spatialDerivative u t x + ProblemStatement.spatialDerivative e t x

The spatial derivative is additive under actual spatial differentiability.

theorem NavierStokes.ResidualCalculus.pressureGradient_add (p q : ProblemStatement.PressureField) (t : ℝ) (x : ProblemStatement.Space) (hp : DifferentiableAt ℝ (fun (y : ProblemStatement.Space) => p (t, y)) x) (hq : DifferentiableAt ℝ (fun (y : ProblemStatement.Space) => q (t, y)) x) : ProblemStatement.pressureGradient (fun (z : ProblemStatement.SpaceTime) => p z + q z) t x = ProblemStatement.pressureGradient p t x + ProblemStatement.pressureGradient q t x

Pressure-gradient additivity follows from derivative additivity and the fixed Euclidean coordinate basis in the PDE target.

theorem NavierStokes.ResidualCalculus.spatialDivergence_add (u e : ProblemStatement.VelocityField) (t : ℝ) (x : ProblemStatement.Space) (hu : DifferentiableAt ℝ (fun (y : ProblemStatement.Space) => u (t, y)) x) (he : DifferentiableAt ℝ (fun (y : ProblemStatement.Space) => e (t, y)) x) : ProblemStatement.spatialDivergence (fun (z : ProblemStatement.SpaceTime) => u z + e z) t x = ProblemStatement.spatialDivergence u t x + ProblemStatement.spatialDivergence e t x

Divergence remains additive for these same genuine spatial derivatives.

theorem NavierStokes.ResidualCalculus.differentiable_spatial_direction (u : ProblemStatement.VelocityField) (t : ℝ) (hu : ContDiff ℝ 2 fun (y : ProblemStatement.Space) => u (t, y)) (v : ProblemStatement.Space) : Differentiable ℝ fun (y : ProblemStatement.Space) => (ProblemStatement.spatialDerivative u t y) v

The spatial C² hypothesis gives differentiability of each first directional derivative. This is the second-derivative fact needed for the Laplacian.

theorem NavierStokes.ResidualCalculus.spatialLaplacian_add (u e : ProblemStatement.VelocityField) (t : ℝ) (x : ProblemStatement.Space) (hu : ContDiff ℝ 2 fun (y : ProblemStatement.Space) => u (t, y)) (he : ContDiff ℝ 2 fun (y : ProblemStatement.Space) => e (t, y)) : ProblemStatement.spatialLaplacian (fun (z : ProblemStatement.SpaceTime) => u z + e z) t x = ProblemStatement.spatialLaplacian u t x + ProblemStatement.spatialLaplacian e t x

Additivity of the concrete iterated-derivative Laplacian on C² slices.

theorem NavierStokes.ResidualCalculus.advection_add (u e : ProblemStatement.VelocityField) (t : ℝ) (x : ProblemStatement.Space) (hu : DifferentiableAt ℝ (fun (y : ProblemStatement.Space) => u (t, y)) x) (he : DifferentiableAt ℝ (fun (y : ProblemStatement.Space) => e (t, y)) x) : ProblemStatement.advection (fun (z : ProblemStatement.SpaceTime) => u z + e z) t x = ProblemStatement.advection u t x + (ProblemStatement.spatialDerivative u t x) (e (t, x)) + (ProblemStatement.spatialDerivative e t x) (u (t, x)) + ProblemStatement.advection e t x

The quadratic advection term produces exactly its two cross terms and the self-advection of the perturbation.

theorem NavierStokes.ResidualCalculus.navierStokesResidual_add_sub (u e : ProblemStatement.VelocityField) (p q : ProblemStatement.PressureField) (t : ℝ) (x : ProblemStatement.Space) (hut : DifferentiableAt ℝ (fun (s : ℝ) => u (s, x)) t) (het : DifferentiableAt ℝ (fun (s : ℝ) => e (s, x)) t) (hu : ContDiff ℝ 2 fun (y : ProblemStatement.Space) => u (t, y)) (he : ContDiff ℝ 2 fun (y : ProblemStatement.Space) => e (t, y)) (hp : DifferentiableAt ℝ (fun (y : ProblemStatement.Space) => p (t, y)) x) (hq : DifferentiableAt ℝ (fun (y : ProblemStatement.Space) => q (t, y)) x) : ProblemStatement.navierStokesResidual (fun (z : ProblemStatement.SpaceTime) => u z + e z) (fun (z : ProblemStatement.SpaceTime) => p z + q z) t x - ProblemStatement.navierStokesResidual u p t x = ProblemStatement.temporalDerivative e t x - ProblemStatement.spatialLaplacian e t x + ProblemStatement.pressureGradient q t x + (ProblemStatement.spatialDerivative u t x) (e (t, x)) + (ProblemStatement.spatialDerivative e t x) (u (t, x)) + (ProblemStatement.spatialDerivative e t x) (e (t, x))

Exact perturbation formula for the physical residual, at viscosity one. Every operator in this statement is the concrete operator in ProblemStatement.

theorem NavierStokes.ResidualCalculus.spatial_contDiff_of_presingular_smooth {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (g : ProblemStatement.SpaceTime → V) (hg : ContDiffOn ℝ (↑⊤) g ProblemStatement.preSingularDomain) (t : ℝ) (ht : t ∈ Set.Ioo 0 1) : ContDiff ℝ ↑⊤ fun (y : ProblemStatement.Space) => g (t, y)

A spatial slice of a field smooth on the actual presingular domain is globally smooth in space at each interior time.

theorem NavierStokes.ResidualCalculus.temporal_differentiable_of_presingular_smooth {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (g : ProblemStatement.SpaceTime → V) (hg : ContDiffOn ℝ (↑⊤) g ProblemStatement.preSingularDomain) (t : ℝ) (ht : t ∈ Set.Ioo 0 1) (x : ProblemStatement.Space) : DifferentiableAt ℝ (fun (s : ℝ) => g (s, x)) t

Interior time differentiability follows from the same domain smoothness; no extension through the singular time is assumed.

theorem NavierStokes.ResidualCalculus.navierStokesResidual_add_sub_of_smooth (u e : ProblemStatement.VelocityField) (p q : ProblemStatement.PressureField) (hu : ContDiffOn ℝ (↑⊤) u ProblemStatement.preSingularDomain) (he : ContDiffOn ℝ (↑⊤) e ProblemStatement.preSingularDomain) (hp : ContDiffOn ℝ (↑⊤) p ProblemStatement.preSingularDomain) (hq : ContDiffOn ℝ (↑⊤) q ProblemStatement.preSingularDomain) (t : ℝ) (ht : t ∈ Set.Ioo 0 1) (x : ProblemStatement.Space) : ProblemStatement.navierStokesResidual (fun (z : ProblemStatement.SpaceTime) => u z + e z) (fun (z : ProblemStatement.SpaceTime) => p z + q z) t x - ProblemStatement.navierStokesResidual u p t x = ProblemStatement.temporalDerivative e t x - ProblemStatement.spatialLaplacian e t x + ProblemStatement.pressureGradient q t x + (ProblemStatement.spatialDerivative u t x) (e (t, x)) + (ProblemStatement.spatialDerivative e t x) (u (t, x)) + (ProblemStatement.spatialDerivative e t x) (e (t, x))

The perturbation identity applies directly to the smoothness conditions appearing in the candidate PDE statement, at every interior time.

theorem NavierStokes.ResidualCalculus.spatialDerivative_const_smul (u : ProblemStatement.VelocityField) (t : ℝ) (x : ProblemStatement.Space) (c : ℝ) (hu : DifferentiableAt ℝ (fun (y : ProblemStatement.Space) => u (t, y)) x) : ProblemStatement.spatialDerivative (fun (z : ProblemStatement.SpaceTime) => c • u z) t x = c • ProblemStatement.spatialDerivative u t x

A constant spatial scalar factors out of the actual spatial derivative.

theorem NavierStokes.ResidualCalculus.pressureGradient_const_smul (p : ProblemStatement.PressureField) (t : ℝ) (x : ProblemStatement.Space) (c : ℝ) (hp : DifferentiableAt ℝ (fun (y : ProblemStatement.Space) => p (t, y)) x) : ProblemStatement.pressureGradient (fun (z : ProblemStatement.SpaceTime) => c • p z) t x = c • ProblemStatement.pressureGradient p t x

Constant-scalar linearity of the actual pressure gradient.

theorem NavierStokes.ResidualCalculus.spatialDivergence_const_smul (u : ProblemStatement.VelocityField) (t : ℝ) (x : ProblemStatement.Space) (c : ℝ) (hu : DifferentiableAt ℝ (fun (y : ProblemStatement.Space) => u (t, y)) x) : ProblemStatement.spatialDivergence (fun (z : ProblemStatement.SpaceTime) => c • u z) t x = c * ProblemStatement.spatialDivergence u t x

Constant-scalar linearity of divergence, using coordinate evaluation.

theorem NavierStokes.ResidualCalculus.spatialLaplacian_const_smul (u : ProblemStatement.VelocityField) (t : ℝ) (x : ProblemStatement.Space) (c : ℝ) (hu : ContDiff ℝ 2 fun (y : ProblemStatement.Space) => u (t, y)) : ProblemStatement.spatialLaplacian (fun (z : ProblemStatement.SpaceTime) => c • u z) t x = c • ProblemStatement.spatialLaplacian u t x

Constant-scalar linearity of the concrete second spatial derivative.

theorem NavierStokes.ResidualCalculus.advection_const_smul (u : ProblemStatement.VelocityField) (t : ℝ) (x : ProblemStatement.Space) (c : ℝ) (hu : DifferentiableAt ℝ (fun (y : ProblemStatement.Space) => u (t, y)) x) : ProblemStatement.advection (fun (z : ProblemStatement.SpaceTime) => c • u z) t x = (c * c) • ProblemStatement.advection u t x

Velocity scaling squares in advection, because both the direction and the spatial derivative scale.

theorem NavierStokes.ResidualCalculus.temporalDerivative_time_smul (u : ProblemStatement.VelocityField) (a : ℝ → ℝ) (t : ℝ) (x : ProblemStatement.Space) (ha : DifferentiableAt ℝ a t) (hu : DifferentiableAt ℝ (fun (s : ℝ) => u (s, x)) t) : ProblemStatement.temporalDerivative (fun (z : ProblemStatement.SpaceTime) => a z.1 • u z) t x = a t • ProblemStatement.temporalDerivative u t x + (fderiv ℝ a t) 1 • u (t, x)

The time derivative of a switched velocity includes the derivative of the switch; it is proved using the Frechet derivative product rule.

theorem NavierStokes.ResidualCalculus.navierStokesResidual_time_smul (u : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (a : ℝ → ℝ) (t : ℝ) (x : ProblemStatement.Space) (ha : DifferentiableAt ℝ a t) (hut : DifferentiableAt ℝ (fun (s : ℝ) => u (s, x)) t) (hu : ContDiff ℝ 2 fun (y : ProblemStatement.Space) => u (t, y)) (hp : DifferentiableAt ℝ (fun (y : ProblemStatement.Space) => p (t, y)) x) : ProblemStatement.navierStokesResidual (fun (z : ProblemStatement.SpaceTime) => a z.1 • u z) (fun (z : ProblemStatement.SpaceTime) => a z.1 • p z) t x = a t • ProblemStatement.navierStokesResidual u p t x + (fderiv ℝ a t) 1 • u (t, x) + (a t * a t - a t) • ProblemStatement.advection u t x

Exact time-switch identity for the physical PDE, when both velocity and pressure are multiplied by the same scalar time switch.

theorem NavierStokes.ResidualCalculus.time_smul_divergence_free (u : ProblemStatement.VelocityField) (a : ℝ → ℝ) (t : ℝ) (x : ProblemStatement.Space) (hu : DifferentiableAt ℝ (fun (y : ProblemStatement.Space) => u (t, y)) x) (hdiv : ProblemStatement.spatialDivergence u t x = 0) : ProblemStatement.spatialDivergence (fun (z : ProblemStatement.SpaceTime) => a z.1 • u z) t x = 0

A scalar time switch preserves the divergence-free condition.