English
A variant of the previous formula, providing a similar finite-sum computation for extDerivWithin on ω with a given v.
Русский
Вариант предыдущей формулы, дающий аналогичное выражение через конечную сумму для extDerivWithin.
LaTeX
$$$ h : DifferentiableWithinAt 𝕜 ω s x, \\ hs : UniqueDiffWithinAt 𝕜 s x, \\ v : Fin (n+1) → E, \\\\ Eq (ContinuousAlternatingMap.funLike.coe (extDerivWithin ω s x) v) \\\\ (\\Finset.univ.sum (fun i => (-1)^i.val \\cdot fderivWithin 𝕜 (ω \\· (i.removeNth v)) s x (v i))) $$$
Lean4
theorem extDeriv_apply (h : DifferentiableAt 𝕜 ω x) (v : Fin (n + 1) → E) :
extDeriv ω x v = ∑ i, (-1) ^ i.val • fderiv 𝕜 (ω · (i.removeNth v)) x (v i) := by
simp [← extDerivWithin_univ, extDerivWithin_apply h.differentiableWithinAt]
