fderiv_eq — Mathlib

English

The Fréchet derivative at x+y equals the first coefficient of the shifted power series.

Русский

Фреше-производная в точке x+y равна первой коэффиценте смещённой степенной серии.

LaTeX

$$$fderiv 𝕜 f (x+y) = \\operatorname{continuousMultilinearCurryFin1}_{\\mathbb{K}} E F (p(1))$$$

Lean4

theorem fderiv_eq [CompleteSpace F] (h : HasFPowerSeriesOnBall f p x r) {y : E} (hy : (‖y‖₊ : ℝ≥0∞) < r) :
    fderiv 𝕜 f (x + y) = continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin y 1) :=
  (h.hasFDerivAt hy).fderiv

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