English
Let hh₂ be differentiable at h(x) with derivative h₂', and hh be differentiable at x with derivative h', then the derivative of the nth iterate (Nat.iterate) is h' raised to the n-th power under appropriate normalization.
Русский
Пусть hh₂ дифференцируема в h(x) с производной h₂', а hh — в x с производной h'. Производная n-й итерации равна h'^n при адекватной нормализации.
LaTeX
$$$$\\forall x, f, f', n:\\; \\text{HasDerivAt}(f,f',x) \\Rightarrow \\text{HasDerivAt}(f^{(n)},f'^{(n)},x). $$$$
Lean4
/-- The chain rule.
Note that the function `h₂` is a function on an algebra. If you are looking for the chain rule
with `h₂` taking values in a vector space, use `HasDerivAt.scomp`. -/
nonrec theorem comp (hh₂ : HasDerivAt h₂ h₂' (h x)) (hh : HasDerivAt h h' x) : HasDerivAt (h₂ ∘ h) (h₂' * h') x :=
hh₂.comp x hh hh.continuousAt
