iteratedFDeriv_apply_eq_iteratedDeriv_mul_prod

English

The norm of iteratedFDeriv equals the norm of iteratedDeriv.

Русский

Норма iteratedFDeriv равна норме iteratedDeriv.

LaTeX

$$$\|\operatorname{iteratedFDeriv} 𝕜 n f x\| = \|\operatorname{iteratedDeriv} n f x\|$$$

Lean4

/-- The `n`-th Fréchet derivative applied to a vector `(m 0, ..., m (n-1))` is the derivative
multiplied by the product of the `m i`s. -/
theorem iteratedFDeriv_apply_eq_iteratedDeriv_mul_prod {m : Fin n → 𝕜} :
    (iteratedFDeriv 𝕜 n f x : (Fin n → 𝕜) → F) m = (∏ i, m i) • iteratedDeriv n f x := by
  rw [iteratedDeriv_eq_iteratedFDeriv, ← ContinuousMultilinearMap.map_smul_univ]; simp

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