Derivative bounds for expanding cutoffs

Subtracting a constant from χ (R⁻¹ • ·) leaves every positive-order derivative unchanged. For R ≥ 1, a bound B on the i-th derivative of χ therefore gives a bound B / R on the corresponding derivative of the cutoff error. Only Cⁱ regularity is needed. Including order zero, the same hypotheses give a uniform bound B + ‖c‖ after subtracting an arbitrary constant c.

This estimate is shared by the Sobolev and Schwartz-space cutoff approximations. It is extracted from the derivative scaling argument in TauCeti/Analysis/Distribution/SchwartzSpace/Cutoff.lean, using Mathlib's iteratedFDeriv_comp_const_smul.

theorem TauCeti.norm_iteratedFDeriv_comp_inv_smul_sub_const_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {χ : E → F} {i : ℕ} (hχ : ContDiff ℝ (↑i) χ) (hi : i ≠ 0) {B : ℝ} (hB : ∀ (x : E), ‖iteratedFDeriv ℝ i χ x‖ ≤ B) {R : ℝ} (hR : 1 ≤ R) (c : F) (x : E) : ‖iteratedFDeriv ℝ i (fun (y : E) => χ (R⁻¹ • y) - c) x‖ ≤ B / R

For a positive derivative order and R ≥ 1, subtracting a constant from an expanding cutoff gives a derivative bound B / R, where B bounds that derivative of the cutoff.

theorem TauCeti.norm_iteratedFDeriv_comp_inv_smul_sub_const_le_add_norm {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {χ : E → F} {i : ℕ} (hχ : ContDiff ℝ (↑i) χ) {B : ℝ} (hB : ∀ (x : E), ‖iteratedFDeriv ℝ i χ x‖ ≤ B) {R : ℝ} (hR : 1 ≤ R) (c : F) (x : E) : ‖iteratedFDeriv ℝ i (fun (y : E) => χ (R⁻¹ • y) - c) x‖ ≤ B + ‖c‖

For any derivative order and R ≥ 1, subtracting a constant from an expanding cutoff gives a derivative bound B + ‖c‖, where B bounds that derivative of the cutoff.