English
A full Faà di Bruno type bound for derivatives of a composition.
Русский
Полное неравенство Фаà ди Брюно для композиции.
LaTeX
$$$\displaystyle \|\operatorname{iteratedFDerivWithin}_{\mathbb{k}} n (g \circ f) s x\| \\le n! \cdot C \cdot D^n$$$
Lean4
/-- If the derivatives of `g` at `f x` are bounded by `C`, and the `i`-th derivative
of `f` at `x` is bounded by `D^i` for all `1 ≤ i ≤ n`, then the `n`-th derivative
of `g ∘ f` is bounded by `n! * C * D^n`. -/
theorem norm_iteratedFDeriv_comp_le {g : F → G} {f : E → F} {n : ℕ} {N : WithTop ℕ∞} (hg : ContDiff 𝕜 N g)
(hf : ContDiff 𝕜 N f) (hn : n ≤ N) (x : E) {C : ℝ} {D : ℝ} (hC : ∀ i, i ≤ n → ‖iteratedFDeriv 𝕜 i g (f x)‖ ≤ C)
(hD : ∀ i, 1 ≤ i → i ≤ n → ‖iteratedFDeriv 𝕜 i f x‖ ≤ D ^ i) : ‖iteratedFDeriv 𝕜 n (g ∘ f) x‖ ≤ n ! * C * D ^ n :=
by
simp_rw [← iteratedFDerivWithin_univ] at hC hD ⊢
exact
norm_iteratedFDerivWithin_comp_le hg.contDiffOn hf.contDiffOn hn uniqueDiffOn_univ uniqueDiffOn_univ
(mapsTo_univ _ _) (mem_univ x) hC hD
