English
Let s be a finite subset of ι, σ a cycle on s, and f, g be functions from ι to a semiring α. Then the product of the sums over s equals the cyclic convolution: (∑_{i∈s} f(i)) (∑_{i∈s} g(i)) = ∑_{k=0}^{|s|-1} ∑_{i∈s} f(i) g(σ^k(i)).
Русский
Пусть s — конечное множество подмножеств индексов ι, σ — цикл на s, а f, g: ι → α. Тогда произведение сумм по s равно свёртке по циклу: (∑_{i∈s} f(i))(∑_{i∈s} g(i)) = ∑_{k=0}^{|s|-1} ∑_{i∈s} f(i) g(σ^k(i)).
LaTeX
$$$\\left(\\sum_{i \\in s} f(i)\\right) \\cdot \\left(\\sum_{i \\in s} g(i)\\right) = \\sum_{k \\in \\{0,1,\n\\dots,|s|-1\\}} \\sum_{i \\in s} f(i) \\cdot g(\\sigma^k i) $$$
Lean4
theorem sum_mul_sum_eq_sum_perm (hσ : σ.IsCycleOn s) (f g : ι → α) :
((∑ i ∈ s, f i) * ∑ i ∈ s, g i) = ∑ k ∈ range #s, ∑ i ∈ s, f i * g ((σ ^ k) i) :=
sum_smul_sum_eq_sum_perm hσ f g
