norm_iteratedFDerivWithin_fderivWithin

English

The operator-norm of the n-th iterated derivative of f within s can be identified with the operator-norm of the n-th derivative of the n-th derivative, via a suitable currying isomorphism.

Русский

Нормa оператора n-й повторной производной функции f внутри s может быть идентифицирована через норму оператора n-й производной n-й производной с помощью подходящего изоморфизма карри.

LaTeX

$$$\| \operatorname{iteratedFDerivWithin}_{\mathbb{K}}^{n} (f \circ) \| = \| \operatorname{iteratedFDerivWithin}_{\mathbb{K}}^{n} (\text{fderivWithin}_{\mathbb{K}} f) \|$$$

Lean4

theorem norm_iteratedFDerivWithin_fderivWithin {n : ℕ} (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
    ‖iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s x‖ = ‖iteratedFDerivWithin 𝕜 (n + 1) f s x‖ := by
  rw [iteratedFDerivWithin_succ_eq_comp_right hs hx, comp_apply, LinearIsometryEquiv.norm_map]

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