Global weak derivatives of zero extensions #
Compact support inside the product domain allows the weak integration-by-parts
identities to extend to the ambient space (lem:carleman-sobolev of the Escauriaza–Seregin–Šverák
manuscript).
theorem
CKN.spaceTimeZeroExtensions_weak_derivatives
{Ω : 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)
(hcompact : HasCompactSupport w)
(htsupport : tsupport w ⊆ spaceTimeSet Ω I)
:
(∀ (i j : Fin 3) (φ : Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) φ →
HasCompactSupport φ →
∫ (y : Foundation.Parabolic.Vec3 × ℝ), zeroExtendField (Ω ×ˢ I)
(fun (q : Foundation.Parabolic.Vec3 × ℝ) => w (Foundation.Parabolic.parabolicHomeomorph.symm q) i) y * (fderiv ℝ φ y) (basisVec j, 0) = -∫ (y : Foundation.Parabolic.Vec3 × ℝ), zeroExtendField (Ω ×ˢ I)
(fun (q : Foundation.Parabolic.Vec3 × ℝ) => Dw (Foundation.Parabolic.parabolicHomeomorph.symm q) i j)
y * φ y) ∧ (∀ (i j k : Fin 3) (φ : Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) φ →
HasCompactSupport φ →
∫ (y : Foundation.Parabolic.Vec3 × ℝ), zeroExtendField (Ω ×ˢ I)
(fun (q : Foundation.Parabolic.Vec3 × ℝ) => Dw (Foundation.Parabolic.parabolicHomeomorph.symm q) i j)
y * (fderiv ℝ φ y) (basisVec k, 0) = -∫ (y : Foundation.Parabolic.Vec3 × ℝ), zeroExtendField (Ω ×ˢ I)
(fun (q : Foundation.Parabolic.Vec3 × ℝ) =>
D2w (Foundation.Parabolic.parabolicHomeomorph.symm q) i j k)
y * φ y) ∧ ∀ (i : Fin 3) (φ : Foundation.Parabolic.Vec3 × ℝ → ℝ),
ContDiff ℝ (↑⊤) φ →
HasCompactSupport φ →
∫ (y : Foundation.Parabolic.Vec3 × ℝ), zeroExtendField (Ω ×ˢ I)
(fun (q : Foundation.Parabolic.Vec3 × ℝ) => w (Foundation.Parabolic.parabolicHomeomorph.symm q) i) y * (fderiv ℝ φ y) (0, 1) = -∫ (y : Foundation.Parabolic.Vec3 × ℝ), zeroExtendField (Ω ×ˢ I)
(fun (q : Foundation.Parabolic.Vec3 × ℝ) => Dtw (Foundation.Parabolic.parabolicHomeomorph.symm q) i)
y * φ y
The zero extensions of a compactly supported space-time field and its weak data satisfy
the corresponding global weak integration-by-parts identities (lem:carleman-sobolev, ESS).