Derivative bounds for the Serrin cutoff profiles

The ball cutoff of radius ρ has n-th derivative of size ρ⁻ⁿ and the time cutoff of parabolic length ρ² has n-th derivative of size ρ⁻²ⁿ, uniformly in the centre. These are the scaling bounds for the cutoffs of the backward windows used in the interior estimates of the proof of lem:aniso:annulus.

theorem CIV.serrinBallCutoff_eq_unit (x : CKN.Foundation.Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (y : CKN.Foundation.Parabolic.Vec3) : serrinBallCutoff x ρ y = serrinBallCutoff 0 1 (ρ⁻¹ • (y - x))

The ball cutoff at x of radius ρ is the unit cutoff at the origin evaluated at ρ⁻¹ (y - x).

theorem CIV.hasCompactSupport_serrinBallCutoff_unit : HasCompactSupport (serrinBallCutoff 0 1)

The unit ball cutoff has compact support.

theorem CIV.norm_iteratedFDeriv_serrinBallCutoff_le : ∃ (C : ℕ → ℝ), ∀ (n : ℕ) (x : CKN.Foundation.Parabolic.Vec3) (ρ : ℝ), 0 < ρ → ∀ (y : CKN.Foundation.Parabolic.Vec3), ‖iteratedFDeriv ℝ n (serrinBallCutoff x ρ) y‖ ≤ C n / ρ ^ n

Scaling bound for the derivatives of the ball cutoff.

theorem CIV.contDiff_serrinTimeBump : ContDiff ℝ (↑⊤) serrinTimeBump

The time profile is smooth.

theorem CIV.hasCompactSupport_deriv_serrinTimeBump : HasCompactSupport (deriv serrinTimeBump)

The derivative of the time profile vanishes off [-1, -1/2].

theorem CIV.exists_abs_iteratedDeriv_serrinTimeBump_le (n : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (τ : ℝ), |iteratedDeriv n serrinTimeBump τ| ≤ C

The derivatives of the time profile are bounded.

theorem CIV.abs_iteratedDeriv_serrinTimeBump_scaled_le : ∃ (C : ℕ → ℝ), ∀ (n : ℕ) (s ρ : ℝ), 0 < ρ → ∀ (s' : ℝ), |iteratedDeriv n (fun (r : ℝ) => serrinTimeBump ((r - s) / ρ ^ 2)) s'| ≤ C n / ρ ^ (2 * n)

Scaling bound for the derivatives of the time cutoff of parabolic length ρ².