A classical ContDiffOn ℝ ⊤ solution on an open space-time box is AEStronglyMeasurable with respect to the restricted volume measure. These are the four per-local-box measurability conjuncts of CKN.IsSuitableWeakSolution for a smooth solution, obtained directly from smoothness rather than from weak-solution hypotheses.

theorem CIV.aestronglyMeasurable_of_contDiffOn_spaceTimeSet {β : Type u_1} [NormedAddCommGroup β] [NormedSpace ℝ β] {v : CKN.Foundation.Parabolic.ParabolicPoint → β} {Ω' : Set CKN.Foundation.Parabolic.Vec3} {J : Set ℝ} (hΩ' : IsOpen Ω') (hJ : IsOpen J) (hv : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => v z) (CKN.spaceTimeSet Ω' J)) : MeasureTheory.AEStronglyMeasurable v (MeasureTheory.volume.restrict (CKN.spaceTimeSet Ω' J))

A function v : ParabolicPoint → β that is ContDiffOn ℝ ⊤ on a space-time set spaceTimeSet Ω' J (with Ω' and J open) is AEStronglyMeasurable with respect to the restricted volume measure on that set. This is the measurability half of the per-local-box conjunct of CKN.IsSuitableWeakSolution for a classical ContDiffOn solution.

theorem CIV.aestronglyMeasurable_u_of_contDiffOn {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Ω' : Set CKN.Foundation.Parabolic.Vec3} {J : Set ℝ} (hΩ' : IsOpen Ω') (hJ : IsOpen J) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) (CKN.spaceTimeSet Ω' J)) : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (CKN.spaceTimeSet Ω' J))

The velocity field u of a classical ContDiffOn solution is AEStronglyMeasurable on any open space-time box.

theorem CIV.aestronglyMeasurable_p_of_contDiffOn {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω' : Set CKN.Foundation.Parabolic.Vec3} {J : Set ℝ} (hΩ' : IsOpen Ω') (hJ : IsOpen J) (hp : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p z) (CKN.spaceTimeSet Ω' J)) : MeasureTheory.AEStronglyMeasurable p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Ω' J))

The pressure field p of a classical ContDiffOn solution is AEStronglyMeasurable on any open space-time box.

theorem CIV.aestronglyMeasurable_f_of_contDiffOn {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Ω' : Set CKN.Foundation.Parabolic.Vec3} {J : Set ℝ} (hΩ' : IsOpen Ω') (hJ : IsOpen J) (hf : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) (CKN.spaceTimeSet Ω' J)) : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (CKN.spaceTimeSet Ω' J))

The forcing term f of a classical ContDiffOn solution is AEStronglyMeasurable on any open space-time box.

theorem CIV.aestronglyMeasurable_Du_of_contDiffOn {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Ω' : Set CKN.Foundation.Parabolic.Vec3} {J : Set ℝ} (hΩ' : IsOpen Ω') (hJ : IsOpen J) (hDu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Du z) (CKN.spaceTimeSet Ω' J)) : MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict (CKN.spaceTimeSet Ω' J))

The spatial gradient Du of a classical ContDiffOn solution is AEStronglyMeasurable on any open space-time box.