comp_sub — Mathlib

English

If f has a power series f = p around x, then f is analytic in a neighborhood of x.

Русский

Если вокруг точки x функция f разворачивается в степенной ряд p, тогда f аналитична в окрестности x.

LaTeX

$$$HasFPowerSeriesOnBall\ f\ p\ x \Rightarrow AnalyticWithinAt\ 𝕜\ f\ s\ x$$$

Lean4

/-- If a function `f` has a power series `p` around `x`, then the function `z ↦ f (z - y)` has the
same power series around `x + y`. -/
theorem comp_sub (hf : HasFPowerSeriesOnBall f p x r) (y : E) :
    HasFPowerSeriesOnBall (fun z => f (z - y)) p (x + y) r :=
  { r_le := hf.r_le
    r_pos := hf.r_pos
    hasSum := fun {z} hz => by
      convert hf.hasSum hz using 2
      abel }

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