Blowup Cutoff Spatial Bound

Cutoff bounds used to localize the rescaled endpoint sequence.

theorem ESS.blowupBallCutoff_derivative_bounds (R : ℝ) (hR : 0 < R) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : CKN.Foundation.Parabolic.Vec3), (∀ (i : Fin 3), |(fderiv ℝ (CKN.canonicalBallCutoff 0 R (R + 1)) x) (CKN.basisVec i)| ≤ C) ∧ ∀ (i : Fin 3), |(fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ (CKN.canonicalBallCutoff 0 R (R + 1)) y) (CKN.basisVec i)) x) (CKN.basisVec i)| ≤ C

The fixed spatial cutoff has bounded first and second coordinate derivatives. The bound depends on the chosen ball but not on the time cutoff.

theorem ESS.blowupEnergyCutoff_coefficient_bounds (R : ℝ) (hR : 0 < R) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (a b : ℝ), b < 0 → ∀ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), CKN.timePartialProd (blowupEnergyCutoff R a b) z ≤ 8 ∧ (∀ (i : Fin 3), |CKN.spatialPartialProd (blowupEnergyCutoff R a b) i z| ≤ C) ∧ ∀ (i : Fin 3), |CKN.spatialSecondPartialProd (blowupEnergyCutoff R a b) i i z| ≤ C

Spatial coefficients of the energy test have one bound independent of the upper time cutoff. Its time derivative has a uniform upper bound.