norm_fderiv_iteratedFDeriv — Mathlib

English

The norm of the n-th iterated derivative of f.derivative equals the norm of the (n+1)-st iterated derivative of f at x.

Русский

Нормa n-й итеративной производной f равна норме (n+1)-й итеративной производной в точке x.

LaTeX

$$$\| fderiv_{\mathbb{k}}(\operatorname{iteratedFDeriv}_{\mathbb{k}}\; n\; f)\, x \| = \| \operatorname{iteratedFDeriv}_{\mathbb{k}}\; (n+1)\; f\; x \|$$$

Lean4

theorem norm_fderiv_iteratedFDeriv {n : ℕ} : ‖fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x‖ = ‖iteratedFDeriv 𝕜 (n + 1) f x‖ := by
  rw [iteratedFDeriv_succ_eq_comp_left, comp_apply, LinearIsometryEquiv.norm_map]

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