Cutoffs for the vorticity bootstrap

Spatial cutoffs between two concentric Euclidean balls and time cutoffs vanishing near the bottom of a time interval, with uniform bounds for their derivatives. The bounds depend only on the radii and on the time collar, which makes the constants of thm:vorticity-regularity of the Escauriaza–Seregin–Šverák manuscript independent of the centre of the cylinder.

theorem CKN.vorticitySpatialCutoff_exists {r R : ℝ} (hr : 0 < r) (hrR : r < R) : ∃ (φ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) φ ∧ HasCompactSupport φ ∧ tsupport φ ⊆ Foundation.Parabolic.vec3Ball 0 R ∧ (∀ (x : Foundation.Parabolic.Vec3), Foundation.Parabolic.vec3EuclideanNorm x ≤ r → φ x = 1) ∧ (∀ (x : Foundation.Parabolic.Vec3), 0 ≤ φ x) ∧ ∀ (x : Foundation.Parabolic.Vec3), φ x ≤ 1

A smooth spatial cutoff centred at the origin: equal to one on the closed ball of radius r, supported in the open ball of radius R, with values in [0, 1].

theorem CKN.vorticitySmooth_derivative_bounds {φ : Foundation.Parabolic.Vec3 → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) : ∃ (L : ℝ), 0 ≤ L ∧ (∀ (x : Foundation.Parabolic.Vec3) (j : Fin 3), |spatialDeriv φ j x| ≤ L) ∧ ∀ (x : Foundation.Parabolic.Vec3) (j k : Fin 3), |spatialDeriv (spatialDeriv φ j) k x| ≤ L

A smooth compactly supported function on space has uniformly bounded first and second coordinate derivatives.

theorem CKN.vorticitySpatialDeriv_translate (φ : Foundation.Parabolic.Vec3 → ℝ) (x₀ x : Foundation.Parabolic.Vec3) (j : Fin 3) : spatialDeriv (fun (y : Foundation.Parabolic.Vec3) => φ (y - x₀)) j x = spatialDeriv φ j (x - x₀)

Translating a function translates its coordinate derivatives.

theorem CKN.vorticityTimeCutoff_exists {κ : ℝ} (hκ : 0 < κ) : ∃ (θ : ℝ → ℝ), ContDiff ℝ (↑⊤) θ ∧ (∀ s ≤ κ / 2, θ s = 0) ∧ (∀ (s : ℝ), κ ≤ s → θ s = 1) ∧ (∀ (s : ℝ), 0 ≤ θ s) ∧ (∀ (s : ℝ), θ s ≤ 1) ∧ ∃ (L : ℝ), 0 ≤ L ∧ ∀ (s : ℝ), |deriv θ s| ≤ L

A smooth time cutoff which vanishes up to κ / 2, equals one from κ on, takes values in [0, 1] and has a bounded derivative.