From 453d1e8444a02c30fbb4b9ad0651bab890ff3529 Mon Sep 17 00:00:00 2001
From: Avi Shinnar <shinnar@us.ibm.com>
Date: Sun, 8 Dec 2024 15:34:36 -0500
Subject: [PATCH] Finish proof of lemma3_counter

Signed-off-by: Avi Shinnar <shinnar@us.ibm.com>
---
 coq/QLearn/jaakkola_vector.v | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/coq/QLearn/jaakkola_vector.v b/coq/QLearn/jaakkola_vector.v
index 1ed15626..f5cd7d8d 100644
--- a/coq/QLearn/jaakkola_vector.v
+++ b/coq/QLearn/jaakkola_vector.v
@@ -3632,9 +3632,17 @@ Section jaakola_vector2.
                  ring.
                }
                
-             
-             admit.
-      Admitted.
+               cut (ps_P (event_le dom (rvlim X) C) <= ps_P (event_complement ev)).
+               {
+                 rewrite ps_complement.
+                 lra.
+               } 
+               apply ps_sub; intros ?; simpl.
+               unfold pre_event_complement.
+               intros ??.
+               specialize (H3 _ H5).
+               lra.
+       Qed.
 
       Lemma vecrvclip_max_bound (rvec : Ts -> vector R (S N)) (C : posreal) :
         forall a,