Formalize pRTA from "Critical Instant for Probabilistic Timing Guarantees: Refuted and Revisited"

Please review this MR commit-by-commit.

probability/conditional.v

@@ -61,6 +61,14 @@ Section ConditionalMeasure.
   Definition restrict : measure Ω :=
     mkDistrib Ω pmf_restricted pmf_nonnegative pmf_sums_to_1.
 
+  Remark pmf_restricted_pred :
+    forall ω, pmf_restricted ω > 0 -> S ω.
+  Proof.
+    clear; intros; unfold pmf_restricted in *.
+    destruct (S ω) eqn:Pω => //.
+    by apply Rlt_irrefl in H.
+  Qed.
+
 End ConditionalMeasure.
 
 (* -------------------------------------------------------------------------- *)
@@ -231,6 +239,27 @@ Section BasicLemmas.
     by apply pr_cond_eq_cond.
   Qed.
 
+  Lemma pr_cond_eq_pred_0 :
+    forall {Ω} (μ : measure Ω) (A B : pred Ω) ρ,
+      (forall ω, B ω -> ~~ A ω) ->
+      ℙ<μ, ρ>{[ A | B ]} = 0.
+  Proof.
+    intros * NE; apply pr_zero => ω POS.
+    apply/negP/negP; apply: NE.
+    by apply pmf_restricted_pred in POS.
+  Qed.
+
+  Lemma pr_cond_mono_pred :
+    forall {Ω} (μ : measure Ω) (P Q C : pred Ω) ρ1 ρ2,
+      (forall ω : Ω, C ω -> P ω → Q ω) →
+      ℙ<μ, ρ1>{[ P | C ]} <= ℙ<μ, ρ2>{[ Q | C ]}.
+  Proof.
+    intros * IMP.
+    erewrite cond_prob_posprob_irrelevance; rewrite /pr_cond; apply pr_mono_pred_pos.
+    move=> ω POS Pω; apply IMP => //.
+    by apply pmf_restricted_pred in POS.
+  Qed.
+
   (** This is a technical lemma that can be skipped. Intuitively, it
       states that if we consider only those outcomes in the _product_
       _space_ where the first component belongs to [B] (i.e., product