iteratedDeriv_const_add — Mathlib

English

For ContDiffOn f, the nth derivative of the inner composition x ↦ f (c x) behaves with c^n under appropriate conditions, showing homogeneous scaling.

Русский

Для ContDiffOn f n-я производная внутри композиции x ↦ f (c x) ведет себя как c^n, при подходящих условиях однородного масштабирования.

LaTeX

$$$\\operatorname{iteratedDerivWithin}_n (\\lambda x. f (c x)) s x = c^n \\cdot \\operatorname{iteratedDerivWithin}_n f s (c x)$$$

Lean4

theorem iteratedDeriv_const_add (hn : 0 < n) (c : F) : iteratedDeriv n (fun z => c + f z) x = iteratedDeriv n f x := by
  simpa only [← iteratedDerivWithin_univ] using iteratedDerivWithin_const_add hn c

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