The compactness hypotheses for the cutoff blow-up sequence

The modified sequence of prop:blowup-limit (cutoffs growing with the index, applied to a reindexed tail of the blow-up fields) satisfies the uniform slice, gradient, and pairing-modulus hypotheses of lem:compactness of the CKN manuscript on all of space and all negative times. Each hypothesis is reduced to the corresponding estimate for the original fields on a fixed bounded past cylinder, valid from a stage-dependent index on.

def ESS.blowupLimitAssemblyIndex (N : ℕ → ℕ) (m : ℕ) : ℕ

A strictly increasing index dominating the first m + 1 stage indices.

Equations

• ESS.blowupLimitAssemblyIndex N m = ∑ j ∈ Finset.range (m + 1), N j + m

theorem ESS.strictMono_blowupLimitAssemblyIndex (N : ℕ → ℕ) : StrictMono (blowupLimitAssemblyIndex N)

theorem ESS.le_blowupLimitAssemblyIndex (N : ℕ → ℕ) {j m : ℕ} (hjm : j ≤ m) : N j ≤ blowupLimitAssemblyIndex N m

Pointwise estimates

theorem ESS.blowupLimitAssembly_ofReal_abs_component_le (v : CKN.Foundation.Parabolic.Vec3) (i : Fin 3) : ENNReal.ofReal |v i| ≤ 1 + ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm v) ^ 2

A velocity component is controlled by one plus the squared Euclidean norm.

theorem ESS.blowupLimitAssembly_ofReal_abs_gradient_le (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) : ENNReal.ofReal |Du z i j| ≤ 1 + ENNReal.ofReal (CKN.spatialGradientSq u Du z)

A gradient entry is controlled by one plus the gradient energy density.

theorem ESS.blowupLimitAssembly_integrableOn_of_le_one_add {B : Set CKN.Foundation.Parabolic.Vec3} (hB : MeasureTheory.volume B < ⊤) {g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.volume.restrict B)) {F : CKN.Foundation.Parabolic.Vec3 → ENNReal} (hpt : ∀ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal |g x| ≤ 1 + F x) (hF : ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in B, F x < ⊤) : MeasureTheory.IntegrableOn g B MeasureTheory.volume

A function dominated by one plus a function of finite integral is integrable on a set of finite measure.

theorem ESS.blowupLimitAssemblyCutoffGradient_sq_le (f : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Df : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (ν : ℕ → ℕ) (k : ℕ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.spatialGradientSq (blowupLimitAssemblyCutoffField f ν k) (blowupLimitAssemblyCutoffGradient f Df ν k) z ≤ 2 * CKN.spatialGradientSq (f (ν k)) (Df (ν k)) z + 2 * 64 ^ 2 * CKN.Foundation.Parabolic.vec3EuclideanNorm (f (ν k) z) ^ 2

The gradient energy density of the modified field is controlled by the original gradient and velocity.

theorem ESS.blowupLimitAssemblyCutoffGradient_eq_zero (f : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Df : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (ν : ℕ → ℕ) (k : ℕ) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z.1 ∉ CKN.Foundation.Parabolic.vec3Ball 0 (↑k + 1) ∨ z.2 ≤ -(↑k + 1)) : blowupLimitAssemblyCutoffGradient f Df ν k z = 0

The modified gradient vanishes off the support of the cutoffs.