Library probsa.probability.brvar
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.
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 ω) }.