Power series expansion

Stream: Is there code for X?

[Andrew Yang]

Given a HasFPowerSeriesOnBall, how can I write the function as an actual sum of power series plus a remainder with the "shifted power series"? Concretely, here is a sorry that I want to fill in, but I don't think this is stated in the right generality and it is probably why I couldn't find API for it.

import Mathlib

open NNReal Finset in
example (f : ℂ → ℂ) (a : ℕ → ℂ) {x : ℂ} {r : ℝ≥0}
    (hf : HasFPowerSeriesOnBall f (.ofScalars ℂ a) x r) (k : ℕ) :
    ∃ g : ℂ → ℂ, HasFPowerSeriesOnBall g (.ofScalars ℂ (a <| · + k)) x r ∧
      f = (fun z ↦ ∑ i ∈ range k, a i * (z - x) ^ i + g z * (z - x) ^ k) := by
  refine ⟨fun z ↦ if z = x then a (k + 1) else
      (f z - ∑ i ∈ range k, a i * (z - x) ^ i) / (z - x) ^ k, ?_, ?_⟩
  · sorry -- I don't know how
  · sorry -- true by definition