The open top of a past cylinder

The top time slice is null for space-time volume, so the open past cylinder and the CKN cylinder give the same energy integral (prop:blowup-limit).

theorem ESS.blowupPastCylinder_restrict_eq (x : CKN.Foundation.Parabolic.Vec3) (t r : ℝ) : MeasureTheory.volume.restrict (goodPointPastCylinder x t r) = MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.parabolicCylinder x t r)

Opening the top face of a past cylinder preserves its volume restriction.

theorem ESS.goodPointEnergy_eq_open_top (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (x : CKN.Foundation.Parabolic.Vec3) (t r : ℝ) : goodPointEnergy u p x t r = ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in goodPointPastCylinder x t r, ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2)

The good-point energy can be integrated over the open past cylinder.