analyticWithinAt_of_mem — Mathlib

English

If a function has a power series expansion on a ball around x, then it is analytic at every point within that ball.

Русский

Если функция имеет степенной ряд на шаре вокруг x, то аналитична во всех точках внутри этого шара.

LaTeX

$$HasFPowerSeriesOnBall f p x r \\Rightarrow AnalyticAt 𝕜 f x' for all x' in Ball x r$$

Lean4

/-- If a function admits a power series expansion `p` on an open ball `B (x, r)`, then
it is analytic at every point of this ball. -/
theorem analyticWithinAt_of_mem (hf : HasFPowerSeriesWithinOnBall f p s x r) (h : y ∈ insert x s ∩ EMetric.ball x r) :
    AnalyticWithinAt 𝕜 f s y :=
  by
  have : (‖y - x‖₊ : ℝ≥0∞) < r := by simpa [edist_eq_enorm_sub] using h.2
  have := hf.changeOrigin this (by simpa using h.1)
  rw [add_sub_cancel] at this
  exact this.analyticWithinAt

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