Random Variables and Product of Probability Spaces

Hiroyuki Okazaki; Yasunari Shidama

Formalized Mathematics (2013)

  • Volume: 21, Issue: 1, page 33-39
  • ISSN: 1426-2630

Abstract

top
We have been working on the formalization of the probability and the randomness. In [15] and [16], we formalized some theorems concerning the real-valued random variables and the product of two probability spaces. In this article, we present the generalized formalization of [15] and [16]. First, we formalize the random variables of arbitrary set and prove the equivalence between random variable on Σ, Borel sets and a real-valued random variable on Σ. Next, we formalize the product of countably infinite probability spaces.

How to cite

top

Hiroyuki Okazaki, and Yasunari Shidama. "Random Variables and Product of Probability Spaces." Formalized Mathematics 21.1 (2013): 33-39. <http://eudml.org/doc/267275>.

@article{HiroyukiOkazaki2013,
abstract = {We have been working on the formalization of the probability and the randomness. In [15] and [16], we formalized some theorems concerning the real-valued random variables and the product of two probability spaces. In this article, we present the generalized formalization of [15] and [16]. First, we formalize the random variables of arbitrary set and prove the equivalence between random variable on Σ, Borel sets and a real-valued random variable on Σ. Next, we formalize the product of countably infinite probability spaces.},
author = {Hiroyuki Okazaki, Yasunari Shidama},
journal = {Formalized Mathematics},
language = {eng},
number = {1},
pages = {33-39},
title = {Random Variables and Product of Probability Spaces},
url = {http://eudml.org/doc/267275},
volume = {21},
year = {2013},
}

TY - JOUR
AU - Hiroyuki Okazaki
AU - Yasunari Shidama
TI - Random Variables and Product of Probability Spaces
JO - Formalized Mathematics
PY - 2013
VL - 21
IS - 1
SP - 33
EP - 39
AB - We have been working on the formalization of the probability and the randomness. In [15] and [16], we formalized some theorems concerning the real-valued random variables and the product of two probability spaces. In this article, we present the generalized formalization of [15] and [16]. First, we formalize the random variables of arbitrary set and prove the equivalence between random variable on Σ, Borel sets and a real-valued random variable on Σ. Next, we formalize the product of countably infinite probability spaces.
LA - eng
UR - http://eudml.org/doc/267275
ER -

References

top
  1. [1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990. 
  2. [2] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990. Zbl06213858
  3. [3] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990. 
  4. [4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990. 
  5. [5] Józef Białas. The σ-additive measure theory. Formalized Mathematics, 2(2):263-270, 1991. 
  6. [6] Józef Białas. Series of positive real numbers. Measure theory. Formalized Mathematics, 2(1):173-183, 1991. 
  7. [7] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990. 
  8. [8] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990. 
  9. [9] Czesław Bylinski. Partial functions. Formalized Mathematics, 1(2):357-367, 1990. 
  10. [10] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990. 
  11. [11] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990. 
  12. [12] Peter Jaeger. Elementary introduction to stochastic finance in discrete time. FormalizedMathematics, 20(1):1-5, 2012. doi:10.2478/v10037-012-0001-5.[Crossref] Zbl1276.91103
  13. [13] Andrzej Nedzusiak. σ-fields and probability. Formalized Mathematics, 1(2):401-407, 1990. 
  14. [14] Hiroyuki Okazaki. Probability on finite and discrete set and uniform distribution. FormalizedMathematics, 17(2):173-178, 2009. doi:10.2478/v10037-009-0020-z.[Crossref] 
  15. [15] Hiroyuki Okazaki and Yasunari Shidama. Probability on finite set and real-valued random variables. Formalized Mathematics, 17(2):129-136, 2009. doi:10.2478/v10037-009-0014-x.[Crossref] Zbl1281.60006
  16. [16] Hiroyuki Okazaki and Yasunari Shidama. Probability measure on discrete spaces and algebra of real-valued random variables. Formalized Mathematics, 18(4):213-217, 2010. doi:10.2478/v10037-010-0026-6.[Crossref] Zbl1281.60006
  17. [17] Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147-152, 1990. 
  18. [18] Andrzej Trybulec and Agata Darmochwał. Boolean domains. Formalized Mathematics, 1 (1):187-190, 1990. 
  19. [19] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990. 
  20. [20] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990. 
  21. [21] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181-186, 1990. 
  22. [22] Bo Zhang, Hiroshi Yamazaki, and Yatsuka Nakamura. The relevance of measure and probability, and definition of completeness of probability. Formalized Mathematics, 14 (4):225-229, 2006. doi:10.2478/v10037-006-0026-8. [Crossref] 

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.