Uniform bounds for the cutoff blow-up sequence

Slice integrability, the local gradient bound, and the pairing modulus of lem:compactness of the CKN manuscript for the modified sequence of prop:blowup-limit, derived from stagewise bounds of the original fields.

theorem ESS.blowupLimitAssembly_measurable_spatialGradientSq (g : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dg : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (hDg : Measurable Dg) : Measurable fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialGradientSq g Dg z

theorem ESS.blowupLimitAssembly_slice_integrability (g : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dg : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (hg : Measurable g) (hDg : Measurable Dg) {R : ℝ} (hR : 0 < R) (a b : ℝ) (hslice : ∃ M < ⊤, ∀ (t : ℝ), ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in closure (CKN.Foundation.Parabolic.vec3Ball 0 R), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (g (x, t))) ^ 2 ≤ M) (G : ENNReal) (hG : G < ⊤) (hgrad : ∫⁻ (t : ℝ) in Set.Icc a b, ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 R, ENNReal.ofReal (CKN.spatialGradientSq g Dg (x, t)) ≤ G) : (∀ (t : ℝ) (i : Fin 3), MeasureTheory.IntegrableOn (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, t) i) (CKN.Foundation.Parabolic.vec3Ball 0 R) MeasureTheory.volume) ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc a b), ∀ (i j : Fin 3), MeasureTheory.IntegrableOn (fun (x : CKN.Foundation.Parabolic.Vec3) => Dg (x, t) i j) (CKN.Foundation.Parabolic.vec3Ball 0 R) MeasureTheory.volume

A uniform compact slice bound and a finite local gradient energy make the velocity slices and, for almost every time, the gradient slices integrable on a ball.

theorem ESS.blowupLimitAssemblyCutoff_gradient_bound_single (f : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Df : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (ν : ℕ → ℕ) (k : ℕ) (hf : ∀ (n : ℕ), Measurable (f n)) (hDf : ∀ (n : ℕ), Measurable (Df n)) (hslice : ∃ M < ⊤, ∀ (t : ℝ), ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in closure (CKN.Foundation.Parabolic.vec3Ball 0 (↑k + 1)), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (f (ν k) (x, t))) ^ 2 ≤ M) (G : ENNReal) (hG : G < ⊤) (hgrad : ∫⁻ (t : ℝ) in Set.Icc (-(↑k + 1)) 0, ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 (↑k + 1), ENNReal.ofReal (CKN.spatialGradientSq (f (ν k)) (Df (ν k)) (x, t)) ≤ G) (C : Set CKN.Foundation.Parabolic.Vec3) (a b : ℝ) (hb : b ≤ 0) : ∃ Bd < ⊤, ∫⁻ (t : ℝ) in Set.Icc a b, ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (CKN.spatialGradientSq (blowupLimitAssemblyCutoffField f ν k) (blowupLimitAssemblyCutoffGradient f Df ν k) (x, t)) ≤ Bd

The local gradient energy of one modified field is finite on every compact set and every past time interval.

theorem ESS.blowupLimitAssemblyCutoffField_pairing (f : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (ν : ℕ → ℕ) (k : ℕ) (w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.L2Vec3) (t : ℝ) : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, blowupLimitAssemblyCutoffField f ν k (x, t) i * (w x).ofLp i = blowupLimitAssemblyTimeRamp k t * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, f (ν k) (x, t) i * (blowupLimitAssemblySpaceCutoff k x • w x).ofLp i

The pairing of a modified field with a test factors through the time ramp and the spatially cut-off test.

theorem ESS.blowupLimitAssemblyCutoff_modulus_single (f : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (ν : ℕ → ℕ) (k Nk : ℕ) (hNk : Nk ≤ ν k) (hmod : ∀ (C : Set CKN.Foundation.Parabolic.Vec3), IsCompact C → C ⊆ CKN.Foundation.Parabolic.vec3Ball 0 (↑k + 1) → ∀ (a b : ℝ), Set.Icc a b ⊆ Set.Icc (-(↑k + 1)) 0 → ∀ (w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.L2Vec3), ContDiff ℝ (↑⊤) w → HasCompactSupport w → tsupport w ⊆ C → ∃ (A : ℝ) (B : ℝ) (θ : ℝ), 0 ≤ A ∧ 0 ≤ B ∧ 0 < θ ∧ ∀ (n : ℕ), Nk ≤ n → ∀ (s t : ℝ), s ∈ Set.Icc a b → t ∈ Set.Icc a b → |(∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, f n (x, t) i * (w x).ofLp i) - ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, f n (x, s) i * (w x).ofLp i| ≤ A * dist t s + B * dist t s ^ θ) (a b : ℝ) (hb : b ≤ 0) (w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.L2Vec3) (hw : ContDiff ℝ (↑⊤) w) : ∃ (A : ℝ) (B : ℝ) (θ : ℝ), 0 ≤ A ∧ 0 ≤ B ∧ 0 < θ ∧ ∀ (s t : ℝ), s ∈ Set.Icc a b → t ∈ Set.Icc a b → |(∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, blowupLimitAssemblyCutoffField f ν k (x, t) i * (w x).ofLp i) - ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, blowupLimitAssemblyCutoffField f ν k (x, s) i * (w x).ofLp i| ≤ A * dist t s + B * dist t s ^ θ

One modified field has a pairing modulus on every past time interval, from the modulus of the original field at its stage.

theorem ESS.blowupLimitAssemblyCutoff_modulus (f : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (N : ℕ → ℕ) (hmod : ∀ (m : ℕ) (C : Set CKN.Foundation.Parabolic.Vec3), IsCompact C → C ⊆ CKN.Foundation.Parabolic.vec3Ball 0 (↑m + 1) → ∀ (a b : ℝ), Set.Icc a b ⊆ Set.Icc (-(↑m + 1)) 0 → ∀ (w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.L2Vec3), ContDiff ℝ (↑⊤) w → HasCompactSupport w → tsupport w ⊆ C → ∃ (A : ℝ) (B : ℝ) (θ : ℝ), 0 ≤ A ∧ 0 ≤ B ∧ 0 < θ ∧ ∀ (n : ℕ), N m ≤ n → ∀ (s t : ℝ), s ∈ Set.Icc a b → t ∈ Set.Icc a b → |(∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, f n (x, t) i * (w x).ofLp i) - ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, f n (x, s) i * (w x).ofLp i| ≤ A * dist t s + B * dist t s ^ θ) (C : Set CKN.Foundation.Parabolic.Vec3) (hC : IsCompact C) (a b : ℝ) (hab : Set.Icc a b ⊆ Set.Iio 0) (w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.L2Vec3) (hw : ContDiff ℝ (↑⊤) w) (hwc : HasCompactSupport w) (hwC : tsupport w ⊆ C) : ∃ (A : ℝ) (B : ℝ) (θ : ℝ), 0 ≤ A ∧ 0 ≤ B ∧ 0 < θ ∧ ∀ (k : ℕ) (s t : ℝ), s ∈ Set.Icc a b → t ∈ Set.Icc a b → |(∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, blowupLimitAssemblyCutoffField f (blowupLimitAssemblyIndex N) k (x, t) i * (w x).ofLp i) - ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, blowupLimitAssemblyCutoffField f (blowupLimitAssemblyIndex N) k (x, s) i * (w x).ofLp i| ≤ A * dist t s + B * dist t s ^ θ

The modified sequence has one pairing modulus for all indices on every compact set and past time interval, as required by lem:compactness of the CKN manuscript.