Uniform weight bound on a fixed spatial cylinder

For a fixed Carleman parameter and spatial radius, the weight remains bounded as the lower-time transition approaches one half.

theorem ESS.buShortCarlemanWeight_continuousOn_positive (a : ℝ) : ContinuousOn (buShortCarlemanWeight a) {z : CKN.Foundation.Parabolic.ParabolicPoint | 0 < z.1 2 ∧ 0 < z.2}

The Carleman density is continuous where height and time are both positive.

theorem ESS.buShortCarlemanWeight_fixedCylinder_bound (R a : ℝ) (hR : 0 < R) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ z ∈ buShortFixedCylinder R, buShortCarlemanWeight a z ≤ C

The weight has a bound on the fixed cylinder that is independent of the lower-time transition width.