English
When ω is differentiable within s at x, extDerivWithin ω s x can be computed by a finite sum of weighted fderivWithin terms.
Русский
Если ω дифференцируема внутри s в точке x, extDerivWithin ω s x может быть вычислена как конечная сумма взвешенных членов fderivWithin.
LaTeX
$$$ h : DifferentiableWithinAt\\ 𝕜\\ ω\\ s\\ x, \\ hs : UniqueDiffWithinAt 𝕜 s x, \\ v : Fin(n+1) \\to E, \\\\ extDerivWithin(ω\\, s\\, x\\, v) = \\sum_i (-1)^i \\cdot fderivWithin\\ 𝕜\\ (ω \\cdot (i.removeNth\\ v))\\ s\\ x\\ (v_i) $$$
Lean4
theorem extDerivWithin_apply (h : DifferentiableWithinAt 𝕜 ω s x) (hs : UniqueDiffWithinAt 𝕜 s x)
(v : Fin (n + 1) → E) :
extDerivWithin ω s x v = ∑ i, (-1) ^ i.val • fderivWithin 𝕜 (ω · (i.removeNth v)) s x (v i) := by
simp [extDerivWithin, ContinuousAlternatingMap.alternatizeUncurryFin_apply,
fderivWithin_continuousAlternatingMap_apply_const_apply, *]
