norm_iteratedFDeriv_eq_norm_iteratedDeriv

English

The (n+1)-th iterated derivative within s equals the derivativeWithin of the n-th iterated derivative, evaluated at x.

Русский

(n+1)-я итеративная производная внутри s равна derivWithin от n-й iteratedDerivWithin.

LaTeX

$$$\operatorname{iteratedDerivWithin}(n+1)\ f\ s x = \operatorname{derivWithin}(\operatorname{iteratedDerivWithin} n f s)\ s x$$$

Lean4

theorem norm_iteratedFDeriv_eq_norm_iteratedDeriv : ‖iteratedFDeriv 𝕜 n f x‖ = ‖iteratedDeriv n f x‖ := by
  rw [iteratedDeriv_eq_equiv_comp, Function.comp_apply, LinearIsometryEquiv.norm_map]

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