Formalization of Normal Random Variables