Compact slice bounds for rescaled trace fields

On any closed time interval whose source times stay in the trace interval, the measurable rescalings satisfy the compact-slice hypothesis of lem:compactness of the CKN manuscript.

theorem ESS.blowup_limit_rescaling_compact_slice_bound (W : CKN.Foundation.Parabolic.Vec3 × ↑(Set.Icc (-(3 / 4) ^ 2) 0) → CKN.Foundation.Parabolic.Vec3) (M : ℝ) (hsource : ∀ (t : ↑(Set.Icc (-(3 / 4) ^ 2) 0)), MeasureTheory.MemLp ((CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4)).indicator fun (x : CKN.Foundation.Parabolic.Vec3) => W (x, t)) 3 MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm ((CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4)).indicator (fun (y : CKN.Foundation.Parabolic.Vec3) => W (y, t)) x)) 3 MeasureTheory.volume ≤ ENNReal.ofReal M) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ : ℝ) (r : ℕ → ℝ) (hr : ∀ (n : ℕ), 0 < r n) (C : Set CKN.Foundation.Parabolic.Vec3) (hC : IsCompact C) (a b : ℝ) (hsourceTime : ∀ (n : ℕ), ∀ t ∈ Set.Icc a b, t₀ + r n ^ 2 * t ∈ Set.Icc (-(3 / 4) ^ 2) 0) (n : ℕ) (t : ℝ) : t ∈ Set.Icc a b → ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (blowupLimitTraceRescaling W x₀ t₀ (r n) (x, t))) ^ 2 ≤ (ENNReal.ofReal M * MeasureTheory.volume C ^ (1 / 6)) ^ 2

The all-time trace representative supplies every-time compact spatial L² bounds for a rescaled sequence, including the closed top time.