English
On a set with unique differentiability, if HasFTaylorSeriesUpToOn n f p s holds, then for all m ≤ n and x ∈ s with UniqueDiffOn, the Taylor coefficient p x m equals the iterated derivative within: p x m = iteratedFDerivWithin 𝕜 m f s x.
Русский
На множестве с уникальной дифференцируемостью, если выполняется HasFTaylorSeriesUpToOn n f p s, то для всех m ≤ n и x ∈ s с UniqueDiffOn коэффициент Тейлора p x m совпадает с iteratedFDerivWithin 𝕜 m f s x.
LaTeX
$$$\forall {m : Nat},\ m \le n \to UniqueDiffOn 𝕜 s \to x \in s\to p\ x\ m = iteratedFDerivWithin 𝕜 m f s x$$$
Lean4
/-- On a set with unique differentiability, any choice of iterated differential has to coincide
with the one we have chosen in `iteratedFDerivWithin 𝕜 m f s`. -/
theorem eq_iteratedFDerivWithin_of_uniqueDiffOn (h : HasFTaylorSeriesUpToOn n f p s) {m : ℕ} (hmn : m ≤ n)
(hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) : p x m = iteratedFDerivWithin 𝕜 m f s x := by
induction m generalizing x with
| zero => rw [h.zero_eq' hx, iteratedFDerivWithin_zero_eq_comp, comp_apply]
| succ m IH =>
have A : m < n := lt_of_lt_of_le (mod_cast lt_add_one m) hmn
have :
HasFDerivWithinAt (fun y : E => iteratedFDerivWithin 𝕜 m f s y)
(ContinuousMultilinearMap.curryLeft (p x (Nat.succ m))) s x :=
(h.fderivWithin m A x hx).congr (fun y hy => (IH (le_of_lt A) hy).symm) (IH (le_of_lt A) hx).symm
rw [iteratedFDerivWithin_succ_eq_comp_left, Function.comp_apply, this.fderivWithin (hs x hx)]
exact (ContinuousMultilinearMap.uncurry_curryLeft _).symm
