Blowup Terminal

Terminal-time properties of the endpoint blow-up limit.

theorem ESS.blowup_rescaled_ball_eq (x₀ c : CKN.Foundation.Parabolic.Vec3) (r : ℝ) (hr : 0 < r) : CKN.rescaledSpace r x₀ (CKN.Foundation.Parabolic.vec3Ball (x₀ + r • c) r) = CKN.Foundation.Parabolic.vec3Ball c 1

A ball centered at the rescaled point is exactly the inverse image of the corresponding source ball.

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

Critical spatial L³ mass is unchanged when a shrinking source ball is rescaled to a fixed unit ball.

theorem ESS.blowup_rescaled_ball_velocity_eLpNorm_three_eq (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) => CKN.Foundation.Parabolic.vec3EuclideanNorm (r • u (x₀ + r • x))) 3 (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.restrict (CKN.Foundation.Parabolic.vec3Ball (x₀ + r • c) r))

The critical L³ seminorm of the Euclidean velocity magnitude is preserved by spatial rescaling between corresponding balls.

theorem ESS.blowup_rescaled_velocitySlice_aestronglyMeasurable (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.AEStronglyMeasurable (fun (x : CKN.Foundation.Parabolic.Vec3) => r • u (x₀ + r • x)) MeasureTheory.volume

A positive spatial rescaling preserves almost everywhere strong measurability of a velocity slice.

theorem ESS.blowup_terminal_shrinking_ball_eLpNorm_tendsto_zero {E : Type u_1} [NormedAddCommGroup E] (u : CKN.Foundation.Parabolic.Vec3 → E) (hu : MeasureTheory.MemLp u 3 MeasureTheory.volume) (x₀ c : CKN.Foundation.Parabolic.Vec3) (r : ℕ → ℝ) (hr0 : Filter.Tendsto r Filter.atTop (nhds 0)) : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm u 3 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball (x₀ + r k • c) (r k)))) Filter.atTop (nhds 0)

The L³ mass of a fixed velocity slice vanishes on balls whose radii shrink to zero, even when their centers move with the radii.

theorem ESS.blowup_terminal_rescaled_eLpNorm_two_tendsto_zero (u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hu : MeasureTheory.AEStronglyMeasurable u MeasureTheory.volume) (hu₃ : MeasureTheory.MemLp (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u y)) 3 MeasureTheory.volume) (x₀ c : CKN.Foundation.Parabolic.Vec3) (r : ℕ → ℝ) (hr : ∀ (k : ℕ), 0 < r k) (hr0 : Filter.Tendsto r Filter.atTop (nhds 0)) : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (r k • u (x₀ + r k • x))) 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball c 1))) Filter.atTop (nhds 0)

The Euclidean magnitude of a rescaled fixed L³ slice vanishes in L² on every unit ball.

theorem ESS.blowup_terminal_rescaled_vector_eLpNorm_two_tendsto_zero (u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hu : MeasureTheory.AEStronglyMeasurable u MeasureTheory.volume) (hu₃ : MeasureTheory.MemLp (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u y)) 3 MeasureTheory.volume) (x₀ c : CKN.Foundation.Parabolic.Vec3) (r : ℕ → ℝ) (hr : ∀ (k : ℕ), 0 < r k) (hr0 : Filter.Tendsto r Filter.atTop (nhds 0)) : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => r k • u (x₀ + r k • x)) 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball c 1))) Filter.atTop (nhds 0)

A rescaled fixed L³ terminal slice converges strongly to zero in local L².

theorem ESS.blowup_terminal_indicator_magnitude_memLp (B : Set CKN.Foundation.Parabolic.Vec3) (hB : MeasurableSet B) (u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hu : MeasureTheory.MemLp u 3 (MeasureTheory.volume.restrict B)) : MeasureTheory.MemLp (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (B.indicator u y)) 3 MeasureTheory.volume

Zero extension of an L³ velocity slice has an L³ Euclidean magnitude.

theorem ESS.blowup_terminal_local_trace_rescaled_tendsto_zero (B : Set CKN.Foundation.Parabolic.Vec3) (hB : MeasurableSet B) (u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hu : MeasureTheory.MemLp u 3 (MeasureTheory.volume.restrict B)) (x₀ c : CKN.Foundation.Parabolic.Vec3) (r : ℕ → ℝ) (hr : ∀ (k : ℕ), 0 < r k) (hr0 : Filter.Tendsto r Filter.atTop (nhds 0)) : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => r k • B.indicator u (x₀ + r k • x)) 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball c 1))) Filter.atTop (nhds 0)

The zero extended local terminal trace has rescalings vanishing in L² on every unit ball.