Library probsa.probability.nrvar

(* ---------------------------------- Prosa --------------------------------- *)
Require Export prosa.behavior.time.

(* --------------------------------- ProBsa --------------------------------- *)
From probsa.probability Require Export brvar.
Local Open Scope nat_scope.

(* ------------------------------ Definitions ------------------------------- *)

Natural Random Variable

For the sake of clarity, we define a random variable nrvar over a countable set Ω with measure μ, whose values are in the natural numbers nrvar. The random variable is defined using the general random variable notion rvar, which takes a set Ω, a measure μ, and a type eqType of nat as arguments.

Definition nrvar {Ω} (μ : measure Ω) :=
@rvar Ω μ [eqType of nat ].

We define a mapping from rvar (option nat) to nrvar.

Definition odflt0 {Ω} {μ : measure Ω} (O : rvar μ [eqType of option instant ]) : nrvar μ :=
mkRvar μ (fun ω ⇒ odflt 0%nat (O ω)).

(* -------------------------------- Instances ------------------------------- *)

Notation Instances

Next, we define notation-related typeclass instances for nrvar.

Instance nrvar_nrvar_pred_leqop {Ω} {μ : measure Ω} : LeqOp (nrvar μ) (nrvar μ) (pred Ω) :=
  { leq_op A B := fun ω ⇒ A ω ≤ B ω }.

Instance nrvar_nrvar_brvar_leqop {Ω} {μ : measure Ω} : LeqOp (nrvar μ) (nrvar μ) (brvar μ) :=
  { leq_op A B := mkRvar μ (fun ω ⇒ A ω ≤ B ω) }.

Instance rvar_nat_pred_leqop {Ω} {μ : measure Ω} : LeqOp (nrvar μ) nat (pred Ω) :=
  { leq_op A c := fun ω ⇒ A ω ≤ c }.

Instance nrvar_addop {Ω} {μ : measure Ω} : AddOp (nrvar μ) :=
  { add_op A B := mkRvar μ (fun ω ⇒ A ω + B ω) }.

Instance nrvar_subop {Ω} {μ : measure Ω} : SubOp (nrvar μ) :=
  { sub_op A B := mkRvar μ (fun ω ⇒ A ω - B ω) }.

Instance nrvar_nat_pred_eqop {Ω} {μ : measure Ω} : EqOp (nrvar μ) nat (pred Ω) :=
  { eq_op X x := mkRvar μ (fun ω ⇒ X ω == x) }.

Instance onrvar_onat_pred_eqop {Ω} {μ : measure Ω} :
  EqOp (rvar μ [eqType of option duration ]) (option duration) (pred Ω) :=
  { eq_op X x := mkRvar μ (fun ω ⇒ X ω == x) }.

Instance onrvar_nrvar_brvar_leqop {Ω} {μ : measure Ω} :
  LeqOp (rvar μ [eqType of option instant ]) (nrvar μ) (brvar μ) :=
  { leq_op := fun X Y ⇒ mkRvar μ (fun ω ⇒ X ω ⟨<=⟩ Y ω) }.

Instance onrvar_onat_pred_leqop {Ω} {μ : measure Ω} :
  LeqOp (rvar μ [eqType of option instant ]) (option nat) (pred Ω) :=
  { leq_op rv ow := fun ω ⇒ rv ω ⟨<=⟩ ow }.