English
Updating the inner variable of the v at position j and then applying the partitioned map equals updating the corresponding output by applying p to the updated variable.
Русский
Обновление внутри переменной v по позиции j и применение разбиения блока даёт обновление вывода по соответствующему блоку через p.
LaTeX
$$c.applyOrderedFinpartition p (update v j z) = update (c.applyOrderedFinpartition p v) (c.index j) (p (c.index j) (Function.update (v ∘ c.emb (c.index j)) (c.invEmbedding j) z))$$
Lean4
/-- Bundled version of `compAlongOrderedFinpartition`, depending linearly on `f`
and multilinearly on `p`. -/
@[simps! apply_apply]
def compAlongOrderedFinpartitionₗ :
(F [×c.length]→L[𝕜] G) →ₗ[𝕜] MultilinearMap 𝕜 (fun i : Fin c.length ↦ E [×c.partSize i]→L[𝕜] F) (E [×n]→L[𝕜] G)
where
toFun
f :=
MultilinearMap.mk' (fun p ↦ c.compAlongOrderedFinpartition f p)
(fun p m q q' ↦ by
ext v
simp [applyOrderedFinpartition_update_left])
(fun p m a q ↦ by
ext v
simp [applyOrderedFinpartition_update_left])
map_add' _ _ := rfl
map_smul' _ _ := rfl
