Faulhaber's Theorem (sum of kth powers)

Stream: maths

[Moritz Firsching]

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?

[Johan Commelin]

Well done!

[Johan Commelin]

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

[Johan Commelin]

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]

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]

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]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

def expk

I think this is power_series.exp

[Moritz Firsching]

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]

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

[Moritz Firsching]

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

[Johan Commelin]

Let me check the sources

[Johan Commelin]

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

[Moritz Firsching]

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

[Kevin Buzzard]

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]

Looking forward to seeing what @Ashvni Narayanan has!

[Ashvni Narayanan]

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]

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]

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]

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

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

you can do

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

[Alex J. Best]

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]

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

[Mario Carneiro]

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]

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

[Alex J. Best]

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]

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]

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

[Mario Carneiro]

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]

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]

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]

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]

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

[Johan Commelin]

Wow! That's pretty polemic

[Kevin Buzzard]

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]

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]

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]

Is "negative Bernoulli number" standard terminology?

[Johan Commelin]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

+ and - won't work

[Moritz Firsching]

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]

Johan Commelin said:

+ and - won't work

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

[Ashvni Narayanan]

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]

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

[Kevin Buzzard]

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]

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]

@Moritz Firsching invitation sent!

[Moritz Firsching]

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

[Moritz Firsching]

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]

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

[Moritz Firsching]

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

[Moritz Firsching]

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