Stirling

Stream: maths

[Moritz Firsching]

Together with @Nikolas Kuhn and @Fabian Kruse , I wrote up a version of Stirling's formula:
see here
https://github.com/mo271/stirling

This is in quite a raw state, but the at least the proof compiles. As next steps we plan to clean it up and start following the code style, naming conventions etc...
It's just first version that was written in a whatever-works style.
Also it doesn't use a very sophisticated proof using the Gamma function, but simply the series for log and Wallis' product (which is already in mathlib, luckily)

[Yaël Dillies]

cc @James Arthur who is doing Stirling with the Gamma function

[Moritz Firsching]

Yaël Dillies said:

cc James Arthur who is doing Stirling with the Gamma function

Cool, didn't know about that!

[Moritz Firsching]

WIP pr here:
https://github.com/leanprover-community/mathlib/pull/14800

[Moritz Firsching]

by now, this is split up into two pull requests:
https://github.com/leanprover-community/mathlib/pull/14874
and
https://github.com/leanprover-community/mathlib/pull/14875

[Moritz Firsching]

We are looking for reviewers for Stirling's approximation hrere: https://github.com/leanprover-community/mathlib/pull/14874

[Yaël Dillies]

You should post this in #PR reviews

[Moritz Firsching]

Thanks @Yaël Dillies, will do!