Document Open Access Logo

A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL

Author Michikazu Hirata

PDF
Thumbnail PDF

File

LIPIcs.ITP.2024.21.pdf
  • Filesize: 0.88 MB
  • 18 pages

Document Identifiers

Author Details

Michikazu Hirata
  • School of Computing, Tokyo Institute of Technology, Japan

Funding

This work is supported by JSPS Research Fellowships for Young Scientists and JSPS KAKENHI Grant Number 23KJ0905.

Acknowledgements

I would like to thank Yasuhiko Minamide and Tetsuya Sato for commenting on a draft of this paper. I also thank anonymous reviewers for their helpful comments and suggestions.

Cite AsGet BibTex

Michikazu Hirata. A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ITP.2024.21

Abstract

The Lévy-Prokhorov metric is a metric between finite measures on a metric space. The metric was introduced to analyze weak convergence of measures. We formalize the Lévy-Prokhorov metric and prove Prokhorov’s theorem in Isabelle/HOL. Prokhorov’s theorem provides a condition for the relative compactness of sets of finite measures and plays essential roles in proofs of the central limit theorem, Sanov’s theorem in large deviation theory, and the existence of optimal coupling in transportation theory. Our formalization includes important results in mathematics such as the Riesz representation theorem, which is a theorem in functional analysis and used to prove Prokhorov’s theorem. We also apply the Lévy-Prokhorov metric to show that the measurable space of finite measures on a standard Borel space is again a standard Borel space.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Probability and statistics
  • Mathematics of computing → Mathematical analysis
