Blowup Slice Rescale Uniform

Spatial slice bounds and rescaling identities in the endpoint compactness argument.

theorem ESS.blowupRescaledVelocity_component_slice_two_essSup_le (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hr : 0 < r) (J : Set ℝ) (hJ : J ⊆ CKN.rescaledTime r t₀ (Set.Ioo (-1) 0)) (M : ENNReal) (hsource : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), MeasureTheory.AEStronglyMeasurable (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, s)) MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, s))) 3 MeasureTheory.volume ≤ M) (c : CKN.Foundation.Parabolic.Vec3) (R : ℝ) (i : Fin 3) : essSup (fun (t : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => parabolicRescaleVelocity x₀ t₀ r u (x, t) i) 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball c R))) (MeasureTheory.volume.restrict J) ≤ M * MeasureTheory.volume (CKN.Foundation.Parabolic.vec3Ball c R) ^ (1 / 6)

The source L³ slice bound controls the local L² essential supremum of each rescaled velocity component on any past interval.