Theorems · Theorem · several complex variables

FormalMultilinearSeries.applyComposition_update

∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup E] [inst_8 : ContinuousConstSMul 𝕜 E] [inst_9 : IsTopologicalAddGroup F]
  [inst_10 : ContinuousConstSMul 𝕜 F] (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))

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.

Defined in

Mathlib.Analysis.Analytic.Composition

Cited by

0 results in Mathlib

Foundations

Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupAddCommGroupModuleModuleTopologicalSpaceTopologicalSpaceIsTopologicalAddGroupContinuousConstSMulIsTopologicalAddGroupContinuousConstSMul