Bad-point lower bound in the blow-up limit

Badness gives a uniform lower bound at sufficiently small radii, while vanishing of both limiting critical fields makes the unit-cylinder energy tend to zero.

theorem ESS.blowup_limit_bad_point_lower_bound (ε₀ : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ : ℝ) (r : ℕ → ℝ) (hx₀ : x₀ ∈ closure (CKN.Foundation.Parabolic.vec3Ball 0 (1 / 2))) (ht₀ : t₀ ∈ Set.Icc (-(1 / 4)) 0) (hbad : ¬IsGoodPoint ε₀ u p (x₀, t₀)) (hr : ∀ (k : ℕ), 0 < r k) (hr0 : Filter.Tendsto r Filter.atTop (nhds 0)) : ∀ᶠ (k : ℕ) in Filter.atTop, ENNReal.ofReal (ε₀ / 8) ≤ goodPointEnergy (blowupVelocity x₀ t₀ (r k) u) (blowupPressure x₀ t₀ (r k) p) 0 0 1

Every sufficiently small scale at a bad point has the stated rescaled unit-cylinder energy lower bound.

theorem ESS.blowup_limit_zero_alternative (v : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hv : ∀ (k : ℕ), MeasureTheory.AEStronglyMeasurable (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (v k z)) (MeasureTheory.volume.restrict (goodPointPastCylinder 0 0 1))) (hp : ∀ (k : ℕ), MeasureTheory.AEStronglyMeasurable (p k) (MeasureTheory.volume.restrict (goodPointPastCylinder 0 0 1))) (hV : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (v k z)) 3 (MeasureTheory.volume.restrict (goodPointPastCylinder 0 0 1))) Filter.atTop (nhds 0)) (hP : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (p k) (3 / 2) (MeasureTheory.volume.restrict (goodPointPastCylinder 0 0 1))) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (k : ℕ) => goodPointEnergy (v k) (p k) 0 0 1) Filter.atTop (nhds 0)

Strong local critical-norm convergence to zero makes the blow-up energy on the unit past cylinder tend to zero.