RV_ring

[hoheinzollern]

We are missing the following: definition of multiplication of random variables and ring structure for RVs.

Definition mul_RV (U : finType) (P : {fdist U}) (X Y : {RV P -> R}) : {RV P -> R} := fun x => X x * Y x.
Notation "X `* Y" := (mul_RV X Y) : proba_scope.
Arguments mul_RV /.

and

Section RV_ring.
Variables (U : finType) (P : fdist U).
Import topology.
Import GRing.Theory.

Lemma add_RV_addr (X Y : {RV P -> R}) : X `+ Y = (X + Y)%ring.
Proof. reflexivity. Qed.

Lemma sub_RV_subr (X Y : {RV P -> R}) : X `- Y = (X - Y)%ring.
Proof. reflexivity. Qed.

Lemma trans_min_RV_subr (X : {RV P -> R}) (y : R) :
  X `-cst y = (X - cst y)%ring.
Proof. reflexivity. Qed.
Definition fdist_supp_choice : U.
by move/set0Pn/xchoose:(fdist_supp_neq0 P).
Defined.

Canonical fdist_supp_pointedType :=
  @classical_sets.Pointed.pack U fdist_supp_choice _ _ idfun.

Lemma mul_RV_mulr (X Y : {RV P -> R}) : X `* Y = (X * Y)%ring.
Proof. reflexivity. Qed.

Lemma sq_RV_sqrr (X : {RV P -> R}) : X `^2 = (X ^+ 2)%ring.
Proof. by rewrite /sq_RV/comp_RV; apply boolp.funext => u /=; rewrite mulR1. Qed.

Definition RV_ringE :=
  (add_RV_addr, sub_RV_subr, trans_min_RV_subr, mul_RV_mulr, sq_RV_sqrr).
End RV_ring.