Zulip Chat Archive

Stream: maths

Topic: Stirling


Moritz Firsching (May 26 2022 at 20:26):

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 (May 26 2022 at 20:29):

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

Moritz Firsching (May 26 2022 at 20:30):

Yaël Dillies said:

cc James Arthur who is doing Stirling with the Gamma function

Cool, didn't know about that!

Moritz Firsching (Jun 17 2022 at 14:29):

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

Moritz Firsching (Jun 29 2022 at 20:24):

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 (Jul 13 2022 at 05:49):

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

Yaël Dillies (Jul 13 2022 at 14:01):

You should post this in #PR reviews

Moritz Firsching (Jul 13 2022 at 19:47):

Thanks @Yaël Dillies, will do!


Last updated: Dec 20 2023 at 11:08 UTC