iteratedFDeriv_const_smul_apply' — Mathlib

English

Let i be a natural number and a a scalar. If f is ContDiffAt 𝕜 i at x, then the i-th iterated derivative of the function x ↦ a·f x at x is a times the i-th iterated derivative of f at x.

Русский

Пусть i — натуральное число, a — скаляр. Если f является ContDiffAt 𝕜 i в точке x, то i-я итеративная производная функции x↦a·f(x) в x равна a·i-й итеративной производной f в x.

LaTeX

$$$\\displaystyle\\text{If } \\mathrm{ContDiffAt}_{\\mathbb{k}}(i,f,x), \\quad \\operatorname{iteratedFDeriv}_{\\mathbb{k}}(i,\\lambda x. a\\,f(x))(x) = a\\cdot \\operatorname{iteratedFDeriv}_{\\mathbb{k}}(i,f)(x).$$$

Lean4

theorem iteratedFDeriv_const_smul_apply' (hf : ContDiffAt 𝕜 i f x) :
    iteratedFDeriv 𝕜 i (fun x ↦ a • f x) x = a • iteratedFDeriv 𝕜 i f x :=
  iteratedFDeriv_const_smul_apply hf

Похожие утверждения