Keywords
  • formalization of mathematics
  • measure theory
  • metric spaces
  • topology
  • Lévy-Prokhorov metric
  • Prokhorov’s theorem
  • Isabelle/HOL

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Jeremy Avigad, Johannes Hölzl, and Luke Serafin. A formally verified proof of the central limit theorem. Journal of Automated Reasoning, 59(4):389-423, 2017. URL: https://doi.org/10.1007/s10817-017-9404-x.
  2. Clemens Ballarin. Tutorial to locales and locale interpretation. Contribuciones científicas en honor de Mirian Andrés Gómez, pages 123-140, 2010. Google Scholar
  3. Patrick Billingsley. Convergence of Probability Measures. Wiley series in probability and mathematical statistics, Tracts on probability and statistics. Wiley, New York, United States, 1968. Google Scholar
  4. Jean-Dominique Deuschel and Daniel W. Stroock. Large Deviations, volume 137 of Pure and Applied Mathematics. Elsevier Science, 1989. Google Scholar
  5. Manuel Eberl, Johannes Hölzl, and Tobias Nipkow. A verified compiler for probability density functions. In European Symposium on Programming (ESOP 2015), volume 9032 of LNCS, pages 80-104. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-46669-8_4.
  6. Christopher E. Heil. Alaoglu’s theorem. https://heil.math.gatech.edu/6338/summer08/section9f.pdf, 2008. Lecture notes on MATH 6338 (Real Analysis II) at Gerogia Insisute of Technology, Accessed: January 5, 2024.
  7. Christopher E. Heil. Nets, directed sets, and convergence. https://heil.math.gatech.edu/6338/summer08/section9b.pdf, 2008. Lecture notes on MATH 6338 (Real Analysis II) at Gerogia Insisute of Technology, Accessed: January 5, 2024.
  8. Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang. A convenient category for higher-order probability theory. In Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017. IEEE Press, 2017. URL: https://doi.org/10.1109/lics.2017.8005137.
  9. Michikazu Hirata. The Lévy-Prokhorov metric. Archive of Formal Proofs, June 2024. , Formal proof development. URL: https://isa-afp.org/entries/Levy_Prokhorov_Metric.html.
  10. Michikazu Hirata. The Riesz representation theorem. Archive of Formal Proofs, June 2024. , Formal proof development. URL: https://isa-afp.org/entries/Riesz_Representation.html.
  11. Michikazu Hirata, Yasuhiko Minamide, and Tetsuya Sato. Semantic foundations of higher-order probabilistic programs in Isabelle/HOL. In Adam Naumowicz and René Thiemann, editors, 14th International Conference on Interactive Theorem Proving (ITP 2023), volume 268 of Leibniz International Proceedings in Informatics (LIPIcs), pages 18:1-18:18, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2023.18.
  12. Johannes Hölzl and Armin Heller. Three chapters of measure theory in Isabelle/HOL. In Marko van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk, editors, Interactive Theorem Proving, pages 135-151, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. Google Scholar
  13. Johannes Hölzl, Fabian Immler, and Brian Huffman. Type classes and filters for mathematical analysis in Isabelle/HOL. In Proceedings of the 4th International Conference on Interactive Theorem Proving, ITP 2013, pages 279-294, Berlin, Heidelberg, 2013. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-39634-2_21.
  14. Alexander S. Kechris. Classical Descriptive Set Theory. Graduate Texts in Mathematics. Springer New York, 1995. URL: https://doi.org/10.1007/978-1-4612-4190-4.
  15. Kalle Kytölä. LevyProkhorovMetric.lean. https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean. Accessed May 27th 2024.
  16. Holden Lee. Vector spaces. Archive of Formal Proofs, August 2014. , Formal proof development. URL: https://isa-afp.org/entries/VectorSpace.html.
  17. Paul Lévy. Thèorie de l'addition des variables alèatoires. Gauthier-Villars, Paris, 1937. Google Scholar
  18. Keiko Narita, Kazuhisa Nakasho, and Yasunari Shidama. F. Riesz theorem. Formalized Mathematics, 25(3):179-184, 2017. URL: https://doi.org/10.1515/forma-2017-0017.
  19. Anthony Narkawicz. A formal proof of the Riesz representation theorem. Journal of Formalized Reasoning, 4(1):1-24, January 2011. URL: https://doi.org/10.6092/issn.1972-5787/1952.
  20. Lawrence C. Paulson. Porting the HOL Light metric space library. https://lawrencecpaulson.github.io/2023/07/12/Metric_spaces.html. Accessed: December 31. 2023.
  21. Yuri Vasilyevich Prokhorov. Convergence of random processes and limit theorems in probability theory. Theory of Probability and Its Applications, 1(2):157-214, 1956. URL: https://doi.org/10.1137/1101016.
  22. Walter Rudin. Real and Complex Analysis, 3rd Ed. McGraw-Hill, Inc., USA, 1987. Google Scholar
  23. Mirah Shi. Nets and filters. https://www.uvm.edu/~smillere/TProjects/MShi20s.pdf, 2020. Accessed November 17th 2023.
  24. Shashi Mohan Srivastava. A Course on Borel Sets. Springer, 1998. URL: https://doi.org/10.1007/b98956.
  25. The mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 367-381. Association for Computing Machinery, 2020. URL: https://doi.org/10.1145/3372885.3373824.
  26. René Thiemann and Akihisa Yamada. Matrices, jordan normal forms, and spectral radius theory. Archive of Formal Proofs, August 2015. , Formal proof development. URL: https://isa-afp.org/entries/Jordan_Normal_Form.html.
  27. Onno van Gaans. Probability measures on metric spaces. https://www.math.leidenuniv.nl/~vangaans/jancol1.pdf. Accessed: February 29. 2024.
  28. Cédric. Villani. Optimal Transport: Old and New. Grundlehren der mathematischen Wissenschaften. Springer Berlin Heidelberg, 2008. URL: https://doi.org/10.1007/978-3-540-71050-9.
  29. Shaoyi Zhang. Existence and application of optimal markovian coupling with respect to non-negative lower semi-continuous functions. Acta Mathematica Sinica, 16(2):261-270, 2000. URL: https://doi.org/10.1007/s101140000049.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact