Fixed constants in the half-space Sobolev passage

The density passage preserves the threshold and constant supplied by the smooth half-space estimate (lem:carleman-sobolev).

theorem ESS.bu_carleman_sobolev_halfspace_fixed (α a₀ c : ℝ) (w : 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) (hderiv : CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 1 < x 2} (Set.Ioo 0 1) w Dw D2w Dtw) (hcompact : HasCompactSupport w) (htsupport : tsupport w ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 1 < x 2} (Set.Ioo 0 1)) (hL2 : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 1 < x 2} (Set.Ioo 0 1), ‖w z‖ₑ ^ 2 + ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤) (hSmooth : ∀ (a : ℝ), a₀ < a → ∀ v ∈ 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 * halfSpacePhase a α z) * (a * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 / z.2 ^ 2 + CKN.spatialGradientSq v (CKN.spatialGradient v) 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 * halfSpacePhase a α z) * (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => v y i) z + ∑ j : Fin 3, CKN.spatialSecondPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => v y i) j j z) ^ 2) (a : ℝ) : a₀ < a → ∫ (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 * halfSpacePhase a α z) * (a * CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2 / z.2 ^ 2 + CKN.spatialGradientSq w Dw 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 * halfSpacePhase a α z) * (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => Dtw z i + ∑ j : Fin 3, D2w z i j j) ^ 2

A fixed smooth half-space Carleman constant passes unchanged to a compactly supported field with weak space-time derivatives.