The blow-up limit

prop:blowup-limit in the form used by the proof of thm:ess-local: at a point that is not good, every sequence of scales tending to zero has a blow-up limit that is a suitable weak solution on every bounded past cylinder, has weak spatial gradients on almost every slice, lies in L^∞((-T,0); L³) for every T, has a pressure in L^(3/2) on every past slab, has zero terminal trace, and cannot vanish on the past of the unit cylinder (the bad-point lower bound).

theorem ESS.blowupLimit_projection {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)))) (hDu : MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)))) (hp : MeasureTheory.AEStronglyMeasurable p (MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)))) (hL2 : essSup (fun (t : ℝ) => ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 1, ‖u (x, t)‖ₑ ^ 2) (MeasureTheory.volume.restrict (Set.Ioo (-1) 0)) < ⊤) (henergy : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 < ⊤) (hpLp : MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)))) (hL3 : essSup (fun (t : ℝ) => ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 1, ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 3) (MeasureTheory.volume.restrict (Set.Ioo (-1) 0)) < ⊤) (hgrad : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), ∀ (i : Fin 3), CKN.HasWeakGradientOn (CKN.Foundation.Parabolic.vec3Ball 0 1) (fun (x : CKN.Vec 3) => u (x, t) i) fun (x : CKN.Vec 3) => Du (x, t) i) (hS2 : ∀ ψ ∈ CKN.spaceTimeTestFunction (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ∑ i : Fin 3, u z i * CKN.spatialPartial ψ i z = 0) (hS3 : ∀ φ ∈ CKN.spaceTimeTestFunction (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), -∑ i : Fin 3, u z i * CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z - p z * ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z - ∑ i : Fin 3, 0 z i * φ z i = 0) (ε₀ : ℝ) : 0 < ε₀ → ∀ (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ : ℝ) (r : ℕ → ℝ), x₀ ∈ closure (CKN.Foundation.Parabolic.vec3Ball 0 (1 / 2)) → t₀ ∈ Set.Icc (-(1 / 4)) 0 → ¬IsGoodPoint ε₀ u p (x₀, t₀) → (∀ (k : ℕ), 0 < r k) → Filter.Tendsto r Filter.atTop (nhds 0) → ∃ (U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (DU : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (q : CKN.Foundation.Parabolic.ParabolicPoint → ℝ), Measurable U ∧ (∀ (R a : ℝ), 0 < R → a < 0 → CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 R) (Set.Ioo a 0) 3 U DU q 0) ∧ (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-2) 0), ∀ (i : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Foundation.Parabolic.Vec3) => U (x, t) i) fun (x : CKN.Foundation.Parabolic.Vec3) => DU (x, t) i) ∧ (∀ (T : ℝ), 0 < T → essSup (fun (t : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (U (x, t))) 3 MeasureTheory.volume) (MeasureTheory.volume.restrict (Set.Ioo (-T) 0)) < ⊤) ∧ (∀ (T : ℝ), 0 < T → MeasureTheory.MemLp q (3 / 2) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo (-T) 0)))) ∧ HasZeroDistributionalVelocityTrace U ∧ (U =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo (-2) 0))] 0 → Filter.Tendsto (fun (k : ℕ) => goodPointEnergy (blowupVelocity x₀ t₀ (r k) u) (blowupPressure x₀ t₀ (r k) p) 0 0 1) Filter.atTop (nhds 0))

The blow-up limit at a point that is not good (prop:blowup-limit), under the hypotheses of thm:ess-local.