Derivatives of x ^ m, m : ℤ within an open set

In this file we prove theorems about iterated derivatives of x ^ m, m : ℤ within an open set.

Keywords

iterated, derivative, power, open set

theorem iteratedDerivWithin_zpow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : Set 𝕜} (m : ℤ) (k : ℕ) (hs : IsOpen s) : Set.EqOn (iteratedDerivWithin k (fun (y : 𝕜) => y ^ m) s) (fun (y : 𝕜) => (∏ i ∈ Finset.range k, (↑m - ↑i)) * y ^ (m - ↑k)) s

theorem iteratedDerivWithin_one_div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {s : Set 𝕜} (k : ℕ) (hs : IsOpen s) : Set.EqOn (iteratedDerivWithin k (fun (y : 𝕜) => 1 / y) s) (fun (y : 𝕜) => (-1) ^ k * ↑k.factorial * y ^ (-1 - ↑k)) s