fderiv — Mathlib

English

The Fréchet derivative of the map x ↦ p.eval x is the linear map sending h to h times p.derivative.eval x.

Русский

Фрэше-производная отображения x ↦ p.eval x равна линейному отображению, отправляющему h в h·p.derivative.eval x.

LaTeX

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

Lean4

@[simp]
protected theorem fderiv : fderiv 𝕜 (fun x => p.eval x) x = smulRight (1 : 𝕜 →L[𝕜] 𝕜) (p.derivative.eval x) :=
  (p.hasFDerivAt x).fderiv

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