English
Given q and p and a composition c of n, the composed series q.compAlongComposition p c uses the c.length-th coefficient of q applied to the blockwise applications of p.
Русский
Дано q и p и композицию c над n: q.compAlongComposition p c использует коэффициент c.length-й перестановки q, применяя блоки p к соответствующим подмвлям.
LaTeX
$$$(q.compAlongComposition p c) = f\\_c : E^{n}→G,\\text{ where } f\_c(v)=q_{c.length}( p_{i_1}(v_1,...),..., p_{i_k}(v_k,...) ).$$$
Lean4
/-- Given two formal multilinear series `q` and `p` and a composition `c` of `n`, one may
form a continuous multilinear map in `n` variables by applying the right coefficient of `p` to each
block of the composition, and then applying `q c.length` to the resulting vector. It is
called `q.compAlongComposition p c`. -/
def compAlongComposition {n : ℕ} (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F)
(c : Composition n) : (E [×n]→L[𝕜] G) :=
(q c.length).compAlongComposition p c
