English
Theorem comp_partialSum shows that composing partial sums of p and q equals the sum over all index compositions in compPartialSumTarget; i.e., the sum of q over p along all compositions equals the partial sum of the composition.
Русский
Теорема comp_partialSum: сумма частичных сумм после композиции p и q равна сумме по всем композициям в compPartialSumTarget; эквивалентная развёртка композиции.
LaTeX
$$$\\text{partialSum}_M( q, p) = \\sum_{i \\in compPartialSumTarget 0 M N} q.compAlongComposition p i.2$.$$
Lean4
/-- `compChangeOfVariables m M N` is a bijection between `compPartialSumSource m M N`
and `compPartialSumTarget m M N`, yielding equal sums for functions that correspond to each
other under the bijection. As `compChangeOfVariables m M N` is a dependent function, stating
that it is a bijection is not directly possible, but the consequence on sums can be stated
more easily. -/
theorem compChangeOfVariables_sum {α : Type*} [AddCommMonoid α] (m M N : ℕ) (f : (Σ n : ℕ, Fin n → ℕ) → α)
(g : (Σ n, Composition n) → α)
(h : ∀ (e) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)) :
∑ e ∈ compPartialSumSource m M N, f e = ∑ e ∈ compPartialSumTarget m M N, g e :=
by
apply
Finset.sum_bij
(compChangeOfVariables m M N)
-- We should show that the correspondence we have set up is indeed a bijection
-- between the index sets of the two sums.
-- 1 - show that the image belongs to `compPartialSumTarget m N N`
· rintro ⟨k, blocks_fun⟩ H
rw [mem_compPartialSumSource_iff] at H
simp only [mem_compPartialSumTarget_iff, Composition.length, H.left, length_ofFn, true_and, compChangeOfVariables]
intro j
simp only [Composition.blocksFun, (H.right _).right, List.get_ofFn]
-- 2 - show that the map is injective
· rintro ⟨k, blocks_fun⟩ H ⟨k', blocks_fun'⟩ H' heq
obtain rfl : k = k' := by
have := (compChangeOfVariables_length m M N H).symm
rwa [heq, compChangeOfVariables_length] at this
congr
funext i
calc
blocks_fun i = (compChangeOfVariables m M N _ H).2.blocksFun _ := (compChangeOfVariables_blocksFun m M N H i).symm
_ = (compChangeOfVariables m M N _ H').2.blocksFun _ := by grind
_ = blocks_fun' i := compChangeOfVariables_blocksFun m M N H' i
· intro i hi
apply compPartialSumTargetSet_image_compPartialSumSource m M N i
simpa [compPartialSumTarget] using hi
· assumption
