Library probsa.probability.brvar
(* --------------------------------- ProBsa --------------------------------- *)
From probsa.util Require Export notation stdpp.
(* ------------------------------- Definition ------------------------------- *)
From probsa.util Require Export notation stdpp.
(* ------------------------------- Definition ------------------------------- *)
Boolean Random Variable
For the sake of clarity, we define a random variable over a countable set Ω with measure μ, whose values are in the booleans brvar. The random variable is defined using the general random variable notion rvar, which takes a set Ω, a measure μ, and a type eqType of bool as arguments.
Definition brvar {Ω} (μ : measure Ω) :=
@rvar Ω μ [eqType of bool].
(* -------------------------------- Instances ------------------------------- *)
@rvar Ω μ [eqType of bool].
(* -------------------------------- Instances ------------------------------- *)
Instance rvar_neg {Ω} {μ : measure Ω} : NegOp (brvar μ) :=
{ neg_op A := mkRvar μ (fun ω ⇒ ~~ A ω) }.
Instance rvar_union {Ω} {μ : measure Ω} : Union (brvar μ) :=
{ union A B := mkRvar μ (fun ω ⇒ A ω || B ω) }.
Instance rvar_intersection {Ω} {μ : measure Ω} : Intersection (brvar μ) :=
{ intersection A B := mkRvar μ (fun ω ⇒ A ω && B ω) }.
{ neg_op A := mkRvar μ (fun ω ⇒ ~~ A ω) }.
Instance rvar_union {Ω} {μ : measure Ω} : Union (brvar μ) :=
{ union A B := mkRvar μ (fun ω ⇒ A ω || B ω) }.
Instance rvar_intersection {Ω} {μ : measure Ω} : Intersection (brvar μ) :=
{ intersection A B := mkRvar μ (fun ω ⇒ A ω && B ω) }.