The compactness limit is a strong solution

The compactness limit of the regularized solutions, with the continuous representative of its gradient and the pressure of the Leray--Hopf limit, is a strong solution on the closed time interval (prop:lps-local-strong).

theorem ESS.LPS.lps_strong_limit_solution (ρ : CKN.Leray.RegMollifierProfile) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (Db : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (hb : IsLpsGoodTime (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => b z.1) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => Db z.1 i) 0) (T M : ℝ) (hT : 0 < T) (hclause : ∀ (ε : ℝ) (hε : 0 < ε), have Uε := CKN.Leray.regR12Velocity ρ ε hε b ⋯; have Dε := fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => Uε y i) j z; have D2ε := fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j k : Fin 3) => CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => Uε x i) j y) k z; (∀ t ∈ Set.Icc 0 T, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (Uε (x, t)) ^ 2 + CKN.spatialGradientSq Uε Dε (x, t) ≤ M) ∧ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), ∑ i : Fin 3, ∑ j : Fin 3, CKN.Foundation.Parabolic.vec3EuclideanNorm (D2ε z i j) ^ 2 ≤ M) : ∃ (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ), IsLpsStrongSolution 0 T u Du p ∧ (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, 0)) =ᵐ[MeasureTheory.volume] b

The limit of the regularized solutions with uniform H¹ and L²_tH² bounds is a strong solution on [0, T] with the good initial datum as trace (prop:lps-local-strong).