hasFDerivAt — Mathlib

English

From a power series on a ball, one obtains a derivative at a translated point x+y with the same first-order coefficient.

Русский

Из степенной серии на шаре следует производная в точке x+y с тем же первым порядком коэффициента.

LaTeX

$$$\\text{HasFPowerSeriesOnBall } f p x r \\Rightarrow \\text{HasFDerivAt } f (\\operatorname{continuousMultilinearCurryFin1}_{\\mathbb{K}} E F (p(1))) (x+y)$$$

Lean4

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

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