iteratedFDerivWithin_succ_eq_comp_left

English

The (n+1)-th iterated derivative equals the left curry of the n-th derivative composed with the previous derivative.

Русский

(n+1)-я итеративная производная равна левой каррированной композиции с предыдущей производной.

LaTeX

$$$$\text{iteratedFDerivWithin}(\mathbb{k},n+1,f,s) = (\text{continuousMultilinearCurryLeftEquiv }\mathbb{k} \; (\text{Fin} (n+1) \Rightarrow E) ).\text{symm} \circ \text{fderivWithin}(\mathbb{k}, \text{iteratedFDerivWithin}(\mathbb{k},n,f,s),s).$$$$

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 iteratedFDerivWithin_succ_eq_comp_left {n : ℕ} :
    iteratedFDerivWithin 𝕜 (n + 1) f s =
      (continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) => E) F).symm ∘
        fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s :=
  rfl

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