## Stream: maths

### Topic: computations in double sum

#### Ashvni Narayanan (Dec 14 2020 at 07:28):

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 (Dec 14 2020 at 07:32):

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

Here is my code.

#### Johan Commelin (Dec 14 2020 at 07:38):

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 (Dec 14 2020 at 07:39):

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

#### Ashvni Narayanan (Dec 14 2020 at 07:44):

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 (Dec 14 2020 at 07:44):

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 (Dec 14 2020 at 08:16):

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

#### Ashvni Narayanan (Dec 14 2020 at 08:20):

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 (Dec 14 2020 at 08:23):

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

#### Patrick Massot (Dec 14 2020 at 08:31):

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

#### Ashvni Narayanan (Dec 14 2020 at 09:39):

I see, thank you!

Last updated: May 18 2021 at 07:19 UTC