Blowup Slice Scaling

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

theorem ESS.blowupPressureSlice_mass_eq (f : CKN.Foundation.Parabolic.Vec3 → ℝ) (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (x₀ : CKN.Foundation.Parabolic.Vec3) (r : ℝ) (hr : 0 < r) : ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal |r ^ 2 * f (x₀ + r • x)| ^ (3 / 2) = ∫⁻ (y : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal |f y| ^ (3 / 2)

Critical spatial L^(3/2) pressure mass is invariant under positive Navier–Stokes spatial scaling.

theorem ESS.blowupVelocityScalarSlice_mass_eq (f : CKN.Foundation.Parabolic.Vec3 → ℝ) (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (x₀ : CKN.Foundation.Parabolic.Vec3) (r : ℝ) (hr : 0 < r) : ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal |r * f (x₀ + r • x)| ^ 3 = ∫⁻ (y : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal |f y| ^ 3

Critical spatial L³ velocity mass is invariant under positive Navier–Stokes spatial scaling.

theorem ESS.blowupVelocitySlice_mass_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) : ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (r • u (x₀ + r • x))) ^ 3 = ∫⁻ (y : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u y)) ^ 3

The critical spatial L³ mass of a velocity slice is invariant under positive Navier–Stokes scaling.