fderivWithin_eq — Mathlib

English

Within a ball, the derivative within equals the first-order coefficient of the shifted power series.

Русский

Внутри шара производная внутри равна первому порядку коэффициента смещённой степенной серии.

LaTeX

$$$\\text{HasFPowerSeriesWithinOnBall } f p s x r \\Rightarrow fderivWithin 𝕜 f (insert x s) (x+y) = \\operatorname{continuousMultilinearCurryFin1}_{\\mathbb{K}} E F (p(1))$$$

Lean4

theorem fderivWithin_eq [CompleteSpace F] (h : HasFPowerSeriesWithinOnBall f p s x r) {y : E} (hy : (‖y‖₊ : ℝ≥0∞) < r)
    (h'y : x + y ∈ insert x s) (hu : UniqueDiffOn 𝕜 (insert x s)) :
    fderivWithin 𝕜 f (insert x s) (x + y) = continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin y 1) :=
  (h.hasFDerivWithinAt hy h'y).fderivWithin (hu _ h'y)

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