The Gaussian Carleman estimate

prop:carleman-gauss: the existential statement, witnessed by the explicit constant of ESS.carlemanGaussian_explicit.

theorem ESS.Main.carlemanGaussian : ∃ (c₀ : ℝ), 0 < c₀ ∧ ∀ (a : ℝ), 0 < a → ∀ w ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo 0 2), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 2), (z.2 * Real.exp ((1 - z.2) / 3)) ^ (-2 * a) * Real.exp (-CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2 / (4 * z.2)) * (a / z.2 * CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2 + CKN.spatialGradientSq w (CKN.spatialGradient w) z) ≤ c₀ * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 2), (z.2 * Real.exp ((1 - z.2) / 3)) ^ (-2 * a) * Real.exp (-CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2 / (4 * z.2)) * (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => w y i) z + ∑ j : Fin 3, CKN.spatialSecondPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => w y i) j j z) ^ 2

Gaussian Carleman inequality on the positive-time cylinder (prop:carleman-gauss).