English
Given p: E → F, c a composition of n, and f: F[×c.length] → L G, the map f.compAlongComposition p c forms a multilinear map E[×n] → G by applying p to each block and then f to the resulting vector.
Русский
Дано p: E→F, композиция c of n и f: F[×c.length]→L G; отображение f.compAlongComposition p c образует много-линейное отображение E[×n]→G, применяя p к каждому блоку и затем f к полученному вектору.
LaTeX
$$$(f.{\\text{compAlongComposition}}\\ p\\ c) : E^{\\otimes n} → G.\\quad (f.compAlongComposition\\ p\\ c)(v) = f( p.applyComposition(c,v) ).$$$
Lean4
/-- Given a formal multilinear series `p`, a composition `c` of `n` and a continuous multilinear
map `f` in `c.length` variables, 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 `f` to
the resulting vector. It is called `f.compAlongComposition p c`. -/
def compAlongComposition {n : ℕ} (p : FormalMultilinearSeries 𝕜 E F) (c : Composition n) (f : F [×c.length]→L[𝕜] G) :
E [×n]→L[𝕜] G
where
toMultilinearMap :=
MultilinearMap.mk' (fun v ↦ f (p.applyComposition c v))
(fun v i x y ↦ by simp only [applyComposition_update, map_update_add])
(fun v i c x ↦ by simp only [applyComposition_update, map_update_smul])
cont := f.cont.comp <| continuous_pi fun _ => (coe_continuous _).comp <| continuous_pi fun _ => continuous_apply _
