norm_iteratedFDeriv_clm_apply_const

English

Derivative of a constant-scaled map is bounded by the same derivative of the base map scaled by the constant.

Русский

Производная константного умножения всего отображения ограничена тем же пределом производной базового отображения.

LaTeX

$$$\displaystyle \|\operatorname{iteratedFDerivWithin}_{\mathbb{k}} n (\lambda y. (f(y)) c) s x\| \\le \\|c\| \cdot \|\operatorname{iteratedFDerivWithin}_{\mathbb{k}} n f s x\|.$$$

Lean4

theorem norm_iteratedFDeriv_clm_apply_const {f : E → F →L[𝕜] G} {c : F} {x : E} {N : WithTop ℕ∞} {n : ℕ}
    (hf : ContDiffAt 𝕜 N f x) (hn : n ≤ N) :
    ‖iteratedFDeriv 𝕜 n (fun y : E => (f y) c) x‖ ≤ ‖c‖ * ‖iteratedFDeriv 𝕜 n f x‖ :=
  by
  simp only [← iteratedFDerivWithin_univ]
  exact norm_iteratedFDerivWithin_clm_apply_const hf.contDiffWithinAt uniqueDiffOn_univ (Set.mem_univ x) hn

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