FiniteConditionalVariance_new

IBM · Nov 27, 2024 · e5ff5e6 · e5ff5e6
1 parent 97cbd9a
commit e5ff5e6
Show file tree

Hide file tree

Showing 3 changed files with 101 additions and 102 deletions.
diff --git a/coq/ProbTheory/ConditionalExpectation.v b/coq/ProbTheory/ConditionalExpectation.v
@@ -6702,12 +6702,6 @@ Section fin_cond_exp.
     apply FiniteCondexp_rv'.
   Qed.
 
-  Lemma FiniteConditionalVariance_exp_from_L2 (f : Ts -> R) 
-    {rv : RandomVariable dom borel_sa f} 
-    {isl:IsLp prts 2 f} : IsFiniteExpectation prts (rvsqr (rvminus f (FiniteConditionalExpectation f))).
-  Proof.
-  Admitted.
-
   Definition ConditionalVariance (f : Ts -> R) 
     {rv : RandomVariable dom borel_sa f} 
     {isfe:IsFiniteExpectation prts f} : Ts -> Rbar :=
@@ -6719,11 +6713,6 @@ Section fin_cond_exp.
     {isfe2:IsFiniteExpectation prts (rvsqr (rvminus f (FiniteConditionalExpectation f)))} : Ts -> R :=
     FiniteConditionalExpectation (rv := variance_rv f) _.
 
-  Definition FiniteConditionalVariance_new (f : Ts -> R) 
-    {rv  : RandomVariable dom borel_sa f} 
-    {isl : IsLp prts 2 f} : Ts -> R :=
-    FiniteConditionalExpectation (rv := variance_rv f) (isfe:=FiniteConditionalVariance_exp_from_L2 f) _.
-
   Lemma ConditionalVariance_ext (f1 f2 : Ts -> R)
         {rv1   : RandomVariable dom borel_sa f1}
         {rv2   : RandomVariable dom borel_sa f2}
@@ -6782,6 +6771,103 @@ Section fin_cond_exp.
       now rewrite (FiniteCondexp_eq f).
   Qed.
 
