cleanup

IBM · Jan 24, 2025 · 62b07b8 · 62b07b8
1 parent 1b55f13
commit 62b07b8
Showing 1 changed file with 0 additions and 96 deletions.
diff --git a/coq/QLearn/jaakkola_vector.v b/coq/QLearn/jaakkola_vector.v
@@ -3037,102 +3037,6 @@ Section jaakola_vector2.
        lra.
    Qed.
 
-   Lemma condexp_sqr_bounded  (XF : Ts -> R) (C : R)
-     {dom2 : SigmaAlgebra Ts}
-     (sa_sub2 : sa_sub dom2 dom) 
-     {rvXF : RandomVariable dom borel_sa XF} :
-     almostR2 prts Rle (rvsqr XF) (const C) ->
-     almostR2 (prob_space_sa_sub prts sa_sub2) Rbar_le (ConditionalExpectation prts sa_sub2 (rvsqr XF)) (const C).
-   Proof.
-     intros.
-     generalize (Condexp_const prts sa_sub2 C); intros.     
-     assert (IsFiniteExpectation prts (rvsqr XF)).
-     {
-       apply (IsFiniteExpectation_abs_bound_almost prts (rvsqr XF) (const C)).
-       - revert H.
-         apply almost_impl.
-         unfold const, rvsqr, rvabs.
-         apply all_almost; intros ??.
-         now rewrite <- Rabs_sqr.
-       - apply IsFiniteExpectation_const.
-     }
-     generalize (Condexp_ale prts sa_sub2 (rvsqr XF) (const C)); intros.
-     rewrite Condexp_const in H2.
-     now apply H2.
-  Qed.
-
-   Lemma condexp_sqr_bounded_prts  (XF : Ts -> R) (C : R)
-     {dom2 : SigmaAlgebra Ts}
-     (sa_sub2 : sa_sub dom2 dom) 
-     {rvXF : RandomVariable dom borel_sa XF} :
-     almostR2 prts Rle (rvsqr XF) (const C) ->
-     almostR2 prts Rbar_le (ConditionalExpectation prts sa_sub2 (rvsqr XF)) (const C).
-   Proof.
-     intros.
-     apply (almost_prob_space_sa_sub_lift prts sa_sub2).
-     now apply condexp_sqr_bounded.
-  Qed.
-
-   Lemma condexp_square_bounded (XF : Ts -> R) (C : R)
-     {dom2 : SigmaAlgebra Ts}
-     (sa_sub2 : sa_sub dom2 dom) 
-     {rvXF : RandomVariable dom borel_sa XF}
-     {isfe : IsFiniteExpectation prts XF} 
-     {rv3 : RandomVariable dom borel_sa (FiniteConditionalExpectation prts sa_sub2 XF)} :
-     (forall ω, Rabs (XF ω) <= C) ->
-     almostR2 prts Rbar_le
-       (ConditionalExpectation
-          prts sa_sub2
-          (rvsqr (rvminus XF
-                    (FiniteConditionalExpectation prts sa_sub2 XF))))
-       (const (Rsqr (2 * C))).
-  Proof.
-    intros.
-    apply condexp_sqr_bounded_prts.
-    assert (almostR2 prts Rle (FiniteConditionalExpectation prts sa_sub2 XF) (const C)).
-    {
-      generalize (FiniteCondexp_ale prts sa_sub2 XF (const C)); intros.
-      apply (almost_prob_space_sa_sub_lift prts sa_sub2).      
-      rewrite FiniteCondexp_const in H0.
-      apply H0.
-      apply all_almost; intros ?.
-      unfold const.
-      specialize (H x).
-      now rewrite Rabs_le_both in H.
-   }
-   assert (almostR2 prts Rle (const (- C)) (FiniteConditionalExpectation prts sa_sub2 XF)).
-   {
-      generalize (FiniteCondexp_ale prts sa_sub2 (const (- C)) XF ); intros.
-      apply (almost_prob_space_sa_sub_lift prts sa_sub2).      
-      rewrite FiniteCondexp_const in H1.
-      apply H1.
-      apply all_almost; intros ?.
-      unfold const.
-      specialize (H x).
-      now rewrite Rabs_le_both in H.
-   }
-   revert H0; apply almost_impl.
-   revert H1; apply almost_impl.
-   unfold const, rvsqr, rvminus, rvplus, rvopp, rvscale.
-   apply all_almost; intros ???.
-   apply Rsqr_le_abs_1.    
-   eapply Rle_trans.
-   apply Rabs_triang.
-   repeat rewrite Rabs_mult.
-   rewrite Rabs_m1, Rmult_1_l.
-   rewrite (Rabs_right 2); try lra.
-   assert (0 <= C).
-   {
-     eapply Rle_trans; cycle 1.
-     apply (H x).
-     apply Rabs_pos.
-   }
-   rewrite (Rabs_right C); try lra.
-   replace (2 * C) with (C + C) by lra.
-   apply Rplus_le_compat; trivial.
-   now rewrite Rabs_le_both.
-  Qed.
-
   Lemma LimSup_pos_0 (f : nat -> R) :
     (forall n, 0 <= f n) ->
     LimSup_seq f = 0->