Classical slice derivatives as weak derivatives

Joint differentiability on a positive-time interval gives the slice weak derivative identity needed to compare the mild equation with the forced weak momentum identity.

theorem CKN.Leray.forcedMollifiedGrad_ae_eq_classical_of_ae_eq (v u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (t : ℝ) (i j : Fin 3) (hVloc : MeasureTheory.LocallyIntegrable (fun (x : Foundation.Parabolic.Vec3) => v (x, t) i) MeasureTheory.volume) (hVae : (fun (x : Foundation.Parabolic.Vec3) => v (x, t)) =ᵐ[MeasureTheory.volume] fun (x : Foundation.Parabolic.Vec3) => u (x, t)) (hC1 : ContDiff ℝ 1 fun (x : Foundation.Parabolic.Vec3) => u (x, t) i) : (fun (x : Foundation.Parabolic.Vec3) => forcedMollifiedGrad v (x, t) i j) =ᵐ[MeasureTheory.volume] fun (x : Foundation.Parabolic.Vec3) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j (x, t)

If a forced representative agrees almost everywhere with a C¹ slice, its mollified weak gradient agrees almost everywhere with the classical spatial partial derivative of that slice.