Blowup Slice Agreement

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

theorem ESS.blowupRescaledVelocity_component_slice_two_essSup_le_of_domain (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hr : 0 < r) (J : Set ℝ) (hJm : MeasurableSet J) (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) => goodPointDomain.indicator u (x, s)) MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (goodPointDomain.indicator u (x, s))) 3 MeasureTheory.volume ≤ M) (c : CKN.Foundation.Parabolic.Vec3) (R : ℝ) (i : Fin 3) (hdomain : CKN.Foundation.Parabolic.vec3Ball c R ×ˢ J ⊆ blowupDomain x₀ t₀ r) : 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)

On an interior rescaled cylinder, the ordinary velocity has the same uniform local L² slice bound as the zero-extended velocity.