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