iteratedFDeriv_eq_equiv_comp — Mathlib

English

The nth Fréchet derivative evaluated at a vector m = (m0,...,m(n-1)) equals the product of the m_i's times iteratedDeriv n f x.

Русский

n-я Фрéше-дериватива на векторе m = (m0,...,m(n-1)) равна произведению m_i на iteratedDeriv n f x.

LaTeX

$$$(\operatorname{iteratedFDeriv} 𝕜 n f x : (Fin n → 𝕜) → F) m = (\prod i, m i) \cdot \operatorname{iteratedDeriv} n f x$$$

Lean4

/-- Write the iterated Fréchet derivative as the composition of a continuous linear equiv and the
iterated derivative. -/
theorem iteratedFDeriv_eq_equiv_comp :
    iteratedFDeriv 𝕜 n f = ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F ∘ iteratedDeriv n f := by
  rw [iteratedDeriv_eq_equiv_comp, ← Function.comp_assoc, LinearIsometryEquiv.self_comp_symm, Function.id_comp]

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