Blowup Slice Bound

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

theorem ESS.blowup_rescaled_velocitySlice_eLpNorm_three_eq (u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hu : MeasureTheory.AEStronglyMeasurable u MeasureTheory.volume) (x₀ : CKN.Foundation.Parabolic.Vec3) (r : ℝ) (hr : 0 < r) : MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (r • u (x₀ + r • x))) 3 MeasureTheory.volume = MeasureTheory.eLpNorm (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u y)) 3 MeasureTheory.volume

The global Euclidean velocity L³ norm is invariant under positive spatial Navier–Stokes rescaling.

theorem ESS.blowup_rescaled_velocitySlice_local_two_le (u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hu : MeasureTheory.AEStronglyMeasurable u MeasureTheory.volume) (x₀ c : CKN.Foundation.Parabolic.Vec3) (r : ℝ) (hr : 0 < r) : MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => r • u (x₀ + r • x)) 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball c 1)) ≤ MeasureTheory.eLpNorm (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u y)) 3 MeasureTheory.volume * MeasureTheory.volume (CKN.Foundation.Parabolic.vec3Ball c 1) ^ (1 / 6)

A global velocity L³ slice bound controls the local L² norm of each positive spatial rescaling.