fun_comp — Mathlib

English

If hg and hf supply C^n conditions for g and f respectively, then the i-th iterated derivative of g ∘ f equals the Taylor series composition up to i.

Русский

Если hg и hf дают условия C^n для g и f, то i-я итеративная производная композиции равна композиции развёртывания по Тейлору до i-й степени.

LaTeX

$$$\forall i\le n,\; \operatorname{iteratedFDerivWithin} 𝕜 i (g \circ f) s x = (\ftaylorSeriesWithin 𝕜 g t (f x)).taylorComp (\ftaylorSeriesWithin 𝕜 f s x) i$$$

Lean4

@[fun_prop]
theorem fun_comp (x : E) (hg : ContDiffAt 𝕜 n g (f x)) (hf : ContDiffAt 𝕜 n f x) :
    ContDiffAt 𝕜 n (fun x => g (f x)) x :=
  hg.comp x hf

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