Gaussian cutoff admissibility

The compact Gaussian cutoff carries all weak derivative and quadratic data required by the Sobolev Carleman estimate in lem:uc-gaussian.

theorem ESS.ucGaussianCutoff_admissible {ρ ε : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) {v : 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} (hweak : CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo 0 2) v Dw D2w Dtw) (hL2 : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in ucCylinder ρ, ‖v z‖ₑ ^ 2 + ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤) : CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo 0 2) (ucCutoffField (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v) (ucCutoffDw (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dw) (ucCutoffD2 (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dw D2w) (ucCutoffDt (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dtw) ∧ HasCompactSupport (ucCutoffField (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v) ∧ tsupport (ucCutoffField (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v) ⊆ ucCylinder ρ ∧ ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in ucCylinder ρ, ‖ucCutoffField (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v z‖ₑ ^ 2 + ‖ucCutoffDw (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dw z‖ₑ ^ 2 + ‖ucCutoffD2 (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dw D2w z‖ₑ ^ 2 + ‖ucCutoffDt (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dtw z‖ₑ ^ 2 < ⊤

The Gaussian cutoff of a field is a compactly supported weak field with finite quadratic derivative data on the normalized cylinder.