Theorems · Theorem · several complex variables

Composition.sizeUpTo_sizeUpTo_add

∀ {n : ℕ} (a : Composition n) (b : Composition a.length) {i j : ℕ} (hi : i < b.length),
  j < b.blocksFun ⟨i, hi⟩ →
    a.sizeUpTo (b.sizeUpTo i + j) = (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo j

Auxiliary lemma to prove that the composition of formal multilinear series is associative. Consider a composition a of n and a composition b of a.length. Grouping together some blocks of a according to b as in a.gather b, one can compute the total size of the blocks of a up to an index sizeUpTo b i + j (where the j corresponds to a set of blocks of a that do not fill a whole block of a.gather b). The first part corresponds to a sum of blocks in a.gather b, and the second one to a sum of blocks in the next block of sigmaCompositionAux a b. This is the content of this lemma.

Defined in

Mathlib.Analysis.Analytic.Composition

Cited by

1 results in Mathlib

Foundations

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