sum — Mathlib

English

If f has a power series within a set on a ball around x, then f(x+y) equals the sum of p for y inside that ball.

Русский

Если у f есть степенной ряд внутри области в шаре вокруг x, то f(x+y) равно сумме p для y внутри этого шара.

LaTeX

$$$ HasFPowerSeriesWithinOnBall f p s x r \Rightarrow \forall {y}, y ∈ EMetric.ball 0 r → f (x + y) = p.sum y $$$

Lean4

theorem sum (h : HasFPowerSeriesWithinOnBall f p s x r) {y : E} (h'y : x + y ∈ insert x s)
    (hy : y ∈ EMetric.ball (0 : E) r) : f (x + y) = p.sum y :=
  (h.hasSum h'y hy).tsum_eq.symm

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