fderiv_iteratedFDeriv — Mathlib

English

The op-norm of the zeroth iterated derivative at x equals the norm of f(x).

Русский

Норма нулевой итеративной производной в точке x равна норме f(x).

LaTeX

$$$\|\operatorname{iteratedFDeriv}_{\mathbb{K}}^{0} f\ (x)\| = \|f(x)\|$$$

Lean4

/-- Writing explicitly the derivative of the `n`-th derivative as the composition of a currying
linear equiv, and the `n + 1`-th derivative. -/
theorem fderiv_iteratedFDeriv {n : ℕ} :
    fderiv 𝕜 (iteratedFDeriv 𝕜 n f) =
      continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) => E) F ∘ iteratedFDeriv 𝕜 (n + 1) f :=
  rfl

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