iteratedDeriv_eq_equiv_comp — Mathlib

English

The nth Fréchet derivative can be written as a composition of the piFieldEquiv with the iteratedDeriv.

Русский

n-й Фрéше производной может быть записан как композиция piFieldEquiv с iteratedDeriv.

LaTeX

$$$\operatorname{iteratedFDeriv} 𝕜 n f = (\operatorname{ContinuousMultilinearMap.piFieldEquiv} 𝕜 (Fin n) F) \circ \operatorname{iteratedDeriv} 𝕜 n f$$$

Lean4

/-- Write the iterated derivative as the composition of a continuous linear equiv and the iterated
Fréchet derivative -/
theorem iteratedDeriv_eq_equiv_comp :
    iteratedDeriv n f = (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).symm ∘ iteratedFDeriv 𝕜 n f := by ext x; rfl

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