Restriction to smaller space-time cylinders

Weak derivatives and the differential inequality restrict to smaller product domains, as used in the radius iteration of thm:uc.

theorem ESS.uc_restrict_data (c₁ : ℝ) (Ω' Ω : Set CKN.Foundation.Parabolic.Vec3) (I' I : Set ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hΩ : IsOpen Ω) (hI : IsOpen I) (hΩsub : Ω' ⊆ Ω) (hIsub : I' ⊆ I) (hcont : ContinuousOn w (Ω ×ˢ I)) (hweak : CKN.HasSpaceTimeWeakDerivs Ω I w Dw D2w Dtw) (hL2 : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Ω I, ‖w z‖ₑ ^ 2 + ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤) (hineq : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet Ω I), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2w Dtw z) ≤ c₁ * (CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) + √(CKN.spatialGradientSq w Dw z))) : ContinuousOn w (Ω' ×ˢ I') ∧ CKN.HasSpaceTimeWeakDerivs Ω' I' w Dw D2w Dtw ∧ ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Ω' I', ‖w z‖ₑ ^ 2 + ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤ ∧ ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet Ω' I'), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2w Dtw z) ≤ c₁ * (CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) + √(CKN.spatialGradientSq w Dw z))

Restriction preserves the weak derivative identities and all source integrability and differential-inequality hypotheses.