+
+  Lemma isfe_L2_variance (x : Ts -> R) 
+        (rv : RandomVariable dom borel_sa x) 
+        {isl2: IsLp prts 2 x} :
+    IsFiniteExpectation prts x /\
+    IsFiniteExpectation prts (rvsqr x) /\
+    RandomVariable 
+      dom borel_sa
+      (rvsqr (rvminus x (FiniteConditionalExpectation x))) /\
+    IsFiniteExpectation 
+      prts
+      (rvsqr (rvminus x (FiniteConditionalExpectation x))) /\
+    IsFiniteExpectation
+      prts
+      (rvsqr (FiniteConditionalExpectation x)) /\
+    IsFiniteExpectation prts  (rvmult (FiniteConditionalExpectation x) x).
+  Proof.
+    generalize (conditional_expectation_L2fun_L2 prts sub x); intros.
+    assert (almostR2 (prob_space_sa_sub prts sub) eq 
+                     (conditional_expectation_L2fun prts sub x)
+                     (FiniteConditionalExpectation x)).
+    {
+      generalize (conditional_expectation_L2fun_eq3 prts sub x); intros.
+      generalize (FiniteCondexp_is_cond_exp x); intros.
+      generalize (is_conditional_expectation_unique prts sub x _ _ H0 H1); intros.
+      revert H2.
+      apply almost_impl, all_almost; intros ??.
+      now apply Rbar_finite_eq in H2.
+   }
+    apply almostR2_prob_space_sa_sub_lift in H0.
+    assert (RandomVariable dom borel_sa (FiniteConditionalExpectation x)).
+    {
+      apply FiniteCondexp_rv'.
+    }
+    repeat split.
+    - typeclasses eauto.
+    - typeclasses eauto.
+    - typeclasses eauto.
+    - assert (IsFiniteExpectation 
+                prts
+                (rvsqr (rvminus x (conditional_expectation_L2fun prts sub x)))).
+      {
+        assert (IsLp prts 2 (rvminus x (conditional_expectation_L2fun prts sub x))).
+        {
+          assert (0 <= 2) by lra.
+          apply (IsLp_minus prts (mknonnegreal 2 H2)); try easy.
+          apply RandomVariable_sa_sub; trivial.
+          apply conditional_expectation_L2fun_rv.
+        }
+        typeclasses eauto.
+      }
+      eapply (IsFiniteExpectation_proper_almostR2 
+               prts
+               (rvsqr (rvminus x (conditional_expectation_L2fun prts sub x)))
+               (rvsqr (rvminus x (FiniteConditionalExpectation x)))).
+      revert H0.
+      apply almost_impl, all_almost; intros ??.
+      rv_unfold.
+      now rewrite H0.
+    - assert (IsFiniteExpectation prts (rvsqr (conditional_expectation_L2fun prts sub x))).
+      {
+        typeclasses eauto.
+      }
+      eapply (IsFiniteExpectation_proper_almostR2
+               prts
+               (rvsqr (conditional_expectation_L2fun prts sub x))
+               (rvsqr (FiniteConditionalExpectation x))).
+      revert H0.
+      apply almost_impl, all_almost; intros ??.
+      rv_unfold.
+      now rewrite H0.
+    - assert (IsFiniteExpectation prts (rvmult (conditional_expectation_L2fun prts sub x) x)).
+      {
+        typeclasses eauto.
+      }
+      eapply (IsFiniteExpectation_proper_almostR2
+                    prts
+                    (rvmult (conditional_expectation_L2fun prts sub x) x)
+                    (rvmult (FiniteConditionalExpectation x) x)).
+      revert H0.
+      apply almost_impl, all_almost; intros ??.
+      rv_unfold.
+      now rewrite H0.
+  Qed.
+
+  Lemma FiniteConditionalVariance_exp_from_L2 (f : Ts -> R) 
+    {rv : RandomVariable dom borel_sa f} 
+    {isl:IsLp prts 2 f} : IsFiniteExpectation prts (rvsqr (rvminus f (FiniteConditionalExpectation f))).
+  Proof.
+    apply (isfe_L2_variance f rv).
+  Qed.
+
+  Definition FiniteConditionalVariance_new (f : Ts -> R) 
+    {rv  : RandomVariable dom borel_sa f} 
+    {isl : IsLp prts 2 f} : Ts -> R :=
+    FiniteConditionalExpectation (rv := variance_rv f) (isfe:=FiniteConditionalVariance_exp_from_L2 f) _.
+
   Theorem FiniteCondexp_cond_exp (f : Ts -> R) 
         {rv : RandomVariable dom borel_sa f}
         {isfe:IsFiniteExpectation prts f}

diff --git a/coq/QLearn/Tsitsiklis.v b/coq/QLearn/Tsitsiklis.v
@@ -9085,92 +9085,6 @@ Proof.
          end
      end.
 
