cleanup

IBM · Jan 24, 2025 · fe6d8e1 · fe6d8e1
1 parent 25540e1
commit fe6d8e1
Show file tree

Hide file tree

Showing 3 changed files with 44 additions and 45 deletions.
diff --git a/coq/ProbTheory/FunctionsToReal.v b/coq/ProbTheory/FunctionsToReal.v
@@ -122,6 +122,20 @@ Section defs.
 
     Definition rvpower (rv_X1 rv_X2 : Ts -> R) := fun omega => power (rv_X1 omega) (rv_X2 omega).
 
+    Definition rvinv (rv_X : Ts -> R) := rvpower rv_X (const (-1)).
+
+    Lemma rvinv_Rinv (rv_X : Ts -> R) (ω : Ts) :
+      0 < rv_X ω ->
+      rvinv rv_X ω = / (rv_X ω).
+    Proof.
+      unfold rvinv, rvpower, const.
+      intros.
+      replace (-1) with (Ropp 1) by lra.
+      rewrite power_Ropp; trivial.
+      f_equal.
+      rewrite power_1; lra.
+    Qed.
+
     Definition rvabs  (rv_X : Ts -> R) := fun omega => Rabs (rv_X omega).
 
     Definition rvsign (rv_X : Ts -> R) := fun omega => sign(rv_X omega).

diff --git a/coq/ProbTheory/RealRandomVariable.v b/coq/ProbTheory/RealRandomVariable.v
@@ -906,6 +906,14 @@ Section RealRandomVariables.
         ; apply rv_measurable; trivial.
       Qed.
 
+      Global Instance rvinv_rv (x : Ts -> R) :
+        RandomVariable dom borel_sa x ->
+        RandomVariable dom borel_sa (rvinv x).
+      Proof.
+        intros.
+        typeclasses eauto.
+      Qed.
+
       Global Instance rvsqr_rv
              (rv_X : Ts -> R)
              {rv : RandomVariable dom borel_sa rv_X} :
@@ -6120,6 +6128,28 @@ Section monotonic.
     now apply decreasing_measurable.
   Qed.
 
+
+  Lemma powerRZ_ge_fun_rv (base : R) :
+    RandomVariable borel_sa borel_sa (fun v => powerRZ_ge_fun base v).
+  Proof.
+    apply increasing_rv.
+    intros.
+    unfold powerRZ_ge_fun.
+    match_destr; try lra.
+    match_destr.
+    - match_destr.
+      + rewrite powerRZ_Rpower; try lra.
+        rewrite powerRZ_Rpower; try lra.
+        apply Rle_Rpower; try lra.
+        apply IZR_le.
+        now apply powerRZ_up_log_alt_increasing.
+      + assert (v <= 0) by lra.
+        generalize (Rlt_le_trans 0 u v); intros.
+        cut_to H1; try lra.
+    - match_destr; try lra.
+      apply powerRZ_le; try lra.
+  Qed.
+
 End monotonic.
 
 Section rv_compose.

diff --git a/coq/QLearn/Tsitsiklis.v b/coq/QLearn/Tsitsiklis.v
@@ -2741,51 +2741,6 @@ Qed.
   Qed.
 *)
 
-  Lemma powerRZ_ge_fun_rv (base : R) :
-    RandomVariable borel_sa borel_sa (fun v => powerRZ_ge_fun base v).
-  Proof.
-    apply increasing_rv.
-    intros.
-    unfold powerRZ_ge_fun.
-    match_destr; try lra.
-    match_destr.
-    - match_destr.
-      + rewrite powerRZ_Rpower; try lra.
-        rewrite powerRZ_Rpower; try lra.
-        apply Rle_Rpower; try lra.
-        apply IZR_le.
-        now apply powerRZ_up_log_alt_increasing.
-      + assert (v <= 0) by lra.
-        generalize (Rlt_le_trans 0 u v); intros.
-        cut_to H1; try lra.
-    - match_destr; try lra.
-      apply powerRZ_le; try lra.
-  Qed.
-
-
-  Definition rvinv (x : Ts -> R) := rvpower x (const (-1)).
-
-  Global Instance rvinv_rv (x : Ts -> R) (dom2 : SigmaAlgebra Ts) :
-    RandomVariable dom2 borel_sa x ->
-    RandomVariable dom2 borel_sa (rvinv x).
-  Proof.
-    intros.
-    typeclasses eauto.
-  Qed.
-
-   Lemma rvinv_Rinv (x : Ts -> R) (ω : Ts) :
-     0 < x ω ->
-     rvinv x ω = / (x ω).
-   Proof.
-     unfold rvinv, rvpower, const.
-     intros.
-     replace (-1) with (Ropp 1) by lra.
-     rewrite power_Ropp; trivial.
-     f_equal.
-     rewrite power_1; lra.
-   Qed.
-
-
   Lemma lemma3_pre0  (ω : Ts) (ε : posreal)
         (G M : nat -> Ts -> R) :
     is_lim_seq (fun k => M k ω) p_infty ->