W BIAŁYMSTOKU
Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/19655Pełny rekord metadanych
| Pole DC | Wartość | Język |
|---|---|---|
| dc.contributor.author | Watase, Yasushige | - |
| dc.date.accessioned | 2026-01-26T12:49:27Z | - |
| dc.date.available | 2026-01-26T12:49:27Z | - |
| dc.date.issued | 2025 | - |
| dc.identifier.citation | Formalized Mathematics, Volume 33, Issue 1, Pages 95-102 | pl |
| dc.identifier.issn | 1426-2630 | - |
| dc.identifier.uri | http://hdl.handle.net/11320/19655 | - |
| dc.description.abstract | In this article, we formalized the proof of the Stirling’s formula, which is considered an essential item in the field of statistics, as shown below: lim n→∞ n! n n+ 1 2 e−n = √ 2π using the Mizar formalism. | pl |
| dc.language.iso | en | pl |
| dc.publisher | University of Białystok | pl |
| dc.rights | Attribution-ShareAlike 4.0 International (CC BY-SA 4.0) | pl |
| dc.rights.uri | https://creativecommons.org/licenses/by-sa/4.0/ | pl |
| dc.subject | Wallis product | pl |
| dc.subject | Stirling formula | pl |
| dc.title | A Formal Proof of Stirling’s Formula | pl |
| dc.type | Article | pl |
| dc.rights.holder | 2025 The Author(s) | pl |
| dc.rights.holder | CC BY-SA 4.0 license | pl |
| dc.identifier.doi | 10.2478/forma-2025-0008 | - |
| dc.description.Affiliation | Faculty of Data Science, University of Rissho, Magechi Kumagaya, Japan | pl |
| dc.description.references | Yves Bertot. A short presentation of Coq. In Otmane Aıt Mohamed, C´esar A. Munoz, and Sofi`ene Tahar, editors, Theorem Proving in Higher Order Logics (TPHOLs 2008), volume 5170 of LNCS, pages 12–16. Springer, 2008. doi:10.1007/978-3-540-71067-7_3. | pl |
| dc.description.references | Richard Courant and Fritz John. Introduction to Calculus and Analysis I. John Wiley and Sons Inc., New York, 1st edition, 1965. | pl |
| dc.description.references | Manuel Eberl. Stirling’s formula. Archive of Formal Proofs, September 2016. https: //isa-afp.org/entries/Stirling_Formula.html, Formal proof development. | pl |
| dc.description.references | Noboru Endou. Relationship between the Riemann and Lebesgue integrals. Formalized Mathematics, 29(4):185–199, 2021. doi:10.2478/forma-2021-0018. | pl |
| dc.description.references | Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191–198, 2015. doi:10.1007/s10817-015-9345-1. | pl |
| dc.description.references | John Harrison. Stirling’s approximation. 2010. Available online at https://github.com/jrh13/hol-light/blob/master/100/stirling.ml. | pl |
| dc.description.references | Nobushige Kurokawa. Modern Trigonometric Function Theory. Iwanami Shoten, Publishers (Tokyo), 1st edition, 2013. In Japanese. | pl |
| dc.description.references | Norman D. Megill and David A. Wheeler. Metamath: A Computer Language for Mathematical Proofs. Lulu Press, Morrisville, North Carolina, 2019. http://us.metamath.org/downloads/metamath.pdf. | pl |
| dc.description.references | Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In Automated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings, pages 625–635, Berlin, Heidelberg, 2021. Springer-Verlag. doi:10.1007/978-3-030-79876-5_37. | pl |
| dc.description.references | Yasunari Shidama. The Taylor expansions. Formalized Mathematics, 12(2):195–200, 2004. | pl |
| dc.description.references | Yasushige Watase. Formal proof of transcendence of the number e. Part II. Formalized Mathematics, 32(1):121–131, 2024. doi:10.2478/forma-2024-0009. | pl |
| dc.description.references | Yasushige Watase. Formalization of Wallis infinite product formula for π and the Wallis integral. Formalized Mathematics, 33(1):85–94, 2025. doi:10.2478/forma-2025-0007. | pl |
| dc.description.references | Freek Wiedijk. Formalizing 100 theorems. Available online at http://www.cs.ru.nl/~freek/100/. | pl |
| dc.description.references | Rafał Ziobro. Fermat’s Little Theorem via divisibility of Newton’s binomial. Formalized Mathematics, 23(3):215–229, 2015. doi:10.1515/forma-2015-0018. | pl |
| dc.identifier.eissn | 1898-9934 | - |
| dc.description.volume | 33 | pl |
| dc.description.issue | 1 | pl |
| dc.description.firstpage | 95 | pl |
| dc.description.lastpage | 102 | pl |
| dc.identifier.citation2 | Formalized Mathematics | pl |
| Występuje w kolekcji(ach): | Formalized Mathematics, 2025, Volume 33, Issue 1 | |
Pliki w tej pozycji:
| Plik | Opis | Rozmiar | Format | |
|---|---|---|---|---|
| A_Formal_Proof_of_Stirling’s_Formula.pdf | 275,55 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL
