文件列表:

LICENSE (11357, 2022-06-17)
leanpkg.toml (241, 2022-06-17)
src/ (0, 2022-06-17)
src/90_stirlings_formula.lean (33904, 2022-06-17)

# A proof of [Stirling's formula](https://en.wikipedia.org/wiki/Stirling%27s_approximation) in [Lean](https://leanprover.github.io/) We provide a proof of Stirling's formula in the following form: $$n! \sim \sqrt{2\pi n}\left(\frac{n}{e}\right)^n.$$ More concretely, we define ```lean noncomputable def an (n : ) : := (n.factorial : ) / ((real.sqrt(2*n)*((n/(exp 1)))^n)) ``` and prove ```lean lemma an_has_limit_sqrt_pi: tendsto (λ (n : ), an n) at_top ( (sqrt π)) := ``` We follow roughly [this proof](https://proofwiki.org/wiki/Stirling%27s_Formula). Currently the proof is complete, but in very messy state. We plan to clean and streamline the proof soon.

近期下载者：

相关文件：

评论：[我要评论] [举报此文件]

收藏者：