Universality of Measure Space

Endou, Noboru; Shidama, Yasunari

doi:10.2478/forma-2024-0012

Abstract

This paper deals with the interconversion between Cartesian product types and tuple types and their integration for measures in higher dimensional spaces. We prove the universality between both types and construct a measure (and also underlying integral) based on the set of tuple types.

References

Charalambos D. Aliprantis and Kim C. Border. Infinite dimensional analysis. Springer-Verlag, Berlin, Heidelberg, 2006.
Search in Google Scholar Back to article
Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8 17.
Open DOI Search in Google Scholar Back to article
Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9–32, 2018. doi:10.1007/s10817-017-9440-6.
Open DOI Search in Google Scholar Back to article
Vladimir Igorevich Bogachev and Maria Aparecida Soares Ruas. Measure theory, volume 1. Springer, 2007.
Search in Google Scholar Back to article
Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Improving real analysis in Coq: A user-friendly approach to integrals and derivatives. In Chris Hawblitzel and Dale Miller, editors, Certified Programs and Proofs – Second International Conference, CPP 2012, Kyoto, Japan, December 13–15, 2012. Proceedings, volume 7679 of Lecture Notes in Computer Science, pages 289–304. Springer, 2012. doi:10.1007/978-3-642-35308-6 22.
Open DOI Search in Google Scholar Back to article
Noboru Endou. Fubini’s theorem on measure. Formalized Mathematics, 25(1):1–29, 2017. doi:10.1515/forma-2017-0001.
Open DOI Search in Google Scholar Back to article
Noboru Endou and Yasunari Shidama. Multidimensional measure space and integration. Formalized Mathematics, 31(1):181–192, 2023. doi:10.2478/forma-2023-0017.
Open DOI Search in Google Scholar Back to article
Noboru Endou and Yasunari Shidama. Integral of continuous functions of two variables. Formalized Mathematics, 31(1):309–324, 2023. doi:10.2478/forma-2023-0025.
Open DOI Search in Google Scholar Back to article
Johannes Hölzl and Armin Heller. Three chapters of measure theory in Isabelle/HOL. In Marko C. J. D. van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk, editors, Interactive Theorem Proving (ITP 2011), volume 6898 of LNCS, pages 135–151, 2011.
Search in Google Scholar Back to article
Tom Leinster. Basic Category Theory. Cambridge University Press, 2014.
Search in Google Scholar Back to article
Beata Perkowska. Functional sequence from a domain to a domain. Formalized Mathematics, 3(1):17–21, 1992.
Search in Google Scholar Back to article
M.M. Rao. Measure Theory and Integration. Marcel Dekker, 2nd edition, 2004.
Search in Google Scholar Back to article

Universality of Measure Space

Abstract

Paradigm

My account