From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg poly ssrnum ssrint interval finmap.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import cardinality.
From HB Require Import structures.
Require Import exp numfun lebesgue_measure lebesgue_integral.
Require Import reals ereal signed topology normedtype sequences esum measure.
Require Import exp numfun lebesgue_measure lebesgue_integral.
# Probability
This file provides basic notions of probability theory. See measure.v for
the type probability T R (a measure that sums to 1).
```
{RV P >-> R} == real random variable: a measurable function from
the measurableType of the probability P to R
distribution X == measure image of P by X : {RV P -> R}, declared
as an instance of probability measure
'E_P[X] == expectation of the real measurable function X
covariance X Y == covariance between real random variable X and Y
'V_P[X] == variance of the real random variable X
mmt_gen_fun X == moment generating function of the random variable
X
{dmfun T >-> R} == type of discrete real-valued measurable functions
{dRV P >-> R} == real-valued discrete random variable
dRV_dom X == domain of the discrete random variable X
dRV_enum X == bijection between the domain and the range of X
pmf X r := fine (P (X @^-1` [set r]))
enum_prob X k == probability of the kth value in the range of X
```
Reserved Notation "'{' 'RV' P >-> R '}'"
(
at level 0, format "'{' 'RV' P '>->' R '}'").
Reserved Notation "''E_' P [ X ]" (format "''E_' P [ X ]", at level 5).
Reserved Notation "''V_' P [ X ]" (format "''V_' P [ X ]", at level 5).
Reserved Notation "{ 'dmfun' aT >-> T }"
(
at level 0, format "{ 'dmfun' aT >-> T }").
Reserved Notation "'{' 'dRV' P >-> R '}'"
(
at level 0, format "'{' 'dRV' P '>->' R '}'").
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Definition
random_variable
(
d
: _) (
T
: measurableType d) (
R
: realType)
(
P
: probability T R)
:= {mfun T >-> R}.
Notation
"{ 'RV' P >-> R }"
:= (
@random_variable _ _ R P)
: form_scope.
Lemma
notin_range_measure
d
(
T
: measurableType d) (
R
: realType)
(
P
: {measure set T -> \bar R}) (
X
: T -> R)
r
:
r \notin range X -> P (
X @^-1` [set r])
= 0%E.
Proof.
Lemma
probability_range
d
(
T
: measurableType d) (
R
: realType)
(
P
: probability T R) (
X
: {RV P >-> R})
: P (
X @^-1` range X)
= 1%E.
Proof.
Definition
distribution
(
d
: _) (
T
: measurableType d) (
R
: realType)
(
P
: probability T R) (
X
: {mfun T >-> R})
:=
pushforward P (
@measurable_funP _ _ _ X).
Section
distribution_is_probability
.
Context
d
(
T
: measurableType d) (
R
: realType) (
P
: probability T R)
(
X
: {mfun T >-> R}).
Let
distribution0
: distribution P X set0 = 0%E.
Proof.
Let
distribution_ge0
A
: (
0 <= distribution P X A)
%E.
Proof.
Let
distribution_sigma_additive
: semi_sigma_additive (
distribution P X).
Proof.
HB.instance Definition _ := isMeasure.Build _ _ R (
distribution P X)
distribution0 distribution_ge0 distribution_sigma_additive.
Let
distribution_is_probability
: distribution P X [set: _] = 1%:E.
Proof.
HB.instance Definition _ := Measure_isProbability.Build _ _ R
(
distribution P X)
distribution_is_probability.
End distribution_is_probability.
Section
transfer_probability
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType) (
P
: probability T R).
Lemma
probability_distribution
(
X
: {RV P >-> R})
r
:
P [set
x
| X x = r] = distribution P X [set r].
Proof.
by []. Qed.
Lemma
integral_distribution
(
X
: {RV P >-> R}) (
f
: R -> \bar R)
:
measurable_fun [set: R] f -> (
forall
y,
0 <= f y)
->
\int[distribution P X]_y f y = \int[P]_x (
f \o X)
x.
Proof.
End transfer_probability.
HB.lock Definition expectation {d} {T : measurableType d} {R : realType}
(
P
: probability T R) (
X
: T -> R)
:= (
\int[P]_w (
X w)
%:E)
%E.
Canonical
expectation_unlockable
:= Unlockable expectation.unlock.
Arguments expectation {d T R} P _%R.
Notation
"''E_' P [ X ]"
:= (
@expectation _ _ _ P X)
: ereal_scope.
Section
expectation_lemmas
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType) (
P
: probability T R).
Lemma
expectation_fin_num
(
X
: {RV P >-> R})
: P.
-integrable setT (
EFin \o X)
->
'E_P[X] \is a fin_num.
Proof.
Lemma
expectation_cst
r
: 'E_P[cst r] = r%:E.
Proof.
Lemma
expectation_indic
(
A
: set T) (
mA
: measurable A)
: 'E_P[\1_A] = P A.
Proof.
Lemma
integrable_expectation
(
X
: {RV P >-> R})
(
iX
: P.
-integrable [set: T] (
EFin \o X))
: `| 'E_P[X] | < +oo.
Proof.
Lemma
expectationM
(
X
: {RV P >-> R}) (
iX
: P.
-integrable [set: T] (
EFin \o X))
(
k
: R)
: 'E_P[k \o* X] = k%:E * 'E_P [X].
Proof.
Lemma
expectation_ge0
(
X
: {RV P >-> R})
:
(
forall
x,
0 <= X x)
%R -> 0 <= 'E_P[X].
Proof.
Lemma
expectation_le
(
X
Y
: T -> R)
:
measurable_fun [set: T] X -> measurable_fun [set: T] Y ->
(
forall
x,
0 <= X x)
%R -> (
forall
x,
0 <= Y x)
%R ->
{ae P, (
forall
x,
X x <= Y x)
%R} -> 'E_P[X] <= 'E_P[Y].
Proof.
move=> mX mY X0 Y0 XY; rewrite unlock ae_ge0_le_integral => //.
- by move=> t _; apply: X0.
- exact/EFin_measurable_fun.
- by move=> t _; apply: Y0.
- exact/EFin_measurable_fun.
- move: XY => [N [mN PN XYN]]; exists N; split => // t /= h.
by apply: XYN => /=; apply: contra_not h; rewrite lee_fin.
Qed.
Lemma
expectationD
(
X
Y
: {RV P >-> R})
:
P.
-integrable [set: T] (
EFin \o X)
-> P.
-integrable [set: T] (
EFin \o Y)
->
'E_P[X \+ Y] = 'E_P[X] + 'E_P[Y].
Proof.
Lemma
expectationB
(
X
Y
: {RV P >-> R})
:
P.
-integrable [set: T] (
EFin \o X)
-> P.
-integrable [set: T] (
EFin \o Y)
->
'E_P[X \- Y] = 'E_P[X] - 'E_P[Y].
Proof.
Lemma
expectation_sum
(
X
: seq {RV P >-> R})
:
(
forall
Xi,
Xi \in X -> P.
-integrable [set: T] (
EFin \o Xi))
->
'E_P[\sum_(
Xi
<- X)
Xi] = \sum_(
Xi
<- X)
'E_P[Xi].
Proof.
End expectation_lemmas.
HB.lock Definition covariance {d} {T : measurableType d} {R : realType}
(
P
: probability T R) (
X
Y
: T -> R)
:=
'E_P[(
X \- cst (
fine 'E_P[X]))
* (
Y \- cst (
fine 'E_P[Y]))
]%E.
Canonical
covariance_unlockable
:= Unlockable covariance.unlock.
Arguments covariance {d T R} P _%R _%R.
Section
covariance_lemmas
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType) (
P
: probability T R).
Lemma
covarianceE
(
X
Y
: {RV P >-> R})
:
P.
-integrable setT (
EFin \o X)
->
P.
-integrable setT (
EFin \o Y)
->
P.
-integrable setT (
EFin \o (
X * Y)
%R)
->
covariance P X Y = 'E_P[X * Y] - 'E_P[X] * 'E_P[Y].
Proof.
Lemma
covarianceC
(
X
Y
: T -> R)
: covariance P X Y = covariance P Y X.
Proof.
Lemma
covariance_fin_num
(
X
Y
: {RV P >-> R})
:
P.
-integrable setT (
EFin \o X)
->
P.
-integrable setT (
EFin \o Y)
->
P.
-integrable setT (
EFin \o (
X * Y)
%R)
->
covariance P X Y \is a fin_num.
Proof.
Lemma
covariance_cst_l
c
(
X
: {RV P >-> R})
: covariance P (
cst c)
X = 0.
Proof.
Lemma
covariance_cst_r
(
X
: {RV P >-> R})
c
: covariance P X (
cst c)
= 0.
Proof.
Lemma
covarianceZl
a
(
X
Y
: {RV P >-> R})
:
P.
-integrable setT (
EFin \o X)
->
P.
-integrable setT (
EFin \o Y)
->
P.
-integrable setT (
EFin \o (
X * Y)
%R)
->
covariance P (
a \o* X)
%R Y = a%:E * covariance P X Y.
Proof.
Lemma
covarianceZr
a
(
X
Y
: {RV P >-> R})
:
P.
-integrable setT (
EFin \o X)
->
P.
-integrable setT (
EFin \o Y)
->
P.
-integrable setT (
EFin \o (
X * Y)
%R)
->
covariance P X (
a \o* Y)
%R = a%:E * covariance P X Y.
Proof.
Lemma
covarianceNl
(
X
Y
: {RV P >-> R})
:
P.
-integrable setT (
EFin \o X)
->
P.
-integrable setT (
EFin \o Y)
->
P.
-integrable setT (
EFin \o (
X * Y)
%R)
->
covariance P (
\- X)
%R Y = - covariance P X Y.
Proof.
Lemma
covarianceNr
(
X
Y
: {RV P >-> R})
:
P.
-integrable setT (
EFin \o X)
->
P.
-integrable setT (
EFin \o Y)
->
P.
-integrable setT (
EFin \o (
X * Y)
%R)
->
covariance P X (
\- Y)
%R = - covariance P X Y.
Proof.
Lemma
covarianceNN
(
X
Y
: {RV P >-> R})
:
P.
-integrable setT (
EFin \o X)
->
P.
-integrable setT (
EFin \o Y)
->
P.
-integrable setT (
EFin \o (
X * Y)
%R)
->
covariance P (
\- X)
%R (
\- Y)
%R = covariance P X Y.
Proof.
Lemma
covarianceDl
(
X
Y
Z
: {RV P >-> R})
:
P.
-integrable setT (
EFin \o X)
-> P.
-integrable setT (
EFin \o (
X ^+ 2)
%R)
->
P.
-integrable setT (
EFin \o Y)
-> P.
-integrable setT (
EFin \o (
Y ^+ 2)
%R)
->
P.
-integrable setT (
EFin \o Z)
-> P.
-integrable setT (
EFin \o (
Z ^+ 2)
%R)
->
P.
-integrable setT (
EFin \o (
X * Z)
%R)
->
P.
-integrable setT (
EFin \o (
Y * Z)
%R)
->
covariance P (
X \+ Y)
%R Z = covariance P X Z + covariance P Y Z.
Proof.
move=> X1 X2 Y1 Y2 Z1 Z2 XZ1 YZ1.
rewrite [LHS]covarianceE//= ?mulrDl ?compreDr// ?integrableD//.
rewrite 2?expectationD//=.
rewrite muleDl ?fin_num_adde_defr ?expectation_fin_num//.
rewrite oppeD ?fin_num_adde_defr ?fin_numM ?expectation_fin_num//.
by rewrite addeACA 2?covarianceE.
Qed.
Lemma
covarianceDr
(
X
Y
Z
: {RV P >-> R})
:
P.
-integrable setT (
EFin \o X)
-> P.
-integrable setT (
EFin \o (
X ^+ 2)
%R)
->
P.
-integrable setT (
EFin \o Y)
-> P.
-integrable setT (
EFin \o (
Y ^+ 2)
%R)
->
P.
-integrable setT (
EFin \o Z)
-> P.
-integrable setT (
EFin \o (
Z ^+ 2)
%R)
->
P.
-integrable setT (
EFin \o (
X * Y)
%R)
->
P.
-integrable setT (
EFin \o (
X * Z)
%R)
->
covariance P X (
Y \+ Z)
%R = covariance P X Y + covariance P X Z.
Proof.
Lemma
covarianceBl
(
X
Y
Z
: {RV P >-> R})
:
P.
-integrable setT (
EFin \o X)
-> P.
-integrable setT (
EFin \o (
X ^+ 2)
%R)
->
P.
-integrable setT (
EFin \o Y)
-> P.
-integrable setT (
EFin \o (
Y ^+ 2)
%R)
->
P.
-integrable setT (
EFin \o Z)
-> P.
-integrable setT (
EFin \o (
Z ^+ 2)
%R)
->
P.
-integrable setT (
EFin \o (
X * Z)
%R)
->
P.
-integrable setT (
EFin \o (
Y * Z)
%R)
->
covariance P (
X \- Y)
%R Z = covariance P X Z - covariance P Y Z.
Proof.
Lemma
covarianceBr
(
X
Y
Z
: {RV P >-> R})
:
P.
-integrable setT (
EFin \o X)
-> P.
-integrable setT (
EFin \o (
X ^+ 2)
%R)
->
P.
-integrable setT (
EFin \o Y)
-> P.
-integrable setT (
EFin \o (
Y ^+ 2)
%R)
->
P.
-integrable setT (
EFin \o Z)
-> P.
-integrable setT (
EFin \o (
Z ^+ 2)
%R)
->
P.
-integrable setT (
EFin \o (
X * Y)
%R)
->
P.
-integrable setT (
EFin \o (
X * Z)
%R)
->
covariance P X (
Y \- Z)
%R = covariance P X Y - covariance P X Z.
Proof.
End covariance_lemmas.
Section
variance
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType) (
P
: probability T R).
Definition
variance
(
X
: T -> R)
:= covariance P X X.
Local Notation
"''V_' P [ X ]"
:= (
variance X).
Lemma
varianceE
(
X
: {RV P >-> R})
:
P.
-integrable setT (
EFin \o X)
-> P.
-integrable setT (
EFin \o (
X ^+ 2)
%R)
->
'V_P[X] = 'E_P[X ^+ 2] - (
'E_P[X])
^+ 2.
Proof.
Lemma
variance_fin_num
(
X
: {RV P >-> R})
:
P.
-integrable setT (
EFin \o X)
-> P.
-integrable setT (
EFin \o X ^+ 2)
%R ->
'V_P[X] \is a fin_num.
Proof.
Lemma
variance_ge0
(
X
: {RV P >-> R})
: (
0 <= 'V_P[X])
%E.
Proof.
Lemma
variance_cst
r
: 'V_P[cst r] = 0%E.
Proof.
Lemma
varianceZ
a
(
X
: {RV P >-> R})
:
P.
-integrable setT (
EFin \o X)
-> P.
-integrable setT (
EFin \o (
X ^+ 2)
%R)
->
'V_P[(
a \o* X)
%R] = (
a ^+ 2)
%:E * 'V_P[X].
Proof.
Lemma
varianceN
(
X
: {RV P >-> R})
:
P.
-integrable setT (
EFin \o X)
-> P.
-integrable setT (
EFin \o (
X ^+ 2)
%R)
->
'V_P[(
\- X)
%R] = 'V_P[X].
Proof.
Lemma
varianceD
(
X
Y
: {RV P >-> R})
:
P.
-integrable setT (
EFin \o X)
-> P.
-integrable setT (
EFin \o (
X ^+ 2)
%R)
->
P.
-integrable setT (
EFin \o Y)
-> P.
-integrable setT (
EFin \o (
Y ^+ 2)
%R)
->
P.
-integrable setT (
EFin \o (
X * Y)
%R)
->
'V_P[X \+ Y]%R = 'V_P[X] + 'V_P[Y] + 2%:E * covariance P X Y.
Proof.
Lemma
varianceB
(
X
Y
: {RV P >-> R})
:
P.
-integrable setT (
EFin \o X)
-> P.
-integrable setT (
EFin \o (
X ^+ 2)
%R)
->
P.
-integrable setT (
EFin \o Y)
-> P.
-integrable setT (
EFin \o (
Y ^+ 2)
%R)
->
P.
-integrable setT (
EFin \o (
X * Y)
%R)
->
'V_P[(
X \- Y)
%R] = 'V_P[X] + 'V_P[Y] - 2%:E * covariance P X Y.
Proof.
move=> X1 X2 Y1 Y2 XY1.
rewrite -[(
X \- Y)
%R]/(
X \+ (
\- Y))
%R.
rewrite varianceD/= ?varianceN ?covarianceNr ?muleN//.
- by rewrite compreN ?integrableN.
- by rewrite mulrNN.
- by rewrite mulrN compreN ?integrableN.
Qed.
Lemma
varianceD_cst_l
c
(
X
: {RV P >-> R})
:
P.
-integrable setT (
EFin \o X)
-> P.
-integrable setT (
EFin \o (
X ^+ 2)
%R)
->
'V_P[(
cst c \+ X)
%R] = 'V_P[X].
Proof.
Lemma
varianceD_cst_r
(
X
: {RV P >-> R})
c
:
P.
-integrable setT (
EFin \o X)
-> P.
-integrable setT (
EFin \o (
X ^+ 2)
%R)
->
'V_P[(
X \+ cst c)
%R] = 'V_P[X].
Proof.
Lemma
varianceB_cst_l
c
(
X
: {RV P >-> R})
:
P.
-integrable setT (
EFin \o X)
-> P.
-integrable setT (
EFin \o (
X ^+ 2)
%R)
->
'V_P[(
cst c \- X)
%R] = 'V_P[X].
Proof.
Lemma
varianceB_cst_r
(
X
: {RV P >-> R})
c
:
P.
-integrable setT (
EFin \o X)
-> P.
-integrable setT (
EFin \o (
X ^+ 2)
%R)
->
'V_P[(
X \- cst c)
%R] = 'V_P[X].
Proof.
Lemma
covariance_le
(
X
Y
: {RV P >-> R})
:
P.
-integrable setT (
EFin \o X)
-> P.
-integrable setT (
EFin \o (
X ^+ 2)
%R)
->
P.
-integrable setT (
EFin \o Y)
-> P.
-integrable setT (
EFin \o (
Y ^+ 2)
%R)
->
P.
-integrable setT (
EFin \o (
X * Y)
%R)
->
covariance P X Y <= sqrte 'V_P[X] * sqrte 'V_P[Y].
Proof.
End variance.
Notation
"'V_ P [ X ]"
:= (
variance P X).
Section
markov_chebyshev_cantelli
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType) (
P
: probability T R).
Lemma
markov
(
X
: {RV P >-> R}) (
f
: R -> R) (
eps
: R)
:
(
0 < eps)
%R ->
measurable_fun [set: R] f -> (
forall
r,
0 <= f r)
%R ->
{in Num.nneg &, {homo f :
x
y
/ x <= y}}%R ->
(
f eps)
%:E * P [set
x
| eps%:E <= `| (
X x)
%:E | ] <=
'E_P[f \o (
fun
x
=> `| x |%R)
\o X].
Proof.
move=> e0 mf f0 f_nd; rewrite -(
setTI [set _ | _]).
apply: (
le_trans (
@le_integral_comp_abse _ _ _ P _ measurableT (
EFin \o X)
eps (
er_map f)
_ _ _ _ e0))
=> //=.
- exact: measurable_er_map.
- by case => //= r _; exact: f0.
- move=> [x| |] [y| |]; rewrite !inE/= !in_itv/= ?andbT ?lee_fin ?leey//.
by move=> ? ? ?; rewrite f_nd.
- exact/EFin_measurable_fun.
- by rewrite unlock.
Qed.
Definition
mmt_gen_fun
(
X
: {RV P >-> R}) (
t
: R)
:= 'E_P[expR \o t \o* X].
Lemma
chernoff
(
X
: {RV P >-> R}) (
r
a
: R)
: (
0 < r)
%R ->
P [set
x
| X x >= a]%R <= mmt_gen_fun X r * (
expR (
- (
r * a)))
%:E.
Proof.
Lemma
chebyshev
(
X
: {RV P >-> R}) (
eps
: R)
: (
0 < eps)
%R ->
P [set
x
| (
eps <= `| X x - fine (
'E_P[X])
|)
%R ] <= (
eps ^- 2)
%:E * 'V_P[X].
Proof.
Lemma
cantelli
(
X
: {RV P >-> R}) (
lambda
: R)
:
P.
-integrable setT (
EFin \o X)
-> P.
-integrable setT (
EFin \o (
X ^+ 2)
%R)
->
(
0 < lambda)
%R ->
P [set
x
| lambda%:E <= (
X x)
%:E - 'E_P[X]]
<= (
fine 'V_P[X] / (
fine 'V_P[X] + lambda^2))
%:E.
Proof.
End markov_chebyshev_cantelli.
HB.mixin Record MeasurableFun_isDiscrete
d
(
T
: measurableType d) (
R
: realType)
(
X
: T -> R)
of @MeasurableFun d T R X := {
countable_range
: countable (
range X)
}.
HB.structure Definition discreteMeasurableFun
d
(
T
: measurableType d)
(
R
: realType)
:= {
X
of isMeasurableFun d T R X & MeasurableFun_isDiscrete d T R X
}.
Notation
"{ 'dmfun' aT >-> T }"
:=
(
@discreteMeasurableFun.
type _ aT T)
: form_scope.
Definition
discrete_random_variable
(
d
: _) (
T
: measurableType d)
(
R
: realType) (
P
: probability T R)
:= {dmfun T >-> R}.
Notation
"{ 'dRV' P >-> R }"
:=
(
@discrete_random_variable _ _ R P)
: form_scope.
Section
dRV_definitions
.
Context
d
(
T
: measurableType d) (
R
: realType) (
P
: probability T R).
Definition
dRV_dom_enum
(
X
: {dRV P >-> R})
:
{
B
: set nat & {splitbij B >-> range X}}.
Proof.
have /countable_bijP/cid[B] := @countable_range _ _ _ X.
move/card_esym/ppcard_eqP/unsquash => f.
exists B; exact: f.
Qed.
Definition
dRV_dom
(
X
: {dRV P >-> R})
: set nat := projT1 (
dRV_dom_enum X).
Definition
dRV_enum
(
X
: {dRV P >-> R})
: {splitbij (
dRV_dom X)
>-> range X} :=
projT2 (
dRV_dom_enum X).
Definition
enum_prob
(
X
: {dRV P >-> R})
:=
(
fun
k
=> P (
X @^-1` [set dRV_enum X k]))
\_ (
dRV_dom X).
End dRV_definitions.
Section
distribution_dRV
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType) (
P
: probability T R).
Variable
X
: {dRV P >-> R}.
Lemma
distribution_dRV_enum
(
n
: nat)
: n \in dRV_dom X ->
distribution P X [set dRV_enum X n] = enum_prob X n.
Proof.
by move=> nX; rewrite /distribution/= /enum_prob/= patchE nX.
Qed.
Lemma
distribution_dRV
A
: measurable A ->
distribution P X A = \sum_(
k
<oo)
enum_prob X k * \d_ (
dRV_enum X k)
A.
Proof.
Lemma
sum_enum_prob
: \sum_(
n
<oo) (
enum_prob X)
n = 1.
Proof.
End distribution_dRV.
Section
discrete_distribution
.
Local Open Scope ereal_scope.
Context
d
(
T
: measurableType d) (
R
: realType) (
P
: probability T R).
Lemma
dRV_expectation
(
X
: {dRV P >-> R})
:
P.
-integrable [set: T] (
EFin \o X)
->
'E_P[X] = \sum_(
n
<oo)
enum_prob X n * (
dRV_enum X n)
%:E.
Proof.
Definition
pmf
(
X
: {RV P >-> R}) (
r
: R)
: R := fine (
P (
X @^-1` [set r])).
Lemma
expectation_pmf
(
X
: {dRV P >-> R})
:
P.
-integrable [set: T] (
EFin \o X)
-> 'E_P[X] =
\sum_(
n
<oo | n \in dRV_dom X) (
pmf X (
dRV_enum X n))
%:E * (
dRV_enum X n)
%:E.
Proof.
End discrete_distribution.