# Zulip Chat Archive

## 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):

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