clean up in [⪯]-relation file

probability/cdf.v

@@ -10,6 +10,8 @@ Local Open Scope nat_scope.
 Definition cdf {Ω} {μ : measure Ω} (X : nrvar μ) (x : nat) := ℙ<μ>{[ X ⟨<=⟩ x ]}.
 Notation "'𝔽<' μ '>{[' X ']}(' x ')'" := (@cdf _ μ X x)
   (at level 10, format "𝔽< μ >{[  X  ]}( x )") : probability_scope.
+Notation "'𝔽<' μ '>{[' X ']}'" := (@cdf _ μ X )
+  (at level 10, format "𝔽< μ >{[  X  ]}") : probability_scope.
 
 (* --------------------------------- Lemmas --------------------------------- *)
 Lemma cdf_nonnegative :

probability/dominance_relation.v

@@ -13,12 +13,35 @@ Notation "X ⪯ Y" := (dominates X Y) (at level 55) : probability_scope.
 
 (* -------------------------------- Instances -------------------------------- *)
 (** * 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) :=
+  forall n, f n >= g n.
+
+Instance dominance_func : DominanceRelation (nat -> R) (nat -> R) :=
+  { dominates := le_func }.
+
+Lemma func_dom_refl :
+  forall (f : nat -> R), f ⪯ f.
+Proof. by intros * ?; apply Rge_refl. Qed.
+
+Lemma func_dom_trans :
+  forall (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) :=
-  forall n, 𝔽<μX>{[ X ]}(n) >= 𝔽<μY>{[ Y ]}(n).
+   𝔽<μX>{[ X ]} ⪯ 𝔽<μY>{[ Y ]}.
 
 Instance dominance_nrvar :
   forall {ΩX ΩY} {μX : measure ΩX} {μY : measure ΩY},
@@ -45,7 +68,7 @@ Qed.
     [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) :=
-  forall x, 𝔽<μ>{[ X ]}(x) >= f x.
+  𝔽<μ>{[ X ]} ⪯ f.
 
 Instance dominance_nrvar_funct :
   forall {Ω} {μ : measure Ω}, DominanceRelation (nrvar μ) (nat -> R) :=
@@ -57,10 +80,14 @@ Instance nat_etimervar_pred_ltop :
   forall {Ω} {μ : 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]) :=
+  forall (t : nat), ℙ<μX>{[ t ⟨<⟩ X ]} <= ℙ<μY>{[ t ⟨<⟩ Y ]}.
+
 Instance dominance_etime_rvar :
   forall {ΩX ΩY} {μX : measure ΩX} {μY : measure ΩY},
     DominanceRelation (rvar μX [eqType of etime]) (rvar μY [eqType of etime]) :=
-  { dominates X Y := forall (t : nat), ℙ<μX>{[ t ⟨<⟩ X ]} <= ℙ<μY>{[ t ⟨<⟩ Y ]} }.
+  { dominates := le_etime_rvar }.
 
 Lemma etime_dom_refl :
   ∀ {Ω} {μ : measure Ω} (X : rvar μ [eqType of etime]),
@@ -73,25 +100,3 @@ Lemma etime_dom_trans :
   forall {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.
-
-
-(** ** [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_n2r (f g : nat -> R) :=
-  forall x, f x >= g x.
-
-Instance dominance_n2r : DominanceRelation (nat -> R) (nat -> R) :=
-  { dominates := le_n2r }.
-
-Lemma n2r_dom_refl :
-  forall (f : nat -> R), f ⪯ f.
-Proof. by intros * ?; apply Rge_refl. Qed.
-
-Lemma n2r_dom_trans :
-  forall (f g h : nat -> R),
-    f ⪯ g -> g ⪯ h -> f ⪯ h.
-Proof.
-  by intros * LE1 LE2 x; eapply Rge_trans with (r2 := g(x)).
-Qed.