English
Definition: Given f and p, define c.compAlongOrderedFinpartition f p as the multilinear map obtained by applying f to the array of blocks formed by p.
Русский
Определение: для функций f и p получить непрерывно-многочленную отображение по разделению на блоки и применить f к получившемуся массиву блоков.
LaTeX
$$def compAlongOrderedFinpartition (f : F [×c.length]→L[𝕜] G) (p : ∀ i, E [×c.partSize i]→L[𝕜] F) : E [×n]→L[𝕜] G :=$$
Lean4
/-- Technical lemma stating how `c.applyOrderedFinpartition` commutes with updating variables. This
will be the key point to show that functions constructed from `applyOrderedFinpartition` retain
multilinearity. -/
theorem applyOrderedFinpartition_update_right (p : ∀ (i : Fin c.length), E [×c.partSize i]→L[𝕜] F) (j : Fin n)
(v : Fin n → E) (z : E) :
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)) :=
by
ext m
by_cases h : m = c.index j
· rw [h]
simp only [applyOrderedFinpartition, update_self]
congr
rw [← Function.update_comp_eq_of_injective]
· simp
· exact (c.emb_strictMono (c.index j)).injective
· simp only [applyOrderedFinpartition, ne_eq, h, not_false_eq_true, update_of_ne]
congr 1
apply Function.update_comp_eq_of_notMem_range
have A : Disjoint (range (c.emb m)) (range (c.emb (c.index j))) := c.disjoint (mem_univ m) (mem_univ (c.index j)) h
have : j ∈ range (c.emb (c.index j)) := mem_range.2 ⟨c.invEmbedding j, by simp⟩
exact Set.disjoint_right.1 A this
