norm_iteratedFDeriv_clm_apply — Mathlib

English

A Faà di Bruno style bound for a composition with derivative bounds.

Русский

Граница Фаà ди Брюно для композиции.

LaTeX

$$$\displaystyle \|\operatorname{iteratedFDerivWithin}_{\mathbb{k}} n (g \circ f) s x\| \\le n! \cdot C \cdot D^n$$$

Lean4

theorem norm_iteratedFDeriv_clm_apply {f : E → F →L[𝕜] G} {g : E → F} {N : WithTop ℕ∞} {n : ℕ} (hf : ContDiff 𝕜 N f)
    (hg : ContDiff 𝕜 N g) (x : E) (hn : n ≤ N) :
    ‖iteratedFDeriv 𝕜 n (fun y : E => (f y) (g y)) x‖ ≤
      ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖ :=
  by
  simp only [← iteratedFDerivWithin_univ]
  exact norm_iteratedFDerivWithin_clm_apply hf.contDiffOn hg.contDiffOn uniqueDiffOn_univ (Set.mem_univ x) hn

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