computations in double sum

Stream: maths

[Ashvni Narayanan]

I am working on defining basic properties of Bernoulli polynomials, and am currently trying to prove that ∑ k in finset.range (n + 1), ((n + 1).choose k : ℚ) * bernoulli_poly k X = (n + 1) * X^n . I am at this stage of the proof :

X: ℚ
n: ℕ
f: ∑ (s : ℕ) in finset.Ico 0 (n.succ + 1), ↑((n.succ + 1).choose s) * X ^ s * ∑ (y : ℕ) in finset.Ico 0 (n.succ + 1 - s), ↑((n.succ + 1 - s).choose y) * bernoulli_neg y = (↑(n.succ) + 1) * X ^ n.succ
⊢ ∑ (i : ℕ) in finset.Ico 0 (n.succ + 1), ∑ (j : ℕ) in finset.Ico i (n.succ + 1), ↑((n.succ + 1).choose j) * (bernoulli_neg (j - i) * ↑(j.choose i) * X ^ i) = (↑(n.succ) + 1) * X ^ n.succ

I want to use the lemma finset.sum_Ico_add in order to change the bounds of the inner sum from i to n.succ + 1,to 0 to n.succ + 1 - i. In general, I am having issues dealing with computations within double sums. I tried to use conv_lhs, however, I am losing the data that i in finset.Ico 0 (n.succ + 1) (This information is needed so I can use nat.sub_add_cancel).

Any help is appreciated, thank you!

[Ashvni Narayanan]

https://github.com/leanprover-community/mathlib/blob/d47e1b70d9e9407b1ac7f0785958ed0bbe071523/src/number_theory/bernoulli%20polynomials.lean#L135

Here is my code.

[Johan Commelin]

Inside conv mode you can use funext I think, to retain some of the data. But I agree that this is not as smooth as we would like

[Johan Commelin]

Does it make sense to take smaller steps? Write a helper lemma that manipulates the inner sum for you.

[Ashvni Narayanan]

Johan Commelin said:

Inside conv mode you can use funext I think, to retain some of the data. But I agree that this is not as smooth as we would like

I tried that, but I lost the info that i ≤ (n.succ + 1)(which I do need). Would it be wise to use convert_to?

[Ashvni Narayanan]

Johan Commelin said:

Does it make sense to take smaller steps? Write a helper lemma that manipulates the inner sum for you.

I will try this.

[Patrick Massot]

@Ashvni Narayanan What if you start your conv block with apply_congr, skip,?

[Ashvni Narayanan]

Yes, that works! Thank you!

I also found a lemma finset.sum_Ico_eq_sum_range which directly gives me the required result.

[Johan Commelin]

ooh, sorry, I said funext but I actually meant apply_congr.

[Patrick Massot]

That apply_congr tactic (which is a conv mode tactic) was written exactly for this purpose of rewriting under big ops.

[Ashvni Narayanan]

I see, thank you!