Формализация бесконечной суммы от отрицательной бесконечности до бесконечности в Coq?
Я могу видеть, что есть формализации для сумм по натуральным, но я не могу найти ничего для суммы по целым числам.
Я хочу закодировать свертку, которая была бы
convolution: (Z -> R) -> (Z -> R) -> (Z -> R)
forall (f g: Z -> R) (x: Z)
convolution f g x = sum_{k = -infinity}^{infinity} f(k) g(x - k)
Как бы это определение выглядело в Coq? В частности, convolution,