English
Explicit expression for size-up-to after combining blocks, used to prove associativity of compositions.
Русский
Явное выражение для размера до объединения блоков, используемое в доказательстве ассоциативности композиций.
LaTeX
$$$sizeUpTo a (sizeUpTo b i + j) = sizeUpTo (a.gather b) i + sizeUpTo (sigmaCompositionAux b i) j$$$
Lean4
/-- 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. -/
theorem sizeUpTo_sizeUpTo_add (a : Composition n) (b : Composition a.length) {i j : ℕ} (hi : i < b.length)
(hj : j < blocksFun b ⟨i, hi⟩) :
sizeUpTo a (sizeUpTo b i + j) =
sizeUpTo (a.gather b) i + sizeUpTo (sigmaCompositionAux a b ⟨i, (length_gather a b).symm ▸ hi⟩) j :=
by
induction j with
|
zero =>
change sum (take (b.blocks.take i).sum a.blocks) = sum (take i (map sum (splitWrtComposition a.blocks b)))
induction i with
| zero => rfl
| succ i IH =>
have A : i < b.length := Nat.lt_of_succ_lt hi
have B : i < List.length (map List.sum (splitWrtComposition a.blocks b)) := by simp [A]
have C : 0 < blocksFun b ⟨i, A⟩ := Composition.blocks_pos' _ _ _
rw [sum_take_succ _ _ B, ← IH A C]
have :
take (sum (take i b.blocks)) a.blocks =
take (sum (take i b.blocks)) (take (sum (take (i + 1) b.blocks)) a.blocks) :=
by
rw [take_take, min_eq_left]
apply monotone_sum_take _ (Nat.le_succ _)
rw [this, getElem_map, getElem_splitWrtComposition, ←
take_append_drop (sum (take i b.blocks)) (take (sum (take (Nat.succ i) b.blocks)) a.blocks), sum_append]
congr
rw [take_append_drop]
| succ j IHj =>
have A : j < blocksFun b ⟨i, hi⟩ := lt_trans (lt_add_one j) hj
have B : j < length (sigmaCompositionAux a b ⟨i, (length_gather a b).symm ▸ hi⟩) := by convert A;
rw [← length_sigmaCompositionAux]
have C : sizeUpTo b i + j < sizeUpTo b (i + 1) :=
by
simp only [sizeUpTo_succ b hi, add_lt_add_iff_left]
exact A
have D : sizeUpTo b i + j < length a := lt_of_lt_of_le C (b.sizeUpTo_le _)
have : sizeUpTo b i + Nat.succ j = (sizeUpTo b i + j).succ := rfl
rw [this, sizeUpTo_succ _ D, IHj A, sizeUpTo_succ _ B]
simp only [sigmaCompositionAux, add_assoc]
rw [getElem_of_eq (getElem_splitWrtComposition _ _ _ _), getElem_drop, getElem_take]
