BUGrowth L2

Local square-integrability consequences of backward-uniqueness growth bounds.

theorem ESS.bu_growth_implies_local_l2 (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} (Set.Ioo 0 1), 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} (Set.Ioo 0 1) → 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 the half-space cylinder (thm:bu).