Multi Partial Congr Space Time Set #
Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.
theorem
CIV.spatialPartial_iterate_congr_of_eqOn_spaceTimeSet
{v u : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{Ω : Set CKN.Foundation.Parabolic.Vec3}
{I : Set ℝ}
(hΩ : IsOpen Ω)
(hI : IsOpen I)
(h : Set.EqOn v u (CKN.spaceTimeSet Ω I))
(j : Fin 3)
(n : ℕ)
:
Set.EqOn ((fun (k : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) => CKN.spatialPartial k j)^[n] v)
((fun (k : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) => CKN.spatialPartial k j)^[n] u) (CKN.spaceTimeSet Ω I)
theorem
CIV.multiPartial_congr_of_eqOn_spaceTimeSet
{v u : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{Ω : Set CKN.Foundation.Parabolic.Vec3}
{I : Set ℝ}
(hΩ : IsOpen Ω)
(hI : IsOpen I)
(h : Set.EqOn v u (CKN.spaceTimeSet Ω I))
(α : Fin 3 → ℕ)
:
Set.EqOn (multiPartial v α) (multiPartial u α) (CKN.spaceTimeSet Ω I)
theorem
CIV.sum_spatialPartial_congr_of_eqOn_spaceTimeSet
{v u : Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{Ω : Set CKN.Foundation.Parabolic.Vec3}
{I : Set ℝ}
(hΩ : IsOpen Ω)
(hI : IsOpen I)
(h : ∀ (k : Fin 3), Set.EqOn (v k) (u k) (CKN.spaceTimeSet Ω I))
{z : CKN.Foundation.Parabolic.ParabolicPoint}
(hz : z ∈ CKN.spaceTimeSet Ω I)
: