Finish proof of lemma3_counter

Signed-off-by: Avi Shinnar <[email protected]>
IBM · Dec 8, 2024 · 453d1e8 · 453d1e8
1 parent 77bdfa6
commit 453d1e8
Showing 1 changed file with 11 additions and 3 deletions.
diff --git 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,