@MISC{RANDOM_2.MIZ,
  AUTHOR = {Okazaki, Hiroyuki, and Shidama, Yasunari},
  TITLE = {Probability Measure on Discrete
     Spaces and Algebra of Real Valued Random Variables},
  ACKNOWLEDGEMENT = {This work was supported by JSPS KAKENHI 2124000101.},
  SECTION1 = {Variance},
  SECTION2 = {Chebyshev's Inequality},
  SECTION3 = {Product Probability Measure},
  SECTION4 = {Algebra of Real-Valued Random Variables},
  DAY = {16},
  MONTH = {March},
  YEAR = {2010},
  ADDRESS1 = {Shinshu University, Nagano, Japan},
  ADDRESS2 = {Shinshu University, Nagano, Japan},
  SUMMARY = {In this article we continue formalizing probability and
  randomness started in \cite{RANDOM_1.ABS}, where we formalized some theorems concerning probability and real-valued random variables.
  In this paper we formalize the variance of a random variable and prove
  Chebyshev's inequality \cite{Goldreich:1998}.
  Next we formalize the product probability measure on the Cartesian product of discrete spaces.
  In the final part of this article we define the algebra of real-valued random
  variables.}}

@ARTICLE{Goldreich:1998,
      AUTHOR  = {Goldreich, Oded},
      TITLE   = {Modern Cryptography, Probabilistic Proofs
        and Pseudorandomness},
      JOURNAL = {Springer-Verlag},
      YEAR    = 1998}
