Blowup Velocity Meas

Velocity estimates for the rescaled sequence used in endpoint compactness.

theorem ESS.blowupRescaledVelocity_aestronglyMeasurable (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : MeasureTheory.AEStronglyMeasurable u MeasureTheory.volume) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hr : 0 < r) : MeasureTheory.AEStronglyMeasurable (parabolicRescaleVelocity x₀ t₀ r u) MeasureTheory.volume

Positive parabolic rescaling preserves almost everywhere strong measurability of a velocity field.

theorem ESS.blowupRescaledVelocity_norm_aestronglyMeasurable_prod (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : MeasureTheory.AEStronglyMeasurable u MeasureTheory.volume) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hr : 0 < r) (J : Set ℝ) : 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))

The scalar velocity norm of a rescaling is jointly measurable on every product past-time region.