In this report, we present the complete HOL theory for the Standard Uniform random variable. The Standard Uniform random variable is defined as the limit value of the sequence of its discrete approximations. The report also contains all the theorems leading to the verification of the probability distribution properties of the Standard Uniform random variable. More details about this formalization can be found in [3].

Download PDF file (PDF File)

Send comments and suggestions to: Osman Hasan