Growing cutoffs for the blow-up sequence

The blow-up fields of prop:blowup-limit are controlled on each fixed bounded past cylinder only for all sufficiently large indices. To apply lem:compactness of the CKN manuscript once on all of space and all negative times, the k-th field of a reindexed sequence is multiplied by a smooth spatial cutoff equal to one on the ball of radius k and by a Lipschitz time ramp equal to one after time -k. On every fixed compact set the modified fields agree with the original ones from some index on.

noncomputable def ESS.blowupLimitAssemblySpaceCutoff (k : ℕ) : CKN.Foundation.Parabolic.Vec3 → ℝ

The smooth spatial cutoff of the k-th modified field: one on the ball of radius k, supported in the ball of radius k + 1/2.

Equations

• ESS.blowupLimitAssemblySpaceCutoff k = CKN.canonicalBallCutoff 0 (↑k) (↑k + 1 / 2)

def ESS.blowupLimitAssemblyTimeRamp (k : ℕ) (t : ℝ) : ℝ

The Lipschitz time ramp of the k-th modified field: zero before time -(k + 1) and one after time -k.

Equations

• ESS.blowupLimitAssemblyTimeRamp k t = max 0 (min 1 (t + (↑k + 1)))

noncomputable def ESS.blowupLimitAssemblyCutoffField (f : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (ν : ℕ → ℕ) (k : ℕ) : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3

The k-th modified velocity: the ν k-th field times the cutoffs.

Equations

• ESS.blowupLimitAssemblyCutoffField f ν k z = (ESS.blowupLimitAssemblyTimeRamp k z.2 * ESS.blowupLimitAssemblySpaceCutoff k z.1) • f (ν k) z

noncomputable def ESS.blowupLimitAssemblyCutoffGradient (f : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Df : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (ν : ℕ → ℕ) (k : ℕ) : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3

The weak spatial gradient of the k-th modified velocity, by the product rule.

Equations

• One or more equations did not get rendered due to their size.

The time ramp

theorem ESS.blowupLimitAssemblyTimeRamp_nonneg (k : ℕ) (t : ℝ) : 0 ≤ blowupLimitAssemblyTimeRamp k t

theorem ESS.blowupLimitAssemblyTimeRamp_le_one (k : ℕ) (t : ℝ) : blowupLimitAssemblyTimeRamp k t ≤ 1

theorem ESS.blowupLimitAssemblyTimeRamp_eq_zero {k : ℕ} {t : ℝ} (ht : t ≤ -(↑k + 1)) : blowupLimitAssemblyTimeRamp k t = 0

theorem ESS.blowupLimitAssemblyTimeRamp_eq_one {k : ℕ} {t : ℝ} (ht : -↑k ≤ t) : blowupLimitAssemblyTimeRamp k t = 1

theorem ESS.blowupLimitAssemblyTimeRamp_lipschitz (k : ℕ) (s t : ℝ) : |blowupLimitAssemblyTimeRamp k t - blowupLimitAssemblyTimeRamp k s| ≤ dist t s

The time ramp is 1-Lipschitz.

theorem ESS.blowupLimitAssemblyTimeRamp_clamp (k : ℕ) (t : ℝ) : blowupLimitAssemblyTimeRamp k t = blowupLimitAssemblyTimeRamp k (max t (-(↑k + 1)))

The time ramp does not see times before -(k + 1).

theorem ESS.continuous_blowupLimitAssemblyTimeRamp (k : ℕ) : Continuous (blowupLimitAssemblyTimeRamp k)

The spatial cutoff

theorem ESS.blowupLimitAssemblySpaceCutoff_contDiff (k : ℕ) : ContDiff ℝ (↑⊤) (blowupLimitAssemblySpaceCutoff k)

theorem ESS.blowupLimitAssemblySpaceCutoff_hasCompactSupport (k : ℕ) : HasCompactSupport (blowupLimitAssemblySpaceCutoff k)

theorem ESS.blowupLimitAssemblySpaceCutoff_nonneg (k : ℕ) (x : CKN.Foundation.Parabolic.Vec3) : 0 ≤ blowupLimitAssemblySpaceCutoff k x

theorem ESS.blowupLimitAssemblySpaceCutoff_le_one (k : ℕ) (x : CKN.Foundation.Parabolic.Vec3) : blowupLimitAssemblySpaceCutoff k x ≤ 1

theorem ESS.blowupLimitAssemblySpaceCutoff_tsupport_subset (k : ℕ) : tsupport (blowupLimitAssemblySpaceCutoff k) ⊆ CKN.Foundation.Parabolic.vec3Ball 0 (↑k + 1)

The closed support of the k-th spatial cutoff lies in the ball of radius k + 1.

theorem ESS.blowupLimitAssemblySpaceCutoff_eq_one {k : ℕ} {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∈ CKN.Foundation.Parabolic.vec3Ball 0 ↑k) : blowupLimitAssemblySpaceCutoff k x = 1

The spatial cutoff is one on the open ball of radius k.

theorem ESS.blowupLimitAssemblySpaceCutoff_gradient_eq_zero {k : ℕ} {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∈ CKN.Foundation.Parabolic.vec3Ball 0 ↑k) : CKN.classicalGradient (blowupLimitAssemblySpaceCutoff k) x = 0

The gradient of the spatial cutoff vanishes on the open ball of radius k.

theorem ESS.blowupLimitAssemblySpaceCutoff_gradient_eq_zero_of_notMem {k : ℕ} {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∉ CKN.Foundation.Parabolic.vec3Ball 0 (↑k + 1)) : CKN.classicalGradient (blowupLimitAssemblySpaceCutoff k) x = 0

The gradient of the spatial cutoff vanishes outside the ball of radius k + 1.

theorem ESS.blowupLimitAssemblySpaceCutoff_eq_zero_of_notMem {k : ℕ} {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∉ CKN.Foundation.Parabolic.vec3Ball 0 (↑k + 1)) : blowupLimitAssemblySpaceCutoff k x = 0

The spatial cutoff vanishes outside the ball of radius k + 1.

theorem ESS.blowupLimitAssemblySpaceCutoff_gradient_sq_le (k : ℕ) (x : CKN.Foundation.Parabolic.Vec3) : ∑ j : Fin 3, CKN.classicalGradient (blowupLimitAssemblySpaceCutoff k) x j ^ 2 ≤ 64 ^ 2

The gradient of every spatial cutoff has Euclidean norm at most 64.

theorem ESS.continuous_blowupLimitAssemblySpaceCutoff_gradient (k : ℕ) : Continuous (CKN.classicalGradient (blowupLimitAssemblySpaceCutoff k))

The modified fields

theorem ESS.measurable_blowupLimitAssemblyCutoffField (f : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (ν : ℕ → ℕ) (hf : ∀ (n : ℕ), Measurable (f n)) (k : ℕ) : Measurable (blowupLimitAssemblyCutoffField f ν k)

theorem ESS.measurable_blowupLimitAssemblyCutoffGradient (f : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Df : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (ν : ℕ → ℕ) (hf : ∀ (n : ℕ), Measurable (f n)) (hDf : ∀ (n : ℕ), Measurable (Df n)) (k : ℕ) : Measurable (blowupLimitAssemblyCutoffGradient f Df ν k)

theorem ESS.blowupLimitAssemblyCutoffField_norm_le (f : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (ν : ℕ → ℕ) (k : ℕ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.Foundation.Parabolic.vec3EuclideanNorm (blowupLimitAssemblyCutoffField f ν k z) ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm (f (ν k) z)

The modified velocity is pointwise no larger than the original one.

theorem ESS.blowupLimitAssemblyCutoff_eq_of_mem (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} (hx : z.1 ∈ CKN.Foundation.Parabolic.vec3Ball 0 ↑k) (ht : -↑k ≤ z.2) : blowupLimitAssemblyCutoffField f ν k z = f (ν k) z ∧ blowupLimitAssemblyCutoffGradient f Df ν k z = Df (ν k) z

On the cylinder where both cutoffs equal one, the modified velocity and its gradient are the original fields.

theorem ESS.blowupLimitAssemblyCutoff_eventually_eq (f : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Df : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (ν : ℕ → ℕ) (ρ : ℝ) : ∃ (K : ℕ), ∀ (k : ℕ), K ≤ k → ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ≤ ρ → -ρ ≤ z.2 → blowupLimitAssemblyCutoffField f ν k z = f (ν k) z ∧ blowupLimitAssemblyCutoffGradient f Df ν k z = Df (ν k) z

For every point, the modified fields agree with the original fields from some index on, uniformly on bounded sets.

theorem ESS.blowupLimitAssembly_hasWeakGradientOn_univ_const_mul {u : CKN.Foundation.Parabolic.Vec3 → ℝ} {G : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (c : ℝ) (h : CKN.HasWeakGradientOn Set.univ u G) : CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => c * u x) fun (x : CKN.Vec 3) => c • G x

Scalar multiples preserve whole-space weak gradients.

theorem ESS.blowupLimitAssemblyCutoff_hasWeakGradientOn (f : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Df : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (ν : ℕ → ℕ) (k : ℕ) (hweak : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-(↑k + 1)) 0), (∀ (i : Fin 3), CKN.HasWeakGradientOn (CKN.Foundation.Parabolic.vec3Ball 0 (↑k + 1)) (fun (x : CKN.Vec 3) => f (ν k) (x, t) i) fun (x : CKN.Vec 3) => Df (ν k) (x, t) i) ∧ (∀ (i : Fin 3), MeasureTheory.IntegrableOn (fun (x : CKN.Foundation.Parabolic.Vec3) => f (ν k) (x, t) i) (CKN.Foundation.Parabolic.vec3Ball 0 (↑k + 1)) MeasureTheory.volume) ∧ ∀ (i j : Fin 3), MeasureTheory.IntegrableOn (fun (x : CKN.Foundation.Parabolic.Vec3) => Df (ν k) (x, t) i j) (CKN.Foundation.Parabolic.vec3Ball 0 (↑k + 1)) MeasureTheory.volume) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Iio 0), ∀ (i : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => blowupLimitAssemblyCutoffField f ν k (x, t) i) fun (x : CKN.Vec 3) => blowupLimitAssemblyCutoffGradient f Df ν k (x, t) i

The modified velocity slices have the modified gradient as weak gradient on all of space, for almost every negative time, once the original slices have weak gradients in the ball of radius k + 1 after time -(k + 1) with locally integrable data.