Blowup Local Box

Bounds on local boxes in the endpoint blow-up construction.

theorem ESS.blowup_inner_past_localBox (R a b : ℝ) (hR : 0 < R) (hab : a < b) (hb : b < 0) : CKN.localBox (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0) (CKN.Foundation.Parabolic.vec3Ball 0 R) (Set.Ioo a b)

A finite inner past cylinder is a local box of the larger rescaled suitable-solution domain.