is_lim_seq'_uniform_is_lim

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

Hide file tree

Showing 2 changed files with 39 additions and 11 deletions.
diff --git a/coq/QLearn/Tsitsiklis.v b/coq/QLearn/Tsitsiklis.v
@@ -984,6 +984,19 @@ Definition is_lim_seq'_uniform_fun {Ts} (u : nat -> Ts -> R) (l : Ts -> R) :=
    forall eps : posreal, 
      eventually (fun n => forall (x:Ts), Rabs (u n x - l x) < eps).
 
+Lemma is_lim_seq'_uniform_is_lim (u : nat -> Ts -> R) (l : Ts -> R) :
+  is_lim_seq'_uniform_fun u l ->
+  forall (x : Ts), is_lim_seq (fun n => u n x) (l x).
+Proof.
+  intros.
+  apply is_lim_seq_spec.
+  intros eps.
+  specialize (H eps).
+  revert H.
+  apply eventually_impl.
+  now apply all_eventually; intros ??.
+Qed.
+
 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)).
@@ -1017,6 +1030,20 @@ Definition is_lim_seq'_uniform_fun_Rbar {Ts} (u : nat -> Ts -> R) (l : Ts -> Rba
                      | m_infty => u n x < - 1/eps
                      end).
 
+Lemma is_lim_seq'_uniform_Rbar_is_lim (u : nat -> Ts -> R) (l : Ts -> Rbar) :
+  is_lim_seq'_uniform_fun_Rbar u l ->
+  forall (x : Ts), is_lim_seq (fun n => u n x) (l x).
+Proof.
+  intros.
+  apply is_lim_seq_spec.
+  unfold is_lim_seq'.
+  match_destr.
+  - intros eps.
+    admit.
+
+Admitted.
+
+
 Lemma uniform_converge_sq (α : nat -> Ts -> R) :
   (forall (n:nat), almostR2 prts Rle (const 0) (α n)) -> 
   is_lim_seq'_uniform_almost (fun n => rvsqr (α n)) (const 0) ->

diff --git a/coq/QLearn/jaakkola_vector.v b/coq/QLearn/jaakkola_vector.v
@@ -7005,17 +7005,18 @@ Proof.
           apply H.
    Qed.
 
- Theorem Jaakkola_alpha_beta_unbounded_uniformly_W_alt (W : vector posreal (S N))
-    (X XF α β : nat -> Ts -> vector R (S N))
-    {F : nat -> SigmaAlgebra Ts}
-    (isfilt : IsFiltration F) 
-    (filt_sub : forall k, sa_sub (F k) dom) 
-    (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))} 
-    {rvXF : forall k, RandomVariable (F (S k)) (Rvector_borel_sa (S N)) (XF k)} :
-
+    Theorem Jaakkola_alpha_beta_unbounded_uniformly_W_final
+      (W : vector posreal (S N))
+      (X XF α β : nat -> Ts -> vector R (S N))
+      {F : nat -> SigmaAlgebra Ts}
+      (isfilt : IsFiltration F) 
+      (filt_sub : forall k, sa_sub (F k) dom) 
+      (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))} 
+      {rvXF : forall k, RandomVariable (F (S k)) (Rvector_borel_sa (S N)) (XF k)} :
+
    (**r α and β are almost always non-negative *)
     almost prts (fun ω => forall k i pf, 0 <= vector_nth i pf (α k ω)) ->
     almost prts (fun ω => forall k i pf, 0 <= vector_nth i pf (β k ω)) ->