iteratedDeriv_eq_iterate — Mathlib

English

The n-th iterated derivative of f equals the n-th iterate of the differentiation operator: iteratedDeriv n f = deriv^n f.

Русский

N-я итеративная производная f равна N-кратному применению оператора производной: iteratedDeriv n f = deriv^n f.

LaTeX

$$$\\forall n \\in \\mathbb{N},\\; iteratedDeriv n f = \\operatorname{iterate}\\\\(\\\\, deriv \\\\, n) f$$$

Lean4

/-- The `n`-th iterated derivative can be obtained by iterating `n` times the
differentiation operation. -/
theorem iteratedDeriv_eq_iterate : iteratedDeriv n f = deriv^[n] f :=
  by
  ext x
  rw [← iteratedDerivWithin_univ]
  convert iteratedDerivWithin_eq_iterate (F := F)
  simp [derivWithin_univ]

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