Density passage for compactly supported Carleman fields #
Smooth weighted estimates pass to compactly supported fields with space-time weak derivatives
(lem:carleman-sobolev).
theorem
ESS.compactlySupportedSpaceTimeCarleman_of_smooth
{Ω : Set CKN.Foundation.Parabolic.Vec3}
{I : Set ℝ}
(hΩ : IsOpen Ω)
(hI : IsOpen I)
{w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hderiv : CKN.HasSpaceTimeWeakDerivs Ω I w Dw D2w Dtw)
(hcompact : HasCompactSupport w)
(htsupport : tsupport w ⊆ CKN.spaceTimeSet Ω I)
(hL2 :
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Ω I, ‖w z‖ₑ ^ 2 + ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤)
{ρ σ τ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hρcont : ContinuousOn ρ (Ω ×ˢ I))
(hσcont : ContinuousOn σ (Ω ×ˢ I))
(hτcont : ContinuousOn τ (Ω ×ˢ I))
{c : ℝ}
(hSmooth :
∀ v ∈ CKN.spaceTimeTestFunction Ω I,
∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in Ω ×ˢ I, σ z * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 + τ z * CKN.spatialGradientSq v (CKN.spatialGradient v) z ≤ c * ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in Ω ×ˢ I, ρ z * (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) =>
CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => v y i) z + ∑ j : Fin 3,
CKN.spatialSecondPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => v y i) j j z) ^ 2)
:
∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in Ω ×ˢ I, σ z * CKN.Foundation.Parabolic.vec3EuclideanNorm (w (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z)) ^ 2 + τ z * ∑ i : Fin 3, ∑ j : Fin 3, Dw (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z) i j ^ 2 ≤ c * ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in Ω ×ˢ I, ρ z * (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) =>
Dtw (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z) i + ∑ j : Fin 3, D2w (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z) i j j) ^ 2