iteratedFDeriv_succ_apply_left — Mathlib

English

For any n, the (n+1)-th derivative equals the derivative of the n-th derivative composed with a currying equivalence; concretely, the left-hand side equals the currying-left of the derivative of the n-th derivative.

Русский

Для любого n+1-ю производную можно выразить через дифференциал n-й производной и карри‑эквивалентность слева.

LaTeX

$$$\text{iteratedFDeriv}_{\mathbb{K}}^{(n+1)} f = (\text{continuousMultilinearCurryLeftEquiv}_{\mathbb{K}} (\lambda _:. E) F)^{-1} \circ \operatorname{fderiv}_{\mathbb{K}} (\operatorname{iteratedFDeriv}_{\mathbb{K}}^{n} f)$$$

Lean4

theorem iteratedFDeriv_succ_apply_left {n : ℕ} (m : Fin (n + 1) → E) :
    (iteratedFDeriv 𝕜 (n + 1) f x : (Fin (n + 1) → E) → F) m =
      (fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x : E → E [×n]→L[𝕜] F) (m 0) (tail m) :=
  rfl

Похожие утверждения