English
For a set s with UniqueDiffOn, x ∈ s, and any natural n, the (n+1)-th iterated derivative of f at x along a finite input m is obtained by composing the n-th derivative of the derivative with a currying isomorphism on the right.
Русский
Для множества s с UniqueDiffOn, x ∈ s и любого натурального n, (n+1)-я повторная производная функции f в точке x по аргументу m получается через композицию n-й производной от производной с помощью правого курарного отображения.
LaTeX
$$$\operatorname{iteratedFDerivWithin}_{\mathbb{K}}^{(n+1)} f\,s\,x = \big( (\text{continuousMultilinearCurryRightEquiv}' \,\mathbb{K}\, n \; E \; F)^{\! -1} \circ \operatorname{iteratedFDerivWithin}_{\mathbb{K}}^{n} ( y \mapsto fderivWithin_{\mathbb{K}} f\,s\,y) \; s \big) x$$$
Lean4
theorem iteratedFDerivWithin_succ_apply_right {n : ℕ} (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (m : Fin (n + 1) → E) :
(iteratedFDerivWithin 𝕜 (n + 1) f s x : (Fin (n + 1) → E) → F) m =
iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s x (init m) (m (last n)) :=
by
induction n generalizing x with
|
zero =>
rw [iteratedFDerivWithin_succ_eq_comp_left, iteratedFDerivWithin_zero_eq_comp, iteratedFDerivWithin_zero_apply,
Function.comp_apply, LinearIsometryEquiv.comp_fderivWithin _ (hs x hx)]
simp
| succ n IH =>
let I := (continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm
have A :
∀ y ∈ s,
iteratedFDerivWithin 𝕜 n.succ f s y = (I ∘ iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s) y :=
fun y hy ↦ by
ext m
simp [IH hy m, I]
calc
(iteratedFDerivWithin 𝕜 (n + 2) f s x : (Fin (n + 2) → E) → F) m =
(fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n.succ f s) s x : E → E [×n + 1]→L[𝕜] F) (m 0) (tail m) :=
by simp [iteratedFDerivWithin_succ_eq_comp_left]
_ =
(fderivWithin 𝕜 (I ∘ iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s) s x : E → E [×n + 1]→L[𝕜] F) (m 0)
(tail m) :=
by rw [fderivWithin_congr A (A x hx)]
_ =
(I ∘ fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s) s x : E → E [×n + 1]→L[𝕜] F) (m 0)
(tail m) :=
by simp [LinearIsometryEquiv.comp_fderivWithin _ (hs x hx)]
_ =
(fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s) s x : E → E [×n]→L[𝕜] E →L[𝕜] F)
(m 0) (init (tail m)) ((tail m) (last n)) :=
by simp [I]
_ = iteratedFDerivWithin 𝕜 (Nat.succ n) (fun y => fderivWithin 𝕜 f s y) s x (init m) (m (last (n + 1))) :=
by
rw [iteratedFDerivWithin_succ_apply_left, tail_init_eq_init_tail]
simp [init, tail]
