Geometry of the metric Gaussian cylinder

At the Gaussian time threshold, the averaging cylinder is bounded and lies strictly inside the positive half-space time slab.

theorem ESS.bu_short_metric_average_subset_half_cylinder (X : CKN.Foundation.Parabolic.Vec3) (t : ℝ) (hX : 2 < X 2) (ht : 0 < t) (htsmall : t < 1 / 12) : CKN.spaceTimeSet (Metric.ball X √(3 * t)) (Set.Ioo t (5 * t / 2)) ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1)

The metric Gaussian averaging cylinder lies in the positive half-space slab when its center is above height two and its time is small (lem:bu-small-time).

theorem ESS.bu_short_metric_average_bounded (X : CKN.Foundation.Parabolic.Vec3) (t : ℝ) : Bornology.IsBounded (CKN.spaceTimeSet (Metric.ball X √(3 * t)) (Set.Ioo t (5 * t / 2)))

The metric Gaussian averaging cylinder is bounded in parabolic space-time (lem:bu-small-time).