English
The source set compPartialSumSource(m,M,N) is defined as the sigma product of lengths n between m and M and, for each coordinate, a Finset of indices from 1 to N, describing all possible shapes of compositions that can occur in the j-th block.
Русский
Источник compPartialSumSource(m,M,N) есть сумма-через-координаты длин n между m и M и для каждой координаты — множество индексов от 1 до N, задающее все возможные формы композиции в блоке.
LaTeX
$$$\\text{compPartialSumSource}(m,M,N) = (\\sum_{n=m}^{M-1} \\; Fin(n) ) \\; \\text{ и для каждого } i, Fin(n) = \\Pi_{j=0}^{n-1} Fin(1,N).$$$
Lean4
/-- Source set in the change of variables to compute the composition of partial sums of formal
power series.
See also `comp_partialSum`. -/
def compPartialSumSource (m M N : ℕ) : Finset (Σ n, Fin n → ℕ) :=
Finset.sigma (Finset.Ico m M) (fun n : ℕ => Fintype.piFinset fun _i : Fin n => Finset.Ico 1 N :)
