The derivative of the transition cutoff ξ_{m,k}

ξ_{m,k}'(t) ≠ 0 forces ξ_{m,k}(t) ≠ 0 and 3/4 ≤ |t/τ_m - k| (both extrema of ξ have zero derivative), and |ξ_{m,k}'| ≤ C_ξ / τ_m.

theorem AVenhance.Infra.Section5.Contracts.sb_one_le_Nstar {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 1 ≤ Nstar β

theorem AVenhance.Infra.Section5.Contracts.sb_xi_nonneg_le_one {β : ℝ} (I : Ingredients β) (s : ℝ) : 0 ≤ I.xi s ∧ I.xi s ≤ 1

theorem AVenhance.Infra.Section5.Contracts.sb_deriv_xi_ne_zero {β : ℝ} (I : Ingredients β) {s : ℝ} (h : deriv I.xi s ≠ 0) : I.xi s ≠ 0 ∧ 3 / 4 < |s|

ξ' (s) ≠ 0 forces ξ s ∈ (0,1)-type support information.

theorem AVenhance.Infra.Section5.Contracts.sb_deriv_xiMK {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) (t : ℝ) : deriv (I.xiMK m k) t = deriv I.xi ((t - ↑k * tau β I.Λ m) / tau β I.Λ m) * (tau β I.Λ m)⁻¹

theorem AVenhance.Infra.Section5.Contracts.sb_deriv_xiMK_facts {β : ℝ} (I : Ingredients β) {m : ℕ} (k : ℤ) {t : ℝ} (h : deriv (I.xiMK m k) t ≠ 0) : I.xiMK m k t ≠ 0 ∧ ((↑k + 3 / 4) * tau β I.Λ m ≤ t ∨ t ≤ (↑k - 3 / 4) * tau β I.Λ m) ∧ |deriv (I.xiMK m k) t| ≤ I.Cxi / tau β I.Λ m

Support and size of ξ'_{m,k}.