-  Lemma isfe_L2_variance (x : Ts -> R) 
-        {dom2 : SigmaAlgebra Ts}
-        (sub : sa_sub dom2 dom)
-        (rv : RandomVariable dom borel_sa x) 
-        {isl2: IsLp prts 2 x} :
-    IsFiniteExpectation prts x /\
-    IsFiniteExpectation prts (rvsqr x) /\
-    RandomVariable 
-      dom borel_sa
-      (rvsqr (rvminus x (FiniteConditionalExpectation prts sub x))) /\
-    IsFiniteExpectation 
-      prts
-      (rvsqr (rvminus x (FiniteConditionalExpectation prts sub x))) /\
-    IsFiniteExpectation
-      prts
-      (rvsqr (FiniteConditionalExpectation prts sub x)) /\
-    IsFiniteExpectation prts  (rvmult (FiniteConditionalExpectation prts sub x) x).
-  Proof.
-    generalize (conditional_expectation_L2fun_L2 prts sub x); intros.
-    assert (almostR2 (prob_space_sa_sub prts sub) eq 
-                     (conditional_expectation_L2fun prts sub x)
-                     (FiniteConditionalExpectation prts sub x)).
-    {
-      generalize (conditional_expectation_L2fun_eq3 prts sub x); intros.
-      generalize (FiniteCondexp_is_cond_exp prts sub x); intros.
-      generalize (is_conditional_expectation_unique prts sub x _ _ H0 H1); intros.
-      revert H2.
-      apply almost_impl, all_almost; intros ??.
-      now apply Rbar_finite_eq in H2.
-   }
-    apply almostR2_prob_space_sa_sub_lift in H0.
-    assert (RandomVariable dom borel_sa (FiniteConditionalExpectation prts sub x)).
-    {
-      apply FiniteCondexp_rv'.
-    }
-    repeat split.
-    - typeclasses eauto.
-    - typeclasses eauto.
-    - typeclasses eauto.
-    - assert (IsFiniteExpectation 
-                prts
-                (rvsqr (rvminus x (conditional_expectation_L2fun prts sub x)))).
-      {
-        assert (IsLp prts 2 (rvminus x (conditional_expectation_L2fun prts sub x))).
-        {
-          assert (0 <= 2) by lra.
-          apply (IsLp_minus prts (mknonnegreal 2 H2)); try easy.
-          apply RandomVariable_sa_sub; trivial.
-          apply conditional_expectation_L2fun_rv.
-        }
-        typeclasses eauto.
-      }
-      eapply (IsFiniteExpectation_proper_almostR2 
-               prts
-               (rvsqr (rvminus x (conditional_expectation_L2fun prts sub x)))
-               (rvsqr (rvminus x (FiniteConditionalExpectation prts sub x)))).
-      revert H0.
-      apply almost_impl, all_almost; intros ??.
-      rv_unfold.
-      now rewrite H0.
-    - assert (IsFiniteExpectation prts (rvsqr (conditional_expectation_L2fun prts sub x))).
-      {
-        typeclasses eauto.
-      }
-      eapply (IsFiniteExpectation_proper_almostR2
-               prts
-               (rvsqr (conditional_expectation_L2fun prts sub x))
-               (rvsqr (FiniteConditionalExpectation prts sub x))).
-      revert H0.
-      apply almost_impl, all_almost; intros ??.
-      rv_unfold.
-      now rewrite H0.
-    - assert (IsFiniteExpectation prts (rvmult (conditional_expectation_L2fun prts sub x) x)).
-      {
-        typeclasses eauto.
-      }
-      eapply (IsFiniteExpectation_proper_almostR2
-                    prts
-                    (rvmult (conditional_expectation_L2fun prts sub x) x)
-                    (rvmult (FiniteConditionalExpectation prts sub x) x)).
-      revert H0.
-      apply almost_impl, all_almost; intros ??.
-      rv_unfold.
-      now rewrite H0.
-  Qed.
-
   Lemma conditional_variance_alt (x : Ts -> R)
         {dom2 : SigmaAlgebra Ts}
         (sub : sa_sub dom2 dom)
@@ -9310,7 +9224,7 @@ Proof.
        dom borel_sa
        (rvsqr (rvminus x (FiniteConditionalExpectation prts sub x))).
    Proof.
-     now generalize (isfe_L2_variance x sub rv); intros.
+     apply (isfe_L2_variance prts sub x).
    Qed.
 
   Instance conditional_variance_L2_alt_isfe (x : Ts -> R)
@@ -9322,7 +9236,7 @@ Proof.
       prts
       (rvsqr (rvminus x (FiniteConditionalExpectation prts sub x))).
    Proof.
-     now generalize (isfe_L2_variance x sub rv); intros.
+     apply (isfe_L2_variance prts sub x).
    Qed.    
 
 
@@ -9338,8 +9252,7 @@ Proof.
              (rvminus (FiniteConditionalExpectation prts sub (rvsqr x))
                       (rvsqr (FiniteConditionalExpectation prts sub x))).
      Proof.
-       generalize (isfe_L2_variance x sub rv); intros.
-       apply conditional_variance_alt; try easy.
+       apply conditional_variance_alt; apply (isfe_L2_variance prts sub x).
      Qed.       
 
   Lemma conditional_variance_bound (x : Ts -> R) (c : R) 

diff --git a/coq/QLearn/jaakkola_vector.v b/coq/QLearn/jaakkola_vector.v
@@ -6198,7 +6198,7 @@ Section jaakola_vector2.
       {
         red; now rewrite rvpower_abs2_unfold.
       }         
-      destruct  (isfe_L2_variance f sub rv) as [_[_[_[_[HH1 HH2]]]]].
+      destruct  (isfe_L2_variance prts sub f rv) as [_[_[_[_[HH1 HH2]]]]].
 
     assert (isfe4 : IsFiniteExpectation prts
                       (rvsqr (FiniteConditionalExpectation prts sub f))).