English
Let p be a formal multilinear series encoding a power series with domain in a normed vector space. For each natural numbers k and l, the k-th origin-changed term of p at level l is obtained by summing the k-th origin-shifted term over all index sets of size l. In particular, the k-th change-origin series is the formal multilinear series whose l-th term is the sum of p.changeOriginSeriesTerm k l over all finite index sets of cardinality l.
Русский
Пусть p — формальная многолинеарная члена́, задающая степенной ряд в нормированном векторном пространстве. Для любых k, l т.н. k-й член ряда после переноса начала равен сумме соответствующих членов p.changeOriginSeriesTerm по всем множествам индексов размером l; таким образом, k-й член p.changeOriginSeries состоит из суммы по всем множествам размера l.
LaTeX
$$$p.changeOriginSeries_k(l) = \\sum_{S:\\{\,S:\\ Finset(Fin(k+l))\\,\\}, |S|=l} p.changeOriginSeriesTerm(k,l,S,S.2)$$$
Lean4
/-- The power series for `f.changeOrigin k`.
Given a formal multilinear series `p` and a point `x` in its ball of convergence,
`p.changeOrigin x` is a formal multilinear series such that
`p.sum (x+y) = (p.changeOrigin x).sum y` when this makes sense. Its `k`-th term is the sum of
the series `p.changeOriginSeries k`. -/
def changeOriginSeries (k : ℕ) : FormalMultilinearSeries 𝕜 E (E [×k]→L[𝕜] F) := fun l =>
∑ s : { s : Finset (Fin (k + l)) // Finset.card s = l }, p.changeOriginSeriesTerm k l s s.2
