English
Updating an input of a block in a composition yields a predictable update in the resulting continuous multilinear map defined by compAlongComposition.
Русский
Обновление входа внутри блока композиции приводит к предсказуемому обновлению выходной непрерывной многолинейной карты, заданной через compAlongComposition.
LaTeX
$$$p.applyComposition(c, v[ j\\mapsto z]) = \\ldots$ (update rule for compAlongComposition).$$
Lean4
/-- Technical lemma stating how `p.applyComposition` commutes with updating variables. This
will be the key point to show that functions constructed from `applyComposition` retain
multilinearity. -/
theorem applyComposition_update (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (c : Composition n) (j : Fin n)
(v : Fin n → E) (z : E) :
p.applyComposition c (Function.update v j z) =
Function.update (p.applyComposition c v) (c.index j)
(p (c.blocksFun (c.index j)) (Function.update (v ∘ c.embedding (c.index j)) (c.invEmbedding j) z)) :=
by
ext k
by_cases h : k = c.index j
· rw [h]
let r : Fin (c.blocksFun (c.index j)) → Fin n := c.embedding (c.index j)
simp only [Function.update_self]
change p (c.blocksFun (c.index j)) (Function.update v j z ∘ r) = _
let j' := c.invEmbedding j
suffices B : Function.update v j z ∘ r = Function.update (v ∘ r) j' z by rw [B]
suffices C : Function.update v (r j') z ∘ r = Function.update (v ∘ r) j' z by convert C;
exact (c.embedding_comp_inv j).symm
exact Function.update_comp_eq_of_injective _ (c.embedding _).injective _ _
· simp only [h, Function.update_of_ne, Ne, not_false_iff]
let r : Fin (c.blocksFun k) → Fin n := c.embedding k
change p (c.blocksFun k) (Function.update v j z ∘ r) = p (c.blocksFun k) (v ∘ r)
suffices B : Function.update v j z ∘ r = v ∘ r by rw [B]
apply Function.update_comp_eq_of_notMem_range
rwa [c.mem_range_embedding_iff']
