norm_iteratedFDeriv_fderiv — Mathlib

English

The norm of iteratedFDeriv of the fderiv equals the norm of iteratedFDeriv of f of order n+1.

Русский

Норма повторной производной fderiv равна норме итеративной производной f порядка n+1.

LaTeX

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

Lean4

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

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