Spatial Sobolev slices of regularized velocities

Positive-time differentiability and finite global dissipation put almost every spatial slice in representative-level H¹.

theorem CKN.Leray.regUniform_velocity_h1_slices (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (hU : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hDuMeasurable : Measurable Du) (hGradientEnergyFinite : ∫⁻ (t : ℝ) in Set.Ioi 0, ∫⁻ (x : Foundation.Parabolic.Vec3) in Set.univ, ENNReal.ofReal (spatialGradientSq u Du (x, t)) < ⊤) (hSpatialC1 : ∀ (t : ℝ), 0 < t → ∀ (i : Fin 3), ContDiff ℝ ↑1 fun (x : Foundation.Parabolic.Vec3) => u (x, t) i) (hDerivative : ∀ (t : ℝ), 0 < t → ∀ (x : Foundation.Parabolic.Vec3) (i j : Fin 3), (fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => u (y, t) i) x) (basisVec j) = Du (x, t) i j) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), ∃ (h : Fin 3 → H1Function Set.univ), (∀ (i : Fin 3) (x : Vec 3), (h i).toFun x = u (x, t) i) ∧ ∀ (i : Fin 3) (x : Vec 3) (j : Fin 3), (h i).grad x j = Du (x, t) i j

Almost every positive-time slice of a regularized velocity has the stated spatial weak gradient in L².