## Stream: maths

### Topic: Faulhaber's Theorem (sum of kth powers)

#### Moritz Firsching (Feb 18 2021 at 20:27):

Here's a proof of Faulhaber's theorem:
https://github.com/mo271/faulhaber/blob/master/src/faulhaber_with_power_series.lean
I did this together with Fabian Kruse.
I think there are some lemmas in that proof that might be nice to have in mathlib. It's probably looking quite ugly to more experienced lean users, but at least I see a "goals accomplished :tada:" in the end.

Is there a linter for lean somewhere?

Well done!

#### Johan Commelin (Feb 18 2021 at 20:28):

There isn't a style linter. But you can write #lint at the bottom of the file to get some useful feedback

#### Johan Commelin (Feb 18 2021 at 20:29):

Things like: your theorem doesn't use hypothesis h, or this def is missing a docstring (all defs in mathlib are required to have docstrings), or a lemma that shouldn't be marked simp, etc...

#### Bryan Gin-ge Chen (Feb 18 2021 at 20:30):

There's a very basic style linter script used in mathlib's CI that just checks things like line length, but you might have to do some hacking to get it to run outside of mathlib: https://github.com/leanprover-community/mathlib/blob/master/scripts/lint-style.sh

#### Moritz Firsching (Feb 18 2021 at 20:35):

I guess I only care about the formatting and linting for the stuff I'd submit as a pr to mathlib. Reading naming conventions and code style guide now..

#### Heather Macbeth (Feb 18 2021 at 20:36):

I think the whole thing would be welcome in mathlib, if you have the energy! (but of course it's reasonable to start by PR'ing just some of the supporting lemmas)

#### Johan Commelin (Feb 18 2021 at 20:42):

theorem bernoulli_power_series':
(exp ℚ - 1) * power_series.mk (λ n,
((-1)^n * bernoulli n / nat.factorial n : ℚ)) = X :=


