Library probsa.probability.dominance_relation

From probsa.util Require Export etime.
From probsa.probability Require Export nrvar cdf.

We introduce a generic notion of dominance between elements of two arbitrary types. The expression a ⪯ b denotes the fact that a : A is dominated by b : B.

Class DominanceRelation (A B : Type) :=
dominates : A → B → Prop.
Notation "X ⪯ Y" := (dominates X Y) (at level 55) : probability_scope.

Instances

nat → R vs nat → R

Given two functions f and g, we say that f ⪯ g iff the graph of f is always above the g's graph. That is, ∀ x, f(x) ≥ g(x).

Definition le_func (f g : nat → R) :=
  ∀ n, f n ≥ g n.

Instance dominance_func : DominanceRelation (nat → R) (nat → R) :=
  { dominates := le_func }.

Lemma func_dom_refl :
  ∀ (f : nat → R), f ⪯ f.
Proof. by intros × ?; apply Rge_refl. Qed.

Lemma func_dom_trans :
  ∀ (f g h : nat → R),
    f ⪯ g → g ⪯ h → f ⪯ h.
Proof.
  by intros × LE1 LE2 n; eapply Rge_trans with (r2 := g n).
Qed.

nrvar vs nrvar

Given two random variables X and Y, we say that X ⪯ Y iff X's CDF is always above Y's CDF. That is, ∀ n, 𝔽[X](n) ≥ 𝔽[Y](n).

Definition le_nrvar {XΩ YΩ} {μX : measure XΩ} {μY : measure YΩ} (X : nrvar μX) (Y : nrvar μY) :=
   𝔽<μX >{[ X ]} ⪯ 𝔽<μY >{[ Y ]}.

Instance dominance_nrvar :
  ∀ {ΩX ΩY} {μX : measure ΩX} {μY : measure ΩY},
    DominanceRelation (nrvar μX) (nrvar μY) :=
  { dominates := le_nrvar }.

Lemma nrvar_dom_refl :
  ∀ {Ω} {μ : measure Ω} (X : nrvar μ),
    X ⪯ X.
Proof. by intros × ?; apply Rge_refl. Qed.

Lemma nrvar_dom_trans :
  ∀ {XΩ} {μX : measure XΩ} (X : nrvar μX),
  ∀ {YΩ} {μY : measure YΩ} (Y : nrvar μY),
  ∀ {ZΩ} {μZ : measure ZΩ} (Z : nrvar μZ),
    X ⪯ Y → Y ⪯ Z → X ⪯ Z.
Proof.
  by intros × LE1 LE2 n; eapply Rge_trans with (r2 := 𝔽<μY>{[ Y ]}(n)).
Qed.

nrvar vs nat → R

Similarly, when a random variable X is compared with a function f : ℝ → [0,1], we say that X ⪯ f iff X's CDF is always above f. That is, ∀ x, 𝔽[X](x) ≥ f x.

Definition le_nrvar_func {Ω} {μ : measure Ω} (X : nrvar μ) (f : nat → R) :=
  𝔽<μ >{[ X ]} ⪯ f.

Instance dominance_nrvar_funct :
  ∀ {Ω} {μ : measure Ω}, DominanceRelation (nrvar μ) (nat → R) :=
  { dominates := le_nrvar_func }.

rvar etime vs rvar etime

Instance nat_etimervar_pred_ltop :
  ∀ {Ω} {μ : measure Ω}, LtOp nat (rvar μ [eqType of etime]) (pred Ω) :=
  { lt_op t X := fun ω ⇒ exceeds (X ω) t }.

Definition le_etime_rvar {XΩ YΩ} {μX : measure XΩ} {μY : measure YΩ}
           (X : rvar μX [eqType of etime]) (Y : rvar μY [eqType of etime]) :=
  ∀ (t : nat), ℙ <μX >{[ t ⟨<⟩ X ]} ≤ ℙ <μY >{[ t ⟨<⟩ Y ]}.

Instance dominance_etime_rvar :
  ∀ {ΩX ΩY} {μX : measure ΩX} {μY : measure ΩY},
    DominanceRelation (rvar μX [eqType of etime]) (rvar μY [eqType of etime]) :=
  { dominates := le_etime_rvar }.

Lemma etime_dom_refl :
  ∀ {Ω} {μ : measure Ω} (X : rvar μ [eqType of etime]),
    X ⪯ X.
Proof. by intros × t; reflexivity. Qed.

Lemma etime_dom_trans :
  ∀ {XΩ} {μX : measure XΩ} (X : rvar μX [eqType of etime]),
  ∀ {YΩ} {μY : measure YΩ} (Y : rvar μY [eqType of etime]),
  ∀ {ZΩ} {μZ : measure ZΩ} (Z : rvar μZ [eqType of etime]),
    X ⪯ Y → Y ⪯ Z → X ⪯ Z.
Proof. by intros × NEQ1 NEQ2 t; specialize (NEQ1 t); specialize (NEQ2 t); nra. Qed.