Derivatives of iterated derivatives within a set

At a point x with s ∈ 𝓝 x, the k-th iterated derivative within a unique-differentiability set s of a function that is C^n with k < n has an ordinary derivative at x, namely the (k+1)-th iterated derivative within s. This upgrades Mathlib's ContDiffWithinAt.differentiableWithinAt_iteratedDerivWithin to a HasDerivAt statement with an explicit derivative.

Main declarations

• ContDiffWithinAt.hasDerivAt_iteratedDerivWithin: the pointwise statement.
• ContDiffOn.hasDerivAt_iteratedDerivWithin: the same, from smoothness on all of s.

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 ContDiffWithinAt.hasDerivAt_iteratedDerivWithin {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {g : 𝕜 → E} {s : Set 𝕜} {x : 𝕜} {n : WithTop ℕ∞} {k : ℕ} (hg : ContDiffWithinAt 𝕜 n g s x) (hk : ↑k < n) (hs : UniqueDiffOn 𝕜 s) (hx : s ∈ nhds x) : HasDerivAt (iteratedDerivWithin k g s) (iteratedDerivWithin (k + 1) g s x) x

If g is C^n within a unique-differentiability set s at a point x with s ∈ 𝓝 x, then for k < n the k-th iterated derivative within s has derivative at x equal to the (k+1)-th iterated derivative within s.

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

If g is C^n on a unique-differentiability set s and s ∈ 𝓝 x, then for k < n the k-th iterated derivative within s has derivative at x equal to the (k+1)-th iterated derivative within s.