Integrability on the physical Gaussian cylinder

Weak derivatives and quadratic growth give finite velocity energy on every bounded averaging cylinder inside the positive half-space.

theorem ESS.bu_short_metric_average_integrable (M : ℝ) (X : CKN.Foundation.Parabolic.Vec3) (t : ℝ) (hX : 2 < X 2) (ht : 0 < t) (htsmall : t < 1 / 12) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hweak : CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1) w Dw D2w Dtw) (hL2 : ∀ S ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1), Bornology.IsBounded S → ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤) (hgrowth : ∀ z ∈ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ≤ Real.exp (M * CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2)) : 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

The velocity square is integrable on the physical metric Gaussian averaging cylinder (lem:bu-small-time).