From 5d99054a9b541b589a5a243bc21a9134982bff0f Mon Sep 17 00:00:00 2001
From: Avi Shinnar <shinnar@us.ibm.com>
Date: Tue, 3 Dec 2024 13:28:48 -0500
Subject: [PATCH] work on Jaakkola_alpha_beta_bounded_uniformly

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

diff --git a/coq/QLearn/jaakkola_vector.v b/coq/QLearn/jaakkola_vector.v
index 9602dae5..141e9fed 100644
--- a/coq/QLearn/jaakkola_vector.v
+++ b/coq/QLearn/jaakkola_vector.v
@@ -5327,9 +5327,8 @@ Section jaakola_vector2.
          }
          generalize 
            (bounded_nat_ex_choice_vector 
-              (A := R) (n := S N)
+              (A := posreal) (n := S N)
               (fun i pf eps =>
-                 0 < eps /\
                    eventually
             (fun n : nat =>
              almostR2 prts Rbar_lt
@@ -5339,18 +5338,24 @@ Section jaakola_vector2.
                (fun x : Ts => const eps x)))); intros.
          cut_to H14.
          + destruct H14.
-           pose (eps := Rvector_max_abs x).
+           pose (eps := Rvector_max_abs (vector_map pos x)).
            assert (0 < eps).
            {
-             assert (forall i pf, 0 < vector_nth i pf x).
-             {
-               intros.
-               specialize (H14 i pf).
-               apply H14.
-             }
-             admit.
-          }
-          exists (mkposreal _ H15).
+             generalize (Rvector_max_abs_nth_le  (vector_map pos x) 0 (Nat.lt_0_succ _)).
+             rewrite vector_nth_map.
+             unfold eps.
+             intros leq.
+             eapply Rlt_le_trans; try eapply leq.
+             destruct ((vector_nth 0 (Nat.lt_0_succ N) x)); simpl in *.
+             rewrite Rabs_right; lra.
+           } 
+           exists (mkposreal _ H15).
+           apply eventually_bounded_forall in H14.
+           revert H14.
+           apply eventually_impl; apply all_eventually; intros ? HH ??.
+           specialize (HH i pf).
+           revert HH.
+           apply almost_impl; apply all_almost; intros ??.
           admit.
      Admitted.