From 50db44c2ae582b74c4ea45285ef0b8ee17a31989 Mon Sep 17 00:00:00 2001
From: Barry Trager <bmt@us.ibm.com>
Date: Thu, 5 Dec 2024 13:19:21 -0500
Subject: [PATCH] cleanup

---
 coq/QLearn/jaakkola_vector.v | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/coq/QLearn/jaakkola_vector.v b/coq/QLearn/jaakkola_vector.v
index dda73a46..6e0cdecd 100644
--- a/coq/QLearn/jaakkola_vector.v
+++ b/coq/QLearn/jaakkola_vector.v
@@ -7016,11 +7016,6 @@ Proof.
     (**r The sum of βs almost always increases without limit *)
     almost prts (fun ω => forall i pf, is_lim_seq (sum_n (fun k => vector_nth i pf (β k ω))) p_infty) ->
     
-    (**r The sum of α²s almost always converges to a finite limit *)
-    (forall i pf, almost prts (fun ω => ex_series (fun n => Rsqr (vector_nth i pf (α n ω))))) ->
-    (**r The sum of β²s almost always converges to a finite limit *)
-    (forall i pf, almost prts (fun ω => ex_series (fun n => Rsqr (vector_nth i pf (β n ω))))) ->
-    
     (exists (γ : R),
         0 < γ < 1 /\
           almost prts 
@@ -7053,7 +7048,7 @@ Proof.
                      is_lim_seq (fun m => vector_nth i pf (X m ω)) 0).
  Proof.
    intros.
-   destruct H6 as [γ [??]].
+   destruct H4 as [γ [??]].
    now 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)).
  Qed.