BUShort Growth Any Interval

Growth bounds for the short-time backward uniqueness argument.

theorem ESS.bu_growth_implies_local_l2_on_interval (I : Set ℝ) (M : ℝ) (hM : 0 < M) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hgrowth : ∀ z ∈ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} I, CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ≤ Real.exp (M * CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2)) (S : Set CKN.Foundation.Parabolic.ParabolicPoint) : S ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} I → Bornology.IsBounded S → ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, ‖w z‖ₑ ^ 2 < ⊤

A Gaussian growth bound makes the velocity square-integrable on bounded subsets of any half-space time cylinder (lem:bu-small-time).