Generic lemmas for iterated derivatives within sets

This file records calculus lemmas about iteratedDerivWithin that are independent of any completely-monotone or Bernstein-function structure.

Main declarations

• TauCeti.ContDiffOn.hasDerivAt_iteratedDerivWithin: differentiability of an iteratedDerivWithin on a neighbourhood inside a unique-differentiability set. For the plain fundamental-theorem identity on a compact interval use Mathlib's intervalIntegral.integral_derivWithin_Icc_of_contDiffOn_Icc together with iteratedDerivWithin_one.

theorem TauCeti.ContDiffOn.hasDerivAt_iteratedDerivWithin {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {g : 𝕜 → E} {s : Set 𝕜} {k : ℕ} (hf : ContDiffOn 𝕜 (↑(k + 1)) g s) (hs : UniqueDiffOn 𝕜 s) {x : 𝕜} (hx : s ∈ nhds x) : HasDerivAt (iteratedDerivWithin k g s) (iteratedDerivWithin (k + 1) g s x) x

At a point x in the interior of a unique-differentiability set s (s ∈ 𝓝 x), the derivative of the k-th iterated derivative-within-s of a C^(k+1) function is the (k+1)-th iterated derivative-within-s.