English
Bound for the nth derivative of a composition under derivative bounds for g and f.
Русский
Предел для n-й производной композиции при ограничениях на производные g и f.
LaTeX
$$$\displaystyle \|\operatorname{iteratedFDerivWithin}_{\mathbb{k}} n (g \circ f) s x\| \le n! \cdot C \cdot D^n$$$
Lean4
theorem norm_iteratedFDeriv_prod_le [DecidableEq ι] [NormOneClass A'] {u : Finset ι} {f : ι → E → A'} {N : WithTop ℕ∞}
(hf : ∀ i ∈ u, ContDiff 𝕜 N (f i)) {x : E} {n : ℕ} (hn : n ≤ N) :
‖iteratedFDeriv 𝕜 n (∏ j ∈ u, f j ·) x‖ ≤
∑ p ∈ u.sym n, (p : Multiset ι).multinomial * ∏ j ∈ u, ‖iteratedFDeriv 𝕜 ((p : Multiset ι).count j) (f j) x‖ :=
by
simpa [iteratedFDerivWithin_univ] using
norm_iteratedFDerivWithin_prod_le (fun i hi ↦ (hf i hi).contDiffOn) uniqueDiffOn_univ (mem_univ x) hn
