English
The functorial application of compAlongOrderedFinpartition: (f) (p) applied to c equals applying f to the list of p-blocks assembled by c.
Русский
Применение compAlongOrderedFinpartition к f и p через c эквивалентно применению f к списку блоков p, составленному c.
LaTeX
$$c.compAlongOrderedFinpartition f p v = f (c.applyOrderedFinpartition p v)$$
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 compAlongOrderedFinpartition {n : ℕ} (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F)
(c : OrderedFinpartition n) : E [×n]→L[𝕜] G :=
c.compAlongOrderedFinpartition (q c.length) (fun m ↦ p (c.partSize m))
