Gaussian averaging box geometry

The local energy cylinder and the Gaussian averaging box occupy a bounded region of the extended normalized half-space.

theorem ESS.bu_short_inner_subset_average (Y : CKN.Foundation.Parabolic.Vec3) (δ : ℝ) (hδ : 0 < δ) : have r := √δ / 8; CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball Y r) (Set.Ioo (1 / 2 + δ - r ^ 2 / 2) (1 / 2 + δ - r ^ 2 / 2 + r ^ 2)) ⊆ CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball Y √(3 * δ / 2)) (Set.Ioo (1 / 2 + δ / 2) (1 / 2 + 5 * δ / 4))

The local energy cylinder is contained in the Gaussian averaging box at the same center and time (lem:bu-small-time).

theorem ESS.bu_short_average_box_bounded (Y : CKN.Foundation.Parabolic.Vec3) (δ : ℝ) (hδ : 0 < δ) : Bornology.IsBounded (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball Y √(3 * δ / 2)) (Set.Ioo (1 / 2 + δ / 2) (1 / 2 + 5 * δ / 4)))

A Gaussian averaging box is bounded in parabolic space-time.

theorem ESS.bu_short_average_box_subset_extended (Y : CKN.Foundation.Parabolic.Vec3) (δ : ℝ) (hδ : 0 < δ) (hδhalf : δ < 1 / 2) (hball : CKN.Foundation.Parabolic.vec3Ball Y √(3 * δ / 2) ⊆ {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2}) : CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball Y √(3 * δ / 2)) (Set.Ioo (1 / 2 + δ / 2) (1 / 2 + 5 * δ / 4)) ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (1 / 2) (3 / 2))

The Gaussian averaging box lies in the extended normalized half-space when its center ball does.