comp_sub — Mathlib

English

If f has a power series at x, then the shifted function z ↦ f(z−y) has a power series at x+y with the same p.

Русский

Если f имеет степенной ряд в точке x, то сдвинутая функция z↦f(z−y) имеет степенной ряд в точке x+y с тем же p.

LaTeX

$$$HasFPowerSeriesAt\ f\ p\ x \Rightarrow HasFPowerSeriesAt\ (\\fun z \\to f (z - y))\ p\ (x + y)$$$

Lean4

theorem comp_sub (hf : AnalyticAt 𝕜 f x) (y : E) : AnalyticAt 𝕜 (fun z ↦ f (z - y)) (x + y) :=
  by
  obtain ⟨p, hf⟩ := hf
  exact ⟨p, hf.comp_sub _⟩

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