Derivatives of compactly supported space-time mollifications

The local weak-derivative identities identify derivatives of the mollification with the mollifications of the zero-extended weak data near the original support (lem:carleman-sobolev of the Escauriaza–Seregin–Šverák manuscript).

theorem CKN.product_component_tsupport_subset {w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hcompact : HasCompactSupport w) (i : Fin 3) : (tsupport fun (q : Foundation.Parabolic.Vec3 × ℝ) => w (Foundation.Parabolic.parabolicHomeomorph.symm q) i) ⊆ ⇑Foundation.Parabolic.parabolicHomeomorph '' tsupport w

The product-coordinate support of a component is contained in the transported vector support (lem:carleman-sobolev, ESS).

theorem CKN.product_field_hasCompactSupport {w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hcompact : HasCompactSupport w) : HasCompactSupport fun (q : Foundation.Parabolic.Vec3 × ℝ) => w (Foundation.Parabolic.parabolicHomeomorph.symm q)

A compactly supported parabolic field remains compactly supported in product coordinates (lem:carleman-sobolev, ESS).

theorem CKN.spatialPartial_tsupport_subset_product {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (j : Fin 3) : (tsupport fun (z : Foundation.Parabolic.Vec3 × ℝ) => spatialPartial (fun (q : Foundation.Parabolic.ParabolicPoint) => f q) j z) ⊆ tsupport f

A spatial derivative of a smooth compactly supported scalar field is supported where the field is supported (lem:carleman-sobolev, ESS).

theorem CKN.spatialSecondPartial_tsupport_subset_product {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (j k : Fin 3) : (tsupport fun (z : Foundation.Parabolic.Vec3 × ℝ) => spatialSecondPartial (fun (q : Foundation.Parabolic.ParabolicPoint) => f q) j k z) ⊆ tsupport f

A second spatial derivative is supported where the underlying scalar field is supported (lem:carleman-sobolev, ESS).

theorem CKN.timePartial_tsupport_subset_product {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} : (tsupport fun (z : Foundation.Parabolic.Vec3 × ℝ) => timePartial (fun (q : Foundation.Parabolic.ParabolicPoint) => f q) z) ⊆ tsupport f

A time derivative is supported where the underlying scalar field is supported (lem:carleman-sobolev, ESS).

theorem CKN.spaceTimeMollify_compactSupport_weakDerivs {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) {w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Dw : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {D2w : Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → Foundation.Parabolic.Vec3} {Dtw : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hderiv : HasSpaceTimeWeakDerivs Ω I w Dw D2w Dtw) (htsupport : tsupport w ⊆ spaceTimeSet Ω I) {r δ : ℝ} (hr : 0 < r) (hthick : Metric.cthickening r (⇑Foundation.Parabolic.parabolicHomeomorph '' tsupport w) ⊆ Ω ×ˢ I) (hδ : 0 < δ) (hδsmall : 4 * δ ≤ r / 2) {z : Foundation.Parabolic.Vec3 × ℝ} (hz : z ∈ Metric.closedBall 0 (r / 4) + ⇑Foundation.Parabolic.parabolicHomeomorph '' tsupport w) : (∀ (i j : Fin 3), spatialPartial (fun (q : Foundation.Parabolic.ParabolicPoint) => spaceTimeMollify (fun (y : Foundation.Parabolic.Vec3 × ℝ) => w (Foundation.Parabolic.parabolicHomeomorph.symm y) i) δ hδ q) j z = spaceTimeMollify (zeroExtendField (Ω ×ˢ I) fun (y : Foundation.Parabolic.Vec3 × ℝ) => Dw (Foundation.Parabolic.parabolicHomeomorph.symm y) i j) δ hδ z) ∧ (∀ (i j k : Fin 3), spatialSecondPartial (fun (q : Foundation.Parabolic.ParabolicPoint) => spaceTimeMollify (fun (y : Foundation.Parabolic.Vec3 × ℝ) => w (Foundation.Parabolic.parabolicHomeomorph.symm y) i) δ hδ q) j k z = spaceTimeMollify (zeroExtendField (Ω ×ˢ I) fun (y : Foundation.Parabolic.Vec3 × ℝ) => D2w (Foundation.Parabolic.parabolicHomeomorph.symm y) i j k) δ hδ z) ∧ ∀ (i : Fin 3), timePartial (fun (q : Foundation.Parabolic.ParabolicPoint) => spaceTimeMollify (fun (y : Foundation.Parabolic.Vec3 × ℝ) => w (Foundation.Parabolic.parabolicHomeomorph.symm y) i) δ hδ q) z = spaceTimeMollify (zeroExtendField (Ω ×ˢ I) fun (y : Foundation.Parabolic.Vec3 × ℝ) => Dtw (Foundation.Parabolic.parabolicHomeomorph.symm y) i) δ hδ z

On a fixed compact neighborhood of the support, the ordinary derivatives of the zero-extended mollification are the mollifications of the zero-extended weak data (lem:carleman-sobolev, ESS).