Critical energy under blow-up scaling

The open-top energy on the unit past cylinder is the normalized energy at the original point and radius (prop:blowup-limit).

theorem ESS.blowupOpenPast_image_subset (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hr : 0 < r) (z : CKN.Foundation.Parabolic.ParabolicPoint) : z ∈ goodPointPastCylinder 0 0 1 → CKN.Foundation.Parabolic.parabolicTranslate x₀ t₀ (CKN.Foundation.Parabolic.parabolicScale r z) ∈ goodPointPastCylinder x₀ t₀ r

Scaling maps the open unit past cylinder to the open past cylinder at the original point.

theorem ESS.blowupEnergy_eq_unextendedRescale (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hr : 0 < r) (hopen : goodPointPastCylinder x₀ t₀ r ⊆ goodPointDomain) : goodPointEnergy (blowupVelocity x₀ t₀ r u) (blowupPressure x₀ t₀ r p) 0 0 1 = goodPointEnergy (parabolicRescaleVelocity x₀ t₀ r u) (parabolicRescalePressure x₀ t₀ r p) 0 0 1

Zero extension has no effect on the rescaled energy inside an admissible open past cylinder.

theorem ESS.blowupEnergy_rescale_of_admissible (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hr : 0 < r) (hopen : goodPointPastCylinder x₀ t₀ r ⊆ goodPointDomain) : goodPointEnergy (blowupVelocity x₀ t₀ r u) (blowupPressure x₀ t₀ r p) 0 0 1 = ENNReal.ofReal (r⁻¹ ^ 2) * goodPointEnergy u p x₀ t₀ r

The zero-extended blow-up fields have exactly the normalized critical energy of the original fields at an admissible open-top radius.

theorem ESS.blowupBadPointRescaledEnergy_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) ≤ goodPointEnergy (blowupVelocity z₀.1 z₀.2 r u) (blowupPressure z₀.1 z₀.2 r p) 0 0 1

At every admissible radius, a bad point gives the same lower bound on the rescaled unit-cylinder energy.

theorem ESS.blowupBadPoint_smallRadius_lower (ε₀ : ℝ) (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 : 0 < r) (hrsmall : r < 1 / 4) : ENNReal.ofReal (ε₀ / 8) ≤ goodPointEnergy (blowupVelocity x₀ t₀ r u) (blowupPressure x₀ t₀ r p) 0 0 1

A sufficiently small radius at a bad point has the quantitative rescaled-unit-cylinder lower bound.

theorem ESS.blowupBadPoint_eventually_lower (ε₀ : ℝ) (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

Along any shrinking positive scale sequence, the bad-point energy lower bound holds on the rescaled unit cylinder from some index onward.