English
The (n+1)-st iterated derivative within a set equals the derivativeWithin of the n-th iterated derivative with respect to the inside derivative operator.
Русский
(n+1)-я итеративная производная внутри множества равна производной внутри от n-ой итеративной производной по внутреннему оператору производной.
LaTeX
$$$\operatorname{iteratedDerivWithin}(n+1)\ f\ s x = \operatorname{iteratedDerivWithin} n(\operatorname{derivWithin} f s) s x$$$
Lean4
/-- The `n+1`-th iterated derivative within a set with unique derivatives can be obtained by
differentiating the `n`-th iterated derivative. -/
theorem iteratedDerivWithin_succ {x : 𝕜} :
iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x :=
by
by_cases hxs : AccPt x (𝓟 s)
· rw [iteratedDerivWithin_eq_iteratedFDerivWithin, iteratedFDerivWithin_succ_apply_left,
iteratedFDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_fderivWithin _ hxs.uniqueDiffWithinAt, derivWithin]
change
((ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) ((fderivWithin 𝕜 (iteratedDerivWithin n f s) s x : 𝕜 → F) 1) :
(Fin n → 𝕜) → F)
fun _ : Fin n => 1) =
(fderivWithin 𝕜 (iteratedDerivWithin n f s) s x : 𝕜 → F) 1
simp
·
simp [derivWithin_zero_of_not_accPt hxs, iteratedDerivWithin, iteratedFDerivWithin,
fderivWithin_zero_of_not_accPt hxs]
