Spatial Partial Congr Space Time Set

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

theorem CIV.spatialPartial_congr_of_eqOn_spaceTimeSet {v u : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (h : ∀ w ∈ CKN.spaceTimeSet Ω I, v w = u w) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ CKN.spaceTimeSet Ω I) (j : Fin 3) : CKN.spatialPartial v j z = CKN.spatialPartial u j z

Pointwise agreement of two scalar fields on an open space-time cylinder transports a spatial partial derivative. These lemmas generalize CIV.spatialPartial_congr_of_eqOn (CIV/Reduction/AveragedClassical.lean) from the unit cylinder to an arbitrary open cylinder spaceTimeSet Ω I, needed to differentiate the momentum equation of a classical solution on the general cylinder that thm:analytic:interior is stated on.

theorem CIV.timePartial_congr_of_eqOn_spaceTimeSet {v u : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (h : ∀ w ∈ CKN.spaceTimeSet Ω I, v w = u w) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ CKN.spaceTimeSet Ω I) : CKN.timePartial v z = CKN.timePartial u z

Pointwise agreement of two scalar fields on an open space-time cylinder transports the time partial derivative.

theorem CIV.spatialSecondPartial_congr_of_eqOn_spaceTimeSet {v u : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (h : ∀ w ∈ CKN.spaceTimeSet Ω I, v w = u w) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ CKN.spaceTimeSet Ω I) (i j : Fin 3) : CKN.spatialSecondPartial v i j z = CKN.spatialSecondPartial u i j z

Pointwise agreement of two scalar fields on an open space-time cylinder transports a second spatial partial derivative.