Uniform derivative estimates for products of translated smooth transitions.

theorem AVenhance.Infra.Cutoff.DerivativeBounds.step_affine_iteratedDeriv (j : ℕ) (a c x : ℝ) : iteratedDeriv j (fun (y : ℝ) => step (a + c * y)) x = c ^ j * iteratedDeriv j step (a + c * x)

theorem AVenhance.Infra.Cutoff.DerivativeBounds.affine_product_iteratedDeriv_bound {N : ℕ} {M : ℝ} (hM : 1 ≤ M) (hstep : ∀ j ≤ N, ∀ (x : ℝ), |iteratedDeriv j step x| ≤ M) {a b c x : ℝ} (hc : |c| ≤ 1) {j : ℕ} (hj : j ≤ N) : |iteratedDeriv j (fun (y : ℝ) => step (a + c * y) * step (b - c * y)) x| ≤ 2 ^ N * M ^ 2

theorem AVenhance.Infra.Cutoff.scaled_translate_iteratedDeriv_bound {F : ℝ → ℝ} {N : ℕ} {B scale shift x : ℝ} (hF : ContDiff ℝ (↑⊤) F) (hbound : ∀ j ≤ N, ∀ (y : ℝ), |iteratedDeriv j F y| ≤ B) (hscale : 0 < scale) {j : ℕ} (hj : j ≤ N) : scale ^ j * |iteratedDeriv j (fun (t : ℝ) => F (t / scale - shift)) x| ≤ B

Scaling a translated profile by scale cancels the corresponding derivative factor.

theorem AVenhance.Infra.Cutoff.affine_product_iteratedDeriv_uniform_bound {N : ℕ} {M : ℝ} (hM : 1 ≤ M) (hstep : ∀ j ≤ N, ∀ (x : ℝ), |iteratedDeriv j step x| ≤ M) {a b x c : ℝ} (hc : |c| ≤ 1) {j : ℕ} (hj : j ≤ N) : |iteratedDeriv j (fun (y : ℝ) => step (a + c * y) * step (b - c * y)) x| ≤ 2 ^ N * M ^ 2