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

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: Dec 20 2023 at 11:08 UTC