English
Bundled version of compAlongOrderedFinpartition: a linear map from F [×c.length] to G, parameterized by p and f.
Русский
Упакованная версия compAlongOrderedFinpartition: линейное отображение из F [×c.length] в G, зависящее от p и f.
LaTeX
$$compAlongOrderedFinpartitionₗ : (F [×c.length]→L[𝕜] G) →ₗ[𝕜] MultilinearMap 𝕜 (fun i => E [×c.partSize i]→L[𝕜] F) (E [×n]→L[𝕜] G)$$
Lean4
/-- Given a an ordered finite partition `c` of `n`, a continuous multilinear map `f` in `c.length`
variables, and for each `m` a continuous multilinear map `p m` in `c.partSize m` variables,
one can form a continuous multilinear map in `n`
variables by applying `p m` to each part of the partition, and then
applying `f` to the resulting vector. It is called `c.compAlongOrderedFinpartition f p`. -/
def compAlongOrderedFinpartition (f : F [×c.length]→L[𝕜] G) (p : ∀ i, E [×c.partSize i]→L[𝕜] F) : E [×n]→L[𝕜] G
where
toMultilinearMap :=
MultilinearMap.mk' (fun v ↦ f (c.applyOrderedFinpartition p v))
(fun v i x y ↦ by simp only [applyOrderedFinpartition_update_right, ContinuousMultilinearMap.map_update_add])
(fun v i c x ↦ by simp only [applyOrderedFinpartition_update_right, ContinuousMultilinearMap.map_update_smul])
cont := by
apply f.cont.comp
change Continuous (fun v m ↦ p m (v ∘ c.emb m))
fun_prop
