Values on the shifted short-time cylinder #
The shifted field is continuous through its lower time face, vanishes there, and inherits the original quadratic spatial growth estimate.
theorem
ESS.bu_short_map_mem_halfClosure
(scale : ℝ)
(hscale : 0 < scale)
(hscale1 : scale ≤ 1)
{z : CKN.Foundation.Parabolic.ParabolicPoint}
(hz : z ∈ {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico (1 / 2) 1)
:
The shifted map carries the half-space cylinder with lower time face included into the original positive-time cylinder with its zero face.
theorem
ESS.bu_short_field_continuousOn
(scale : ℝ)
(hscale : 0 < scale)
(hscale1 : scale ≤ 1)
(w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(hcont : ContinuousOn w ({x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico 0 1))
:
ContinuousOn (buAffineField (-scale ^ 2 / 2) scale w)
({x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico (1 / 2) 1)
The shifted field is continuous on the cylinder with its lower time face included.
theorem
ESS.bu_short_field_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) 1))
:
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 to the shifted initial interval.