English
On an open set s, iteratedFDerivWithin coincides with iteratedFDeriv on s.
Русский
На открытом множестве s итеративная производная внутри совпадает с глобальной.
LaTeX
$$$\forall n,\ IsOpen\ s \Rightarrow\ EqOn(\operatorname{iteratedFDerivWithin}_{\mathbb{k}}\ n\ f\ s) (\operatorname{iteratedFDeriv}_{\mathbb{k}}\ n\ f)\ s$$$
Lean4
/-- In an open set, the iterated derivative within this set coincides with the global iterated
derivative. -/
theorem iteratedFDerivWithin_of_isOpen (n : ℕ) (hs : IsOpen s) :
EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s := by
induction n with
| zero =>
intro x _
ext1
simp only [iteratedFDerivWithin_zero_apply, iteratedFDeriv_zero_apply]
| succ n IH =>
intro x hx
rw [iteratedFDeriv_succ_eq_comp_left, iteratedFDerivWithin_succ_eq_comp_left]
dsimp
congr 1
rw [fderivWithin_of_isOpen hs hx]
apply Filter.EventuallyEq.fderiv_eq
filter_upwards [hs.mem_nhds hx]
exact IH
