English
For any n, (q, p, c, v), the value of (q.compAlongOrderedFinpartition p c) v equals the evaluation of the composition at v.
Русский
Для любых n, (q, p, c, v) величина (q.compAlongOrderedFinpartition p c) v равна значению композиции в v.
LaTeX
$$c.compAlongOrderedFinpartition f p v = f (c.applyOrderedFinpartition p v)$$
Lean4
/-- Taylor formal composition of two formal multilinear series. The `n`-th coefficient in the
composition is defined to be the sum of `q.compAlongOrderedFinpartition p c` over all
ordered partitions of `n`.
In other words, this term (as a multilinear function applied to `v₀, ..., vₙ₋₁`) is
`∑'_{k} ∑'_{I₀ ⊔ ... ⊔ Iₖ₋₁ = {0, ..., n-1}} qₖ (p_{i₀} (...), ..., p_{iₖ₋₁} (...))`, where
`iₘ` is the size of `Iₘ` and one puts all variables of `Iₘ` as arguments to `p_{iₘ}`, in
increasing order. The sets `I₀, ..., Iₖ₋₁` are ordered so that `max I₀ < max I₁ < ... < max Iₖ₋₁`.
This definition is chosen so that the `n`-th derivative of `g ∘ f` is the Taylor composition of
the iterated derivatives of `g` and of `f`.
Not to be confused with another notion of composition for formal multilinear series, called just
`FormalMultilinearSeries.comp`, appearing in the composition of analytic functions.
-/
protected noncomputable def taylorComp (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) :
FormalMultilinearSeries 𝕜 E G := fun n ↦ ∑ c : OrderedFinpartition n, q.compAlongOrderedFinpartition p c
