English
Let f have a power series on a ball around x with radius r; for any y with y ∈ Ball(0,r), we have f(x+y) = p.sum y.
Русский
Пусть у f есть степенной ряд на шаре с центром x и радиусом r; для любого y с y ∈ Ball(0,r) выполняется f(x+y) = p.sum y.
LaTeX
$$$ HasFPowerSeriesOnBall f p x r \Rightarrow \forall {y}, y \in EMetric.ball 0 r \Rightarrow f (x+y) = p.sum y $$$
Lean4
/-- In a complete space, the sum of a converging power series `p` admits `p` as a power series.
This is not totally obvious as we need to check the convergence of the series. -/
protected theorem hasFPowerSeriesOnBall [CompleteSpace F] (p : FormalMultilinearSeries 𝕜 E F) (h : 0 < p.radius) :
HasFPowerSeriesOnBall p.sum p 0 p.radius :=
{ r_le := le_rfl
r_pos := h
hasSum := fun hy => by
rw [zero_add]
exact p.hasSum hy }
