English
Under a finite-origin hypothesis, HasFiniteFPowerSeriesOnBall can be shifted: HasFiniteFPowerSeriesOnBall (p.changeOrigin · k) (p.changeOriginSeries k) 0 n ⊤.
Русский
При условии конечности происхождения можно сдвинуть: HasFiniteFPowerSeriesOnBall (p.changeOrigin · k) (p.changeOriginSeries k) 0 n ⊤.
LaTeX
$$HasFiniteFPowerSeriesOnBall (p.changeOrigin · k) (p.changeOriginSeries k) 0 n ⊤$$
Lean4
/-- If a function admits a finite power series expansion `p` on an open ball `B (x, r)`, then
it is continuously polynomial at every point of this ball. -/
theorem cpolynomialAt_of_mem (hf : HasFiniteFPowerSeriesOnBall f p x n r) (h : y ∈ EMetric.ball x r) :
CPolynomialAt 𝕜 f y :=
by
have : (‖y - x‖₊ : ℝ≥0∞) < r := by simpa [edist_eq_enorm_sub] using h
have := hf.changeOrigin this
rw [add_sub_cancel] at this
exact this.cpolynomialAt
