English
Let m ∈ ℤ, k ∈ ℕ, and s an open subset of 𝕜. On s, the k-th iterated derivative of the function y ↦ y^m equals a constant times y^(m−k), namely the product ∏_{i=0}^{k−1} (m − i) times y^(m−k).
Русский
Пусть m ∈ ℤ, k ∈ ℕ и s — открытое множество в 𝕜. Внутри s k-я кратная производная функции y ↦ y^m равна константе, равной произведению ∏_{i=0}^{k−1} (m − i), умноженной на y^(m−k).
LaTeX
$$$$ s.\\text{EqOn} \\bigl(\\operatorname{iteratedDerivWithin} k (\\lambda y. y^m) s\\bigr) \\bigl(\\lambda y. \\bigl(\\prod_{i \\in \\operatorname{Finset.range}(k)} (m - i)\\bigr) y^{m-k} \\bigr) $$$$
Lean4
theorem iteratedDerivWithin_zpow (m : ℤ) (k : ℕ) (hs : IsOpen s) :
s.EqOn (iteratedDerivWithin k (fun y ↦ y ^ m) s) (fun y ↦ (∏ i ∈ Finset.range k, ((m : 𝕜) - i)) * y ^ (m - k)) :=
by
apply Set.EqOn.trans (iteratedDerivWithin_of_isOpen_eq_iterate hs)
intro t ht
simp
