Source box of the Gaussian estimate

The output box remains inside the source cylinder, so its field energy is integrable from the weak derivative data.

theorem ESS.uc_source_target_box_subset (R T scale ρ t : ℝ) (hR : 0 < R) (hT : 0 < T) (hscale : 0 < scale) (hρ : 4 ≤ ρ) (hball : scale * ρ ≤ 3 * R / 4) (htime : 2 * scale ^ 2 ≤ 3 * T / 4) (hscaleSq : scale ^ 2 = 2 * t) (x₀ x : CKN.Foundation.Parabolic.Vec3) (hx : CKN.Foundation.Parabolic.vec3EuclideanNorm (x - x₀) ≤ 3 / 8 * √(2 / 100) * R) : CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x scale) (Set.Ioo t (2 * t)) ⊆ CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ R) (Set.Ioo 0 T)

The Gaussian target box lies inside the original space-time cylinder.