Uniform half-space Carleman constant for short-time cutoffs

The smooth half-space estimate supplies one threshold and one constant for every compact short-time cutoff, independently of its radius and initial time transition.

theorem ESS.bu_short_cutoff_carleman_uniform : ∃ (a₀ : ℝ) (c : ℝ), 0 < a₀ ∧ 0 < c ∧ ∀ (scale R ε : ℝ), 0 < scale → scale ≤ 1 → ∀ (hR : 0 < R), 0 < ε → ∀ (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), ContinuousOn w ({x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico 0 1) → CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1) w Dw D2w Dtw → (∀ S ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1), Bornology.IsBounded S → ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤) → ∀ (a : ℝ), a₀ < a → have κ := buShortFullCutoff scale R hR ε; have v := buAffineField (-scale ^ 2 / 2) scale w; have Dv := buAffineDw (-scale ^ 2 / 2) scale Dw; have D2v := buAffineD2w (-scale ^ 2 / 2) scale D2w; have Dtv := buAffineDtw (-scale ^ 2 / 2) scale Dtw; have W := buCutField κ v; have DW := buCutDw κ v Dv; have D2W := buCutD2 κ v Dv D2v; have DtW := buCutDt κ v Dtv; ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in halfSpaceDomain, buShortCarlemanWeight 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 halfSpaceDomain, buShortCarlemanWeight a z * CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2W DtW z) ^ 2

One half-space Carleman threshold and constant work for all short-time cutoffs of a field satisfying the weak derivative assumptions.