iteratedFDeriv_succ_apply_right — Mathlib

English

The norm of the iterated derivative equals the norm of the corresponding higher derivative.

Русский

Нормa повторной производной равна норме соответствующей более высокой производной.

LaTeX

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

Lean4

theorem iteratedFDeriv_succ_apply_right {n : ℕ} (m : Fin (n + 1) → E) :
    (iteratedFDeriv 𝕜 (n + 1) f x : (Fin (n + 1) → E) → F) m =
      iteratedFDeriv 𝕜 n (fun y => fderiv 𝕜 f y) x (init m) (m (last n)) :=
  by
  rw [← iteratedFDerivWithin_univ, ← iteratedFDerivWithin_univ, ← fderivWithin_univ]
  exact iteratedFDerivWithin_succ_apply_right uniqueDiffOn_univ (mem_univ _) _

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