From 7b65a39f38c37a3e67dbae50ca4f87d5c07f6b3e Mon Sep 17 00:00:00 2001
From: Barry Trager <bmt@us.ibm.com>
Date: Wed, 4 Dec 2024 17:56:12 -0500
Subject: [PATCH] wip

---
 coq/QLearn/jaakkola_vector.v | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

diff --git a/coq/QLearn/jaakkola_vector.v b/coq/QLearn/jaakkola_vector.v
index a0d98acf..25b1ce74 100644
--- a/coq/QLearn/jaakkola_vector.v
+++ b/coq/QLearn/jaakkola_vector.v
@@ -6978,11 +6978,7 @@ Proof.
     (adapt_beta : IsAdapted (Rvector_borel_sa (S N)) β F)    
     {rvX0 : RandomVariable (F 0%nat) (Rvector_borel_sa (S N)) (X 0%nat)}
     {isl2 : forall k i pf, IsLp prts 2 (vecrvnth i pf (XF k))} 
-    {rvXF : forall k, RandomVariable (F (S k)) (Rvector_borel_sa (S N)) (XF k)}
-(* should be able to remove following *)
-    {vec_rvXF_I : forall k, RandomVariable dom (Rvector_borel_sa (S N)) (XF k)}
-(*    {vec_isfe : forall k, vector_IsFiniteExpectation prts (XF k)} *) :
-
+    {rvXF : forall k, RandomVariable (F (S k)) (Rvector_borel_sa (S N)) (XF k)} :
     0 < γ < 1 ->
 
     almost prts (fun ω => forall k i pf, 0 <= vector_nth i pf (α k ω)) ->
@@ -6994,10 +6990,10 @@ Proof.
     almost prts (fun ω => forall i pf, is_lim_seq (sum_n (fun k => vector_nth i pf (β k ω))) p_infty) ->
     (forall i pf, almost prts (fun ω => ex_series (fun n => Rsqr (vector_nth i pf (α n ω))))) ->
     (forall i pf, almost prts (fun ω => ex_series (fun n => Rsqr (vector_nth i pf (β n ω))))) ->
-    almost prts 
+   almost prts 
       (fun ω =>
          (forall k,
-             (pos_scaled_Rvector_max_abs ((vector_FiniteConditionalExpectation _ (filt_sub k) (XF k) (* (rv := vec_rvXF_I filt_sub XF k) *)) ω) W) <
+             (pos_scaled_Rvector_max_abs ((vector_FiniteConditionalExpectation prts (filt_sub k) (XF k) (rv := vec_rvXF_I filt_sub XF k) (isfe := vec_isfe XF (vec_rvXF_I := vec_rvXF_I filt_sub XF) k)) ω) W) <
                (γ * (pos_scaled_Rvector_max_abs (X k ω) W))))  ->
     (forall i pf,
         is_lim_seq'_uniform_almost (fun n ω => sum_n (fun k => rvsqr (vecrvnth i pf (α k)) ω) n) 
@@ -7005,7 +7001,7 @@ Proof.
     (forall i pf, 
         is_lim_seq'_uniform_almost (fun n ω => sum_n (fun k => rvsqr (vecrvnth i pf (β k)) ω) n) 
           (fun ω => Lim_seq (sum_n (fun k => rvsqr (vecrvnth i pf (β k)) ω)))) ->
-    (exists (C : R),
+   (exists (C : R),
         (0 < C)  /\
           almost prts 
             (fun ω =>
@@ -7019,7 +7015,8 @@ Proof.
                      is_lim_seq (fun m => vector_nth i pf (X m ω)) 0).
  Proof.
    intros.
-   apply (Jaakkola_alpha_beta_unbounded_uniformly_W W γ X XF α β isfilt filt_sub) with (isl2 := isl2) (vec_rvXF_I := vec_rvXF_I) (vec_isfe := vec_isfe XF).
+   apply (Jaakkola_alpha_beta_unbounded_uniformly_W W γ X XF α β isfilt filt_sub)
+      with (isl2 := isl2) (vec_rvXF_I := vec_rvXF_I filt_sub XF) (vec_isfe := vec_isfe XF (vec_rvXF_I := vec_rvXF_I filt_sub XF)).
    - trivial.
    - trivial.
    - trivial.