Blowup Velocity Time

Velocity estimates for the rescaled sequence used in endpoint compactness.

theorem ESS.blowupScalarTimeThree_eq {Ω : Set CKN.Foundation.Parabolic.Vec3} {J : Set ℝ} (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hg : MeasureTheory.AEStronglyMeasurable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g (z.1, z.2)) ((MeasureTheory.volume.restrict Ω).prod (MeasureTheory.volume.restrict J))) : ∫⁻ (t : ℝ) in J, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, t)) 3 (MeasureTheory.volume.restrict Ω) ^ 3 = ∫⁻ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), ENNReal.ofReal |g z| ^ 3 ∂(MeasureTheory.volume.restrict Ω).prod (MeasureTheory.volume.restrict J)

Tonelli identifies the time-integrated spatial cubic norm with the space-time cubic mass.

theorem ESS.blowupRescaledVelocity_slice_bound_ae (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) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (parabolicRescaleVelocity x₀ t₀ r u (x, t))) 3 MeasureTheory.volume ≤ M

A source-time uniform whole-space velocity bound persists on a rescaled past time interval.

theorem ESS.blowupRescaledVelocity_spaceTime_mass_bound (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) (hjoint : MeasureTheory.AEStronglyMeasurable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.Foundation.Parabolic.vec3EuclideanNorm (parabolicRescaleVelocity x₀ t₀ r u (z.1, z.2))) ((MeasureTheory.volume.restrict Set.univ).prod (MeasureTheory.volume.restrict J))) : ∫⁻ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (parabolicRescaleVelocity x₀ t₀ r u z)) ^ 3 ∂(MeasureTheory.volume.restrict Set.univ).prod (MeasureTheory.volume.restrict J) ≤ MeasureTheory.volume J * M ^ 3

The rescaled velocity has a uniform whole-space cubic mass on a finite past time interval.