English
The derivative of the iterated derivative is the composition of the left curry-equivalence with the iterated derivative of higher order: fderiv 𝕜 (iteratedFDeriv 𝕜 n f) = continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) => E) F ∘ iteratedFDeriv 𝕜 (n + 1) f.
Русский
Производная от итеративной производной равна композиции с карри‑левым эквивалентом и далее интегрированной производной: fderiv 𝕜 (iteratedFDeriv 𝕜 n f) = continuousMultilinearCurryLeftEquiv 𝕜 (Fin (n+1) => E) ∘ iteratedFDeriv 𝕜 (n+1) f.
LaTeX
$$$\, fderiv 𝕜 (\operatorname{iteratedFDeriv}_{\mathbb{K}}^{n} f) = (\operatorname{continuousMultilinearCurryLeftEquiv}_{\mathbb{K}} (\lambda _ : Fin (n+1) => E) F) \circ \operatorname{iteratedFDeriv}_{\mathbb{K}}^{(n+1)} f$$$
Lean4
/-- Writing explicitly the `n+1`-th derivative as the composition of a currying linear equiv,
and the derivative of the `n`-th derivative. -/
theorem iteratedFDeriv_succ_eq_comp_left {n : ℕ} :
iteratedFDeriv 𝕜 (n + 1) f =
(continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) => E) F).symm ∘ fderiv 𝕜 (iteratedFDeriv 𝕜 n f) :=
rfl
