English
Two-form composition: q.compAlongComposition p c is a continuous multilinear map built from q and p and c.
Русский
Композиция двух формальных много-линейных рядов: q.compAlongComposition p c строит непрерывную мультиляйн карту из q, p и c.
LaTeX
$$$(q.comp p)(n) = \\sum_{c:\\mathrm{Composition}(n)} q.compAlongComposition p c$$$
Lean4
/-- Formal composition of two formal multilinear series. The `n`-th coefficient in the composition
is defined to be the sum of `q.compAlongComposition p c` over all compositions of
`n`. In other words, this term (as a multilinear function applied to `v_0, ..., v_{n-1}`) is
`∑'_{k} ∑'_{i₁ + ... + iₖ = n} qₖ (p_{i_1} (...), ..., p_{i_k} (...))`, where one puts all variables
`v_0, ..., v_{n-1}` in increasing order in the dots.
In general, the composition `q ∘ p` only makes sense when the constant coefficient of `p` vanishes.
We give a general formula but which ignores the value of `p 0` instead.
-/
protected def comp (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) :
FormalMultilinearSeries 𝕜 E G := fun n => ∑ c : Composition n, q.compAlongComposition p c
