analyticAt_changeOrigin — Mathlib

English

If p encodes a power series with nonzero radius, then for any fixed k, the function x ↦ p.changeOrigin x k is analytic at 0.

Русский

Если p кодирует степенной ряд с ненулевым радиусом, то функция x ↦ p.changeOrigin x k аналитична в 0.

LaTeX

$$$\\text{AnalyticAt } 𝕜 (p.changeOrigin x k)\\; 0$ for each k with p.radius > 0$$

Lean4

/-- Power series terms are analytic as we vary the origin -/
theorem analyticAt_changeOrigin (p : FormalMultilinearSeries 𝕜 E F) (rp : p.radius > 0) (n : ℕ) :
    AnalyticAt 𝕜 (fun x ↦ p.changeOrigin x n) 0 :=
  (FormalMultilinearSeries.hasFPowerSeriesOnBall_changeOrigin p n rp).analyticAt

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