iteratedDerivWithin_one_div — Mathlib

English

Let k ∈ ℕ and s open in 𝕜. The k-th iterated derivative within s of the function y ↦ 1/y equals (−1)^k k! times y^(−1−k) on s.

Русский

Пусть k ∈ ℕ и s — открытое множество в 𝕜. k-й итерационный предел внутри s функции y ↦ 1/y равен (−1)^k k! · y^(−1−k) на s.

LaTeX

$$$$ s.\\text{EqOn} \\bigl(\\operatorname{iteratedDerivWithin} k (\\lambda y. 1/y) s\\bigr) \\bigl( (−1)^k k! \\cdot y^{-(1+k)} \\bigr) $$$$

Lean4

theorem iteratedDerivWithin_one_div (k : ℕ) (hs : IsOpen s) :
    s.EqOn (iteratedDerivWithin k (fun y ↦ 1 / y) s) (fun y ↦ (-1) ^ k * (k !) * (y ^ (-1 - k : ℤ))) :=
  by
  apply Set.EqOn.trans (iteratedDerivWithin_of_isOpen_eq_iterate hs)
  intro t ht
  simp

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