Restriction of a suitable weak solution to a smaller open subcylinder #
The missing step of the printed proof of Corollary 2.3 (cor:interior:nonanalytic):
showing that the hypotheses of thm:main hold on the smaller cylinder B(R')x(-δ',0) with
ρ(t) replaced by min{ρ(t),R'/2} requires knowing that a suitable weak solution on the
standing cylinder is still a suitable weak solution on that smaller cylinder.
theorem
CIV.spatialPartial_eq_zero_of_notMem_tsupport
{φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{z : CKN.Foundation.Parabolic.Vec3 × ℝ}
(hz : z ∉ tsupport φ)
(i : Fin 3)
:
theorem
CIV.timePartial_eq_zero_of_notMem_tsupport
{φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{z : CKN.Foundation.Parabolic.Vec3 × ℝ}
(hz : z ∉ tsupport φ)
:
theorem
CIV.tsupport_spatialPartial_subset
(φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(i : Fin 3)
:
(tsupport fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialPartial φ i w) ⊆ tsupport φ
theorem
CIV.spatialSecondPartial_eq_zero_of_notMem_tsupport
{φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{z : CKN.Foundation.Parabolic.Vec3 × ℝ}
(hz : z ∉ tsupport φ)
(i j : Fin 3)
:
theorem
CIV.notMem_tsupport_apply_of_notMem_tsupport
{φ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3}
{z : CKN.Foundation.Parabolic.Vec3 × ℝ}
(hz : z ∉ tsupport φ)
(i : Fin 3)
:
z ∉ tsupport fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => φ w i
theorem
CIV.localBox_mono
{Ω Ω' : Set CKN.Foundation.Parabolic.Vec3}
{I I' : Set ℝ}
(hΩ : Ω' ⊆ Ω)
(hI : I' ⊆ I)
{Ω'' : Set CKN.Foundation.Parabolic.Vec3}
{J : Set ℝ}
(hbox : CKN.localBox Ω' I' Ω'' J)
:
CKN.localBox Ω I Ω'' J
theorem
CIV.setIntegral_spaceTimeSet_eq_of_support_subset
{Ω Ω' : Set CKN.Foundation.Parabolic.Vec3}
{I I' : Set ℝ}
{F : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{S : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)}
(hΩopen : IsOpen Ω)
(hIopen : IsOpen I)
(hΩ'sub : Ω' ⊆ Ω)
(hI'sub : I' ⊆ I)
(hSsub : S ⊆ CKN.spaceTimeSet Ω' I')
(hvanish : ∀ z ∉ S, F z = 0)
:
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Ω I, F z = ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Ω' I', F z
theorem
CIV.isSuitableWeakSolution_restrict
{Ω Ω' : Set CKN.Foundation.Parabolic.Vec3}
{I I' : Set ℝ}
{q : ℝ}
{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 → ℝ}
{f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hsol : CKN.IsSuitableWeakSolution Ω I q u Du p f)
(hΩ'open : IsOpen Ω')
(hΩ'sub : Ω' ⊆ Ω)
(hI'open : IsOpen I')
(hI'ord : I'.OrdConnected)
(hI'sub : I' ⊆ I)
:
CKN.IsSuitableWeakSolution Ω' I' q u Du p f