From 34e672e70aaca8d31637ba4e925e2f148c2143d8 Mon Sep 17 00:00:00 2001
From: Barry Trager <bmt@us.ibm.com>
Date: Thu, 12 Dec 2024 14:23:07 -0500
Subject: [PATCH] genharmonic_series_sq'

---
 coq/QLearn/infprod.v | 48 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 48 insertions(+)

diff --git a/coq/QLearn/infprod.v b/coq/QLearn/infprod.v
index 204c4660..6941e50e 100644
--- a/coq/QLearn/infprod.v
+++ b/coq/QLearn/infprod.v
@@ -1382,6 +1382,15 @@ Proof.
     apply cond_pos.
 Qed.
 
+Lemma inv_bound_ge (a : posreal) (b : nonnegreal) :
+  / a  >= / (a + b).
+Proof.
+  apply Rle_ge.
+  generalize (cond_pos a); intros.
+  generalize (cond_nonneg b); intros.
+  apply Rinv_le_contravar; lra.
+Qed.
+
 Lemma inv_bound_sq_gt (a b : posreal) :
   Rsqr (/ a)  > Rsqr (/ (a + b)).
 Proof.
@@ -1394,6 +1403,21 @@ Proof.
     apply Rinv_0_lt_compat; apply cond_pos.
 Qed.
 
+Lemma inv_bound_sq_ge (a : posreal) (b : nonnegreal) :
+  Rsqr (/ a)  >= Rsqr (/ (a + b)).
+Proof.
+  generalize (cond_pos a); intros.
+  generalize (cond_nonneg b); intros.
+  apply Rle_ge.
+  apply Rsqr_incr_1.
+  + apply Rge_le.
+    apply inv_bound_ge.
+  + left.
+    apply Rinv_0_lt_compat; lra.
+  + left.
+    apply Rinv_0_lt_compat; lra.
+Qed.
+
 Lemma inv_bound_exists_lt  (a b : posreal) :
   exists (j : nat), forall (n:nat), / (a * (INR ((S n) + j))) < / (a * INR (S n) + b).
 Proof.
@@ -1471,6 +1495,23 @@ Proof.
   - apply genharmonic_series_sq0.
  Qed.
 
+Lemma genharmonic_series_sq' (b : nonnegreal) (c : posreal) :
+  ex_series (fun n => Rsqr (/ (b + c * INR (S n)))).
+Proof.
+  apply (@ex_series_le R_AbsRing) with (b := fun n => Rsqr ( / (c * INR (S n)))).
+  - intros.
+    assert (0 < c * INR (S n)).    
+    + apply Rmult_lt_0_compat; [apply cond_pos | ].
+      apply lt_0_INR; lia.
+    + rewrite Rabs_right.
+      * apply Rge_le.
+        rewrite Rplus_comm.
+        apply (inv_bound_sq_ge (mkposreal _ H) b).
+      * apply Rle_ge.
+        apply Rle_0_sqr.
+  - apply genharmonic_series_sq0.
+ Qed.
+
 Lemma genharmonic_sq_lim (b c : posreal) :
   is_lim_seq (fun n => Rsqr (/ (b + c * INR (S n)))) 0.
 Proof.  
@@ -1478,6 +1519,13 @@ Proof.
   apply genharmonic_series_sq.
 Qed.
 
+Lemma genharmonic_sq_lim' (b : nonnegreal) (c : posreal) :
+  is_lim_seq (fun n => Rsqr (/ (b + c * INR (S n)))) 0.
+Proof.  
+  apply ex_series_lim_0.
+  apply genharmonic_series_sq'.
+Qed.
+
 Lemma harmonic_increasing :
   let f := fun i => sum_f_R0' (fun n => 1 / INR (S n)) i in
   forall n m : nat, (n <= m)%nat -> f n <= f m.