Integration in Probability Theory #
Integration results for independent random variables. Specifically, for two
independent random variables X and Y over the extended non-negative
reals, E[X * Y] = E[X] * E[Y]
, and similar results.
This (roughly) proves that if a random variable f
is independent of an event T
,
then if you restrict the random variable to T
, then
E[f * indicator T c 0]=E[f] * E[indicator T c 0]
. It is useful for
lintegral_mul_eq_lintegral_mul_lintegral_of_independent_measurable_space
.
This (roughly) proves that if f
and g
are independent random variables,
then E[f * g] = E[f] * E[g]
. However, instead of directly using the independence
of the random variables, it uses the independence of measurable spaces for the
domains of f
and g
. This is similar to the sigma-algebra approach to
independence. See lintegral_mul_eq_lintegral_mul_lintegral_of_independent_fn
for
a more common variant of the product of independent variables.
This proves that if f
and g
are independent random variables,
then E[f * g] = E[f] * E[g]
.