Energy at a bad point

Failure of the good-point criterion gives the quantitative lower bound at each admissible past radius (prop:blowup-limit).

theorem ESS.blowupSmallRadius_admissible (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hx₀ : x₀ ∈ closure (CKN.Foundation.Parabolic.vec3Ball 0 (1 / 2))) (ht₀ : t₀ ∈ Set.Icc (-(1 / 4)) 0) (hr : 0 < r) (hrsmall : r < 1 / 4) : (x₀, t₀) ∈ goodPointClosedTopDomain ∧ goodPointPastCylinder x₀ t₀ r ⊆ goodPointDomain ∧ closure (CKN.Foundation.Parabolic.parabolicCylinder x₀ t₀ r) ⊆ goodPointClosedTopDomain

A small past cylinder centered in the blow-up region is admissible for the good-point criterion.

theorem ESS.blowupBadPointEnergy_lower (ε₀ : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (z₀ : CKN.Foundation.Parabolic.ParabolicPoint) (r : ℝ) (hbad : ¬IsGoodPoint ε₀ u p z₀) (hbase : z₀ ∈ goodPointClosedTopDomain) (hr : 0 < r) (hopen : goodPointPastCylinder z₀.1 z₀.2 r ⊆ goodPointDomain) (hclosed : closure (CKN.Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 r) ⊆ goodPointClosedTopDomain) : ENNReal.ofReal (ε₀ / 8) ≤ ENNReal.ofReal (r⁻¹ ^ 2) * goodPointEnergy u p z₀.1 z₀.2 r

The negation of the good-point criterion supplies the fixed energy threshold at every admissible past radius.