Ryan Shao (May 06 2023 at 13:29): Ryan Shao (May 06 2023 at 13:29):Hello,
I have proved the following about reordering of summations on arbitrary functions:
∀r. (∑m::nat=1..Suc(r). ∑j::nat=0..m-1. f(m, j))
= (∑j::nat=0..r. ∑m::nat=j+1..Suc(r). f(m, j))"
I want to show:
(∑m::nat=1..Suc(r-1).
∑j::nat=0..m-1.
list_sum(
(map (λy. (multinomial_term k (j#(m-j)#y)) * (prod_term (a # lis)
((m - j)#y)) * x^j)
(generate (r - m) (length(lis)))))) =
(∑j::nat=0..r - 1.
∑m::nat=j+1..Suc(r - 1).
list_sum(
(map (λy. (multinomial_term k (j#(m-j)#y)) * (prod_term (a # lis)
((m - j)#y)) * x^j)
(generate (r - m) (length(lis))))))
Where the inner functions are the same. However using the lemma I proved previously and trying sledgehammer led to nothing. What am I missing?
Last updated: Apr 28 2024 at 04:17 UTC