Quadratic growth and local energy on the extended cylinder #
The physical growth hypothesis supplies local velocity energy after the short-time rescaling.
theorem
ESS.bu_short_extended_growth
(M scale : ℝ)
(hscale : 0 < scale)
(hscale1 : scale ≤ 1)
(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))
{z : CKN.Foundation.Parabolic.ParabolicPoint}
(hz : z ∈ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (1 / 2) (3 / 2)))
:
CKN.Foundation.Parabolic.vec3EuclideanNorm (buAffineField (-scale ^ 2 / 2) scale w z) ≤ Real.exp (M * scale ^ 2 * CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2)
Quadratic spatial growth transfers through the extended short-time parabolic rescaling.
theorem
ESS.bu_short_extended_local_quadratic_l2
(M scale : ℝ)
(hscale : 0 < scale)
(hscale1 : scale ≤ 1)
(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))
(S : Set CKN.Foundation.Parabolic.ParabolicPoint)
:
S ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (1 / 2) (3 / 2)) →
Bornology.IsBounded S →
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, ‖buAffineField (-scale ^ 2 / 2) scale w z‖ₑ ^ 2 + ‖buAffineDw (-scale ^ 2 / 2) scale Dw z‖ₑ ^ 2 + ‖buAffineD2w (-scale ^ 2 / 2) scale D2w z‖ₑ ^ 2 + ‖buAffineDtw (-scale ^ 2 / 2) scale Dtw z‖ₑ ^ 2 < ⊤
The extended short-time cylinder has finite full quadratic data on every bounded measurable subset.