comp_hasStrictFDerivAt — Mathlib

English

If y = f x and HasStrictDerivAt h₂ h₂' y, and f has strict Frechet derivative f' at x, then HasStrictFDerivAt (h₂ ∘ f) (h₂' · f') x.

Русский

Если y = f x и HasStrictDerivAt h₂ h₂' y, и у f есть строгая Фрéш-производная f' в x, то HasStrictFDerivAt (h₂ ∘ f) (h₂' · f') x.

LaTeX

$$$\text{If } y = f x \text{ and } HasStrictDerivAt h_2 h_2' y, \text{ then } HasStrictFDerivAt (h_2 \circ f) (h_2' \cdot f') x.$$$

Lean4

theorem comp_hasStrictFDerivAt {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x) (hh : HasStrictDerivAt h₂ h₂' (f x))
    (hf : HasStrictFDerivAt f f' x) : HasStrictFDerivAt (h₂ ∘ f) (h₂' • f') x :=
  by
  rw [HasStrictDerivAt] at hh
  convert (hh.restrictScalars 𝕜).comp x hf
  ext x
  simp [mul_comm]

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