Blowup Cutoff Product

Cutoff bounds used to localize the rescaled endpoint sequence.

noncomputable def ESS.blowupEnergyCutoff (R a b : ℝ) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) : ℝ

The spatial cutoff times the past time cutoff used in the rescaled local energy inequality.

Equations

• ESS.blowupEnergyCutoff R a b z = CKN.canonicalBallCutoff 0 R (R + 1) z.1 * ESS.blowupTimeCutoff a b z.2

theorem ESS.blowupEnergyCutoff_test (R a b : ℝ) (hR : 0 < R) (hb : b < 0) : blowupEnergyCutoff R a b ∈ CKN.spaceTimeTestFunction (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0) ∧ ∀ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), 0 ≤ blowupEnergyCutoff R a b z

The energy cutoff is an admissible nonnegative test on a fixed larger past cylinder.

theorem ESS.blowupEnergyCutoff_eq_one {R a b : ℝ} (hR : 0 < R) (hb : b < 0) {z : CKN.Foundation.Parabolic.Vec3 × ℝ} (hz : z.1 ∈ CKN.euclideanBall 0 R ∧ z.2 ∈ Set.Icc a b) : blowupEnergyCutoff R a b z = 1

The energy cutoff equals one on the target spatial ball and past time plateau.