English
Let R be a nonunit, nonassociative semiring. For natural numbers m,n and functions f,g: N → R, the product of the partial sums of f and g satisfies a bilinear expansion: (sum_{i=0}^{m} f(i)) (sum_{i=0}^{n} g(i)) equals (sum_{i=0}^{m-1} f(i)) (sum_{i=0}^{n-1} g(i)) + f(m) (sum_{i=0}^{n-1} g(i)) + (sum_{i=0}^{m-1} f(i)) g(n) + f(m) g(n).
Русский
Пусть R — полугруппа без единицы, неассоциативная. Для натуральных чисел m,n и отображений f,g: N → R имеем распределение произведения частичных сумм: (∑_{i=0}^{m} f(i)) (∑_{i=0}^{n} g(i)) = (∑_{i=0}^{m-1} f(i)) (∑_{i=0}^{n-1} g(i)) + f(m) (∑_{i=0}^{n-1} g(i)) + (∑_{i=0}^{m-1} f(i)) g(n) + f(m) g(n).
LaTeX
$$$\\left(\\sum_{i=0}^{m} f(i)\\right)\\left(\\sum_{i=0}^{n} g(i)\\right) = \\left(\\sum_{i=0}^{m-1} f(i)\\right)\\left(\\sum_{i=0}^{n-1} g(i)\\right) + f(m)\\left(\\sum_{i=0}^{n-1} g(i)\\right) + \\left(\\sum_{i=0}^{m-1} f(i)\\right) g(n) + f(m) g(n) $$$
Lean4
theorem sum_range_succ_mul_sum_range_succ (m n : ℕ) (f g : ℕ → R) :
(∑ i ∈ range (m + 1), f i) * ∑ i ∈ range (n + 1), g i =
(∑ i ∈ range m, f i) * ∑ i ∈ range n, g i + f m * ∑ i ∈ range n, g i + (∑ i ∈ range m, f i) * g n + f m * g n :=
by simp only [add_mul, mul_add, add_assoc, sum_range_succ]
