The half-space Carleman inequality

theorem ESS.carlemanHalfSpace (α : ℝ) : 1 / 2 < α → α < 1 → ∃ (a₀ : ℝ) (c : ℝ), 0 < a₀ ∧ 0 < c ∧ ∀ (a : ℝ), a₀ < a → ∀ w ∈ CKN.spaceTimeTestFunction {x : CKN.Foundation.Parabolic.Vec3 | 1 < x 2} (Set.Ioo 0 1), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 1 < x 2} (Set.Ioo 0 1), z.2 ^ 2 * Real.exp (2 * (-(z.1 0 ^ 2 + z.1 1 ^ 2) / (8 * z.2) + a * (1 - z.2) * z.1 2 ^ (2 * α) / z.2 ^ α)) * (a * CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2 / z.2 ^ 2 + CKN.spatialGradientSq w (CKN.spatialGradient w) z / z.2) ≤ c * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 1 < x 2} (Set.Ioo 0 1), z.2 ^ 2 * Real.exp (2 * (-(z.1 0 ^ 2 + z.1 1 ^ 2) / (8 * z.2) + a * (1 - z.2) * z.1 2 ^ (2 * α) / 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

Carleman inequality on a half-space with an anisotropic weight (prop:carleman-halfspace; ESS Proposition 6.2).