The Definition of Finite Sequences and Matrices of Probability, and Addition of Matrices of Real Elements
Bo Zhang, Yatsuka Nakamura · Formalized Mathematics · 2006
The Definition of Finite Sequences and Matrices of Probability, and Addition of Matrices of Real Elements In this article, we first define finite sequences of probability distribution and matrices of joint probability and conditional probability. We discuss also the concept of marginal probability. Further, we describe some theorems of matrices of real elements including quadratic form.