Assume that a probability space
is given. A
*random variable*^{9.1}
is a function that maps into
. Thus, assigns a real
value to every element of the sample space. This enables statistics
to be conveniently computed over a probability space. If is
already a subset of
, may by default represent the identity
function.

Steven M LaValle 2020-08-14