I think @Ashvni Narayanan recently brought this to mathlib (-;

#### Moritz Firsching (Feb 18 2021 at 20:42):

Cool, I suppose small PRs are prefered, so submitting each of relevant lemmas separately is preferred to one larger PR

#### Johan Commelin (Feb 18 2021 at 20:43):

Yeah, certainly for a first PR I would aim for ~50 lines

#### Johan Commelin (Feb 18 2021 at 20:44):

def expk


I think this is power_series.exp

#### Moritz Firsching (Feb 18 2021 at 20:44):

Johan Commelin said:

theorem bernoulli_power_series':
(exp ℚ - 1) * power_series.mk (λ n,
((-1)^n * bernoulli n / nat.factorial n : ℚ)) = X :=


I think Ashvni Narayanan recently brought this to mathlib (-;

That's great. I thought I had just synced I can't see it in bernoulli.lean

#### Johan Commelin (Feb 18 2021 at 20:44):

Ooh, scratch that... I can't read

#### Moritz Firsching (Feb 18 2021 at 20:45):

what was recently added is bernoulli_odd_eq_zero, which is most useful here of course..

#### Johan Commelin (Feb 18 2021 at 20:45):

Let me check the sources

#### Johan Commelin (Feb 18 2021 at 20:47):

You are right... I'm too sloppy in my feedback. Sorry.

#### Moritz Firsching (Feb 18 2021 at 20:48):

good, I though there were some secret branches beside master or search was broken or something...

#### Kevin Buzzard (Feb 18 2021 at 20:49):

I think Ashvni has a Bernoulli polynomial branch, but I suggested that she waited until this PR was accepted before she made the next PR. I'll see if her next branch is ready.

#### Moritz Firsching (Feb 18 2021 at 20:55):

Looking forward to seeing what @Ashvni Narayanan has!

#### Ashvni Narayanan (Feb 18 2021 at 22:09):

Johan Commelin said:

theorem bernoulli_power_series':
(exp ℚ - 1) * power_series.mk (λ n,
((-1)^n * bernoulli n / nat.factorial n : ℚ)) = X :=


I think Ashvni Narayanan recently brought this to mathlib (-;

Hello! Glad to know Faulhaber's theorem is on the way :)
Also, the above theorem is in mathlib in bernoulli.lean, the name is bernoulli_power_series.

#### Ashvni Narayanan (Feb 18 2021 at 22:14):

Moritz Firsching said:

Here's a proof of Faulhaber's theorem:
https://github.com/mo271/faulhaber/blob/master/src/faulhaber_with_power_series.lean
I did this together with Fabian Kruse.
I think there are some lemmas in that proof that might be nice to have in mathlib. It's probably looking quite ugly to more experienced lean users, but at least I see a "goals accomplished :tada:" in the end.

Is there a linter for lean somewhere?

Also, I believe expk and exp_inv are now in mathlib, as rescale k (exp ℚ) and exp_mul_exp_neg_eq_one respectively.

#### Ashvni Narayanan (Feb 18 2021 at 22:17):

Moritz Firsching said:

Looking forward to seeing what Ashvni Narayanan has!

The next PR (which I can make once leanpkg build confirms everything is okay) will be about Bernoulli polynomials. Here is the branch : https://github.com/leanprover-community/mathlib/tree/bernoulli-polynomials

#### Thomas Browning (Feb 18 2021 at 22:18):

@Moritz Firsching Here's a style thing. Rather than doing

have ... : ... :=
begin
...,
...,
end,


you can do

have ... : ...,
{ ...,
..., },


#### Alex J. Best (Feb 19 2021 at 01:18):

Thomas Browning said:

Moritz Firsching Here's a style thing. Rather than doing

have ... : ... :=
begin
...,
...,
end,


you can do

have ... : ...,
{ ...,
..., },


Is this the recommended style now? I pretty much exclusively use the former as I always like there to be only 1 goal at a time wherever you click.

#### Yakov Pechersky (Feb 19 2021 at 01:22):

That's still be the case inside the { ... }.

#### Mario Carneiro (Feb 19 2021 at 01:24):

You shouldn't use have := begin end in tactic mode, because that nests a tactic block inside a term inside a tactic block, which takes longer to parse/elaborate and also leads to more nested contexts in error messages

#### Mario Carneiro (Feb 19 2021 at 01:25):

In have : T, { ... } the ... is still part of the main tactic block structure

#### Alex J. Best (Feb 19 2021 at 01:29):

Yakov Pechersky said:

That's still be the case inside the { ... }.

Of course, I was just explaining my weird internal reasoning :smile: of not liking having two goals after writing comma lol.

#### Alex J. Best (Feb 19 2021 at 01:30):

Mario Carneiro said:

You shouldn't use have := begin end in tactic mode, because that nests a tactic block inside a term inside a tactic block, which takes longer to parse/elaborate and also leads to more nested contexts in error messages

Very good to know thanks, should we add this to the style guide then (assuming its not already there and I'm not missing it).

#### Alex J. Best (Feb 19 2021 at 01:34):

Looks like there are a few (< 10) instances of this pattern in mathlib, at least one due to me...

#### Mario Carneiro (Feb 19 2021 at 01:35):

It's not a really big deal, certainly nested tactic blocks come up in patterns like exact foo (by simp) bar, but if you want to shove a whole sequence of tactics in there you can always pop it out as a subgoal using refine

#### Moritz Firsching (Feb 19 2021 at 08:09):

Ashvni Narayanan said:

Johan Commelin said:

theorem bernoulli_power_series':
(exp ℚ - 1) * power_series.mk (λ n,
((-1)^n * bernoulli n / nat.factorial n : ℚ)) = X :=


I think Ashvni Narayanan recently brought this to mathlib (-;

Hello! Glad to know Faulhaber's theorem is on the way :)
Also, the above theorem is in mathlib in bernoulli.lean, the name is bernoulli_power_series.

I think bernoulli_power_series in bernoulli.lean is the version with bernoulli numbers without the (-1)^n (which only makes a difference for bernoulli 1, but still it is a different power series.

theorem bernoulli_power_series :
power_series.mk (λ n, (bernoulli n / nat.factorial n : ℚ)) * (exp ℚ - 1) = X * exp ℚ


In our proof for bernoulli_power_series' we use bernoulli_power_series this essentially then just follows by substituting (-X) for (X).

In general some formulas would be prettier using a definition bernoulli' n := (-1)^n*bernoulli n. Wikipedia says the convention currently used in lean is "sometimes used in the older literature". However for Faulhaber's theorem the formula becomes slightly prettier with lean's definition, since using the convention with bernoulli 1 = + 1/2, there is no (-1)^k appearing. I have no strong opinion on what convention is better.

#### Kevin Buzzard (Feb 19 2021 at 08:16):

Eberl told me that when he was thinking about this stuff in Isabelle he couldn't figure out which one was "the canonical Bernoulli number" so just did both, which is why we also have both. Eberl told me that Knuth had a strong opinion about which one was "right" but that he couldn't really understand it. Knuth's opinion might be biased towards combinatorial applications anyway. My gut feeling is that it's something to do with the fact that the Riemann zeta function has a functional equation relating $\zeta(s)$ to $\zeta(1-s)$ and the two conventions somehow correspond to the $s$ and $1-s$ points of view -- but there's something funny going on with the pole at $s=1$ which makes things inevitably asymmetric. Note that $s=1$ is in some sense the only positive odd integer value of $s$ for which we understand $\zeta(s)$ in some sense.

#### Moritz Firsching (Feb 19 2021 at 08:24):

What do you mean by "we also have both"? I see only the comment "To get the "minus" convention, just use (-1)^n * bernoulli n." But then the formula for the corresponding power series is missing, and (-1)^n * bernoulli n isn't used in any theorems or lemmas. The zeta function stuff makes sense.

#### Moritz Firsching (Feb 19 2021 at 08:29):

http://luschny.de/math/zeta/The-Bernoulli-Manifesto.html

#### Johan Commelin (Feb 19 2021 at 08:46):

Wow! That's pretty polemic

#### Kevin Buzzard (Feb 19 2021 at 08:53):

Oh, in some earlier version of the work we had bernoulli_neg n := ... for the other variant.

What convinced me that this was just bikeshedding was that the formula for sum of k'th powers for i<n and i<=n are different, of course they differ by n^k, and if you write down the polynomials of degree k+1 representing these sums then the smaller one has coefficient -1/2*n^k and the larger one +1/2*n^k. So asking about which one is best is like arguing which is best out of < and <=. It's not surprising that the computer scientists prefer < for sums (because it's more functorial) and the number theorists prefer <= (because product of power series uses i+j=n so 0<=i<=n). e.g. Knuth likes -1/2 and Conway likes +1/2.

#### Kevin Buzzard (Feb 19 2021 at 08:57):

The other issue is that Bernoulli polynomials have this internal symmetry s -> 1-s, related again I think to the functional equation of the zeta function, and the bernoulli numbers are either the values are 0 of these polynomials, or the values at 1, depending on which convention you use. The zeta function has a pole at 1 and everyone agrees with this, and I think that the two conventions are in some sense some weird consequence of this.

#### Ashvni Narayanan (Feb 19 2021 at 10:50):

bernoulli_neg is now on its way! (https://github.com/leanprover-community/mathlib/pull/6309) Unfortunately, I removed the bernoulli_neg_power_series version at the last moment, so a proof exists in previous commits. I could take a look and PR that too, if you need it, @Moritz Firsching .

#### Johan Commelin (Feb 19 2021 at 12:22):

Is "negative Bernoulli number" standard terminology?

#### Johan Commelin (Feb 19 2021 at 12:23):

Otherwise I would suggest calling them bernoulli' or something like that.

#### Kevin Buzzard (Feb 19 2021 at 12:27):

They're called bernoulli and bernoulli' in Isabelle, however the primed one is our bernoulli. Perhaps we should go with the "all the computer algebra packages say B_1=-1/2" idea and rename our original bernoulli numbers to the primed ones?

#### Johan Commelin (Feb 19 2021 at 12:32):

It would be good to be consistent, to the extent possible.

#### Kevin Buzzard (Feb 19 2021 at 12:37):

Yeah I am now concerned that our choice of +1/2 is not used in pari-gp or on the Wolfram Alpha page. Wikipedia used two notations for them (and of course 99% of the time people are only talking about the even ones so you can use B_n unambiguously). Maybe we should redefine bernoulli to be bernoulli' and bernoulli_neg to be bernoulli.

#### Moritz Firsching (Feb 19 2021 at 12:37):

In sagemath bernoulli(1) is -1/2, so I guess switching the names between bernoulli and bernoulli_neg might make sense.

#### Johan Commelin (Feb 19 2021 at 12:38):

The guy from the Manifesto thinks we made the right choice, isn't it? :rofl:

#### Kevin Buzzard (Feb 19 2021 at 12:39):

Yeah I'm not sure I'm going to place too much weight on the manifesto guy.

#### Kevin Buzzard (Feb 19 2021 at 12:41):

Ok so I'm assuming it's -1/2 in mathematica given that that's what it says on the wolfram alpha page, so I am definitely behind switching names. I'm not suggesting a refactor of the maths, just putting primes everywhere. I hadn't realised there was some essentially universally-agreed upon convention, I'd just read Wikipedia which as I say tended to treat both cases independently and not get drawn about "the" value of B(1).

#### Moritz Firsching (Feb 19 2021 at 12:42):

is it ok to have "+" or "-" in a name, then we could take bernoulli+ and bernoulli- or since utf is working we could go with bernoulli♯ bernoulli♭ :stuck_out_tongue_wink:

#### Johan Commelin (Feb 19 2021 at 12:43):

+ and - won't work

#### Moritz Firsching (Feb 19 2021 at 13:08):

Ashvni Narayanan said:

bernoulli_neg is now on its way! (https://github.com/leanprover-community/mathlib/pull/6309) Unfortunately, I removed the bernoulli_neg_power_series version at the last moment, so a proof exists in previous commits. I could take a look and PR that too, if you need it, Moritz Firsching .

Yes, so to summarize, I think it would be useful to have :
(1) bernoulli n, defined to be consistent with sagemath, parigp etc, so that bernoulli 1 = -1/2
(2) bernoulli' n, defined in a way that bernoulli' 1 = 1/2 substituting the name "bernoulli'" for "bernoulli" everywhere. This would mean for example that there will be already a lemma bernoulli' = 1/2.
(3) a new power_series lemma for the new bernoulli
(4) perhaps even a lemma like lemma bernoulli_to_bernoulli' (n:ℕ): bernoulli n = (-1)^n * bernoulli' n and
bernoulli'_to_bernoulli (n:ℕ) bernoulli' n = (-1)^n * bernoulli n, one of which should be true by definition.
(5) possibly something like ∀ x : ℕ , 1 < n → bernoulli n = (-1)^n * bernoulli n.

#### Eric Wieser (Feb 19 2021 at 13:20):

Johan Commelin said:

+ and - won't work

bernoulli«+» and bernoulli«-» are legal... (and identical to «bernoulli+» and «bernoulli-»)

#### Ashvni Narayanan (Feb 19 2021 at 13:52):

Moritz Firsching said:

Ashvni Narayanan said:

bernoulli_neg is now on its way! (https://github.com/leanprover-community/mathlib/pull/6309) Unfortunately, I removed the bernoulli_neg_power_series version at the last moment, so a proof exists in previous commits. I could take a look and PR that too, if you need it, Moritz Firsching .

Yes, so to summarize, I think it would be useful to have :
(1) bernoulli n, defined to be consistent with sagemath, parigp etc, so that bernoulli 1 = -1/2
(2) bernoulli' n, defined in a way that bernoulli' 1 = 1/2 substituting the name "bernoulli'" for "bernoulli" everywhere. This would mean for example that there will be already a lemma bernoulli' = 1/2.
(3) a new power_series lemma for the new bernoulli
(4) perhaps even a lemma like lemma bernoulli_to_bernoulli' (n:ℕ): bernoulli n = (-1)^n * bernoulli' n and
bernoulli'_to_bernoulli (n:ℕ) bernoulli' n = (-1)^n * bernoulli n, one of which should be true by definition.
(5) possibly something like ∀ x : ℕ , 1 < n → bernoulli n = (-1)^n * bernoulli n.

I am not a fan of changing the definition of bernoulli_neg or bernoulli (since I have now done it twice). I think bernoulli_pos and bernoulli_neg are clear? If not, bernoulli' and bernoulli seem okay too. Everything except (3) exists in the new PR, and I can add (3) soon.

#### Kevin Buzzard (Feb 19 2021 at 13:53):

Just to be clear -- we're not suggesting changing any of the actual mathematics, just the names of the functions.

#### Kevin Buzzard (Feb 19 2021 at 13:54):

And the new theorem doesn't have to be added in this PR either, but you may as well make the name change

#### Moritz Firsching (Feb 20 2021 at 22:13):

So I have prepared a commit with the first step towards Faulhaber's theorem. For this I would like to obtain write access to the mathlib repo, please. My github username is mo271.

#### Johan Commelin (Feb 20 2021 at 22:15):

@Moritz Firsching invitation sent!

#### Moritz Firsching (Feb 20 2021 at 22:20):

Many thanks, that was quick! Made the pull request..

#### Moritz Firsching (Feb 25 2021 at 09:27):

Ashvni Narayanan said:

Moritz Firsching said:

[...]
(3) a new power_series lemma for the new bernoulli
[...]

I am not a fan of changing the definition of bernoulli_neg or bernoulli (since I have now done it twice). I think bernoulli_pos and bernoulli_neg are clear? If not, bernoulli' and bernoulli seem okay too. Everything except (3) exists in the new PR, and I can add (3) soon.

I think the it's quite good to have now bernoulli and bernoulli', thanks @Ashvni Narayanan!

https://github.com/leanprover-community/mathlib/pull/6409 contains a proof of Faulhaber that uses the new lemmas I added during the last few days. It depends on a version of (3), namely:

  (exp ℚ - 1) * power_series.mk (λ n, (bernoulli n / nat.factorial n)) = X


(this is using the new definition of bernoulli). Are you planning to add that @Ashvni Narayanan ?

#### Ashvni Narayanan (Feb 25 2021 at 10:04):

I have an almost complete proof, but if you have a proof ready, pls feel free to go ahead with it!

#### Moritz Firsching (Feb 27 2021 at 15:03):

Made a combination of both of our proofs here: https://github.com/leanprover-community/mathlib/pull/6456

#### Moritz Firsching (Mar 16 2021 at 07:14):

Faulhaber's Theorem has now all dependencies resolved and is ready for review here: #6409

Last updated: May 11 2021 at 00:31 UTC