Restricting Carleman integrals to the cutoff support #
The cutoff field and all specified weak derivative data vanish outside the compact support of the scalar cutoff, so its Carleman integrals are unchanged when restricted to that support.
theorem
ESS.bu_short_cutoff_carleman_integral_eq_support
(scale R ε a : ℝ)
(hscale : 0 < scale)
(hscale1 : scale ≤ 1)
(hR : 0 < R)
(hε : 0 < ε)
(v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3)
(D2v : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3)
(Dtv : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
:
have κ := buShortFullCutoff scale R hR ε;
have K := buCutSupportSet κ;
have W := buCutField κ v;
have DW := buCutDw κ v Dv;
have D2W := buCutD2 κ v Dv D2v;
have DtW := buCutDt κ v Dtv;
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in halfSpaceDomain, buShortCarlemanWeight a z * (a * CKN.Foundation.Parabolic.vec3EuclideanNorm (W z) ^ 2 / z.2 ^ 2 + CKN.spatialGradientSq W DW z / z.2) = ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in K, buShortCarlemanWeight a z * (a * CKN.Foundation.Parabolic.vec3EuclideanNorm (W z) ^ 2 / z.2 ^ 2 + CKN.spatialGradientSq W DW z / z.2) ∧ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in halfSpaceDomain, buShortCarlemanWeight a z * (CKN.Foundation.Parabolic.vec3EuclideanNorm (W z) ^ 2 + CKN.spatialGradientSq W DW z) = ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in K, buShortCarlemanWeight a z * (CKN.Foundation.Parabolic.vec3EuclideanNorm (W z) ^ 2 + CKN.spatialGradientSq W DW z) ∧ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in halfSpaceDomain, buShortCarlemanWeight a z * CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2W DtW z) ^ 2 = ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in K, buShortCarlemanWeight a z * CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2W DtW z) ^ 2
The mass-gradient and weak-heat Carleman integrals of a scalar cutoff are exactly their restrictions to the scalar cutoff support.