iteratedDerivWithin_eq_iterate — Mathlib

English

The nth iterated derivative within s can be realized as the nth iterate of the operator derivWithin f s.

Русский

(n)-я итеративная производная внутри s равна n-му повторному применению оператора derivWithin.

LaTeX

$$$\operatorname{iteratedDerivWithin} n f s x = (\operatorname{derivWithin} g s)^{[n]}(f)(x)$$$

Lean4

/-- The `n`-th iterated derivative within a set with unique derivatives can be obtained by
iterating `n` times the differentiation operation. -/
theorem iteratedDerivWithin_eq_iterate {x : 𝕜} :
    iteratedDerivWithin n f s x = (fun g : 𝕜 → F => derivWithin g s)^[n] f x := by
  induction n generalizing x with
  | zero => simp
  | succ n IH =>
    rw [iteratedDerivWithin_succ, Function.iterate_succ']
    exact derivWithin_congr (fun y hy => IH) IH

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