Classical time derivative of the regularized velocity

The zero-force weak momentum identity, paired with a compactly supported smooth spatial field η, gives each spatial pairing a weak time derivative (regularisedR12TimePairing_weakDeriv). It is classical by regularisedR12TimeCore_hasDerivAt_of_weakDeriv, and spatial integration by parts (regularisedR12TimeIBP_flux_eq) identifies it with the pairing of the right-hand side Δu − (J_ε u · ∇) u − ∇p. Integrating in time and exchanging the order of integration gives the paired time increments. Spatial separation (regularisedR12TimeSeparation_eq_zero_of_interval_tests) then gives the pointwise increments, and the fundamental theorem of calculus gives the classical time derivative of thm:regularised.

theorem CKN.Leray.regularisedR12_timeDerivative (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (hCurve : ∀ (t : ℝ), 0 ≤ t → (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) =ᵐ[MeasureTheory.volume] realVectorL2Representative (regularizedGlobalMildCurve ρ ε hε (realVectorL2OfCoordinateFunction (regUniformMollifiedInitial ρ ε hε a) ⋯) ⋯ t)) (hPressure : ∀ (z : Foundation.Parabolic.ParabolicPoint), 0 < z.2 → p z = forcedQuadPressure ρ ε hε (regularizedGlobalMildCurve ρ ε hε (realVectorL2OfCoordinateFunction (regUniformMollifiedInitial ρ ε hε a) ⋯) ⋯) z) (hU : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (spaceTimeSet Set.univ (Set.Ioi 0))) (hD : ∀ (i j : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z) (spaceTimeSet Set.univ (Set.Ioi 0))) (hDD : ∀ (i j k : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (x : Foundation.Parabolic.ParabolicPoint) => u x i) j y) k z) (spaceTimeSet Set.univ (Set.Ioi 0))) (hP : ContinuousOn p (spaceTimeSet Set.univ (Set.Ioi 0))) (hDp : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => p y) i z) (spaceTimeSet Set.univ (Set.Ioi 0))) (hUdiff : ∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0), ∀ (i : Fin 3), DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => u (x, z.2) i) z.1) (hDdiff : ∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0), ∀ (i j : Fin 3), DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j (x, z.2)) z.1) (hPdiff : ∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0), DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => p (x, z.2)) z.1) (z : Foundation.Parabolic.ParabolicPoint) : 0 < z.2 → ∀ (i : Fin 3), HasDerivAt (fun (s : ℝ) => u (z.1, s) i) (∑ j : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (x : Foundation.Parabolic.ParabolicPoint) => u x i) j y) j z - ∑ j : Fin 3, regUniformMollifiedVelocity ρ ε hε u z j * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z - spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => p y) i z) z.2

The canonical pointwise regularized velocity has its classical time derivative given by the regularized momentum equation (thm:regularised).