Product Pre-Measure

Noboru Endou

Formalized Mathematics (2016)

  • Volume: 24, Issue: 1, page 69-79
  • ISSN: 1426-2630

Abstract

top
In this article we formalize in Mizar [5] product pre-measure on product sets of measurable sets. Although there are some approaches to construct product measure [22], [6], [9], [21], [25], we start it from σ-measure because existence of σ-measure on any semialgebras has been proved in [15]. In this approach, we use some theorems for integrals.

How to cite

top

Noboru Endou. "Product Pre-Measure." Formalized Mathematics 24.1 (2016): 69-79. <http://eudml.org/doc/286749>.

@article{NoboruEndou2016,
abstract = {In this article we formalize in Mizar [5] product pre-measure on product sets of measurable sets. Although there are some approaches to construct product measure [22], [6], [9], [21], [25], we start it from σ-measure because existence of σ-measure on any semialgebras has been proved in [15]. In this approach, we use some theorems for integrals.},
author = {Noboru Endou},
journal = {Formalized Mathematics},
keywords = {product measure; pre-measure},
language = {eng},
number = {1},
pages = {69-79},
title = {Product Pre-Measure},
url = {http://eudml.org/doc/286749},
volume = {24},
year = {2016},
}

TY - JOUR
AU - Noboru Endou
TI - Product Pre-Measure
JO - Formalized Mathematics
PY - 2016
VL - 24
IS - 1
SP - 69
EP - 79
AB - In this article we formalize in Mizar [5] product pre-measure on product sets of measurable sets. Although there are some approaches to construct product measure [22], [6], [9], [21], [25], we start it from σ-measure because existence of σ-measure on any semialgebras has been proved in [15]. In this approach, we use some theorems for integrals.
LA - eng
KW - product measure; pre-measure
UR - http://eudml.org/doc/286749
ER -

References

top
  1. [1] Grzegorz Bancerek. Towards the construction of a model of Mizar concepts. Formalized Mathematics, 16(2):207-230, 2008. doi:10.2478/v10037-008-0027-x. 
  2. [2] Grzegorz Bancerek. Curried and uncurried functions. Formalized Mathematics, 1(3): 537-541, 1990. 
  3. [3] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990. Zbl06213858
  4. [4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990. 
  5. [5] 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. Zbl06512423
  6. [6] Heinz Bauer. Measure and Integration Theory. Walter de Gruyter Inc. Zbl0619.28001
  7. [7] Józef Białas. The σ-additive measure theory. Formalized Mathematics, 2(2):263-270, 1991. 
  8. [8] Józef Białas. Series of positive real numbers. Measure theory. Formalized Mathematics, 2(1):173-183, 1991. 
  9. [9] Vladimir Igorevich Bogachev and Maria Aparecida Soares Ruas. Measure theory, volume 1. Springer, 2007. 
  10. [10] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990. 
  11. [11] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990. 
  12. [12] Czesław Byliński. Basic functions and operations on functions. Formalized Mathematics, 1(1):245-254, 1990. 
  13. [13] Czesław Byliński. Partial functions. Formalized Mathematics, 1(2):357-367, 1990. 
  14. [14] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990. 
  15. [15] Noboru Endou. Construction of measure from semialgebra of sets. Formalized Mathematics, 23(4):309-323, 2015. doi:10.1515/forma-2015-0025. Zbl1334.28002
  16. [16] Noboru Endou and Yasunari Shidama. Integral of measurable function. Formalized Mathematics, 14(2):53-70, 2006. doi:10.2478/v10037-006-0008-x. 
  17. [17] Noboru Endou, Katsumi Wasaki, and Yasunari Shidama. Definitions and basic properties of measurable functions. Formalized Mathematics, 9(3):495-500, 2001. 
  18. [18] Noboru Endou, Katsumi Wasaki, and Yasunari Shidama. The measurability of extended real valued functions. Formalized Mathematics, 9(3):525-529, 2001. 
  19. [19] Noboru Endou, Keiko Narita, and Yasunari Shidama. The Lebesgue monotone convergence theorem. Formalized Mathematics, 16(2):167-175, 2008. doi:10.2478/v10037-008-0023-1. Zbl1321.46022
  20. [20] Noboru Endou, Hiroyuki Okazaki, and Yasunari Shidama. Hopf extension theorem of measure. Formalized Mathematics, 17(2):157-162, 2009. doi:10.2478/v10037-009-0018-6. Zbl1276.46015
  21. [21] Gerald B. Folland. Real Analysis: Modern Techniques and Their Applications. Wiley, 2 edition, 1999. Zbl0924.28001
  22. [22] P. R. Halmos. Measure Theory. Springer-Verlag, 1974. Zbl0283.28001
  23. [23] Andrzej Nędzusiak. σ-fields and probability. Formalized Mathematics, 1(2):401-407, 1990. 
  24. [24] Beata Perkowska. Functional sequence from a domain to a domain. Formalized Mathematics, 3(1):17-21, 1992. 
  25. [25] M.M. Rao. Measure Theory and Integration. Marcel Dekker, 2nd edition, 2004. 
  26. [26] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1 (2):329-334, 1990. 
  27. [27] Wojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. Formalized Mathematics, 1(3):569-573, 1990. 
  28. [28] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990. 
  29. [29] Hiroshi Yamazaki, Noboru Endou, Yasunari Shidama, and Hiroyuki Okazaki. Inferior limit, superior limit and convergence of sequences of extended real numbers. Formalized Mathematics, 15(4):231-236, 2007. doi:10.2478/v10037-007-0026-3.  

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.