English
Theorem compPartialSum combines the previous ideas to express the total partial sum as a sum over the target set using compPartialSumTarget; it just restates the earlier result in the HasFPowerSeriesWithinAt framework.
Русский
Теорема compPartialSum объединяет предыдущие идеи и выражает общую частичную сумму через целевой набор; снова изложение в рамках HasFPowerSeriesWithinAt.
LaTeX
$$$ q.partialSum M (\\sum_{i\\in I} p_i(z)) = \\sum_{i\\in compPartialSumTarget 0 M N} q.compAlongComposition p i.2 (z) $$$
Lean4
/-- Composing the partial sums of two multilinear series coincides with the sum over all
compositions in `compPartialSumTarget 0 N N`. This is precisely the motivation for the
definition of `compPartialSumTarget`. -/
theorem comp_partialSum (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (M N : ℕ) (z : E) :
q.partialSum M (∑ i ∈ Finset.Ico 1 N, p i fun _j => z) =
∑ i ∈ compPartialSumTarget 0 M N, q.compAlongComposition p i.2 fun _j => z :=
by
-- we expand the composition, using the multilinearity of `q` to expand along each coordinate.
suffices H :
(∑ n ∈ Finset.range M,
∑ r ∈ Fintype.piFinset fun i : Fin n => Finset.Ico 1 N, q n fun i : Fin n => p (r i) fun _j => z) =
∑ i ∈ compPartialSumTarget 0 M N, q.compAlongComposition p i.2 fun _j => z
by simpa only [FormalMultilinearSeries.partialSum, ContinuousMultilinearMap.map_sum_finset] using H
rw [Finset.range_eq_Ico, Finset.sum_sigma']
-- use `compChangeOfVariables_sum`, saying that this change of variables respects sums
apply compChangeOfVariables_sum 0 M N
rintro ⟨k, blocks_fun⟩ H
apply congr _ (compChangeOfVariables_length 0 M N H).symm
intros
rw [← compChangeOfVariables_blocksFun 0 M N H, applyComposition, Function.comp_def]
