is_lim_seq'_uniform_Rbar_is_lim

IBM · Dec 5, 2024 · 31cc893 · 31cc893
1 parent 2547bf2
commit 31cc893
Show file tree

Hide file tree

Showing 2 changed files with 60 additions and 7 deletions.
diff --git a/coq/QLearn/Tsitsiklis.v b/coq/QLearn/Tsitsiklis.v
@@ -1001,6 +1001,13 @@ Definition is_lim_seq'_uniform_almost (u : nat -> Ts -> R) (l : Ts -> R) :=
    forall eps : posreal, 
      eventually (fun n => almostR2 prts Rlt (rvabs (rvminus (u n) l)) (const eps)).
 
+Lemma is_lim_seq'_uniform_is_lim_almost (u : nat -> Ts -> R) (l : Ts -> R) :
+  is_lim_seq'_uniform_almost u l ->
+  almost prts (fun x => is_lim_seq (fun n => u n x) (l x)).
+Proof.
+  Admitted.
+
+
 Lemma uniform_lim_all_almost (u : nat -> Ts -> R) (l : Ts -> R) :
   is_lim_seq'_uniform_fun u l ->
   is_lim_seq'_uniform_almost u l.
@@ -1037,12 +1044,55 @@ Proof.
   intros.
   apply is_lim_seq_spec.
   unfold is_lim_seq'.
-  match_destr.
-  - intros eps.
-    admit.
-
-Admitted.
-
+  match_case; intros.
+  - specialize (H eps).
+    revert H.
+    apply eventually_impl.
+    apply all_eventually; intros ??.
+    specialize (H x).
+    now rewrite H0 in H.
+  - pose (eps := / Rmax M 1).
+    assert (0 < eps).
+    {
+      unfold eps.
+      apply Rinv_0_lt_compat.
+      generalize (Rmax_r M 1); intros.
+      lra.
+   }
+   generalize (H (mkposreal _ H1)).
+   apply eventually_impl.
+   apply all_eventually; intros ??.
+   specialize (H2 x).
+   rewrite H0 in H2.
+   simpl in H2.
+   eapply Rle_lt_trans; cycle 1.
+   apply H2.
+   unfold eps.
+   unfold Rdiv.
+   rewrite Rinv_inv, Rmult_1_l.
+   apply Rmax_l.
+ - pose (eps := / (- (Rmin M (-1)))).
+   assert (0 < eps).
+   {
+     unfold eps.
+     apply Rinv_0_lt_compat.
+     generalize (Rmin_r M (-1)); intros.
+     lra.
+   }
+   generalize (H (mkposreal _ H1)).
+   apply eventually_impl.
+   apply all_eventually; intros ??.
+   specialize (H2 x).
+   rewrite H0 in H2.
+   simpl in H2.
+   eapply Rlt_le_trans.
+   apply H2.
+   unfold eps.
+   unfold Rdiv.
+   rewrite Rinv_inv.
+   ring_simplify.
+   apply Rmin_l.
+ Qed.
 
 Lemma uniform_converge_sq (α : nat -> Ts -> R) :
   (forall (n:nat), almostR2 prts Rle (const 0) (α n)) -> 

diff --git a/coq/QLearn/jaakkola_vector.v b/coq/QLearn/jaakkola_vector.v
@@ -7014,7 +7014,10 @@ Proof.
       (adapt_alpha : IsAdapted (Rvector_borel_sa (S N)) α F)
       (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))} 
+      {isl2 : forall k i pf, IsLp prts 2 (vecrvnth i pf (XF k))}
+(*
+      {rvXF : IsAdpated (Rvector_borel_sa (S N)) XF (fun k => F (S k))} 
+*)
       {rvXF : forall k, RandomVariable (F (S k)) (Rvector_borel_sa (S N)) (XF k)} :
 
    (**r α and β are almost always non-negative *)