Classical solution slices on the unit cylinder

These lemmas extract the smoothness and divergence-free hypotheses of IsClassicalSolutionOn on time slices inside the unit cylinder, producing the ball-restricted hypotheses that the closure-lemma assembly's Sobolev and elliptic steps consume.

theorem CIV.hdiv_of_isClassicalSolutionOn {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {U : Set CKN.Foundation.Parabolic.Vec3} {tη : ℝ} (hsol : IsClassicalSolutionOn u p f unitCylinder) (hUt : ∀ t ∈ Set.Ioo tη 0, ∀ x ∈ U, (x, t) ∈ unitCylinder) (t : ℝ) : t ∈ Set.Ioo tη 0 → ∀ x ∈ U, ∑ j : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, t) j) x) (CKN.basisVec j) = 0

Reading the divergence-free clause of IsClassicalSolutionOn off as a time-sliced, ball-restricted hypothesis: for every t ∈ (tη, 0) and x ∈ U the point (x, t) lies in the cylinder, so ∑ j, spatialPartial (fun w => u w j) j (x, t) = 0 holds.

theorem CIV.hdiv_of_isClassicalSolutionOn_vec3Ball {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Rstar : ℝ} (hRstar : Rstar ≤ 1) (hsol : IsClassicalSolutionOn u p f unitCylinder) (t : ℝ) : t ∈ Set.Ioo (-1) 0 → ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar, ∑ j : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, t) j) x) (CKN.basisVec j) = 0

Specialising hdiv_of_isClassicalSolutionOn to the unit cylinder: any Rstar ≤ 1 gives a ball B(0, Rstar) that is contained in B(0, 1), so the pair (x, t) stays in the unit cylinder whenever t ∈ (-1, 0) and x ∈ B(0, Rstar).

theorem CIV.hu_of_isClassicalSolutionOn_vec3Ball {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Rstar : ℝ} (hRstar : Rstar ≤ 1) (hsol : IsClassicalSolutionOn u p f unitCylinder) (t : ℝ) : t ∈ Set.Ioo (-1) 0 → ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) (CKN.Foundation.Parabolic.vec3Ball 0 Rstar)

Reading the smoothness clause of IsClassicalSolutionOn off as a time-sliced, ball-restricted hypothesis: hsol.1 gives ContDiffOn on unitCylinder = B(1) × (-1, 0). Restricting to B(Rstar) × (-1, 0) and then slicing at t ∈ (-1, 0) yields ContDiffOn ℝ (⊤ : ℕ∞) of each component of u(·, t) on B(Rstar, 0).