@MISC{RANDOM_3.MIZ,
  AUTHOR = {Okazaki, Hiroyuki and Shidama, Yasunari},
  TITLE = {Random Variables and Product of Probability Spaces},
  SECTION1 = {Random Variables},
  SECTION2 = {Product of Probability Spaces},
  DAY = {1},
  MONTH = {December},
  YEAR = {2012},
  ADDRESS1 = {Shinshu University, Nagano, JAPAN},
  ADDRESS2 = {Shinshu University, Nagano, JAPAN},
  SUMMARY = {We have been working on the formalization of
  the probability and the randomness. In \cite{RANDOM_1.ABS}
  and \cite{RANDOM_2.ABS}, 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
  \cite{RANDOM_1.ABS} and \cite{RANDOM_2.ABS}.
  First, we formalize the random variables of arbitrary set and
  prove the equivalence between \verb!random_variable_on Sigma!,
  \verb!Borel_Sets!
  and \verb!Real-Valued-Random-Variable of Sigma!.
  Next, we formalize the product of countably infinite probability spaces.},
  NOTE = {The 1st author was supported by JSPS KAKENHI 21240001,
  and the 2nd author was supported by JSPS KAKENHI 22300285.}}
