Continuity of short-time density factors

The fixed scalar factors are continuous where the normal height and normalized time are positive.

theorem ESS.bu_short_tangential_factor_continuousOn_positive : ContinuousOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => Real.exp (-(z.1 0 ^ 2 + z.1 1 ^ 2) / (4 * z.2)) * (1 + z.1 2) ^ 4) {z : CKN.Foundation.Parabolic.ParabolicPoint | 0 < z.1 2 ∧ 0 < z.2}

The tangential Gaussian and normal polynomial are continuous on positive normalized times (lem:bu-small-time).

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

The shifted Carleman factor is continuous on the positive cylinder (lem:bu-small-time).

theorem ESS.bu_short_shifted_polynomial_factor_continuousOn_positive (scale a : ℝ) : ContinuousOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => buShortShiftedWeight scale a z * (1 + z.1 2) ^ 4) {z : CKN.Foundation.Parabolic.ParabolicPoint | 0 < z.1 2 ∧ 0 < z.2}

The shifted Carleman factor times the normal polynomial is continuous on the positive cylinder (lem:bu-small-time).