Series for f(-x)

Stream: Is there code for X?

[Vasilii Nesterov]

Is there an operation on FormalMultilinearSeries that alternates the signs of the terms in a given series? Something like the following:

import Mathlib.Analysis.Analytic.Basic

universe u v w

variable {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {pf : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal}

noncomputable def FormalMultilinearSeries.alternate (pf : FormalMultilinearSeries 𝕜 E F) :
    FormalMultilinearSeries 𝕜 E F := fun n ↦ (-1)^n • pf n

theorem HasFPowerSeriesOnBall.alternate (hf : HasFPowerSeriesOnBall f pf x r) :
    HasFPowerSeriesOnBall (fun y ↦ f (x - y)) pf.alternate 0 r := sorry

I'd like to use such theorem to prove that $1-x+x^2-\dots$ converges to $(1 + x)^{-1}$ with docs#hasFPowerSeriesOnBall_inverse_one_sub. It also can be used to express the binomial series through hypergeometric series (which is already in Mathlib) as $(1 + x)^a = {}_2F_1(-a, b; b; -x)$.

[Jireh Loreaux]

That's just docs#FormalMultilinearSeries.compContinuousLinearMap with docs#ContinuousLinearMap.neg