The critical slice bound of the blow-up limit

Every slice of the rescaled trace has global L³ norm at most the trace bound, and strong local L³ convergence passes this bound to almost every negative-time slice of the limit (prop:blowup-limit, the bound u ∈ L^∞((-∞,0); L³)).

theorem ESS.blowupLimitAssembly_trace_slice_Lthree (W : CKN.Foundation.Parabolic.Vec3 × ↑(Set.Icc (-(3 / 4) ^ 2) 0) → CKN.Foundation.Parabolic.Vec3) (M : ℝ) (hsource : ∀ (t : ↑(Set.Icc (-(3 / 4) ^ 2) 0)), MeasureTheory.MemLp ((CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4)).indicator fun (x : CKN.Foundation.Parabolic.Vec3) => W (x, t)) 3 MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm ((CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4)).indicator (fun (y : CKN.Foundation.Parabolic.Vec3) => W (y, t)) x)) 3 MeasureTheory.volume ≤ ENNReal.ofReal M) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hr : 0 < r) (t : ℝ) : MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (blowupLimitTraceRescaling W x₀ t₀ r (x, t))) 3 MeasureTheory.volume ≤ ENNReal.ofReal M

Every slice of the rescaled trace has global L³ norm bounded by the trace bound.

theorem ESS.blowupLimitAssembly_slice_Lthree_of_local_convergence (U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hU : Measurable U) (v : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hv : ∀ (k : ℕ), Measurable (v k)) (M : ENNReal) (hvslice : ∀ (k : ℕ) (t : ℝ), MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (v k (x, t))) 3 MeasureTheory.volume ≤ M) (hconv : ∀ (N : ℕ), Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => v k z - U z) 3 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (↑N + 1) ×ˢ Set.Ioo (-(↑N + 1)) 0))) Filter.atTop (nhds 0)) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Iio 0), MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (U (x, t))) 3 MeasureTheory.volume ≤ M

Strong local L³ convergence of fields with uniformly bounded global L³ slices bounds almost every negative-time slice of the limit.