Carleman inequality for the translated Gaussian cutoff

The compact cutoff data satisfy the Gaussian Carleman inequality with explicit constant exp(4/3) * (9 + 2 * sqrt 6).

theorem ESS.buGaussian_shifted_cutoff_carleman {ρ ε : ℝ} (hρ : 0 < ρ) (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} (hweak : CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo 0 (2 - 1 / 6)) v Dv D2v Dtv) (hL2 : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo (1 / 6) 2), ‖buGaussianShiftedField (1 / 6) v z‖ₑ ^ 2 + ‖buGaussianShiftedDw (1 / 6) Dv z‖ₑ ^ 2 + ‖buGaussianShiftedD2w (1 / 6) D2v z‖ₑ ^ 2 + ‖buGaussianShiftedDtw (1 / 6) Dtv z‖ₑ ^ 2 < ⊤) (a : ℝ) : 0 < a → ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 2), CKN.gaussCarlemanTimeWeight z.2 ^ (-2 * a) * Real.exp (-CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2 / (4 * z.2)) * (a / z.2 * CKN.Foundation.Parabolic.vec3EuclideanNorm (buGaussianShiftedCutoffField ρ hρ ε v z) ^ 2 + CKN.spatialGradientSq (buGaussianShiftedCutoffField ρ hρ ε v) (buGaussianShiftedCutoffDw ρ hρ ε v Dv) z) ≤ Real.exp (4 / 3) * (9 + 2 * √6) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 2), CKN.gaussCarlemanTimeWeight z.2 ^ (-2 * a) * Real.exp (-CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2 / (4 * z.2)) * (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => buGaussianShiftedCutoffDtw ρ hρ ε v Dtv z i + ∑ j : Fin 3, buGaussianShiftedCutoffD2w ρ hρ ε v Dv D2v z i j j) ^ 2

The translated cutoff of rescaled data is an admissible input for the Gaussian Carleman estimate, with its explicit constant.