English
Let k, n be nonnegative integers. For any Schwartz map f and any scalar c, the weighted n-th derivative norm of c · f at x scales by |c|: ‖x‖^k · ‖D^n(c f)(x)‖ = ‖c‖ · ‖x‖^k · ‖D^n f(x)‖. In words, scalar multiplication by c commutes with the n-th iterated derivative up to a factor ‖c‖.
Русский
Пусть k, n ∈ ℕ, f — Schwartz-образ, c — скаляр. Тогда взвешенная норма n-й производной функции f при умножении на скаляра масштабируется линейно по модулю скаляра: ‖x‖^k · ‖D^n(c f)(x)‖ = ‖c‖ · ‖x‖^k · ‖D^n f(x)‖.
LaTeX
$$$\\|x\\|^k \\cdot \\| \\mathrm{D}^n (c f)(x) \\| = \\|c\\| \\cdot \\|x\\|^k \\cdot \\| \\mathrm{D}^n f(x) \\|$$$
Lean4
theorem decay_smul_aux (k n : ℕ) (f : 𝓢(E, F)) (c : 𝕜) (x : E) :
‖x‖ ^ k * ‖iteratedFDeriv ℝ n (c • (f : E → F)) x‖ = ‖c‖ * ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ := by
rw [mul_comm ‖c‖, mul_assoc, iteratedFDeriv_const_smul_apply (f.smooth _).contDiffAt,
norm_smul c (iteratedFDeriv ℝ n (⇑f) x)]
