English
Shift operation on a formal multilinear series p is defined by (shift p)_n = (p(n+1)).curryRight, i.e., it forgets the zeroth term and curries the rest.
Русский
Сдвиг формального мультилинейного ряда: (shift p)_n = (p(n+1)).curryRight, то есть забывается нулевой член и остальные приводятся к коренной форме.
LaTeX
$$$(\\mathrm{shift}\, p)_n = (p(n+1)).\\text{curryRight}$$$
Lean4
/-- Forgetting the zeroth term in a formal multilinear series, and interpreting the following terms
as multilinear maps into `E →L[𝕜] F`. If `p` is the Taylor series (`HasFTaylorSeriesUpTo`) of a
function, then `p.shift` is the Taylor series of the derivative of the function. Note that the
`p.sum` of a Taylor series `p` does not give the original function; for a formal multilinear
series that sums to the derivative of `p.sum`, see `HasFPowerSeriesOnBall.fderiv`. -/
def shift : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F) := fun n => (p n.succ).curryRight
