Passing from metric to Euclidean averaging balls

The Euclidean ball is contained in the ambient metric ball used by the Gaussian average estimate, so its nonnegative velocity integral obeys the same bound.

theorem ESS.bu_short_euclidean_average_le_metric (X : CKN.Foundation.Parabolic.Vec3) (t : ℝ) (ht : 0 < t) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hMetricInt : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2) (CKN.spaceTimeSet (Metric.ball X √(3 * t)) (Set.Ioo t (5 * t / 2))) MeasureTheory.volume) : t.rpow (-(5 / 2)) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball X √(3 * t)) (Set.Ioo t (5 * t / 2)), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2 ≤ t.rpow (-(5 / 2)) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (Metric.ball X √(3 * t)) (Set.Ioo t (5 * t / 2)), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2

A Gaussian bound over the ambient metric ball also bounds the Euclidean averaging cylinder (lem:bu-small-time).