fderiv_aeval — Mathlib

English

The Fréchet derivative of x ↦ aeval x q equals smulRight 1 ( aeval x (derivative q) ).

Русский

Фрэше-производная от x ↦ aeval x q равна smulRight 1 ( aeval x (derivative q) ).

LaTeX

$$$fderiv\_\{\mathbb{K}\}\left(\lambda x, aeval x q\right) x = smulRight\left(1 : \mathbb{K} \toL[\mathbb{K}] \mathbb{K}\right)\left( aeval x (derivative q)\right)$$$

Lean4

@[simp]
protected theorem fderiv_aeval : fderiv 𝕜 (fun x => aeval x q) x = smulRight (1 : 𝕜 →L[𝕜] 𝕜) (aeval x (derivative q)) :=
  (q.hasFDerivAt_aeval x).fderiv

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