comp_hasStrictDerivAt — Mathlib

English

If hl has a Fréchet derivative l' at f(x) and hf has a derivative f' at x, then the derivative of l ∘ f at x is the Fréchet derivative applied to f'.

Русский

Если у hl есть Фреше-дериватив l' в f(x) и hf — производная f в x, то дериватив лямбда-отображения композиции в x равен l' применённому к f'.

LaTeX

$$$$HasFDerivAt l l' (f x) \land HasDerivAt f f' x \Rightarrow HasDerivAt (l \circ f) (l' f') x$$$$

Lean4

theorem comp_hasStrictDerivAt (hl : HasStrictFDerivAt l l' (f x)) (hf : HasStrictDerivAt f f' x) :
    HasStrictDerivAt (l ∘ f) (l' f') x := by
  simpa only [one_apply, one_smul, smulRight_apply, coe_comp', (· ∘ ·)] using
    (hl.comp x hf.hasStrictFDerivAt).hasStrictDerivAt

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